820 apply (simp add: yyy) |
820 apply (simp add: yyy) |
821 apply (simp add: QUOT_TYPE_I_fset.thm10) |
821 apply (simp add: QUOT_TYPE_I_fset.thm10) |
822 done |
822 done |
823 |
823 |
824 ML {* |
824 ML {* |
825 fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x) |
825 fun mk_rep x = @{term REP_fset} $ x; |
|
826 fun mk_abs x = @{term ABS_fset} $ x; |
826 val consts = [@{const_name "Nil"}, @{const_name "append"}, |
827 val consts = [@{const_name "Nil"}, @{const_name "append"}, |
827 @{const_name "Cons"}, @{const_name "membship"}, |
828 @{const_name "Cons"}, @{const_name "membship"}, |
828 @{const_name "card1"}] |
829 @{const_name "card1"}] |
829 *} |
830 *} |
830 |
831 |
831 ML {* |
832 ML {* |
832 fun build_goal ctxt thm constructors qty mk_rep_abs = |
833 fun build_goal ctxt thm constructors rty qty mk_rep mk_abs = |
833 let |
834 let |
|
835 fun mk_rep_abs x = mk_rep (mk_abs x); |
|
836 |
834 fun is_constructor (Const (x, _)) = member (op =) constructors x |
837 fun is_constructor (Const (x, _)) = member (op =) constructors x |
835 | is_constructor _ = false; |
838 | is_constructor _ = false; |
836 |
839 |
837 fun maybe_mk_rep_abs t = |
840 fun maybe_mk_rep_abs t = |
838 let |
841 let |
839 val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t) |
842 val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t) |
840 in |
843 in |
841 if type_of t = qty then mk_rep_abs t else t |
844 if fastype_of t = rty then mk_rep_abs t else t |
842 end; |
845 end; |
843 |
846 |
844 fun build_aux ctxt1 tm = |
847 fun build_aux ctxt1 tm = |
845 let |
848 let |
846 val (head, args) = Term.strip_comb tm; |
849 val (head, args) = Term.strip_comb tm; |
847 val args' = map (build_aux ctxt1) args; |
850 val args' = map (build_aux ctxt1) args; |
848 in |
851 in |
849 (case head of |
852 (case head of |
850 Abs (x, T, t) => |
853 Abs (x, T, t) => |
851 let |
854 if T = rty then let |
|
855 val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1; |
|
856 val v = Free (x', qty); |
|
857 val t' = subst_bound (mk_rep v, t); |
|
858 val rec_term = build_aux ctxt2 t'; |
|
859 val _ = tracing (Syntax.string_of_term ctxt2 t') |
|
860 val _ = tracing (Syntax.string_of_term ctxt2 (Term.lambda_name (x, v) rec_term)) |
|
861 in |
|
862 Term.lambda_name (x, v) rec_term |
|
863 end else let |
852 val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1; |
864 val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1; |
853 val v = Free (x', T); |
865 val v = Free (x', T); |
854 val t' = subst_bound (v, t); |
866 val t' = subst_bound (v, t); |
855 val rec_term = build_aux ctxt2 t'; |
867 val rec_term = build_aux ctxt2 t'; |
856 in Term.lambda_name (x, v) rec_term end |
868 in Term.lambda_name (x, v) rec_term end |
971 ]) |
983 ]) |
972 *} |
984 *} |
973 |
985 |
974 ML {* |
986 ML {* |
975 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) |
987 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) |
976 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs |
988 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
977 val cgoal = cterm_of @{theory} goal |
989 val cgoal = cterm_of @{theory} goal |
978 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
990 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
979 *} |
991 *} |
980 |
992 |
981 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
993 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
1007 done |
1019 done |
1008 |
1020 |
1009 thm length_append (* Not true but worth checking that the goal is correct *) |
1021 thm length_append (* Not true but worth checking that the goal is correct *) |
1010 ML {* |
1022 ML {* |
1011 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append})) |
1023 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append})) |
1012 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs |
1024 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
1013 val cgoal = cterm_of @{theory} goal |
1025 val cgoal = cterm_of @{theory} goal |
1014 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1026 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1015 *} |
1027 *} |
1016 prove {* Thm.term_of cgoal2 *} |
1028 prove {* Thm.term_of cgoal2 *} |
1017 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1029 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1019 sorry |
1031 sorry |
1020 |
1032 |
1021 thm m2 |
1033 thm m2 |
1022 ML {* |
1034 ML {* |
1023 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) |
1035 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) |
1024 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs |
1036 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
1025 val cgoal = cterm_of @{theory} goal |
1037 val cgoal = cterm_of @{theory} goal |
1026 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1038 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1027 *} |
1039 *} |
1028 prove {* Thm.term_of cgoal2 *} |
1040 prove {* Thm.term_of cgoal2 *} |
1029 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1041 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1031 done |
1043 done |
1032 |
1044 |
1033 thm list_eq.intros(4) |
1045 thm list_eq.intros(4) |
1034 ML {* |
1046 ML {* |
1035 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)})) |
1047 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)})) |
1036 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs |
1048 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
1037 val cgoal = cterm_of @{theory} goal |
1049 val cgoal = cterm_of @{theory} goal |
1038 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1050 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1039 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
1051 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
1040 *} |
1052 *} |
1041 |
1053 |
1078 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) |
1090 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) |
1079 *} |
1091 *} |
1080 ML {* |
1092 ML {* |
1081 val goal = |
1093 val goal = |
1082 Toplevel.program (fn () => |
1094 Toplevel.program (fn () => |
1083 build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs |
1095 build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
1084 ) |
1096 ) |
1085 *} |
1097 *} |
1086 ML {* |
1098 term all |
1087 val cgoal = cterm_of @{theory} goal |
1099 ML {* |
|
1100 val cgoal = |
|
1101 Toplevel.program (fn () => |
|
1102 cterm_of @{theory} goal |
|
1103 ) |
1088 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1104 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1089 *} |
1105 *} |
1090 |
1106 |
1091 prove {* (Thm.term_of cgoal2) *} |
1107 prove {* (Thm.term_of cgoal2) *} |
1092 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1108 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1095 |
1111 |
1096 ML {* |
1112 ML {* |
1097 fun lift_theorem_fset_aux thm lthy = |
1113 fun lift_theorem_fset_aux thm lthy = |
1098 let |
1114 let |
1099 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
1115 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
1100 val goal = build_goal @{context} novars consts @{typ "'a list"} mk_rep_abs; |
1116 val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs; |
1101 val cgoal = cterm_of @{theory} goal; |
1117 val cgoal = cterm_of @{theory} goal; |
1102 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); |
1118 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); |
1103 val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (foo_tac' @{context}) 1; |
1119 val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (foo_tac' @{context}) 1; |
1104 val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); |
1120 val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); |
1105 val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) |
1121 val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) |