282 (bnf', (unfold', lthy')) |
282 (bnf', (unfold', lthy')) |
283 end; |
283 end; |
284 |
284 |
285 (* Killing live variables *) |
285 (* Killing live variables *) |
286 |
286 |
287 fun killN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else |
287 fun kill_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else |
288 let |
288 let |
289 val b = Binding.prefix_name (mk_killN n) (name_of_bnf bnf); |
289 val b = Binding.prefix_name (mk_killN n) (name_of_bnf bnf); |
290 val live = live_of_bnf bnf; |
290 val live = live_of_bnf bnf; |
291 val dead = dead_of_bnf bnf; |
291 val dead = dead_of_bnf bnf; |
292 val nwits = nwits_of_bnf bnf; |
292 val nwits = nwits_of_bnf bnf; |
321 fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1; |
321 fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1; |
322 fun map_comp_tac {context, ...} = |
322 fun map_comp_tac {context, ...} = |
323 Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN |
323 Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN |
324 rtac refl 1; |
324 rtac refl 1; |
325 fun map_cong_tac {context, ...} = |
325 fun map_cong_tac {context, ...} = |
326 mk_killN_map_cong_tac context n (live - n) (map_cong_of_bnf bnf); |
326 mk_kill_map_cong_tac context n (live - n) (map_cong_of_bnf bnf); |
327 val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf)); |
327 val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf)); |
328 fun bd_card_order_tac _ = mk_killN_bd_card_order_tac n (bd_card_order_of_bnf bnf); |
328 fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf); |
329 fun bd_cinfinite_tac _ = mk_killN_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf); |
329 fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf); |
330 val set_bd_tacs = |
330 val set_bd_tacs = |
331 map (fn thm => fn _ => mk_killN_set_bd_tac (bd_Card_order_of_bnf bnf) thm) |
331 map (fn thm => fn _ => mk_kill_set_bd_tac (bd_Card_order_of_bnf bnf) thm) |
332 (drop n (set_bd_of_bnf bnf)); |
332 (drop n (set_bd_of_bnf bnf)); |
333 |
333 |
334 val in_alt_thm = |
334 val in_alt_thm = |
335 let |
335 let |
336 val inx = mk_in Asets sets T; |
336 val inx = mk_in Asets sets T; |
337 val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T; |
337 val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T; |
338 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
338 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
339 in |
339 in |
340 Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac) |> Thm.close_derivation |
340 Skip_Proof.prove lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation |
341 end; |
341 end; |
342 |
342 |
343 fun in_bd_tac _ = |
343 fun in_bd_tac _ = |
344 mk_killN_in_bd_tac n (live > n) in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf) |
344 mk_kill_in_bd_tac n (live > n) in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf) |
345 (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf); |
345 (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf); |
346 fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); |
346 fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); |
347 |
347 |
348 val tacs = [map_id_tac, map_comp_tac, map_cong_tac] @ set_natural_tacs @ [bd_card_order_tac, |
348 val tacs = [map_id_tac, map_comp_tac, map_cong_tac] @ set_natural_tacs @ [bd_card_order_tac, |
349 bd_cinfinite_tac] @ set_bd_tacs @ [in_bd_tac, map_wpull_tac]; |
349 bd_cinfinite_tac] @ set_bd_tacs @ [in_bd_tac, map_wpull_tac]; |
381 (bnf', (unfold', lthy')) |
381 (bnf', (unfold', lthy')) |
382 end; |
382 end; |
383 |
383 |
384 (* Adding dummy live variables *) |
384 (* Adding dummy live variables *) |
385 |
385 |
386 fun liftN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else |
386 fun lift_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else |
387 let |
387 let |
388 val b = Binding.prefix_name (mk_liftN n) (name_of_bnf bnf); |
388 val b = Binding.prefix_name (mk_liftN n) (name_of_bnf bnf); |
389 val live = live_of_bnf bnf; |
389 val live = live_of_bnf bnf; |
390 val dead = dead_of_bnf bnf; |
390 val dead = dead_of_bnf bnf; |
391 val nwits = nwits_of_bnf bnf; |
391 val nwits = nwits_of_bnf bnf; |
429 fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; |
429 fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; |
430 val set_bd_tacs = |
430 val set_bd_tacs = |
431 if ! quick_and_dirty then |
431 if ! quick_and_dirty then |
432 replicate (n + live) (K all_tac) |
432 replicate (n + live) (K all_tac) |
433 else |
433 else |
434 replicate n (K (mk_liftN_set_bd_tac (bd_Card_order_of_bnf bnf))) @ |
434 replicate n (K (mk_lift_set_bd_tac (bd_Card_order_of_bnf bnf))) @ |
435 (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf)); |
435 (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf)); |
436 |
436 |
437 val in_alt_thm = |
437 val in_alt_thm = |
438 let |
438 let |
439 val inx = mk_in Asets sets T; |
439 val inx = mk_in Asets sets T; |
440 val in_alt = mk_in (drop n Asets) bnf_sets T; |
440 val in_alt = mk_in (drop n Asets) bnf_sets T; |
441 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
441 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
442 in |
442 in |
443 Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac) |> Thm.close_derivation |
443 Skip_Proof.prove lthy [] [] goal (K lift_in_alt_tac) |> Thm.close_derivation |
444 end; |
444 end; |
445 |
445 |
446 fun in_bd_tac _ = mk_liftN_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf); |
446 fun in_bd_tac _ = mk_lift_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf); |
447 fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); |
447 fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); |
448 |
448 |
449 val tacs = [map_id_tac, map_comp_tac, map_cong_tac] @ set_natural_tacs @ [bd_card_order_tac, |
449 val tacs = [map_id_tac, map_comp_tac, map_cong_tac] @ set_natural_tacs @ [bd_card_order_tac, |
450 bd_cinfinite_tac] @ set_bd_tacs @ [in_bd_tac, map_wpull_tac]; |
450 bd_cinfinite_tac] @ set_bd_tacs @ [in_bd_tac, map_wpull_tac]; |
451 |
451 |
553 (* Composition pipeline *) |
553 (* Composition pipeline *) |
554 |
554 |
555 fun permute_and_kill qualify n src dest bnf = |
555 fun permute_and_kill qualify n src dest bnf = |
556 bnf |
556 bnf |
557 |> permute_bnf qualify src dest |
557 |> permute_bnf qualify src dest |
558 #> uncurry (killN_bnf qualify n); |
558 #> uncurry (kill_bnf qualify n); |
559 |
559 |
560 fun lift_and_permute qualify n src dest bnf = |
560 fun lift_and_permute qualify n src dest bnf = |
561 bnf |
561 bnf |
562 |> liftN_bnf qualify n |
562 |> lift_bnf qualify n |
563 #> uncurry (permute_bnf qualify src dest); |
563 #> uncurry (permute_bnf qualify src dest); |
564 |
564 |
565 fun normalize_bnfs qualify Ass Ds sort bnfs unfold lthy = |
565 fun normalize_bnfs qualify Ass Ds sort bnfs unfold lthy = |
566 let |
566 let |
567 val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass; |
567 val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass; |