equal
deleted
inserted
replaced
733 *} |
733 *} |
734 |
734 |
735 ML {* |
735 ML {* |
736 fun quotient_tac ctxt = |
736 fun quotient_tac ctxt = |
737 REPEAT_ALL_NEW (FIRST' |
737 REPEAT_ALL_NEW (FIRST' |
738 [resolve_tac (quotient_rules_get ctxt), |
738 [rtac @{thm IDENTITY_QUOTIENT}, |
739 (* For functional identity quotients, (op = ---> op =) *) |
739 resolve_tac (quotient_rules_get ctxt)]) |
740 (* TODO: think about the other way around, if we need to shorten the relation *) |
|
741 CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))]) |
|
742 *} |
740 *} |
743 |
741 |
744 |
742 |
745 lemma FUN_REL_I: |
743 lemma FUN_REL_I: |
746 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
744 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
952 (* reflexivity of the basic relations *) |
950 (* reflexivity of the basic relations *) |
953 (* R \<dots> \<dots> *) |
951 (* R \<dots> \<dots> *) |
954 NDT ctxt "D" (resolve_tac rel_refl), |
952 NDT ctxt "D" (resolve_tac rel_refl), |
955 |
953 |
956 (* resolving with R x y assumptions *) |
954 (* resolving with R x y assumptions *) |
957 NDT ctxt "E" (atac), |
955 NDT ctxt "E" (atac) |
958 |
956 |
959 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
957 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
960 (* global simplification *) |
958 (* global simplification *) |
961 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ] eq_reflection[OF LIST_REL_EQ]})))]) |
959 (*NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ] eq_reflection[OF LIST_REL_EQ]})))*) |
|
960 ]) |
962 *} |
961 *} |
963 |
962 |
964 ML {* |
963 ML {* |
965 fun all_inj_repabs_tac ctxt rel_refl trans2 = |
964 fun all_inj_repabs_tac ctxt rel_refl trans2 = |
966 REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) |
965 REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) |