167 definition |
167 definition |
168 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
168 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
169 where |
169 where |
170 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
170 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
171 |
171 |
172 section {* ATOMIZE *} |
172 section {* atomize *} |
173 |
173 |
174 lemma atomize_eqv[atomize]: |
174 lemma atomize_eqv[atomize]: |
175 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
175 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
176 proof |
176 proof |
177 assume "A \<equiv> B" |
177 assume "A \<equiv> B" |
624 simp_tac simp_ctxt |
624 simp_tac simp_ctxt |
625 ]) |
625 ]) |
626 end |
626 end |
627 *} |
627 *} |
628 |
628 |
629 section {* Injections of REP and ABSes *} |
629 section {* Injections of rep and abses *} |
630 |
630 |
631 (* |
631 (* |
632 Injecting REPABS means: |
632 Injecting repabs means: |
633 |
633 |
634 For abstractions: |
634 For abstractions: |
635 * If the type of the abstraction doesn't need lifting we recurse. |
635 * If the type of the abstraction doesn't need lifting we recurse. |
636 * If it does we add RepAbs around the whole term and check if the |
636 * If it does we add RepAbs around the whole term and check if the |
637 variable needs lifting. |
637 variable needs lifting. |
724 fun quotient_tac ctxt = |
725 fun quotient_tac ctxt = |
725 REPEAT_ALL_NEW (FIRST' |
726 REPEAT_ALL_NEW (FIRST' |
726 [rtac @{thm identity_quotient}, |
727 [rtac @{thm identity_quotient}, |
727 resolve_tac (quotient_rules_get ctxt)]) |
728 resolve_tac (quotient_rules_get ctxt)]) |
728 *} |
729 *} |
729 |
|
730 lemma fun_rel_id: |
|
731 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
|
732 shows "(R1 ===> R2) f g" |
|
733 using a by simp |
|
734 |
730 |
735 definition |
731 definition |
736 "QUOT_TRUE x \<equiv> True" |
732 "QUOT_TRUE x \<equiv> True" |
737 |
733 |
738 ML {* |
734 ML {* |
902 compose_tac (false, thm, 1) 1 |
898 compose_tac (false, thm, 1) 1 |
903 end |
899 end |
904 handle _ => no_tac) |
900 handle _ => no_tac) |
905 | _ => no_tac) |
901 | _ => no_tac) |
906 *} |
902 *} |
|
903 |
|
904 lemma fun_rel_id: |
|
905 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
|
906 shows "(R1 ===> R2) f g" |
|
907 using a by simp |
|
908 |
907 |
909 |
908 ML {* |
910 ML {* |
909 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => |
911 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => |
910 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
912 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
911 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
913 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
1013 | (Const (@{const_name Ball}, _) $ (Const (@{const_name Respects}, _) $ R) $ |
1015 | (Const (@{const_name Ball}, _) $ (Const (@{const_name Respects}, _) $ R) $ |
1014 (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => |
1016 (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => |
1015 let |
1017 let |
1016 val (ty_a, ty_b) = dest_fun_type (fastype_of absf); |
1018 val (ty_a, ty_b) = dest_fun_type (fastype_of absf); |
1017 val thy = ProofContext.theory_of ctxt; |
1019 val thy = ProofContext.theory_of ctxt; |
1018 val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b); |
1020 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
1019 val tyinst = [SOME cty_a, SOME cty_b]; |
|
1020 val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
1021 val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
1021 val thm = Drule.instantiate' tyinst tinst @{thm all_prs}; |
1022 val thm = Drule.instantiate' tyinst tinst @{thm all_prs}; |
1022 val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm]; |
1023 val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm]; |
1023 in |
1024 in |
1024 Conv.rewr_conv ti ctrm |
1025 Conv.rewr_conv ti ctrm |
1026 | (Const (@{const_name Bex}, _) $ (Const (@{const_name Respects}, _) $ R) $ |
1027 | (Const (@{const_name Bex}, _) $ (Const (@{const_name Respects}, _) $ R) $ |
1027 (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => |
1028 (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => |
1028 let |
1029 let |
1029 val (ty_a, ty_b) = dest_fun_type (fastype_of absf); |
1030 val (ty_a, ty_b) = dest_fun_type (fastype_of absf); |
1030 val thy = ProofContext.theory_of ctxt; |
1031 val thy = ProofContext.theory_of ctxt; |
1031 val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b); |
1032 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
1032 val tyinst = [SOME cty_a, SOME cty_b]; |
|
1033 val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
1033 val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
1034 val thm = Drule.instantiate' tyinst tinst @{thm ex_prs}; |
1034 val thm = Drule.instantiate' tyinst tinst @{thm ex_prs}; |
1035 val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm]; |
1035 val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm]; |
1036 in |
1036 in |
1037 Conv.rewr_conv ti ctrm |
1037 Conv.rewr_conv ti ctrm |