
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 \<Longrightarrow> P \<longrightarrow> Q"
skalberg@14516:   by auto
skalberg@14516: 
skalberg@14516: lemma HOLallI: "(!! bogus. P bogus) \<Longrightarrow> (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 \<Rightarrow> 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 \<longrightarrow> 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 \<in> (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) \<in> (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 \<Longrightarrow> EX x. x \<in> (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




