1

I am trying to write a predicate such that, "if a certain constant is true"(in this case if 'sec=ok') then the predicate will evaluate to False, because I've written an expression in the consequent of that particular implication that contradicts with another expression elsewhere in the predicate. (f%^x ≠ g%^x) ∧ (f%^ci = g%^ci) should contradict, given the fact that both x and ci are universally quantified and have the same type.

However, Nitpick produces a counter example that I am not able to understand. I was hoping if someone could kindly check this lemma and see whether a contradiction can be proved. Or else let me know where I'm going wrong. So a brief description is as follows;

  • f and g are two partial functions from arbitrary types 'a to 'b.

  • 'sec' is a constant with values 'ok' and 'notok'

    f::'a-|->'b
g::'a-|->'b

lemma simpleExample: 
shows "∀ (ci::'a ) (a::'a set) (b::'b set) ( f::'a  <=> 'b) . f ∈ (a-|-> b) ∧ card f > 0 -->       
    (∃  ( g::'a  <=> 'b) . g ∈ (a-|->b) ∧ a=(dom f ∪ dom g) ∧
    (  ∀ (x ::'a) . sec=ok --> f%^x ≠ g%^x) ∧  f%^ci = g%^ci )  "

I've also seen a 'subtle' difference between two Z Math toolkits regarding Function Application. I've tried both but the problem remains.

    In HIVE Z Math toolkit :  "R %^ x      == The(λy. (x,y) : R )  "
    In HOL-Z Math Toolkit :   "R %^ x      == (@y. (x,y) : R)"

The Nitpick error can be seen here http://i58.tinypic.com/316te1t.png

NOTE: For reference, please find the definition of partial function I'm using currently from HOL-Z.

     type_synonym  ('a,'b) lts = "('a*'b) set"     (infixr "<=>" 20)

     prodZ         ::"['a set,'b set] => ('a <=> 'b) " ("_ %x _"  [81,80] 80)

     "a %x b"      == "a <*> b"

     rel           ::"['a set, 'b set] => ('a <=> 'b) set"  ("_ <--> _"   [54,53] 53)
     rel_def       : "A <--> B    == Pow (A %x B)"

     partial_func  ::"['a set,'b set] => ('a <=> 'b) set"   ("_ -|-> _"   [54,53] 53)
     partial_func_def  : "S -|-> R    == 
          {f. f:(S <--> R) & (! x y1 y2. (x,y1):f & (x,y2):f  --> (y1=y2))}"

     rel_appl      :: "['a<=>'b,'a] => 'b"    ("_ %^ _"  [90,91] 90)
     rel_appl_def  :  "R %^ x       == The(λy. (x,y) : R)"
David Young
  • 10,713
  • 2
  • 33
  • 47
user3896306
  • 11
  • 1
  • I don’t understand everything you are trying to do, but as you say, “predicate will evaluate to False”, i.e. the lemma is false. So it should not be a surprise that nitpick finds a counter example! – Joachim Breitner Feb 05 '15 at 12:16
  • 1
    I thought it should ask me to prove `goal (1 subgoal): 1. False` , that's what I was expecting. right now Nitpick is saying there might be a possible counter argument. I wan't to write it in such a way that there cannot be a possible counter argument. – user3896306 Feb 05 '15 at 12:59
  • 1
    You can simply ignore nitpick and attempt to prove `False`... but if you succeed, something would be seriously broken. Why do you expect that you can prove a false statement? – Joachim Breitner Feb 05 '15 at 16:20
  • 1
    I am not trying to prove a false statement. I want Isabelle to evaluate it to False, so that "I can conclude" that the predicate has a contradiction and cannot be proven. But because of the nitpick counter example and since Isabelle does not evalute my predicate to false, I cannot conclude it. I'm doing code generation to generate a number of predicates after assigning various values to system variables, in a formal system specification. Based on Isabelle output, I can reason about certain properties of the system, in relation to the changes in system variables. – user3896306 Feb 05 '15 at 16:43
  • 1
    Maybe you want to have `definition "simpleExample = ∀ (ci::'a ) ..."`, followed by `lemma "simpleExample = False"`? – Joachim Breitner Feb 05 '15 at 18:40

0 Answers0