src/HOL/Import/HOL4Setup.thy
 author wenzelm Sat Oct 08 22:39:39 2005 +0200 (2005-10-08) changeset 17801 30cbd2685e73 parent 17322 781abf7011e6 child 19064 bf19cc5a7899 permissions -rw-r--r--
uses susp.ML, lazy_seq.ML, lazy_scan.ML;
 skalberg@14620 1 (* Title: HOL/Import/HOL4Setup.thy skalberg@14620 2 ID: \$Id\$ skalberg@14620 3 Author: Sebastian Skalberg (TU Muenchen) skalberg@14620 4 *) skalberg@14620 5 haftmann@16417 6 theory HOL4Setup imports MakeEqual wenzelm@17801 7 uses "susp.ML" "lazy_seq.ML" "lazy_scan.ML" wenzelm@17801 8 ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin skalberg@14516 9 skalberg@14516 10 section {* General Setup *} skalberg@14516 11 skalberg@14516 12 lemma eq_imp: "P = Q \ P \ Q" skalberg@14516 13 by auto skalberg@14516 14 skalberg@14516 15 lemma HOLallI: "(!! bogus. P bogus) \ (ALL bogus. P bogus)" skalberg@14516 16 proof - skalberg@14516 17 assume "!! bogus. P bogus" skalberg@14516 18 thus "ALL x. P x" skalberg@14516 19 .. skalberg@14516 20 qed skalberg@14516 21 skalberg@14516 22 consts skalberg@14516 23 ONE_ONE :: "('a => 'b) => bool" skalberg@14516 24 ONTO :: "('a => 'b) => bool" skalberg@14516 25 skalberg@14516 26 defs skalberg@14516 27 ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y" skalberg@14516 28 skalberg@14516 29 lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV" skalberg@14516 30 by (simp add: ONE_ONE_DEF inj_on_def) skalberg@14516 31 obua@17322 32 lemma INFINITY_AX: "EX (f::ind \ ind). (inj f & ~(surj f))" skalberg@14516 33 proof (rule exI,safe) skalberg@14516 34 show "inj Suc_Rep" skalberg@14516 35 by (rule inj_Suc_Rep) skalberg@14516 36 next obua@17322 37 assume "surj Suc_Rep" skalberg@14516 38 hence "ALL y. EX x. y = Suc_Rep x" obua@17322 39 by (simp add: surj_def) skalberg@14516 40 hence "EX x. Zero_Rep = Suc_Rep x" skalberg@14516 41 by (rule spec) skalberg@14516 42 thus False skalberg@14516 43 proof (rule exE) skalberg@14516 44 fix x skalberg@14516 45 assume "Zero_Rep = Suc_Rep x" skalberg@14516 46 hence "Suc_Rep x = Zero_Rep" skalberg@14516 47 .. skalberg@14516 48 with Suc_Rep_not_Zero_Rep skalberg@14516 49 show False skalberg@14516 50 .. skalberg@14516 51 qed skalberg@14516 52 qed skalberg@14516 53 skalberg@14516 54 lemma EXISTS_DEF: "Ex P = P (Eps P)" skalberg@14516 55 proof (rule iffI) skalberg@14516 56 assume "Ex P" skalberg@14516 57 thus "P (Eps P)" skalberg@14516 58 .. skalberg@14516 59 next skalberg@14516 60 assume "P (Eps P)" skalberg@14516 61 thus "Ex P" skalberg@14516 62 .. skalberg@14516 63 qed skalberg@14516 64 skalberg@14516 65 consts skalberg@14516 66 TYPE_DEFINITION :: "('a => bool) => ('b => 'a) => bool" skalberg@14516 67 skalberg@14516 68 defs skalberg@14516 69 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 70 skalberg@14516 71 lemma ex_imp_nonempty: "Ex P ==> EX x. x : (Collect P)" skalberg@14516 72 by simp skalberg@14516 73 skalberg@14516 74 lemma light_ex_imp_nonempty: "P t ==> EX x. x : (Collect P)" skalberg@14516 75 proof - skalberg@14516 76 assume "P t" skalberg@14516 77 hence "EX x. P x" skalberg@14516 78 .. skalberg@14516 79 thus ?thesis skalberg@14516 80 by (rule ex_imp_nonempty) skalberg@14516 81 qed skalberg@14516 82 skalberg@14516 83 lemma light_imp_as: "[| Q --> P; P --> Q |] ==> P = Q" skalberg@14516 84 by blast skalberg@14516 85 skalberg@14516 86 lemma typedef_hol2hol4: skalberg@14516 87 assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)" skalberg@14516 88 shows "EX rep. TYPE_DEFINITION P (rep::'a=>'b)" skalberg@14516 89 proof - skalberg@14516 90 from a skalberg@14516 91 have td: "(ALL x. P (Rep x)) & (ALL x. Abs (Rep x) = x) & (ALL y. P y \ Rep (Abs y) = y)" skalberg@14516 92 by (simp add: type_definition_def) skalberg@14516 93 have ed: "TYPE_DEFINITION P Rep" skalberg@14516 94 proof (auto simp add: TYPE_DEFINITION) skalberg@14516 95 fix x y skalberg@14516 96 assume "Rep x = Rep y" skalberg@14516 97 from td have "x = Abs (Rep x)" skalberg@14516 98 by auto skalberg@14516 99 also have "Abs (Rep x) = Abs (Rep y)" skalberg@14516 100 by (simp add: prems) skalberg@14516 101 also from td have "Abs (Rep y) = y" skalberg@14516 102 by auto skalberg@14516 103 finally show "x = y" . skalberg@14516 104 next skalberg@14516 105 fix x skalberg@14516 106 assume "P x" skalberg@14516 107 with td skalberg@14516 108 have "Rep (Abs x) = x" skalberg@14516 109 by auto skalberg@14516 110 hence "x = Rep (Abs x)" skalberg@14516 111 .. skalberg@14516 112 thus "EX y. x = Rep y" skalberg@14516 113 .. skalberg@14516 114 next skalberg@14516 115 fix y skalberg@14516 116 from td skalberg@14516 117 show "P (Rep y)" skalberg@14516 118 by auto skalberg@14516 119 qed skalberg@14516 120 show ?thesis skalberg@14516 121 apply (rule exI [of _ Rep]) skalberg@14516 122 apply (rule ed) skalberg@14516 123 . skalberg@14516 124 qed skalberg@14516 125 skalberg@14516 126 lemma typedef_hol2hollight: skalberg@14516 127 assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)" skalberg@14516 128 shows "(Abs (Rep a) = a) & (P r = (Rep (Abs r) = r))" skalberg@14516 129 proof skalberg@14516 130 from a skalberg@14516 131 show "Abs (Rep a) = a" skalberg@14516 132 by (rule type_definition.Rep_inverse) skalberg@14516 133 next skalberg@14516 134 show "P r = (Rep (Abs r) = r)" skalberg@14516 135 proof skalberg@14516 136 assume "P r" skalberg@14516 137 hence "r \ (Collect P)" skalberg@14516 138 by simp skalberg@14516 139 with a skalberg@14516 140 show "Rep (Abs r) = r" skalberg@14516 141 by (rule type_definition.Abs_inverse) skalberg@14516 142 next skalberg@14516 143 assume ra: "Rep (Abs r) = r" skalberg@14516 144 from a skalberg@14516 145 have "Rep (Abs r) \ (Collect P)" skalberg@14516 146 by (rule type_definition.Rep) skalberg@14516 147 thus "P r" skalberg@14516 148 by (simp add: ra) skalberg@14516 149 qed skalberg@14516 150 qed skalberg@14516 151 skalberg@14516 152 lemma termspec_help: "[| Ex P ; c == Eps P |] ==> P c" skalberg@14516 153 apply simp skalberg@14516 154 apply (rule someI_ex) skalberg@14516 155 . skalberg@14516 156 skalberg@14516 157 lemma typedef_helper: "EX x. P x \ EX x. x \ (Collect P)" skalberg@14516 158 by simp skalberg@14516 159 skalberg@14516 160 use "hol4rews.ML" skalberg@14516 161 skalberg@14516 162 setup hol4_setup skalberg@14516 163 parse_ast_translation smarter_trueprop_parsing skalberg@14516 164 skalberg@14516 165 use "proof_kernel.ML" skalberg@14516 166 use "replay.ML" skalberg@14516 167 use "import_package.ML" skalberg@14516 168 skalberg@14516 169 setup ImportPackage.setup skalberg@14516 170 skalberg@14516 171 end