95 val ms = map length ctr_Tss; |
96 val ms = map length ctr_Tss; |
96 |
97 |
97 val disc_names = |
98 val disc_names = |
98 pad_list default_name n raw_disc_names |
99 pad_list default_name n raw_disc_names |
99 |> map2 (fn ctr => fn disc => |
100 |> map2 (fn ctr => fn disc => |
100 if Binding.eq_name (disc, default_name) then |
101 if Binding.eq_name (disc, no_name) then |
101 Binding.name (prefix is_N (Long_Name.base_name (name_of_ctr ctr))) |
102 NONE |
|
103 else if Binding.eq_name (disc, default_name) then |
|
104 SOME (Binding.name (prefix is_N (Long_Name.base_name (name_of_ctr ctr)))) |
102 else |
105 else |
103 disc) ctrs0; |
106 SOME disc) ctrs0; |
104 |
107 |
105 val sel_namess = |
108 val sel_namess = |
106 pad_list [] n raw_sel_namess |
109 pad_list [] n raw_sel_namess |
107 |> map3 (fn ctr => fn m => map2 (fn l => fn sel => |
110 |> map3 (fn ctr => fn m => map2 (fn l => fn sel => |
108 if Binding.eq_name (sel, default_name) then |
111 if Binding.eq_name (sel, default_name) then |
155 let val T' = fastype_of x in |
158 let val T' = fastype_of x in |
156 mk_Trueprop_eq (Free (Binding.name_of b, T --> T') $ v, |
159 mk_Trueprop_eq (Free (Binding.name_of b, T --> T') $ v, |
157 Term.list_comb (mk_caseof As T', mk_sel_caseof_args k xs x T') $ v) |
160 Term.list_comb (mk_caseof As T', mk_sel_caseof_args k xs x T') $ v) |
158 end; |
161 end; |
159 |
162 |
160 val (((raw_discs, (_, raw_disc_defs)), (raw_selss, (_, raw_sel_defss))), (lthy', lthy)) = |
163 val (((raw_discs, raw_disc_defs), (raw_selss, raw_sel_defss)), (lthy', lthy)) = |
161 no_defs_lthy |
164 no_defs_lthy |
162 |> apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn exist_xs_v_eq_ctr => |
165 |> apfst split_list o fold_map2 (fn exist_xs_v_eq_ctr => |
163 Specification.definition (SOME (b, NONE, NoSyn), |
166 fn NONE => pair (Term.lambda v exist_xs_v_eq_ctr, refl) |
164 ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr))) disc_names exist_xs_v_eq_ctrs |
167 | SOME b => Specification.definition (SOME (b, NONE, NoSyn), |
165 ||>> apfst (apsnd split_list o split_list) o fold_map3 (fn bs => fn xs => fn k => |
168 ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd) |
166 apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn x => |
169 exist_xs_v_eq_ctrs disc_names |
167 Specification.definition (SOME (b, NONE, NoSyn), |
170 ||>> apfst split_list o fold_map3 (fn bs => fn xs => fn k => apfst split_list o |
168 ((Thm.def_binding b, []), sel_spec b x xs k))) bs xs) sel_namess xss ks |
171 fold_map2 (fn b => fn x => Specification.definition (SOME (b, NONE, NoSyn), |
|
172 ((Thm.def_binding b, []), sel_spec b x xs k)) #>> apsnd snd) bs xs) sel_namess xss ks |
169 ||> `Local_Theory.restore; |
173 ||> `Local_Theory.restore; |
170 |
174 |
171 (*transforms defined frees into consts (and more)*) |
175 (*transforms defined frees into consts (and more)*) |
172 val phi = Proof_Context.export_morphism lthy lthy'; |
176 val phi = Proof_Context.export_morphism lthy lthy'; |
173 |
177 |
257 val discD_thms = map (fn def => def RS iffD1) disc_defs; |
261 val discD_thms = map (fn def => def RS iffD1) disc_defs; |
258 val discI_thms = |
262 val discI_thms = |
259 map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs; |
263 map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs; |
260 val not_disc_thms = |
264 val not_disc_thms = |
261 map2 (fn m => fn def => funpow m (fn thm => allI RS thm) |
265 map2 (fn m => fn def => funpow m (fn thm => allI RS thm) |
262 (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) |
266 (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) |
263 ms disc_defs; |
267 ms disc_defs; |
264 |
268 |
265 val (disc_thmss', disc_thmss) = |
269 val (disc_thmss', disc_thmss) = |
266 let |
270 let |
267 fun mk_thm discI _ [] = refl RS discI |
271 fun mk_thm discI _ [] = refl RS discI |
268 | mk_thm _ not_disc [distinct] = distinct RS not_disc; |
272 | mk_thm _ not_disc [distinct] = distinct RS not_disc; |
269 fun mk_thms discI not_disc distinctss = map (mk_thm discI not_disc) distinctss; |
273 fun mk_thms discI not_disc distinctss = map (mk_thm discI not_disc) distinctss; |
270 in |
274 in |
271 map3 mk_thms discI_thms not_disc_thms distinct_thmsss' |
275 map3 mk_thms discI_thms not_disc_thms distinct_thmsss' |> `transpose |
272 |> `transpose |
|
273 end; |
276 end; |
274 |
277 |
275 val disc_exclus_thms = |
278 val disc_exclus_thms = |
276 let |
279 let |
277 fun mk_goal ((_, disc), (_, disc')) = |
280 fun mk_goal ((_, disc), (_, disc')) = |
278 Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), |
281 Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (betapply (disc, v)), |
279 HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v)))); |
282 HOLogic.mk_Trueprop (HOLogic.mk_not (betapply (disc', v))))); |
280 fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); |
283 fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); |
281 |
284 |
282 val bundles = ms ~~ discD_thms ~~ discs; |
285 val bundles = ms ~~ discD_thms ~~ discs; |
283 val half_pairss = mk_half_pairss bundles; |
286 val half_pairss = mk_half_pairss bundles; |
284 |
287 |
296 interleave (flat half_thmss) (flat other_half_thmss) |
299 interleave (flat half_thmss) (flat other_half_thmss) |
297 end; |
300 end; |
298 |
301 |
299 val disc_exhaust_thm = |
302 val disc_exhaust_thm = |
300 let |
303 let |
301 fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (disc $ v)]; |
304 fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (betapply (disc, v))]; |
302 val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs)); |
305 val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs)); |
303 in |
306 in |
304 Skip_Proof.prove lthy [] [] goal (fn _ => mk_disc_exhaust_tac n exhaust_thm discI_thms) |
307 Skip_Proof.prove lthy [] [] goal (fn _ => mk_disc_exhaust_tac n exhaust_thm discI_thms) |
305 end; |
308 end; |
306 |
309 |
307 val ctr_sel_thms = |
310 val ctr_sel_thms = |
308 let |
311 let |
309 fun mk_goal ctr disc sels = |
312 fun mk_goal ctr disc sels = |
310 Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), |
313 let |
311 mk_Trueprop_eq ((null sels ? swap) |
314 val prem = HOLogic.mk_Trueprop (betapply (disc, v)); |
312 (Term.list_comb (ctr, map (fn sel => sel $ v) sels), v)))); |
315 val concl = |
|
316 mk_Trueprop_eq ((null sels ? swap) |
|
317 (Term.list_comb (ctr, map (fn sel => sel $ v) sels), v)); |
|
318 in |
|
319 if prem aconv concl then NONE |
|
320 else SOME (Logic.all v (Logic.mk_implies (prem, concl))) |
|
321 end; |
313 val goals = map3 mk_goal ctrs discs selss; |
322 val goals = map3 mk_goal ctrs discs selss; |
314 in |
323 in |
315 map4 (fn goal => fn m => fn discD => fn sel_thms => |
324 map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal => |
316 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
325 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
317 mk_ctr_sel_tac ctxt m discD sel_thms)) |
326 mk_ctr_sel_tac ctxt m discD sel_thms))) ms discD_thms sel_thmss goals |
318 goals ms discD_thms sel_thmss |
327 |> map_filter I |
319 end; |
328 end; |
320 |
329 |
321 val case_disc_thm = |
330 val case_disc_thm = |
322 let |
331 let |
323 fun mk_core f sels = Term.list_comb (f, map (fn sel => sel $ v) sels); |
332 fun mk_core f sels = Term.list_comb (f, map (fn sel => sel $ v) sels); |
324 fun mk_rhs _ [f] [sels] = mk_core f sels |
333 fun mk_rhs _ [f] [sels] = mk_core f sels |
325 | mk_rhs (disc :: discs) (f :: fs) (sels :: selss) = |
334 | mk_rhs (disc :: discs) (f :: fs) (sels :: selss) = |
326 Const (@{const_name If}, HOLogic.boolT --> B --> B --> B) $ |
335 Const (@{const_name If}, HOLogic.boolT --> B --> B --> B) $ |
327 (disc $ v) $ mk_core f sels $ mk_rhs discs fs selss; |
336 betapply (disc, v) $ mk_core f sels $ mk_rhs discs fs selss; |
328 val goal = mk_Trueprop_eq (caseofB_fs $ v, mk_rhs discs fs selss); |
337 val goal = mk_Trueprop_eq (caseofB_fs $ v, mk_rhs discs fs selss); |
329 in |
338 in |
330 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
339 Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => |
331 mk_case_disc_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss) |
340 mk_case_disc_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss) |
332 |> singleton (Proof_Context.export names_lthy lthy) |
341 |> singleton (Proof_Context.export names_lthy lthy) |
409 fun wrap tacss = (fn (goalss, after_qed, lthy) => |
418 fun wrap tacss = (fn (goalss, after_qed, lthy) => |
410 map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss |
419 map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss |
411 |> (fn thms => after_qed thms lthy)) oo |
420 |> (fn thms => after_qed thms lthy)) oo |
412 prepare_wrap (singleton o Type_Infer_Context.infer_types) |
421 prepare_wrap (singleton o Type_Infer_Context.infer_types) |
413 |
422 |
414 val parse_bindings = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]"; |
423 val parse_bindings = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]"; |
415 |
|
416 val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]"; |
424 val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]"; |
417 |
425 |
418 val wrap_data_cmd = (fn (goalss, after_qed, lthy) => |
426 val wrap_data_cmd = (fn (goalss, after_qed, lthy) => |
419 Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo |
427 Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo |
420 prepare_wrap Syntax.read_term; |
428 prepare_wrap Syntax.read_term; |