240 end |
240 end |
241 *} |
241 *} |
242 |
242 |
243 (* mapfuns for some standard types *) |
243 (* mapfuns for some standard types *) |
244 setup {* |
244 setup {* |
245 update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #> |
245 update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #> |
246 update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = "???"} #> |
246 update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #> |
247 update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}} |
247 update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}} |
248 *} |
248 *} |
249 |
249 |
250 ML {* lookup @{theory} @{type_name list} *} |
250 ML {* lookup @{theory} @{type_name list} *} |
251 |
251 |
1128 |
1128 |
1129 thm list.induct |
1129 thm list.induct |
1130 |
1130 |
1131 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *} |
1131 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *} |
1132 |
1132 |
|
1133 (* TODO: the following 2 lemmas should go to quotscript.thy after all are done *) |
|
1134 lemma RIGHT_RES_FORALL_REGULAR: |
|
1135 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
|
1136 shows "All P ==> Ball R Q" |
|
1137 using a |
|
1138 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
|
1139 done |
|
1140 |
|
1141 lemma LEFT_RES_FORALL_REGULAR: |
|
1142 assumes a: "!x. (R x \<and> (Q x --> P x))" |
|
1143 shows "Ball R Q ==> All P" |
|
1144 using a |
|
1145 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
|
1146 done |
|
1147 |
1133 prove {* |
1148 prove {* |
1134 Logic.mk_equals |
1149 Logic.mk_implies |
1135 ((regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}), |
1150 ((regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}), |
1136 (prop_of li)) *} |
1151 (prop_of li)) *} |
|
1152 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
|
1153 thm LEFT_RES_FORALL_REGULAR |
|
1154 apply (rule LEFT_RES_FORALL_REGULAR) |
|
1155 prefer 2 |
|
1156 apply (assumption) |
|
1157 apply (erule thin_rl) |
|
1158 apply (rule allI) |
|
1159 apply (rule conjI) |
|
1160 prefer 2 |
|
1161 apply (rule impI) |
|
1162 |
|
1163 apply (auto) |
|
1164 |
|
1165 apply (simp) |
|
1166 apply (thin_tac 1) |
|
1167 . |
|
1168 apply (simp) |
|
1169 |
|
1170 apply (unfold Ball_def) |
|
1171 apply (simp only: IN_RESPECTS) |
|
1172 apply (simp add: expand_fun_eq) |
|
1173 |
|
1174 |
|
1175 apply (tactic {* foo_tac' @{context} 1 *}) |
1137 apply (atomize(full)) |
1176 apply (atomize(full)) |
1138 apply (unfold Ball_def) |
1177 apply (simp) |
1139 apply (tactic {* foo_tac' @{context} 1 *}) |
|
1140 apply (simp only: IN_RESPECTS) |
|
1141 apply (simp_all add: expand_fun_eq) |
|
1142 prefer 2 |
1178 prefer 2 |
1143 apply (simp only: IN_RESPECTS) |
1179 apply (simp only: IN_RESPECTS) |
1144 apply (simp add:list_eq_refl) |
1180 apply (simp add:list_eq_refl) |
1145 apply (tactic {* foo_tac' @{context} 1 *}) |
1181 apply (tactic {* foo_tac' @{context} 1 *}) |
1146 prefer 2 |
1182 prefer 2 |