skalberg@14620: (* Title: HOL/Import/HOL4Setup.thy skalberg@14620: ID: $Id$ skalberg@14620: Author: Sebastian Skalberg (TU Muenchen) skalberg@14620: *) skalberg@14620: obua@19064: theory HOL4Setup imports MakeEqual ImportRecorder obua@19064: uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin skalberg@14516: skalberg@14516: section {* General Setup *} skalberg@14516: skalberg@14516: lemma eq_imp: "P = Q \ P \ Q" skalberg@14516: by auto skalberg@14516: skalberg@14516: lemma HOLallI: "(!! bogus. P bogus) \ (ALL bogus. P bogus)" skalberg@14516: proof - skalberg@14516: assume "!! bogus. P bogus" skalberg@14516: thus "ALL x. P x" skalberg@14516: .. skalberg@14516: qed skalberg@14516: skalberg@14516: consts skalberg@14516: ONE_ONE :: "('a => 'b) => bool" skalberg@14516: ONTO :: "('a => 'b) => bool" skalberg@14516: skalberg@14516: defs skalberg@14516: ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y" skalberg@14516: skalberg@14516: lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV" skalberg@14516: by (simp add: ONE_ONE_DEF inj_on_def) skalberg@14516: obua@17322: lemma INFINITY_AX: "EX (f::ind \ ind). (inj f & ~(surj f))" skalberg@14516: proof (rule exI,safe) skalberg@14516: show "inj Suc_Rep" skalberg@14516: by (rule inj_Suc_Rep) skalberg@14516: next obua@17322: assume "surj Suc_Rep" skalberg@14516: hence "ALL y. EX x. y = Suc_Rep x" obua@17322: by (simp add: surj_def) skalberg@14516: hence "EX x. Zero_Rep = Suc_Rep x" skalberg@14516: by (rule spec) skalberg@14516: thus False skalberg@14516: proof (rule exE) skalberg@14516: fix x skalberg@14516: assume "Zero_Rep = Suc_Rep x" skalberg@14516: hence "Suc_Rep x = Zero_Rep" skalberg@14516: .. skalberg@14516: with Suc_Rep_not_Zero_Rep skalberg@14516: show False skalberg@14516: .. skalberg@14516: qed skalberg@14516: qed skalberg@14516: skalberg@14516: lemma EXISTS_DEF: "Ex P = P (Eps P)" skalberg@14516: proof (rule iffI) skalberg@14516: assume "Ex P" skalberg@14516: thus "P (Eps P)" skalberg@14516: .. skalberg@14516: next skalberg@14516: assume "P (Eps P)" skalberg@14516: thus "Ex P" skalberg@14516: .. skalberg@14516: qed skalberg@14516: skalberg@14516: consts skalberg@14516: TYPE_DEFINITION :: "('a => bool) => ('b => 'a) => bool" skalberg@14516: skalberg@14516: defs skalberg@14516: TYPE_DEFINITION: "TYPE_DEFINITION p rep == ((ALL x y. (rep x = rep y) --> (x = y)) & (ALL x. (p x = (EX y. x = rep y))))" skalberg@14516: skalberg@14516: lemma ex_imp_nonempty: "Ex P ==> EX x. x : (Collect P)" skalberg@14516: by simp skalberg@14516: skalberg@14516: lemma light_ex_imp_nonempty: "P t ==> EX x. x : (Collect P)" skalberg@14516: proof - skalberg@14516: assume "P t" skalberg@14516: hence "EX x. P x" skalberg@14516: .. skalberg@14516: thus ?thesis skalberg@14516: by (rule ex_imp_nonempty) skalberg@14516: qed skalberg@14516: skalberg@14516: lemma light_imp_as: "[| Q --> P; P --> Q |] ==> P = Q" skalberg@14516: by blast skalberg@14516: skalberg@14516: lemma typedef_hol2hol4: skalberg@14516: assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)" skalberg@14516: shows "EX rep. TYPE_DEFINITION P (rep::'a=>'b)" skalberg@14516: proof - skalberg@14516: from a skalberg@14516: have td: "(ALL x. P (Rep x)) & (ALL x. Abs (Rep x) = x) & (ALL y. P y \ Rep (Abs y) = y)" skalberg@14516: by (simp add: type_definition_def) skalberg@14516: have ed: "TYPE_DEFINITION P Rep" skalberg@14516: proof (auto simp add: TYPE_DEFINITION) skalberg@14516: fix x y skalberg@14516: assume "Rep x = Rep y" skalberg@14516: from td have "x = Abs (Rep x)" skalberg@14516: by auto skalberg@14516: also have "Abs (Rep x) = Abs (Rep y)" skalberg@14516: by (simp add: prems) skalberg@14516: also from td have "Abs (Rep y) = y" skalberg@14516: by auto skalberg@14516: finally show "x = y" . skalberg@14516: next skalberg@14516: fix x skalberg@14516: assume "P x" skalberg@14516: with td skalberg@14516: have "Rep (Abs x) = x" skalberg@14516: by auto skalberg@14516: hence "x = Rep (Abs x)" skalberg@14516: .. skalberg@14516: thus "EX y. x = Rep y" skalberg@14516: .. skalberg@14516: next skalberg@14516: fix y skalberg@14516: from td skalberg@14516: show "P (Rep y)" skalberg@14516: by auto skalberg@14516: qed skalberg@14516: show ?thesis skalberg@14516: apply (rule exI [of _ Rep]) skalberg@14516: apply (rule ed) skalberg@14516: . skalberg@14516: qed skalberg@14516: skalberg@14516: lemma typedef_hol2hollight: skalberg@14516: assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)" skalberg@14516: shows "(Abs (Rep a) = a) & (P r = (Rep (Abs r) = r))" skalberg@14516: proof skalberg@14516: from a skalberg@14516: show "Abs (Rep a) = a" skalberg@14516: by (rule type_definition.Rep_inverse) skalberg@14516: next skalberg@14516: show "P r = (Rep (Abs r) = r)" skalberg@14516: proof skalberg@14516: assume "P r" skalberg@14516: hence "r \ (Collect P)" skalberg@14516: by simp skalberg@14516: with a skalberg@14516: show "Rep (Abs r) = r" skalberg@14516: by (rule type_definition.Abs_inverse) skalberg@14516: next skalberg@14516: assume ra: "Rep (Abs r) = r" skalberg@14516: from a skalberg@14516: have "Rep (Abs r) \ (Collect P)" skalberg@14516: by (rule type_definition.Rep) skalberg@14516: thus "P r" skalberg@14516: by (simp add: ra) skalberg@14516: qed skalberg@14516: qed skalberg@14516: skalberg@14516: lemma termspec_help: "[| Ex P ; c == Eps P |] ==> P c" skalberg@14516: apply simp skalberg@14516: apply (rule someI_ex) skalberg@14516: . skalberg@14516: skalberg@14516: lemma typedef_helper: "EX x. P x \ EX x. x \ (Collect P)" skalberg@14516: by simp skalberg@14516: skalberg@14516: use "hol4rews.ML" skalberg@14516: skalberg@14516: setup hol4_setup skalberg@14516: parse_ast_translation smarter_trueprop_parsing skalberg@14516: skalberg@14516: use "proof_kernel.ML" skalberg@14516: use "replay.ML" skalberg@14516: use "import_package.ML" skalberg@14516: skalberg@14516: setup ImportPackage.setup skalberg@14516: skalberg@14516: end