948 handle CTERM _ => Seq.empty |
948 handle CTERM _ => Seq.empty |
949 *} |
949 *} |
950 |
950 |
951 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *) |
951 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *) |
952 |
952 |
|
953 lemma trueprop_cong: |
|
954 shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)" |
|
955 by auto |
|
956 |
953 ML {* |
957 ML {* |
954 fun foo_tac' ctxt = |
958 fun foo_tac' ctxt = |
955 REPEAT_ALL_NEW (FIRST' [ |
959 REPEAT_ALL_NEW (FIRST' [ |
|
960 rtac @{thm trueprop_cong}, |
956 rtac @{thm list_eq_sym}, |
961 rtac @{thm list_eq_sym}, |
957 rtac @{thm cons_preserves}, |
962 rtac @{thm cons_preserves}, |
958 rtac @{thm mem_respects}, |
963 rtac @{thm mem_respects}, |
959 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
964 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
960 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
965 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
961 foo_tac |
966 foo_tac, |
|
967 CHANGED o (ObjectLogic.full_atomize_tac) |
962 ]) |
968 ]) |
963 *} |
969 *} |
964 |
970 |
965 ML {* |
971 ML {* |
966 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1})) |
972 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1})) |
970 *} |
976 *} |
971 |
977 |
972 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
978 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
973 notation ( output) "Trueprop" ("#_" [1000] 1000) |
979 notation ( output) "Trueprop" ("#_" [1000] 1000) |
974 |
980 |
975 lemma tp: |
|
976 shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)" |
|
977 by auto |
|
978 |
|
979 prove {* (Thm.term_of cgoal2) *} |
981 prove {* (Thm.term_of cgoal2) *} |
980 apply (rule tp) |
|
981 apply (tactic {* ObjectLogic.full_atomize_tac 1 *}) |
|
982 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
982 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
983 apply (tactic {* foo_tac' @{context} 1 *}) |
983 apply (tactic {* foo_tac' @{context} 1 *}) |
984 done |
984 done |
985 |
985 |
986 thm length_append (* Not true but worth checking that the goal is correct *) |
986 thm length_append (* Not true but worth checking that the goal is correct *) |
989 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
989 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
990 val cgoal = cterm_of @{theory} goal |
990 val cgoal = cterm_of @{theory} goal |
991 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
991 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
992 *} |
992 *} |
993 prove {* Thm.term_of cgoal2 *} |
993 prove {* Thm.term_of cgoal2 *} |
994 apply (rule tp) |
|
995 apply (tactic {* ObjectLogic.full_atomize_tac 1 *}) |
|
996 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
994 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
997 apply (tactic {* foo_tac' @{context} 1 *}) |
995 apply (tactic {* foo_tac' @{context} 1 *}) |
998 sorry |
996 sorry |
999 |
997 |
1000 thm m2 |
998 thm m2 |
1003 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1001 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1004 val cgoal = cterm_of @{theory} goal |
1002 val cgoal = cterm_of @{theory} goal |
1005 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1003 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1006 *} |
1004 *} |
1007 prove {* Thm.term_of cgoal2 *} |
1005 prove {* Thm.term_of cgoal2 *} |
1008 apply (rule tp) |
|
1009 apply (tactic {* ObjectLogic.full_atomize_tac 1 *}) |
|
1010 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1006 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1011 apply (tactic {* foo_tac' @{context} 1 *}) |
1007 apply (tactic {* foo_tac' @{context} 1 *}) |
1012 done |
1008 done |
1013 |
1009 |
1014 thm list_eq.intros(4) |
1010 thm list_eq.intros(4) |
1020 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
1016 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
1021 *} |
1017 *} |
1022 |
1018 |
1023 (* It is the same, but we need a name for it. *) |
1019 (* It is the same, but we need a name for it. *) |
1024 prove {* Thm.term_of cgoal3 *} |
1020 prove {* Thm.term_of cgoal3 *} |
1025 apply (rule tp) |
|
1026 apply (tactic {* ObjectLogic.full_atomize_tac 1 *}) |
|
1027 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1021 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1028 apply (tactic {* foo_tac' @{context} 1 *}) |
1022 apply (tactic {* foo_tac' @{context} 1 *}) |
1029 done |
1023 done |
1030 lemma zzz : |
1024 lemma zzz : |
1031 "Trueprop (REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs))) |
1025 "Trueprop (REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs))) |
1032 \<equiv> Trueprop (a # a # xs \<approx> a # xs)" |
1026 \<equiv> Trueprop (a # a # xs \<approx> a # xs)" |
1033 apply (rule tp) |
|
1034 apply (tactic {* ObjectLogic.full_atomize_tac 1 *}) |
|
1035 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1027 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1036 apply (tactic {* foo_tac' @{context} 1 *}) |
1028 apply (tactic {* foo_tac' @{context} 1 *}) |
1037 done |
1029 done |
1038 |
1030 |
1039 lemma zzz' : |
1031 lemma zzz' : |
1070 *} |
1062 *} |
1071 ML {* |
1063 ML {* |
1072 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1064 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1073 *} |
1065 *} |
1074 prove {* Thm.term_of cgoal2 *} |
1066 prove {* Thm.term_of cgoal2 *} |
1075 apply (tactic {* ObjectLogic.full_atomize_tac 1 *}) |
|
1076 apply (rule tp) |
|
1077 apply (tactic {* ObjectLogic.full_atomize_tac 1 *}) |
|
1078 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1067 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1079 apply (tactic {* foo_tac' @{context} 1 *}) |
1068 apply (tactic {* foo_tac' @{context} 1 *}) |
1080 done |
1069 done |
1081 |
1070 |
1082 thm list.induct |
1071 thm list.induct |