288 | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty') |
290 | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty') |
289 | (Bound i, Bound j) => i = j |
291 | (Bound i, Bound j) => i = j |
290 | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t') |
292 | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t') |
291 | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') |
293 | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') |
292 | _ => false |
294 | _ => false |
293 *} |
|
294 |
|
295 section {* Infrastructure for collecting theorems for starting the lifting *} |
|
296 |
|
297 ML {* |
|
298 fun lookup_quot_data lthy qty = |
|
299 let |
|
300 val qty_name = fst (dest_Type qty) |
|
301 val SOME quotdata = quotdata_lookup lthy qty_name |
|
302 (* TODO: Should no longer be needed *) |
|
303 val rty = Logic.unvarifyT (#rtyp quotdata) |
|
304 val rel = #rel quotdata |
|
305 val rel_eqv = #equiv_thm quotdata |
|
306 val rel_refl = @{thm equivp_reflp} OF [rel_eqv] |
|
307 in |
|
308 (rty, rel, rel_refl, rel_eqv) |
|
309 end |
|
310 *} |
|
311 |
|
312 ML {* |
|
313 fun lookup_quot_thms lthy qty_name = |
|
314 let |
|
315 val thy = ProofContext.theory_of lthy; |
|
316 val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2") |
|
317 val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same") |
|
318 val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10") |
|
319 val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name) |
|
320 in |
|
321 (trans2, reps_same, absrep, quot) |
|
322 end |
|
323 *} |
295 *} |
324 |
296 |
325 section {* Regularization *} |
297 section {* Regularization *} |
326 |
298 |
327 (* |
299 (* |
701 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
673 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
702 *} |
674 *} |
703 |
675 |
704 ML {* |
676 ML {* |
705 fun solve_quotient_assums ctxt thm = |
677 fun solve_quotient_assums ctxt thm = |
706 let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in |
678 let |
707 thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)] |
679 val goal = hd (Drule.strip_imp_prems (cprop_of thm)) |
708 end |
680 in |
709 handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" |
681 thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)] |
|
682 end |
|
683 handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" |
710 *} |
684 *} |
711 |
685 |
712 (* Not used *) |
686 (* Not used *) |
713 (* It proves the Quotient assumptions by calling quotient_tac *) |
687 (* It proves the Quotient assumptions by calling quotient_tac *) |
714 ML {* |
688 ML {* |
912 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
886 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
913 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] |
887 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] |
914 |
888 |
915 (* reflexivity of operators arising from Cong_tac *) |
889 (* reflexivity of operators arising from Cong_tac *) |
916 | Const (@{const_name "op ="},_) $ _ $ _ |
890 | Const (@{const_name "op ="},_) $ _ $ _ |
917 => rtac @{thm refl} ORELSE' |
891 => rtac @{thm refl} (*ORELSE' |
918 (resolve_tac trans2 THEN' RANGE [ |
892 (resolve_tac trans2 THEN' RANGE [ |
919 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
893 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])*) |
920 |
894 |
921 (* TODO: These patterns should should be somehow combined and generalized... *) |
895 (* TODO: These patterns should should be somehow combined and generalized... *) |
922 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
896 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
923 (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
897 (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
924 (Const (@{const_name fun_rel}, _) $ _ $ _) |
898 (Const (@{const_name fun_rel}, _) $ _ $ _) |
941 | _ => error "inj_repabs_tac not a relation" |
915 | _ => error "inj_repabs_tac not a relation" |
942 ) i) |
916 ) i) |
943 *} |
917 *} |
944 |
918 |
945 ML {* |
919 ML {* |
946 fun inj_repabs_tac ctxt rel_refl trans2 = |
920 fun inj_repabs_step_tac ctxt rel_refl trans2 = |
947 (FIRST' [ |
921 (FIRST' [ |
948 inj_repabs_tac_match ctxt trans2, |
922 NDT ctxt "0" (inj_repabs_tac_match ctxt trans2), |
949 (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *) |
923 (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *) |
|
924 |
950 NDT ctxt "A" (apply_rsp_tac ctxt THEN' |
925 NDT ctxt "A" (apply_rsp_tac ctxt THEN' |
951 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
926 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)]), |
|
927 |
|
928 (* TODO/FIXME: I had to move this after the apply_rsp_tac - is this right *) |
|
929 NDT ctxt "B" (resolve_tac trans2 THEN' |
|
930 RANGE [quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]), |
|
931 |
952 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
932 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
953 (* merge with previous tactic *) |
933 (* merge with previous tactic *) |
954 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
934 NDT ctxt "C" (Cong_Tac.cong_tac @{thm cong} THEN' |
955 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
935 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
|
936 |
956 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
937 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
957 NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
938 NDT ctxt "D" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
|
939 |
958 (* resolving with R x y assumptions *) |
940 (* resolving with R x y assumptions *) |
959 NDT ctxt "E" (atac), |
941 NDT ctxt "E" (atac), |
|
942 |
960 (* reflexivity of the basic relations *) |
943 (* reflexivity of the basic relations *) |
961 (* R \<dots> \<dots> *) |
944 (* R \<dots> \<dots> *) |
962 NDT ctxt "D" (resolve_tac rel_refl) |
945 NDT ctxt "F" (resolve_tac rel_refl) |
963 ]) |
946 ]) |
964 *} |
947 *} |
965 |
948 |
966 ML {* |
949 ML {* |
967 fun all_inj_repabs_tac ctxt rel_refl trans2 = |
950 fun inj_repabs_tac ctxt = |
968 REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) |
951 let |
|
952 val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt) |
|
953 val trans2 = map (fn x => @{thm equals_rsp} OF [x]) (quotient_rules_get ctxt) |
|
954 in |
|
955 inj_repabs_step_tac ctxt rel_refl trans2 |
|
956 end |
|
957 *} |
|
958 |
|
959 ML {* |
|
960 fun all_inj_repabs_tac ctxt = |
|
961 REPEAT_ALL_NEW (inj_repabs_tac ctxt) |
|
962 (* if this is too slow we can inline the code above *) |
969 *} |
963 *} |
970 |
964 |
971 section {* Cleaning of the theorem *} |
965 section {* Cleaning of the theorem *} |
972 |
966 |
973 ML {* |
967 ML {* |
1188 (rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i |
1182 (rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i |
1189 end) |
1183 end) |
1190 *} |
1184 *} |
1191 |
1185 |
1192 ML {* |
1186 ML {* |
1193 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
|
1194 |
|
1195 fun lift_tac ctxt rthm = |
1187 fun lift_tac ctxt rthm = |
1196 ObjectLogic.full_atomize_tac |
1188 ObjectLogic.full_atomize_tac |
1197 THEN' gen_frees_tac ctxt |
1189 THEN' gen_frees_tac ctxt |
1198 THEN' CSUBGOAL (fn (gl, i) => |
1190 THEN' CSUBGOAL (fn (goal, i) => |
1199 let |
1191 let |
1200 val rthm' = atomize_thm rthm |
1192 val rthm' = atomize_thm rthm |
1201 val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) |
1193 val rule = procedure_inst ctxt (prop_of rthm') (term_of goal) |
1202 val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt) |
1194 val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb goal))] @{thm QUOT_TRUE_i} |
1203 val quotients = quotient_rules_get ctxt |
|
1204 val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients |
|
1205 val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} |
|
1206 in |
1195 in |
1207 (rtac rule THEN' |
1196 (rtac rule THEN' |
1208 RANGE [rtac rthm', |
1197 RANGE [rtac rthm', |
1209 regularize_tac ctxt, |
1198 regularize_tac ctxt, |
1210 rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2, |
1199 rtac thm THEN' all_inj_repabs_tac ctxt, |
1211 clean_tac ctxt]) i |
1200 clean_tac ctxt]) i |
1212 end) |
1201 end) |
1213 *} |
1202 *} |
1214 |
1203 |
1215 end |
1204 end |