834 D) unfolding lambda on one side |
834 D) unfolding lambda on one side |
835 E) simplifying (= ===> =) for simpler respectfulness |
835 E) simplifying (= ===> =) for simpler respectfulness |
836 |
836 |
837 *) |
837 *) |
838 |
838 |
|
839 definition |
|
840 "QUOT_TRUE x \<equiv> True" |
|
841 |
|
842 lemma quot_true_dests: |
|
843 shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
|
844 and QT_appL: "QUOT_TRUE (A B) \<Longrightarrow> QUOT_TRUE A" |
|
845 and QT_appR: "QUOT_TRUE (A B) \<Longrightarrow> QUOT_TRUE B" |
|
846 and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
|
847 apply(simp_all add: QUOT_TRUE_def) |
|
848 done |
|
849 |
|
850 |
839 ML {* |
851 ML {* |
840 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
852 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
841 (FIRST' [ |
853 (FIRST' [ |
842 (* "cong" rule of the of the relation / transitivity*) |
854 (* "cong" rule of the of the relation / transitivity*) |
843 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
855 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
844 NDT ctxt "1" (resolve_tac trans2), |
856 DT ctxt "1" (resolve_tac trans2), |
845 |
857 |
846 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
858 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
847 NDT ctxt "2" (lambda_res_tac ctxt), |
859 NDT ctxt "2" (lambda_res_tac ctxt), |
848 |
860 |
849 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
861 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
885 NDT ctxt "D" (resolve_tac rel_refl), |
897 NDT ctxt "D" (resolve_tac rel_refl), |
886 |
898 |
887 (* resolving with R x y assumptions *) |
899 (* resolving with R x y assumptions *) |
888 NDT ctxt "E" (atac), |
900 NDT ctxt "E" (atac), |
889 |
901 |
890 (* seems not necessay:: NDT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*) |
|
891 |
|
892 (* (R1 ===> R2) (\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
|
893 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
|
894 (*NDT ctxt "G" (weak_lambda_res_tac ctxt),*) |
|
895 |
|
896 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
902 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
897 (* global simplification *) |
903 (* global simplification *) |
898 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
904 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
899 *} |
905 *} |
900 |
906 |
927 val _ $ (Abs (_, _, g)) = t; |
933 val _ $ (Abs (_, _, g)) = t; |
928 fun mk_abs i t = |
934 fun mk_abs i t = |
929 if incr_boundvars i u aconv t then Bound i |
935 if incr_boundvars i u aconv t then Bound i |
930 else (case t of |
936 else (case t of |
931 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
937 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
932 | Abs (s, T, t') => Abs (s, T, mk_abs (i+1) t') |
938 | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') |
933 | Bound j => if i = j then error "make_inst" else t |
939 | Bound j => if i = j then error "make_inst" else t |
934 | _ => t); |
940 | _ => t); |
935 in (f, Abs ("x", T, mk_abs 0 g)) end; |
941 in (f, Abs ("x", T, mk_abs 0 g)) end; |
936 |
942 |
937 fun lambda_prs_conv1 ctxt quot_thms ctrm = |
943 fun lambda_prs_conv1 ctxt quot_thms ctrm = |
984 (* |
990 (* |
985 Cleaning the theorem consists of 6 kinds of rewrites. |
991 Cleaning the theorem consists of 6 kinds of rewrites. |
986 The first two need to be done before fun_map is unfolded |
992 The first two need to be done before fun_map is unfolded |
987 |
993 |
988 - LAMBDA_PRS: |
994 - LAMBDA_PRS: |
989 (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) \<Longrightarrow> f |
995 (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f |
|
996 |
990 - FORALL_PRS (and the same for exists: EXISTS_PRS) |
997 - FORALL_PRS (and the same for exists: EXISTS_PRS) |
991 \<forall>x\<in>Respects R. (abs ---> id) ?f \<Longrightarrow> \<forall>x. ?f |
998 \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f |
|
999 |
992 - Rewriting with definitions from the argument defs |
1000 - Rewriting with definitions from the argument defs |
993 NewConst \<Longrightarrow> (rep ---> abs) oldConst |
1001 NewConst ----> (rep ---> abs) oldConst |
|
1002 |
994 - QUOTIENT_REL_REP: |
1003 - QUOTIENT_REL_REP: |
995 Rel (Rep x) (Rep y) \<Longrightarrow> x = y |
1004 Rel (Rep x) (Rep y) ----> x = y |
|
1005 |
996 - ABS_REP |
1006 - ABS_REP |
997 Abs (Rep x) \<Longrightarrow> x |
1007 Abs (Rep x) ----> x |
|
1008 |
998 - id_simps; fun_map.simps |
1009 - id_simps; fun_map.simps |
999 |
1010 |
1000 The first one is implemented as a conversion (fast). |
1011 The first one is implemented as a conversion (fast). |
1001 The second one is an EqSubst (slow). |
1012 The second one is an EqSubst (slow). |
1002 The rest are a simp_tac and are fast. |
1013 The rest are a simp_tac and are fast. |
1003 *) |
1014 *) |
|
1015 |
|
1016 thm all_prs ex_prs |
|
1017 |
|
1018 |
1004 ML {* |
1019 ML {* |
1005 fun clean_tac lthy quot defs = |
1020 fun clean_tac lthy quot defs = |
1006 let |
1021 let |
1007 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
1022 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
1008 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
1023 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |