equal
deleted
inserted
replaced
701 apply(induct xs) |
701 apply(induct xs) |
702 apply (metis Suc_neq_Zero card1_0) |
702 apply (metis Suc_neq_Zero card1_0) |
703 apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_refl mem_cons) |
703 apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_refl mem_cons) |
704 done |
704 done |
705 |
705 |
|
706 primrec |
|
707 fold1 |
|
708 where |
|
709 "fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z" |
|
710 | "fold1 f g z (a # A) = |
|
711 (if ((!u v. (f u v = f v u)) |
|
712 \<and> (!u v w. ((f u (f v w) = f (f u v) w)))) |
|
713 then ( |
|
714 if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A)) |
|
715 ) else z)" |
|
716 |
|
717 thm fold1.simps |
|
718 |
706 lemma cons_preserves: |
719 lemma cons_preserves: |
707 fixes z |
720 fixes z |
708 assumes a: "xs \<approx> ys" |
721 assumes a: "xs \<approx> ys" |
709 shows "(z # xs) \<approx> (z # ys)" |
722 shows "(z # xs) \<approx> (z # ys)" |
710 using a by (rule QuotMain.list_eq.intros(5)) |
723 using a by (rule QuotMain.list_eq.intros(5)) |
1173 done |
1186 done |
1174 |
1187 |
1175 thm card1_suc |
1188 thm card1_suc |
1176 ML {* @{thm card1_suc_r} OF [li] *} |
1189 ML {* @{thm card1_suc_r} OF [li] *} |
1177 |
1190 |
|
1191 ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *} |
|
1192 prove fold1_def_2_r: {* |
|
1193 Logic.mk_implies |
|
1194 ((prop_of li), |
|
1195 (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *} |
|
1196 apply (simp add: equiv_res_forall[OF equiv_list_eq]) |
|
1197 done |
|
1198 |
|
1199 ML {* @{thm fold1_def_2_r} OF [li] *} |
|
1200 |
1178 ML {* |
1201 ML {* |
1179 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) |
1202 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) |
1180 *} |
1203 *} |
1181 |
1204 |
1182 ML {* |
1205 ML {* |