[isabelle] Interpretation of Partial Functions from Z to Isabelle/HOL



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(
http://i58.tinypic.com/316te1t.png) 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 'suttle' 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)"

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)"

rgrds
Ibrahim



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.