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 |
810 *} |
811 *} |
811 ML Thm.instantiate |
812 ML Thm.instantiate |
812 ML {*@{thm arg_cong2}*} |
813 ML {*@{thm arg_cong2}*} |
813 ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *} |
814 ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *} |
814 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *} |
815 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *} |
815 ML {* |
816 ML {* |
816 Toplevel.program (fn () => |
817 Toplevel.program (fn () => |
817 Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2} |
818 Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2} |
818 ) |
819 ) |
819 *} |
820 *} |
820 |
821 |
834 fun foo_tac n thm = |
835 fun foo_tac n thm = |
835 let |
836 let |
836 val concl = Thm.cprem_of thm n; |
837 val concl = Thm.cprem_of thm n; |
837 val (_, cconcl) = Thm.dest_comb concl; |
838 val (_, cconcl) = Thm.dest_comb concl; |
838 val rewr = foo_conv cconcl; |
839 val rewr = foo_conv cconcl; |
839 val _ = tracing (Display.string_of_thm @{context} rewr) |
840 (* val _ = tracing (Display.string_of_thm @{context} rewr) |
840 val _ = tracing (Display.string_of_thm @{context} thm) |
841 val _ = tracing (Display.string_of_thm @{context} thm)*) |
841 in |
842 in |
842 rtac rewr n thm |
843 rtac rewr n thm |
843 end |
844 end |
844 handle CTERM _ => Seq.empty |
845 handle CTERM _ => Seq.empty |
845 *} |
846 *} |
846 |
847 |
847 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *) |
848 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *) |
848 |
849 |
849 ML {* |
850 ML {* |
850 val foo_tac' = |
851 fun foo_tac' ctxt = |
851 FIRST' [ |
852 REPEAT_ALL_NEW (FIRST' [ |
852 rtac @{thm list_eq_sym}, |
853 rtac @{thm list_eq_sym}, |
853 rtac @{thm cons_preserves}, |
854 rtac @{thm cons_preserves}, |
854 rtac @{thm mem_respects}, |
855 rtac @{thm mem_respects}, |
855 foo_tac, |
856 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
856 simp_tac (@{simpset} addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp}) |
857 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
857 ] |
858 foo_tac |
|
859 ]) |
858 *} |
860 *} |
859 |
861 |
860 thm m1 |
862 thm m1 |
861 |
863 |
862 ML {* |
864 ML {* |
866 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
868 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
867 *} |
869 *} |
868 |
870 |
869 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
871 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
870 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
872 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
871 apply (tactic {* foo_tac' 1 *}) |
873 apply (tactic {* foo_tac' @{context} 1 *}) |
872 apply (tactic {* foo_tac' 1 *}) |
|
873 apply (tactic {* foo_tac' 1 *}) |
|
874 apply (tactic {* foo_tac' 1 *}) |
|
875 apply (tactic {* foo_tac' 1 *}) |
|
876 done |
874 done |
877 |
875 |
878 |
876 |
879 thm length_append (* Not true but worth checking that the goal is correct *) |
877 thm length_append (* Not true but worth checking that the goal is correct *) |
880 ML {* |
878 ML {* |
881 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
879 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
882 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
880 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
883 val cgoal = cterm_of @{theory} goal |
881 val cgoal = cterm_of @{theory} goal |
884 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
882 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
885 *} |
883 *} |
886 (* prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
884 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
887 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
885 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
888 apply (tactic {* foo_tac' 1 *}) |
886 apply (tactic {* foo_tac' @{context} 1 *}) |
889 apply (tactic {* foo_tac' 2 *}) |
887 sorry |
890 apply (tactic {* foo_tac' 2 *}) |
|
891 apply (tactic {* foo_tac' 2 *}) |
|
892 apply (tactic {* foo_tac' 1 *}) *) |
|
893 |
888 |
894 thm m2 |
889 thm m2 |
895 ML {* |
890 ML {* |
896 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2})) |
891 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2})) |
897 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
892 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
898 val cgoal = cterm_of @{theory} goal |
893 val cgoal = cterm_of @{theory} goal |
899 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
894 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
900 *} |
895 *} |
901 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
896 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
902 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
897 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
903 apply (tactic {* foo_tac' 1 *}) |
898 apply (tactic {* foo_tac' @{context} 1 *}) |
904 apply (tactic {* foo_tac' 1 *}) |
|
905 apply (tactic {* foo_tac' 1 *}) |
|
906 apply (tactic {* foo_tac' 1 *}) |
|
907 apply (tactic {* foo_tac' 1 *}) |
|
908 apply (tactic {* foo_tac' 1 *}) |
|
909 apply (tactic {* foo_tac' 1 *}) |
|
910 apply (tactic {* foo_tac' 1 *}) |
|
911 apply (tactic {* foo_tac' 1 *}) |
|
912 apply (tactic {* foo_tac' 1 *}) |
|
913 apply (tactic {* foo_tac' 1 *}) |
|
914 apply (tactic {* foo_tac' 1 *}) |
|
915 apply (tactic {* foo_tac' 1 *}) |
|
916 done |
899 done |
917 |
900 |
918 thm list_eq.intros(4) |
901 thm list_eq.intros(4) |
919 ML {* |
902 ML {* |
920 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)})) |
903 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)})) |
925 *} |
908 *} |
926 |
909 |
927 (* It is the same, but we need a name for it. *) |
910 (* It is the same, but we need a name for it. *) |
928 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} sorry |
911 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} sorry |
929 lemma zzz : |
912 lemma zzz : |
930 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> |
913 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs))) |
931 REP_fset (INSERT a (ABS_fset xs))) = (a # a # xs \<approx> a # xs)" |
914 = (a # a # xs \<approx> a # xs)" |
932 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
915 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
933 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
916 apply (tactic {* foo_tac' @{context} 1 *}) |
934 apply (rule QUOT_TYPE_I_fset.R_trans2) |
|
935 apply (tactic {* foo_tac' 1 *}) |
|
936 apply (tactic {* foo_tac' 1 *}) |
|
937 apply (tactic {* foo_tac' 1 *}) |
|
938 apply (tactic {* foo_tac' 1 *}) |
|
939 apply (tactic {* foo_tac' 1 *}) |
|
940 apply (tactic {* foo_tac' 1 *}) |
|
941 apply (tactic {* foo_tac' 1 *}) |
|
942 apply (tactic {* foo_tac' 1 *}) |
|
943 done |
917 done |
944 |
918 |
945 lemma zzz' : |
919 lemma zzz' : |
946 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))" |
920 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))" |
947 using list_eq.intros(4) by (simp only: zzz) |
921 using list_eq.intros(4) by (simp only: zzz) |
948 |
922 |
949 thm QUOT_TYPE_I_fset.REPS_same |
923 thm QUOT_TYPE_I_fset.REPS_same |
950 ML {* MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} |
924 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} |
|
925 |
|
926 ML Drule.instantiate' |
|
927 ML {* zzz'' *} |
|
928 text {* |
|
929 A variable export will still be necessary in the end, but this is already the final theorem. |
|
930 *} |
|
931 ML {* |
|
932 Toplevel.program (fn () => |
|
933 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
|
934 Drule.instantiate' [] [NONE,SOME (@{cpat "REP_fset x"})] zzz'' |
|
935 ) |
|
936 ) |
|
937 *} |
951 |
938 |
952 thm list_eq.intros(5) |
939 thm list_eq.intros(5) |
953 ML {* |
940 ML {* |
954 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)})) |
941 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)})) |
955 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
942 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
956 val cgoal = cterm_of @{theory} goal |
943 val cgoal = cterm_of @{theory} goal |
957 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
944 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
958 *} |
945 *} |
959 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
946 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
960 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
947 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
961 apply (rule QUOT_TYPE_I_fset.R_trans2) |
948 apply (tactic {* foo_tac' @{context} 1 *}) |
962 apply (tactic {* foo_tac' 1 *}) |
|
963 apply (tactic {* foo_tac' 1 *}) |
|
964 apply (tactic {* foo_tac' 1 *}) |
|
965 apply (tactic {* foo_tac' 1 *}) |
|
966 apply (tactic {* foo_tac' 1 *}) |
|
967 apply (tactic {* foo_tac' 1 *}) |
|
968 apply (tactic {* foo_tac' 1 *}) |
|
969 apply (tactic {* foo_tac' 1 *}) |
|
970 done |
949 done |
971 |
950 |
972 (* |
951 (* |
973 datatype obj1 = |
952 datatype obj1 = |
974 OVAR1 "string" |
953 OVAR1 "string" |