summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Sun, 04 Mar 2012 00:03:21 +0100 | |

changeset 46801 | b778cc539601 |

parent 46800 | 9696218b02fe |

child 46802 | 13a3657d0dac |

actually add "the" Importer theory

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Import/Importer.thy Sun Mar 04 00:03:21 2012 +0100 @@ -0,0 +1,239 @@ +(* Title: HOL/Import/Importer.thy + Author: Sebastian Skalberg, TU Muenchen +*) + +theory Importer +imports Main +uses "shuffler.ML" ("import_rews.ML") ("proof_kernel.ML") ("replay.ML") ("import.ML") ("import_syntax.ML") +begin + +setup Shuffler.setup + +lemma conj_norm [shuffle_rule]: "(A & B ==> PROP C) == ([| A ; B |] ==> PROP C)" +proof + assume "A & B ==> PROP C" A B + thus "PROP C" + by auto +next + assume "[| A; B |] ==> PROP C" "A & B" + thus "PROP C" + by auto +qed + +lemma imp_norm [shuffle_rule]: "(Trueprop (A --> B)) == (A ==> B)" +proof + assume "A --> B" A + thus B .. +next + assume "A ==> B" + thus "A --> B" + by auto +qed + +lemma all_norm [shuffle_rule]: "(Trueprop (ALL x. P x)) == (!!x. P x)" +proof + fix x + assume "ALL x. P x" + thus "P x" .. +next + assume "!!x. P x" + thus "ALL x. P x" + .. +qed + +lemma ex_norm [shuffle_rule]: "(EX x. P x ==> PROP Q) == (!!x. P x ==> PROP Q)" +proof + fix x + assume ex: "EX x. P x ==> PROP Q" + assume "P x" + hence "EX x. P x" .. + with ex show "PROP Q" . +next + assume allx: "!!x. P x ==> PROP Q" + assume "EX x. P x" + hence p: "P (SOME x. P x)" + .. + from allx + have "P (SOME x. P x) ==> PROP Q" + . + with p + show "PROP Q" + by auto +qed + +lemma eq_norm [shuffle_rule]: "Trueprop (t = u) == (t == u)" +proof + assume "t = u" + thus "t == u" by simp +next + assume "t == u" + thus "t = u" + by simp +qed + +section {* General Setup *} + +lemma eq_imp: "P = Q \<Longrightarrow> P \<longrightarrow> Q" + by auto + +lemma HOLallI: "(!! bogus. P bogus) \<Longrightarrow> (ALL bogus. P bogus)" +proof - + assume "!! bogus. P bogus" + thus "ALL x. P x" + .. +qed + +consts + ONE_ONE :: "('a => 'b) => bool" + +defs + ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y" + +lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV" + by (simp add: ONE_ONE_DEF inj_on_def) + +lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(surj f))" +proof (rule exI,safe) + show "inj Suc_Rep" + by (rule injI) (rule Suc_Rep_inject) +next + assume "surj Suc_Rep" + hence "ALL y. EX x. y = Suc_Rep x" + by (simp add: surj_def) + hence "EX x. Zero_Rep = Suc_Rep x" + by (rule spec) + thus False + proof (rule exE) + fix x + assume "Zero_Rep = Suc_Rep x" + hence "Suc_Rep x = Zero_Rep" + .. + with Suc_Rep_not_Zero_Rep + show False + .. + qed +qed + +lemma EXISTS_DEF: "Ex P = P (Eps P)" +proof (rule iffI) + assume "Ex P" + thus "P (Eps P)" + .. +next + assume "P (Eps P)" + thus "Ex P" + .. +qed + +consts + TYPE_DEFINITION :: "('a => bool) => ('b => 'a) => bool" + +defs + TYPE_DEFINITION: "TYPE_DEFINITION p rep == ((ALL x y. (rep x = rep y) --> (x = y)) & (ALL x. (p x = (EX y. x = rep y))))" + +lemma ex_imp_nonempty: "Ex P ==> EX x. x : (Collect P)" + by simp + +lemma light_ex_imp_nonempty: "P t ==> EX x. x : (Collect P)" +proof - + assume "P t" + hence "EX x. P x" + .. + thus ?thesis + by (rule ex_imp_nonempty) +qed + +lemma light_imp_as: "[| Q --> P; P --> Q |] ==> P = Q" + by blast + +lemma typedef_hol2hol4: + assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)" + shows "EX rep. TYPE_DEFINITION P (rep::'a=>'b)" +proof - + from a + have td: "(ALL x. P (Rep x)) & (ALL x. Abs (Rep x) = x) & (ALL y. P y \<longrightarrow> Rep (Abs y) = y)" + by (simp add: type_definition_def) + have ed: "TYPE_DEFINITION P Rep" + proof (auto simp add: TYPE_DEFINITION) + fix x y + assume b: "Rep x = Rep y" + from td have "x = Abs (Rep x)" + by auto + also have "Abs (Rep x) = Abs (Rep y)" + by (simp add: b) + also from td have "Abs (Rep y) = y" + by auto + finally show "x = y" . + next + fix x + assume "P x" + with td + have "Rep (Abs x) = x" + by auto + hence "x = Rep (Abs x)" + .. + thus "EX y. x = Rep y" + .. + next + fix y + from td + show "P (Rep y)" + by auto + qed + show ?thesis + apply (rule exI [of _ Rep]) + apply (rule ed) + . +qed + +lemma typedef_hol2hollight: + assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)" + shows "(Abs (Rep a) = a) & (P r = (Rep (Abs r) = r))" +proof + from a + show "Abs (Rep a) = a" + by (rule type_definition.Rep_inverse) +next + show "P r = (Rep (Abs r) = r)" + proof + assume "P r" + hence "r \<in> (Collect P)" + by simp + with a + show "Rep (Abs r) = r" + by (rule type_definition.Abs_inverse) + next + assume ra: "Rep (Abs r) = r" + from a + have "Rep (Abs r) \<in> (Collect P)" + by (rule type_definition.Rep) + thus "P r" + by (simp add: ra) + qed +qed + +lemma termspec_help: "[| Ex P ; c == Eps P |] ==> P c" + apply simp + apply (rule someI_ex) + . + +lemma typedef_helper: "EX x. P x \<Longrightarrow> EX x. x \<in> (Collect P)" + by simp + +use "import_rews.ML" + +setup importer_setup +parse_ast_translation smarter_trueprop_parsing + +use "proof_kernel.ML" +use "replay.ML" +use "import.ML" + +setup Import.setup + +use "import_syntax.ML" + +ML {* Importer_Import_Syntax.setup() *} + +end +