112 then have "R b a" using bd R_trans by blast |
112 then have "R b a" using bd R_trans by blast |
113 then show "R a b" using R_sym by blast |
113 then show "R a b" using R_sym by blast |
114 qed |
114 qed |
115 |
115 |
116 lemma REPS_same: |
116 lemma REPS_same: |
117 shows "R (REP a) (REP b) = (a = b)" |
117 shows "R (REP a) (REP b) \<equiv> (a = b)" |
|
118 apply (rule eq_reflection) |
118 proof |
119 proof |
119 assume as: "R (REP a) (REP b)" |
120 assume as: "R (REP a) (REP b)" |
120 from rep_prop |
121 from rep_prop |
121 obtain x y |
122 obtain x y |
122 where eqs: "Rep a = R x" "Rep b = R y" by blast |
123 where eqs: "Rep a = R x" "Rep b = R y" by blast |
123 from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp |
124 from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp |
124 then have "R x (Eps (R y))" using lem9 by simp |
125 then have "R x (Eps (R y))" using lem9 by simp |
125 then have "R (Eps (R y)) x" using R_sym by blast |
126 then have "R (Eps (R y)) x" using R_sym by blast |
126 then have "R y x" using lem9 by simp |
127 then have "R y x" using lem9 by simp |
825 *} |
826 *} |
826 ML Thm.instantiate |
827 ML Thm.instantiate |
827 ML {*@{thm arg_cong2}*} |
828 ML {*@{thm arg_cong2}*} |
828 ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *} |
829 ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *} |
829 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *} |
830 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *} |
830 ML {* |
831 ML {* |
831 Toplevel.program (fn () => |
832 Toplevel.program (fn () => |
832 Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2} |
833 Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2} |
833 ) |
834 ) |
834 *} |
835 *} |
835 |
836 |
849 fun foo_tac n thm = |
850 fun foo_tac n thm = |
850 let |
851 let |
851 val concl = Thm.cprem_of thm n; |
852 val concl = Thm.cprem_of thm n; |
852 val (_, cconcl) = Thm.dest_comb concl; |
853 val (_, cconcl) = Thm.dest_comb concl; |
853 val rewr = foo_conv cconcl; |
854 val rewr = foo_conv cconcl; |
854 val _ = tracing (Display.string_of_thm @{context} rewr) |
855 (* val _ = tracing (Display.string_of_thm @{context} rewr) |
855 val _ = tracing (Display.string_of_thm @{context} thm) |
856 val _ = tracing (Display.string_of_thm @{context} thm)*) |
856 in |
857 in |
857 rtac rewr n thm |
858 rtac rewr n thm |
858 end |
859 end |
859 handle CTERM _ => Seq.empty |
860 handle CTERM _ => Seq.empty |
860 *} |
861 *} |
861 |
862 |
862 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *) |
863 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *) |
863 |
864 |
864 ML {* |
865 ML {* |
865 val foo_tac' = |
866 fun foo_tac' ctxt = |
866 FIRST' [ |
867 REPEAT_ALL_NEW (FIRST' [ |
867 rtac @{thm list_eq_sym}, |
868 rtac @{thm list_eq_sym}, |
868 rtac @{thm cons_preserves}, |
869 rtac @{thm cons_preserves}, |
869 rtac @{thm mem_respects}, |
870 rtac @{thm mem_respects}, |
870 foo_tac, |
871 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
871 simp_tac (@{simpset} addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp}) |
872 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
872 ] |
873 foo_tac |
|
874 ]) |
873 *} |
875 *} |
874 |
876 |
875 thm m1 |
877 thm m1 |
876 |
878 |
877 ML {* |
879 ML {* |
881 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
883 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
882 *} |
884 *} |
883 |
885 |
884 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
886 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
885 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
887 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
886 apply (tactic {* foo_tac' 1 *}) |
888 apply (tactic {* foo_tac' @{context} 1 *}) |
887 apply (tactic {* foo_tac' 1 *}) |
|
888 apply (tactic {* foo_tac' 1 *}) |
|
889 apply (tactic {* foo_tac' 1 *}) |
|
890 apply (tactic {* foo_tac' 1 *}) |
|
891 done |
889 done |
892 |
890 |
893 |
891 |
894 thm length_append (* Not true but worth checking that the goal is correct *) |
892 thm length_append (* Not true but worth checking that the goal is correct *) |
895 ML {* |
893 ML {* |
896 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
894 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
897 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
895 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
898 val cgoal = cterm_of @{theory} goal |
896 val cgoal = cterm_of @{theory} goal |
899 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
897 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
900 *} |
898 *} |
901 (* prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
899 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
902 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
900 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
903 apply (tactic {* foo_tac' 1 *}) |
901 apply (tactic {* foo_tac' @{context} 1 *}) |
904 apply (tactic {* foo_tac' 2 *}) |
902 sorry |
905 apply (tactic {* foo_tac' 2 *}) |
|
906 apply (tactic {* foo_tac' 2 *}) |
|
907 apply (tactic {* foo_tac' 1 *}) *) |
|
908 |
903 |
909 thm m2 |
904 thm m2 |
910 ML {* |
905 ML {* |
911 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2})) |
906 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2})) |
912 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
907 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
913 val cgoal = cterm_of @{theory} goal |
908 val cgoal = cterm_of @{theory} goal |
914 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
909 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
915 *} |
910 *} |
916 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
911 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
917 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
912 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
918 apply (tactic {* foo_tac' 1 *}) |
913 apply (tactic {* foo_tac' @{context} 1 *}) |
919 apply (tactic {* foo_tac' 1 *}) |
|
920 apply (tactic {* foo_tac' 1 *}) |
|
921 apply (tactic {* foo_tac' 1 *}) |
|
922 apply (tactic {* foo_tac' 1 *}) |
|
923 apply (tactic {* foo_tac' 1 *}) |
|
924 apply (tactic {* foo_tac' 1 *}) |
|
925 apply (tactic {* foo_tac' 1 *}) |
|
926 apply (tactic {* foo_tac' 1 *}) |
|
927 apply (tactic {* foo_tac' 1 *}) |
|
928 apply (tactic {* foo_tac' 1 *}) |
|
929 apply (tactic {* foo_tac' 1 *}) |
|
930 apply (tactic {* foo_tac' 1 *}) |
|
931 done |
914 done |
932 |
915 |
933 thm list_eq.intros(4) |
916 thm list_eq.intros(4) |
934 ML {* |
917 ML {* |
935 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)})) |
918 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)})) |
940 *} |
923 *} |
941 |
924 |
942 (* It is the same, but we need a name for it. *) |
925 (* It is the same, but we need a name for it. *) |
943 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} sorry |
926 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} sorry |
944 lemma zzz : |
927 lemma zzz : |
945 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> |
928 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs))) |
946 REP_fset (INSERT a (ABS_fset xs))) = (a # a # xs \<approx> a # xs)" |
929 = (a # a # xs \<approx> a # xs)" |
947 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
930 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
948 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
931 apply (tactic {* foo_tac' @{context} 1 *}) |
949 apply (rule QUOT_TYPE_I_fset.R_trans2) |
|
950 apply (tactic {* foo_tac' 1 *}) |
|
951 apply (tactic {* foo_tac' 1 *}) |
|
952 apply (tactic {* foo_tac' 1 *}) |
|
953 apply (tactic {* foo_tac' 1 *}) |
|
954 apply (tactic {* foo_tac' 1 *}) |
|
955 apply (tactic {* foo_tac' 1 *}) |
|
956 apply (tactic {* foo_tac' 1 *}) |
|
957 apply (tactic {* foo_tac' 1 *}) |
|
958 done |
932 done |
959 |
933 |
960 lemma zzz' : |
934 lemma zzz' : |
961 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))" |
935 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))" |
962 using list_eq.intros(4) by (simp only: zzz) |
936 using list_eq.intros(4) by (simp only: zzz) |
963 |
937 |
964 thm QUOT_TYPE_I_fset.REPS_same |
938 thm QUOT_TYPE_I_fset.REPS_same |
965 ML {* MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} |
939 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} |
|
940 |
|
941 ML Drule.instantiate' |
|
942 ML {* zzz'' *} |
|
943 text {* |
|
944 A variable export will still be necessary in the end, but this is already the final theorem. |
|
945 *} |
|
946 ML {* |
|
947 Toplevel.program (fn () => |
|
948 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
|
949 Drule.instantiate' [] [NONE,SOME (@{cpat "REP_fset x"})] zzz'' |
|
950 ) |
|
951 ) |
|
952 *} |
966 |
953 |
967 thm list_eq.intros(5) |
954 thm list_eq.intros(5) |
968 ML {* |
955 ML {* |
969 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)})) |
956 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)})) |
970 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
957 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
971 val cgoal = cterm_of @{theory} goal |
958 val cgoal = cterm_of @{theory} goal |
972 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
959 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
973 *} |
960 *} |
974 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
961 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
975 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
962 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
976 apply (rule QUOT_TYPE_I_fset.R_trans2) |
963 apply (tactic {* foo_tac' @{context} 1 *}) |
977 apply (tactic {* foo_tac' 1 *}) |
|
978 apply (tactic {* foo_tac' 1 *}) |
|
979 apply (tactic {* foo_tac' 1 *}) |
|
980 apply (tactic {* foo_tac' 1 *}) |
|
981 apply (tactic {* foo_tac' 1 *}) |
|
982 apply (tactic {* foo_tac' 1 *}) |
|
983 apply (tactic {* foo_tac' 1 *}) |
|
984 apply (tactic {* foo_tac' 1 *}) |
|
985 done |
964 done |
986 |
965 |
987 (* |
966 (* |
988 datatype obj1 = |
967 datatype obj1 = |
989 OVAR1 "string" |
968 OVAR1 "string" |