src/HOL/Import/HOL4Setup.thy
 author skalberg Fri Apr 02 17:37:45 2004 +0200 (2004-04-02) changeset 14516 a183dec876ab child 14620 1be590fd2422 permissions -rw-r--r--
1 theory HOL4Setup = MakeEqual
2   files ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML"):
4 section {* General Setup *}
6 lemma eq_imp: "P = Q \<Longrightarrow> P \<longrightarrow> Q"
7   by auto
9 lemma HOLallI: "(!! bogus. P bogus) \<Longrightarrow> (ALL bogus. P bogus)"
10 proof -
11   assume "!! bogus. P bogus"
12   thus "ALL x. P x"
13     ..
14 qed
16 consts
17   ONE_ONE :: "('a => 'b) => bool"
18   ONTO    :: "('a => 'b) => bool"
20 defs
21   ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y"
22   ONTO_DEF   : "ONTO f == ALL y. EX x. y = f x"
24 lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV"
25   by (simp add: ONE_ONE_DEF inj_on_def)
27 lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(ONTO f))"
28 proof (rule exI,safe)
29   show "inj Suc_Rep"
30     by (rule inj_Suc_Rep)
31 next
32   assume "ONTO Suc_Rep"
33   hence "ALL y. EX x. y = Suc_Rep x"
34     by (simp add: ONTO_DEF surj_def)
35   hence "EX x. Zero_Rep = Suc_Rep x"
36     by (rule spec)
37   thus False
38   proof (rule exE)
39     fix x
40     assume "Zero_Rep = Suc_Rep x"
41     hence "Suc_Rep x = Zero_Rep"
42       ..
43     with Suc_Rep_not_Zero_Rep
44     show False
45       ..
46   qed
47 qed
49 lemma EXISTS_DEF: "Ex P = P (Eps P)"
50 proof (rule iffI)
51   assume "Ex P"
52   thus "P (Eps P)"
53     ..
54 next
55   assume "P (Eps P)"
56   thus "Ex P"
57     ..
58 qed
60 consts
61   TYPE_DEFINITION :: "('a => bool) => ('b => 'a) => bool"
63 defs
64   TYPE_DEFINITION: "TYPE_DEFINITION p rep == ((ALL x y. (rep x = rep y) --> (x = y)) & (ALL x. (p x = (EX y. x = rep y))))"
66 lemma ex_imp_nonempty: "Ex P ==> EX x. x : (Collect P)"
67   by simp
69 lemma light_ex_imp_nonempty: "P t ==> EX x. x : (Collect P)"
70 proof -
71   assume "P t"
72   hence "EX x. P x"
73     ..
74   thus ?thesis
75     by (rule ex_imp_nonempty)
76 qed
78 lemma light_imp_as: "[| Q --> P; P --> Q |] ==> P = Q"
79   by blast
81 lemma typedef_hol2hol4:
82   assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)"
83   shows "EX rep. TYPE_DEFINITION P (rep::'a=>'b)"
84 proof -
85   from a
86   have td: "(ALL x. P (Rep x)) & (ALL x. Abs (Rep x) = x) & (ALL y. P y \<longrightarrow> Rep (Abs y) = y)"
88   have ed: "TYPE_DEFINITION P Rep"
89   proof (auto simp add: TYPE_DEFINITION)
90     fix x y
91     assume "Rep x = Rep y"
92     from td have "x = Abs (Rep x)"
93       by auto
94     also have "Abs (Rep x) = Abs (Rep y)"
96     also from td have "Abs (Rep y) = y"
97       by auto
98     finally show "x = y" .
99   next
100     fix x
101     assume "P x"
102     with td
103     have "Rep (Abs x) = x"
104       by auto
105     hence "x = Rep (Abs x)"
106       ..
107     thus "EX y. x = Rep y"
108       ..
109   next
110     fix y
111     from td
112     show "P (Rep y)"
113       by auto
114   qed
115   show ?thesis
116     apply (rule exI [of _ Rep])
117     apply (rule ed)
118     .
119 qed
121 lemma typedef_hol2hollight:
122   assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)"
123   shows "(Abs (Rep a) = a) & (P r = (Rep (Abs r) = r))"
124 proof
125   from a
126   show "Abs (Rep a) = a"
127     by (rule type_definition.Rep_inverse)
128 next
129   show "P r = (Rep (Abs r) = r)"
130   proof
131     assume "P r"
132     hence "r \<in> (Collect P)"
133       by simp
134     with a
135     show "Rep (Abs r) = r"
136       by (rule type_definition.Abs_inverse)
137   next
138     assume ra: "Rep (Abs r) = r"
139     from a
140     have "Rep (Abs r) \<in> (Collect P)"
141       by (rule type_definition.Rep)
142     thus "P r"
144   qed
145 qed
147 lemma termspec_help: "[| Ex P ; c == Eps P |] ==> P c"
148   apply simp
149   apply (rule someI_ex)
150   .
152 lemma typedef_helper: "EX x. P x \<Longrightarrow> EX x. x \<in> (Collect P)"
153   by simp
155 use "hol4rews.ML"
157 setup hol4_setup
158 parse_ast_translation smarter_trueprop_parsing
160 use "proof_kernel.ML"
161 use "replay.ML"
162 use "import_package.ML"
164 setup ImportPackage.setup
166 end