*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Interpretation of Partial Functions from Z to Isabelle/HOL*From*: Ibrahim Shiyam <ibrahimshiyam at gmail.com>*Date*: Thu, 5 Feb 2015 12:03:46 +0000

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

- Previous by Date: [isabelle] Changes in the use of the tab key
- Next by Date: [isabelle] Fwd: Fw: The development of a large proof script.
- Previous by Thread: Re: [isabelle] Changes in the use of the tab key
- Next by Thread: [isabelle] Fwd: Fw: The development of a large proof script.
- Cl-isabelle-users February 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list