145 declare [[map * = (prod_fun, prod_rel)]] |
145 declare [[map * = (prod_fun, prod_rel)]] |
146 declare [[map "fun" = (fun_map, fun_rel)]] |
146 declare [[map "fun" = (fun_map, fun_rel)]] |
147 (* Throws now an exception: *) |
147 (* Throws now an exception: *) |
148 (* declare [[map "option" = (bla, blu)]] *) |
148 (* declare [[map "option" = (bla, blu)]] *) |
149 |
149 |
150 |
|
151 (* identity quotient is not here as it has to be applied first *) |
|
152 lemmas [quotient_thm] = |
150 lemmas [quotient_thm] = |
153 fun_quotient prod_quotient |
151 fun_quotient prod_quotient |
154 |
152 |
155 lemmas [quotient_rsp] = |
153 lemmas [quotient_rsp] = |
156 quot_rel_rsp pair_rsp |
154 quot_rel_rsp pair_rsp |
158 (* fun_map is not here since equivp is not true *) |
156 (* fun_map is not here since equivp is not true *) |
159 (* TODO: option, ... *) |
157 (* TODO: option, ... *) |
160 lemmas [quotient_equiv] = |
158 lemmas [quotient_equiv] = |
161 identity_equivp prod_equivp |
159 identity_equivp prod_equivp |
162 |
160 |
163 |
|
164 (* definition of the quotient types *) |
161 (* definition of the quotient types *) |
165 (* FIXME: should be called quotient_typ.ML *) |
162 (* FIXME: should be called quotient_typ.ML *) |
166 use "quotient.ML" |
163 use "quotient.ML" |
167 |
164 |
168 |
|
169 (* lifting of constants *) |
165 (* lifting of constants *) |
170 use "quotient_def.ML" |
166 use "quotient_def.ML" |
171 |
167 |
172 section {* Simset setup *} |
168 section {* Simset setup *} |
173 |
169 |
174 (* since HOL_basic_ss is too "big", we need to set up *) |
170 (* Since HOL_basic_ss is too "big" for us, *) |
175 (* our own minimal simpset *) |
171 (* we set up our own minimal simpset. *) |
176 ML {* |
172 ML {* |
177 fun mk_minimal_ss ctxt = |
173 fun mk_minimal_ss ctxt = |
178 Simplifier.context ctxt empty_ss |
174 Simplifier.context ctxt empty_ss |
179 setsubgoaler asm_simp_tac |
175 setsubgoaler asm_simp_tac |
180 setmksimps (mksimps []) |
176 setmksimps (mksimps []) |
181 *} |
177 *} |
182 |
178 |
183 ML {* |
179 ML {* |
184 (* TODO/FIXME not needed anymore? *) |
|
185 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
|
186 |
|
187 fun OF1 thm1 thm2 = thm2 RS thm1 |
180 fun OF1 thm1 thm2 = thm2 RS thm1 |
188 *} |
181 *} |
189 |
182 |
190 section {* atomize *} |
183 section {* Atomize Infrastructure *} |
191 |
184 |
192 lemma atomize_eqv[atomize]: |
185 lemma atomize_eqv[atomize]: |
193 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
186 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
194 proof |
187 proof |
195 assume "A \<equiv> B" |
188 assume "A \<equiv> B" |
217 in |
210 in |
218 @{thm equal_elim_rule1} OF [thm'', thm'] |
211 @{thm equal_elim_rule1} OF [thm'', thm'] |
219 end |
212 end |
220 *} |
213 *} |
221 |
214 |
222 section {* infrastructure about id *} |
215 section {* Infrastructure about id *} |
|
216 |
|
217 print_attributes |
223 |
218 |
224 (* TODO: think where should this be *) |
219 (* TODO: think where should this be *) |
225 lemma prod_fun_id: "prod_fun id id \<equiv> id" |
220 lemma prod_fun_id: "prod_fun id id \<equiv> id" |
226 by (rule eq_reflection) (simp add: prod_fun_def) |
221 by (rule eq_reflection) (simp add: prod_fun_def) |
227 |
222 |
228 (* FIXME: make it a list and add map_id to it *) |
223 lemmas [id_simps] = |
229 lemmas id_simps = |
|
230 fun_map_id[THEN eq_reflection] |
224 fun_map_id[THEN eq_reflection] |
231 id_apply[THEN eq_reflection] |
225 id_apply[THEN eq_reflection] |
232 id_def[THEN eq_reflection,symmetric] |
226 id_def[THEN eq_reflection,symmetric] |
233 prod_fun_id |
227 prod_fun_id |
234 |
|
235 ML {* |
|
236 fun simp_ids thm = |
|
237 MetaSimplifier.rewrite_rule @{thms id_simps} thm |
|
238 *} |
|
239 |
228 |
240 section {* Debugging infrastructure for testing tactics *} |
229 section {* Debugging infrastructure for testing tactics *} |
241 |
230 |
242 ML {* |
231 ML {* |
243 fun my_print_tac ctxt s i thm = |
232 fun my_print_tac ctxt s i thm = |
1006 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
995 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
1007 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
996 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
1008 val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
997 val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
1009 val ti = |
998 val ti = |
1010 (let |
999 (let |
1011 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1000 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
1012 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
1001 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
1013 in |
1002 in |
1014 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1003 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1015 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
1004 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
1016 let |
1005 let |
1017 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) |
1006 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) |
1018 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
1007 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
1019 in |
1008 in |
1020 MetaSimplifier.rewrite_rule @{thms id_simps} td |
1009 MetaSimplifier.rewrite_rule (id_simps_get ctxt) td |
1021 end); |
1010 end); |
1022 val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then |
1011 val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then |
1023 (tracing "lambda_prs"; |
1012 (tracing "lambda_prs"; |
1024 tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); |
1013 tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); |
1025 tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi))); |
1014 tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi))); |
1043 (* 1. conversion (is not a pattern) *) |
1032 (* 1. conversion (is not a pattern) *) |
1044 thm lambda_prs |
1033 thm lambda_prs |
1045 (* 2. folding of definitions: (rep ---> abs) oldConst == newconst *) |
1034 (* 2. folding of definitions: (rep ---> abs) oldConst == newconst *) |
1046 (* and simplification with *) |
1035 (* and simplification with *) |
1047 thm all_prs ex_prs |
1036 thm all_prs ex_prs |
1048 (* 3. simplification with *) |
1037 (* 3. simplification with id_simps and *) |
1049 thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep |
1038 thm fun_map.simps Quotient_abs_rep Quotient_rel_rep |
1050 (* 4. Test for refl *) |
1039 (* 4. Test for refl *) |
1051 |
1040 |
1052 ML {* |
1041 ML {* |
1053 fun clean_tac lthy = |
1042 fun clean_tac lthy = |
1054 let |
1043 let |
1055 val thy = ProofContext.theory_of lthy; |
1044 val thy = ProofContext.theory_of lthy; |
1056 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1045 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1057 (* FIXME: shouldn't the definitions already be varified? *) |
1046 (* FIXME: shouldn't the definitions already be varified? *) |
1058 val thms1 = @{thms all_prs ex_prs} @ defs |
1047 val thms1 = @{thms all_prs ex_prs} @ defs |
1059 val thms2 = @{thms eq_reflection[OF fun_map.simps]} |
1048 val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ (id_simps_get lthy) |
1060 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} |
1049 @ @{thms Quotient_abs_rep Quotient_rel_rep} |
1061 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1050 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1062 in |
1051 in |
1063 EVERY' [lambda_prs_tac lthy, |
1052 EVERY' [lambda_prs_tac lthy, |
1064 simp_tac (simps thms1), |
1053 simp_tac (simps thms1), |
1065 simp_tac (simps thms2), |
1054 simp_tac (simps thms2), |