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