equal
deleted
inserted
replaced
1052 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
1052 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
1053 thm RIGHT_RES_FORALL_REGULAR |
1053 thm RIGHT_RES_FORALL_REGULAR |
1054 apply (rule RIGHT_RES_FORALL_REGULAR) |
1054 apply (rule RIGHT_RES_FORALL_REGULAR) |
1055 prefer 2 |
1055 prefer 2 |
1056 apply (assumption) |
1056 apply (assumption) |
1057 apply (auto) |
1057 apply (metis) |
1058 apply (rule allI) |
|
1059 apply (rule impI) |
|
1060 apply (rule impI) |
|
1061 apply (assumption) |
|
1062 done |
1058 done |
1063 |
1059 |
1064 ML {* val li = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
1060 ML {* val li = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
1065 |
1061 |
1066 prove card1_suc_r: {* |
1062 prove card1_suc_r: {* |
1067 Logic.mk_implies |
1063 Logic.mk_implies |
1068 ((prop_of li), |
1064 ((prop_of li), |
1069 (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *} |
1065 (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *} |
1070 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
1066 apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) |
1071 apply (simp only: equiv_res_exists[OF equiv_list_eq]) |
1067 done |
1072 done |
1068 |
1073 |
|
1074 thm card1_suc |
|
1075 ML {* @{thm card1_suc_r} OF [li] *} |
1069 ML {* @{thm card1_suc_r} OF [li] *} |
1076 |
1070 |
1077 ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *} |
1071 ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *} |
1078 prove fold1_def_2_r: {* |
1072 prove fold1_def_2_r: {* |
1079 Logic.mk_implies |
1073 Logic.mk_implies |