*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Brilliant but broken theory*From*: Victor Porton <porton at narod.ru>*Date*: Tue, 17 Mar 2009 22:40:24 +0200

I have written my first Isabelle theory. It does not verify and my Isar proofs are a monkey-nonsense. Indeed (after being corrected) this will be a very important theory for Isabelle/ZF project. The idea is brilliant, the implementation is poor. My theory defines (bijective) modification ("newbig") of a set ("big") in such a way that an another set "small" becomes it subset. "small" is embedded into big by an injection "embed". Example: We may modify the set of integers ("big") into an another exemplar ("newbig") (that is bijective image) of integers which will contain the set of naturals ("small"); "embed" is the correspondence of naturals to integers. (In the current Isabelle/ZF naturals are not a subset of integers and this needs to be corrected.) We can further extend it to rational, real, and complex numbers, so that our exemplars of these would contain each previous set. Another example: We may want to identify the set of principal filters with the corresponding lattice elements. Then filters is "big", our lattice is "small" and "embed" is the function which maps a lattice element into the corresponding principla filter. I ask you several things: 1. Edit my broken theory in such the way that it would become good quality (first, it should verify). I even ask you to create a perfect example of Isar proofs. I would learn from this example. 2. Put the theory into the Isabelle package. 3. Decide how we will deal and how we will name sets produces using my theory. (The bijective copy of the set "int" could become "int_obj", "int_gen", "int_over_nat", etc. We need to chose a naming convention.) My theory follows: ----------------------------------------------- theory Generalization imports ZF Perm upair begin locale generalization = fixes big::i and small::i fixes embed::i assumes is_inj: "embded: inj(small, big)" begin definition "small2 == range(embed)" definition converse_embed: "spec == converse(embed)" theorem spec_bij: "spec: bij(small2, small)" by auto definition "token == Pow(Union(Union(small)))" lemma token_not_small: "<token,x>~: small" proof assume "<token,x>: small" have "{{token,token}, {token,x}}: small" then "{{token}, {token,x}}: small" then "{token}: Union(small)" then "token <= Union(Union(small))" then "token: Pow(Union(Union(small)))" then "token: token" then show False by mem_not_refl qed definition move_fun::"i=>i" where "move_fun(x) == if x: small2 then spec`x else <token,x>" definition "move == (lam x:big. move_fun(x))" definition "newbig == range(move)" definition ret_def: "ret == converse(move)" theorem "small <= newbig" proof assume "x: small" have "embed`x: small2" then "move`(embed`x) = spec`(embed`x)" then "move`(embed`x) = x" then "x: range(move)" show "x: newbig" qed theorem move_inj: "move: inj(big, newbig)" proof assume "a: big" "b:big" and "move`a = move`b" proof cases assume "a: small2" "b: small2" have "move`a = spec`a" have "move`b = spec`b" have "spec`a = spec`b" using spec_bij show "a = b" next assume "a: small2" "b~: small2" have "move`a = spec`a" have "move`b = <token,b>" have "move`a: small" have "move`b~: small" by token_not_small show "False" next assume "a~: small2" "b: small2" have "move`a = <token,a>" have "move`b = spec`b" have "move`a~: small" have "move`b: small" by token_not_small show "False" next assume "a~: small2" "b~: small2" have "move`a = <token,a>" have "move`b = <token,b>" have "<token,a>=<token,b>" show "a = b" qed show "a = b" qed theorem move_surj: "move: surj(big, newbig)" by auto theorem move_bij: "move: bij(big, newbig)" by auto theorem ret_bij: "ret: bij(newbig, big)" unfolding ret_def using move_bij bij_converse_bij by simp theorem embed_move: "move O embded = id(small)" proof assume "x: small" have "embed`x: small2" have "move`(embed`x) = spec`(embed`x)" from converse_embed have "move`(embed`x) = x" show "move O embded = id(small)" qed end end;

- Previous by Date: [isabelle] More complete theory?
- Next by Date: Re: [isabelle] Slow rule application in case of many parameters?
- Previous by Thread: [isabelle] More complete theory?
- Next by Thread: [isabelle] INRIA post-doc position on proof reconstruction from SMT solvers
- Cl-isabelle-users March 2009 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