1065 using list_eq.intros(4) by (simp only: zzz) |
1065 using list_eq.intros(4) by (simp only: zzz) |
1066 |
1066 |
1067 thm QUOT_TYPE_I_fset.REPS_same |
1067 thm QUOT_TYPE_I_fset.REPS_same |
1068 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} |
1068 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} |
1069 |
1069 |
1070 ML Drule.instantiate' |
|
1071 ML {* zzz'' *} |
|
1072 text {* |
|
1073 A variable export will still be necessary in the end, but this is already the final theorem. |
|
1074 *} |
|
1075 ML {* |
|
1076 Toplevel.program (fn () => |
|
1077 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
|
1078 Drule.instantiate' [] [NONE, SOME (@{cpat "REP_fset x"})] zzz'' |
|
1079 ) |
|
1080 ) |
|
1081 *} |
|
1082 |
|
1083 |
|
1084 thm list_eq.intros(5) |
1070 thm list_eq.intros(5) |
1085 ML {* |
1071 ML {* |
1086 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)})) |
1072 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)})) |
1087 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1073 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1088 *} |
1074 *} |
1121 prove {* (Thm.term_of cgoal2) *} |
1107 prove {* (Thm.term_of cgoal2) *} |
1122 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1108 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1123 apply (tactic {* foo_tac' @{context} 1 *}) |
1109 apply (tactic {* foo_tac' @{context} 1 *}) |
1124 sorry |
1110 sorry |
1125 |
1111 |
|
1112 ML {* |
|
1113 fun lift_theorem_fset_aux thm lthy = |
|
1114 let |
|
1115 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
|
1116 val goal = build_goal novars consts @{typ "'a list"} mk_rep_abs; |
|
1117 val cgoal = cterm_of @{theory} goal; |
|
1118 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); |
|
1119 val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (foo_tac' @{context}) 1; |
|
1120 val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); |
|
1121 val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) |
|
1122 val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm; |
|
1123 val [nthm3] = ProofContext.export lthy2 lthy [nthm2] |
|
1124 in |
|
1125 nthm3 |
|
1126 end |
|
1127 *} |
|
1128 |
|
1129 ML {* lift_theorem_fset_aux @{thm m1} @{context} *} |
|
1130 |
|
1131 ML {* |
|
1132 fun lift_theorem_fset name thm lthy = |
|
1133 let |
|
1134 val lifted_thm = lift_theorem_fset_aux thm lthy; |
|
1135 val (_, lthy2) = note_thm (name, lifted_thm) lthy; |
|
1136 in |
|
1137 lthy2 |
|
1138 end; |
|
1139 *} |
|
1140 |
|
1141 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
|
1142 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
|
1143 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
|
1144 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
|
1145 |
|
1146 thm m1_lift |
|
1147 thm leqi4_lift |
|
1148 thm leqi5_lift |
|
1149 thm m2_lift |
|
1150 |
|
1151 ML Drule.instantiate' |
|
1152 text {* |
|
1153 We lost the schematic variable again :(. |
|
1154 Another variable export will still be necessary... |
|
1155 *} |
|
1156 ML {* |
|
1157 Toplevel.program (fn () => |
|
1158 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
|
1159 Drule.instantiate' [] [NONE, NONE, SOME (@{cpat "REP_fset x"})] @{thm m2_lift} |
|
1160 ) |
|
1161 ) |
|
1162 *} |
|
1163 |
|
1164 |
|
1165 |
|
1166 |
|
1167 ML {* MRS *} |
1126 thm card1_suc |
1168 thm card1_suc |
1127 |
1169 |
1128 ML {* |
1170 ML {* |
1129 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc})) |
1171 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc})) |
1130 *} |
1172 *} |