36 val simplify = Simplifier.simplify; |
35 val simplify = Simplifier.simplify; |
37 open Hypsubst; |
36 open Hypsubst; |
38 open BasicClassical; |
37 open BasicClassical; |
39 open Clasimp; |
38 open Clasimp; |
40 |
39 |
41 val eq_reflection = thm "eq_reflection"; |
40 val all_conj_distrib = thm "all_conj_distrib"; |
42 val def_imp_eq = thm "def_imp_eq"; |
41 val all_dupE = thm "all_dupE" |
43 val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"; |
42 val allE = thm "allE"; |
|
43 val allI = thm "allI"; |
|
44 val all_simps = thms "all_simps"; |
|
45 val arg_cong = thm "arg_cong"; |
|
46 val atomize_not = thm "atomize_not"; |
|
47 val box_equals = thm "box_equals" |
|
48 val case_split = thm "case_split_thm"; |
|
49 val case_split_thm = thm "case_split_thm" |
|
50 val cases_simp = thm "cases_simp"; |
44 val ccontr = thm "ccontr"; |
51 val ccontr = thm "ccontr"; |
45 val impI = thm "impI"; |
52 val choice_eq = thm "choice_eq" |
46 val impCE = thm "impCE"; |
53 val classical = thm "classical"; |
47 val notI = thm "notI"; |
54 val cong = thm "cong" |
48 val notE = thm "notE"; |
55 val conj_comms = thms "conj_comms"; |
49 val iffI = thm "iffI"; |
56 val conj_cong = thm "conj_cong"; |
50 val iffCE = thm "iffCE"; |
57 val conjE = thm "conjE" |
|
58 val conjE = thm "conjE"; |
51 val conjI = thm "conjI"; |
59 val conjI = thm "conjI"; |
52 val conjE = thm "conjE"; |
|
53 val disjCI = thm "disjCI"; |
|
54 val disjE = thm "disjE"; |
|
55 val TrueI = thm "TrueI"; |
|
56 val FalseE = thm "FalseE"; |
|
57 val allI = thm "allI"; |
|
58 val allE = thm "allE"; |
|
59 val exI = thm "exI"; |
|
60 val exE = thm "exE"; |
|
61 val ex_ex1I = thm "ex_ex1I"; |
|
62 val the_equality = thm "the_equality"; |
|
63 val mp = thm "mp"; |
|
64 val rev_mp = thm "rev_mp" |
|
65 val classical = thm "classical"; |
|
66 val subst = thm "subst"; |
|
67 val refl = thm "refl"; |
|
68 val sym = thm "sym"; |
|
69 val trans = thm "trans"; |
|
70 val arg_cong = thm "arg_cong"; |
|
71 val iffD1 = thm "iffD1"; |
|
72 val iffD2 = thm "iffD2"; |
|
73 val disjE = thm "disjE"; |
|
74 val conjE = thm "conjE"; |
|
75 val exE = thm "exE"; |
|
76 val contrapos_nn = thm "contrapos_nn"; |
|
77 val contrapos_pp = thm "contrapos_pp"; |
|
78 val notnotD = thm "notnotD"; |
|
79 val conjunct1 = thm "conjunct1"; |
60 val conjunct1 = thm "conjunct1"; |
80 val conjunct2 = thm "conjunct2"; |
61 val conjunct2 = thm "conjunct2"; |
81 val spec = thm "spec"; |
62 val def_imp_eq = thm "def_imp_eq"; |
82 val imp_cong = thm "imp_cong"; |
|
83 val the_sym_eq_trivial = thm "the_sym_eq_trivial"; |
|
84 val triv_forall_equality = thm "triv_forall_equality"; |
|
85 val case_split = thm "case_split_thm"; |
|
86 val ext = thm "ext" |
|
87 val True_def = thm "True_def" |
|
88 val All_def = thm "All_def" |
|
89 val Ex_def = thm "Ex_def" |
|
90 val False_def = thm "False_def" |
|
91 val not_def = thm "not_def" |
|
92 val and_def = thm "and_def" |
|
93 val or_def = thm "or_def" |
|
94 val Ex1_def = thm "Ex1_def" |
|
95 val iff = thm "iff" |
|
96 val True_or_False = thm "True_or_False" |
|
97 val Let_def = thm "Let_def" |
|
98 val if_def = thm "if_def" |
|
99 val ssubst = thm "ssubst" |
|
100 val box_equals = thm "box_equals" |
|
101 val fun_cong = thm "fun_cong" |
|
102 val cong = thm "cong" |
|
103 val rev_iffD2 = thm "rev_iffD2" |
|
104 val rev_iffD1 = thm "rev_iffD1" |
|
105 val iffE = thm "iffE" |
|
106 val eqTrueI = thm "eqTrueI" |
|
107 val eqTrueE = thm "eqTrueE" |
|
108 val all_dupE = thm "all_dupE" |
|
109 val FalseE = thm "FalseE" |
|
110 val False_neq_True = thm "False_neq_True" |
|
111 val False_not_True = thm "False_not_True" |
|
112 val True_not_False = thm "True_not_False" |
|
113 val notI2 = thm "notI2" |
|
114 val impE = thm "impE" |
|
115 val not_sym = thm "not_sym" |
|
116 val rev_contrapos = thm "rev_contrapos" |
|
117 val conjE = thm "conjE" |
|
118 val context_conjI = thm "context_conjI" |
|
119 val disjI1 = thm "disjI1" |
|
120 val disjI2 = thm "disjI2" |
|
121 val rev_notE = thm "rev_notE" |
|
122 val ex1I = thm "ex1I" |
|
123 val ex1E = thm "ex1E" |
|
124 val ex1_implies_ex = thm "ex1_implies_ex" |
|
125 val the_equality = thm "the_equality" |
|
126 val theI = thm "theI" |
|
127 val theI' = thm "theI'" |
|
128 val theI2 = thm "theI2" |
|
129 val the1_equality = thm "the1_equality" |
|
130 val excluded_middle = thm "excluded_middle" |
|
131 val case_split_thm = thm "case_split_thm" |
|
132 val exCI = thm "exCI" |
|
133 val choice_eq = thm "choice_eq" |
|
134 val eq_cong2 = thm "eq_cong2" |
|
135 val if_cong = thm "if_cong" |
|
136 val if_weak_cong = thm "if_weak_cong" |
|
137 val let_weak_cong = thm "let_weak_cong" |
|
138 val eq_cong2 = thm "eq_cong2" |
|
139 val if_distrib = thm "if_distrib" |
|
140 val restrict_to_left = thm "restrict_to_left" |
|
141 val all_conj_distrib = thm "all_conj_distrib"; |
|
142 val atomize_not = thm "atomize_not"; |
|
143 val split_if = thm "split_if"; |
|
144 val split_if_asm = thm "split_if_asm"; |
|
145 val rev_conj_cong = thm "rev_conj_cong"; |
|
146 val not_all = thm "not_all"; |
|
147 val not_ex = thm "not_ex"; |
|
148 val not_iff = thm "not_iff"; |
|
149 val not_imp = thm "not_imp"; |
|
150 val not_not = thm "not_not"; |
|
151 val eta_contract_eq = thm "eta_contract_eq"; |
|
152 val eq_ac = thms "eq_ac"; |
|
153 val eq_commute = thm "eq_commute"; |
|
154 val eq_sym_conv = thm "eq_commute"; |
|
155 val neq_commute = thm "neq_commute"; |
|
156 val conj_comms = thms "conj_comms"; |
|
157 val conj_commute = thm "conj_commute"; |
|
158 val conj_cong = thm "conj_cong"; |
|
159 val conj_disj_distribL = thm "conj_disj_distribL"; |
|
160 val conj_disj_distribR = thm "conj_disj_distribR"; |
|
161 val conj_left_commute = thm "conj_left_commute"; |
|
162 val disj_comms = thms "disj_comms"; |
|
163 val disj_commute = thm "disj_commute"; |
|
164 val disj_cong = thm "disj_cong"; |
|
165 val disj_conj_distribL = thm "disj_conj_distribL"; |
|
166 val disj_conj_distribR = thm "disj_conj_distribR"; |
|
167 val disj_left_commute = thm "disj_left_commute"; |
|
168 val eq_assoc = thm "eq_assoc"; |
|
169 val eq_left_commute = thm "eq_left_commute"; |
|
170 val ex_disj_distrib = thm "ex_disj_distrib"; |
|
171 val if_P = thm "if_P"; |
|
172 val if_bool_eq_disj = thm "if_bool_eq_disj"; |
|
173 val if_def2 = thm "if_bool_eq_conj"; |
|
174 val if_not_P = thm "if_not_P"; |
|
175 val if_splits = thms "if_splits"; |
|
176 val imp_all = thm "imp_all"; |
|
177 val imp_conjL = thm "imp_conjL"; |
|
178 val imp_conjR = thm "imp_conjR"; |
|
179 val imp_disj_not1 = thm "imp_disj_not1"; |
|
180 val imp_disj_not2 = thm "imp_disj_not2"; |
|
181 val imp_ex = thm "imp_ex"; |
|
182 val meta_eq_to_obj_eq = thm "def_imp_eq"; |
|
183 val ex_simps = thms "ex_simps"; |
|
184 val all_simps = thms "all_simps"; |
|
185 val simp_thms = thms "simp_thms"; |
|
186 val Eq_FalseI = thm "Eq_FalseI"; |
|
187 val Eq_TrueI = thm "Eq_TrueI"; |
|
188 val cases_simp = thm "cases_simp"; |
|
189 val conj_assoc = thm "conj_assoc"; |
|
190 val de_Morgan_conj = thm "de_Morgan_conj"; |
63 val de_Morgan_conj = thm "de_Morgan_conj"; |
191 val de_Morgan_disj = thm "de_Morgan_disj"; |
64 val de_Morgan_disj = thm "de_Morgan_disj"; |
192 val disj_assoc = thm "disj_assoc"; |
65 val disj_assoc = thm "disj_assoc"; |
193 val disj_not1 = thm "disj_not1"; |
66 val disjCI = thm "disjCI"; |
194 val disj_not2 = thm "disj_not2"; |
67 val disj_comms = thms "disj_comms"; |
195 val if_False = thm "if_False"; |
68 val disj_cong = thm "disj_cong"; |
196 val if_True = thm "if_True"; |
69 val disjE = thm "disjE"; |
197 val if_bool_eq_conj = thm "if_bool_eq_conj"; |
70 val disjI1 = thm "disjI1" |
|
71 val disjI2 = thm "disjI2" |
|
72 val eq_ac = thms "eq_ac"; |
|
73 val eq_cong2 = thm "eq_cong2" |
|
74 val Eq_FalseI = thm "Eq_FalseI"; |
|
75 val eq_reflection = thm "eq_reflection"; |
|
76 val Eq_TrueI = thm "Eq_TrueI"; |
|
77 val Ex1_def = thm "Ex1_def" |
|
78 val ex1E = thm "ex1E" |
|
79 val ex1_implies_ex = thm "ex1_implies_ex" |
|
80 val ex1I = thm "ex1I" |
|
81 val excluded_middle = thm "excluded_middle" |
|
82 val ex_disj_distrib = thm "ex_disj_distrib"; |
|
83 val exE = thm "exE"; |
|
84 val exI = thm "exI"; |
|
85 val ex_simps = thms "ex_simps"; |
|
86 val ext = thm "ext" |
|
87 val FalseE = thm "FalseE" |
|
88 val FalseE = thm "FalseE"; |
|
89 val fun_cong = thm "fun_cong" |
198 val if_cancel = thm "if_cancel"; |
90 val if_cancel = thm "if_cancel"; |
199 val if_eq_cancel = thm "if_eq_cancel"; |
91 val if_eq_cancel = thm "if_eq_cancel"; |
|
92 val if_False = thm "if_False"; |
200 val iff_conv_conj_imp = thm "iff_conv_conj_imp"; |
93 val iff_conv_conj_imp = thm "iff_conv_conj_imp"; |
|
94 val iffD1 = thm "iffD1"; |
|
95 val iffD2 = thm "iffD2"; |
|
96 val iffI = thm "iffI"; |
|
97 val iff = thm "iff" |
|
98 val if_splits = thms "if_splits"; |
|
99 val if_True = thm "if_True"; |
|
100 val if_weak_cong = thm "if_weak_cong" |
|
101 val imp_all = thm "imp_all"; |
201 val imp_cong = thm "imp_cong"; |
102 val imp_cong = thm "imp_cong"; |
|
103 val imp_conjL = thm "imp_conjL"; |
|
104 val imp_conjR = thm "imp_conjR"; |
202 val imp_conv_disj = thm "imp_conv_disj"; |
105 val imp_conv_disj = thm "imp_conv_disj"; |
203 val imp_disj1 = thm "imp_disj1"; |
106 val impE = thm "impE" |
204 val imp_disj2 = thm "imp_disj2"; |
107 val impI = thm "impI"; |
205 val imp_disjL = thm "imp_disjL"; |
108 val Let_def = thm "Let_def" |
206 val simp_impliesI = thm "simp_impliesI"; |
109 val meta_eq_to_obj_eq = thm "def_imp_eq"; |
207 val simp_implies_cong = thm "simp_implies_cong"; |
110 val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"; |
|
111 val mp = thm "mp"; |
|
112 val not_all = thm "not_all"; |
|
113 val notE = thm "notE"; |
|
114 val not_ex = thm "not_ex"; |
|
115 val not_iff = thm "not_iff"; |
|
116 val notI = thm "notI"; |
|
117 val not_not = thm "not_not"; |
|
118 val not_sym = thm "not_sym" |
|
119 val refl = thm "refl"; |
|
120 val rev_mp = thm "rev_mp" |
208 val simp_implies_def = thm "simp_implies_def"; |
121 val simp_implies_def = thm "simp_implies_def"; |
|
122 val simp_thms = thms "simp_thms"; |
|
123 val spec = thm "spec"; |
|
124 val split_if = thm "split_if"; |
|
125 val ssubst = thm "ssubst" |
|
126 val subst = thm "subst"; |
|
127 val sym = thm "sym"; |
|
128 val the1_equality = thm "the1_equality" |
|
129 val theI = thm "theI" |
|
130 val theI' = thm "theI'" |
|
131 val trans = thm "trans"; |
209 val True_implies_equals = thm "True_implies_equals"; |
132 val True_implies_equals = thm "True_implies_equals"; |
|
133 val TrueI = thm "TrueI"; |
210 |
134 |
211 structure HOL = |
135 structure HOL = |
212 struct |
136 struct |
213 |
137 |
214 val thy = the_context (); |
138 val thy = the_context (); |