1056 prefer 2 |
1056 prefer 2 |
1057 apply (assumption) |
1057 apply (assumption) |
1058 apply (metis) |
1058 apply (metis) |
1059 done |
1059 done |
1060 |
1060 |
1061 ML {* val li = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
1061 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
1062 |
1062 |
1063 prove card1_suc_r: {* |
1063 prove card1_suc_r: {* |
1064 Logic.mk_implies |
1064 Logic.mk_implies |
1065 ((prop_of li), |
1065 ((prop_of card1_suc_f), |
1066 (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *} |
1066 (regularise (prop_of card1_suc_f) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *} |
1067 apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) |
1067 apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) |
1068 done |
1068 done |
1069 |
1069 |
1070 ML {* @{thm card1_suc_r} OF [li] *} |
1070 ML {* @{thm card1_suc_r} OF [card1_suc_f] *} |
1071 |
1071 |
1072 ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *} |
1072 ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *} |
1073 prove fold1_def_2_r: {* |
1073 prove fold1_def_2_r: {* |
1074 Logic.mk_implies |
1074 Logic.mk_implies |
1075 ((prop_of li), |
1075 ((prop_of li), |
1096 ) |
1096 ) |
1097 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1097 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1098 *} |
1098 *} |
1099 |
1099 |
1100 prove {* (Thm.term_of cgoal2) *} |
1100 prove {* (Thm.term_of cgoal2) *} |
1101 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1101 apply (tactic {* transconv_fset_tac' @{context} *}) |
1102 apply (atomize(full)) |
|
1103 apply (tactic {* transconv_fset_tac' @{context} 1 *}) |
|
1104 sorry |
1102 sorry |
1105 |
1103 |
1106 ML {* |
1104 ML {* |
1107 fun lift_theorem_fset_aux thm lthy = |
1105 fun lift_theorem_fset_aux thm lthy = |
1108 let |
1106 let |
1109 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
1107 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
1110 val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs; |
1108 val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs; |
1111 val cgoal = cterm_of @{theory} goal; |
1109 val cgoal = cterm_of @{theory} goal; |
1112 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); |
1110 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); |
1113 val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (ObjectLogic.full_atomize_tac 1) THEN (transconv_fset_tac' @{context}) 1; |
1111 val tac = transconv_fset_tac' @{context}; |
1114 val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); |
1112 val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); |
1115 val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) |
1113 val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) |
1116 val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm; |
1114 val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm; |
1117 val [nthm3] = ProofContext.export lthy2 lthy [nthm2] |
1115 val [nthm3] = ProofContext.export lthy2 lthy [nthm2] |
1118 in |
1116 in |
1134 |
1132 |
1135 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
1133 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
1136 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
1134 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
1137 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
1135 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
1138 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
1136 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
1139 thm card1_suc_r |
|
1140 (* ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc_r} @{context}) *}*) |
|
1141 (*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*) |
|
1142 |
|
1143 thm m1_lift |
1137 thm m1_lift |
1144 thm leqi4_lift |
1138 thm leqi4_lift |
1145 thm leqi5_lift |
1139 thm leqi5_lift |
1146 thm m2_lift |
1140 thm m2_lift |
1147 (*thm card_suc*) |
1141 ML {* @{thm card1_suc_r} OF [card1_suc_f] *} |
|
1142 (*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} |
|
1143 (@{thm card1_suc_r} OF [card1_suc_f]) @{context}) *}*) |
|
1144 (*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*) |
1148 |
1145 |
1149 thm leqi4_lift |
1146 thm leqi4_lift |
1150 ML {* |
1147 ML {* |
1151 val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) []) |
1148 val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) []) |
1152 val (_, l) = dest_Type typ |
1149 val (_, l) = dest_Type typ |
1159 Toplevel.program (fn () => |
1156 Toplevel.program (fn () => |
1160 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
1157 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
1161 Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift} |
1158 Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift} |
1162 ) |
1159 ) |
1163 ) |
1160 ) |
1164 *} |
|
1165 |
|
1166 (* |
|
1167 thm card_suc |
|
1168 ML {* |
|
1169 val (nam, typ) = hd (tl (Term.add_vars (prop_of @{thm card_suc})) []) |
|
1170 val (_, l) = dest_Type typ |
|
1171 val t = Type ("QuotMain.fset", l) |
|
1172 val v = Var (nam, t) |
|
1173 val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v) |
|
1174 *} |
|
1175 |
|
1176 ML {* |
|
1177 Toplevel.program (fn () => |
|
1178 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
|
1179 Drule.instantiate' [] [SOME (cv)] @{thm card_suc} |
|
1180 ) |
|
1181 ) |
|
1182 *} |
|
1183 *) |
|
1184 |
|
1185 |
|
1186 |
|
1187 |
|
1188 thm card1_suc |
|
1189 |
|
1190 ML {* |
|
1191 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc})) |
|
1192 *} |
|
1193 ML {* |
|
1194 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
|
1195 *} |
|
1196 ML {* term_of @{cpat "all"} *} |
|
1197 ML {* |
|
1198 val cgoal = |
|
1199 Toplevel.program (fn () => |
|
1200 cterm_of @{theory} goal |
|
1201 ); |
|
1202 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
|
1203 *} |
1161 *} |
1204 |
1162 |
1205 lemma "(Ball (Respects ((op \<approx>) ===> (op =))) |
1163 lemma "(Ball (Respects ((op \<approx>) ===> (op =))) |
1206 (((REP_fset ---> id) ---> id) |
1164 (((REP_fset ---> id) ---> id) |
1207 (((ABS_fset ---> id) ---> id) |
1165 (((ABS_fset ---> id) ---> id) |
1234 = Ball (Respects ((op \<approx>) ===> (op =))) |
1192 = Ball (Respects ((op \<approx>) ===> (op =))) |
1235 (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow> |
1193 (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow> |
1236 (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))" |
1194 (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))" |
1237 thm APPLY_RSP |
1195 thm APPLY_RSP |
1238 thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op =" "id" "id"] |
1196 thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op =" "id" "id"] |
|
1197 . |
1239 apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op ="]) |
1198 apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op ="]) |
1240 term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))" |
1199 term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))" |
1241 thm LAMBDA_PRS1[symmetric] |
1200 thm LAMBDA_PRS1[symmetric] |
1242 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*) |
1201 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*) |
1243 apply (unfold Ball_def) |
1202 apply (unfold Ball_def) |