equal
deleted
inserted
replaced
93 term Quot_Type.abs |
93 term Quot_Type.abs |
94 |
94 |
95 section {* ML setup *} |
95 section {* ML setup *} |
96 |
96 |
97 (* Auxiliary data for the quotient package *) |
97 (* Auxiliary data for the quotient package *) |
|
98 |
98 use "quotient_info.ML" |
99 use "quotient_info.ML" |
99 |
100 |
100 declare [[map "fun" = (fun_map, fun_rel)]] |
101 declare [[map "fun" = (fun_map, fun_rel)]] |
101 |
102 |
102 lemmas [quot_thm] = fun_quotient |
103 lemmas [quot_thm] = fun_quotient |
145 by (simp add: Quot_True_def) |
146 by (simp add: Quot_True_def) |
146 |
147 |
147 use "quotient_tacs.ML" |
148 use "quotient_tacs.ML" |
148 |
149 |
149 |
150 |
150 (* Atomize infrastructure *) |
|
151 (* FIXME/TODO: is this really needed? *) |
|
152 (* |
|
153 lemma atomize_eqv[atomize]: |
|
154 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
|
155 proof |
|
156 assume "A \<equiv> B" |
|
157 then show "Trueprop A \<equiv> Trueprop B" by unfold |
|
158 next |
|
159 assume *: "Trueprop A \<equiv> Trueprop B" |
|
160 have "A = B" |
|
161 proof (cases A) |
|
162 case True |
|
163 have "A" by fact |
|
164 then show "A = B" using * by simp |
|
165 next |
|
166 case False |
|
167 have "\<not>A" by fact |
|
168 then show "A = B" using * by auto |
|
169 qed |
|
170 then show "A \<equiv> B" by (rule eq_reflection) |
|
171 qed |
|
172 *) |
|
173 |
|
174 section {* Methods / Interface *} |
151 section {* Methods / Interface *} |
175 |
152 |
176 ML {* |
153 ML {* |
177 fun mk_method1 tac thm ctxt = |
154 fun mk_method1 tac thm ctxt = |
178 SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) |
155 SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) |