src/HOL/BNF/Tools/bnf_comp.ML
changeset 51766 f19a4d0ab1bf
parent 51761 4c9f08836d87
child 51767 bbcdd8519253
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 17:03:43 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 17:47:22 2013 +0200
     1.3 @@ -157,12 +157,12 @@
     1.4        mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
     1.5          (map map_comp_of_bnf inners);
     1.6  
     1.7 -    fun mk_single_set_natural_tac i _ =
     1.8 -      mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
     1.9 -        (collect_set_natural_of_bnf outer)
    1.10 -        (map ((fn thms => nth thms i) o set_natural_of_bnf) inners);
    1.11 +    fun mk_single_set_map_tac i _ =
    1.12 +      mk_comp_set_map_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
    1.13 +        (collect_set_map_of_bnf outer)
    1.14 +        (map ((fn thms => nth thms i) o set_map_of_bnf) inners);
    1.15  
    1.16 -    val set_natural_tacs = map mk_single_set_natural_tac (0 upto ilive - 1);
    1.17 +    val set_map_tacs = map mk_single_set_map_tac (0 upto ilive - 1);
    1.18  
    1.19      fun bd_card_order_tac _ =
    1.20        mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer);
    1.21 @@ -177,7 +177,7 @@
    1.22          map (fn goal =>
    1.23            Goal.prove_sorry lthy [] [] goal
    1.24              (fn {context = ctxt, prems = _} =>
    1.25 -              mk_comp_set_alt_tac ctxt (collect_set_natural_of_bnf outer))
    1.26 +              mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer))
    1.27            |> Thm.close_derivation)
    1.28          (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt);
    1.29  
    1.30 @@ -238,7 +238,7 @@
    1.31          unfold_thms_tac lthy basic_thms THEN rtac thm 1
    1.32        end;
    1.33  
    1.34 -    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
    1.35 +    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
    1.36        bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
    1.37  
    1.38      val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
    1.39 @@ -257,7 +257,7 @@
    1.40        |> map (fn (frees, t) => fold absfree frees t);
    1.41  
    1.42      fun wit_tac {context = ctxt, prems = _} =
    1.43 -      mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_natural_of_bnf outer)
    1.44 +      mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer)
    1.45          (maps wit_thms_of_bnf inners);
    1.46  
    1.47      val (bnf', lthy') =
    1.48 @@ -311,7 +311,7 @@
    1.49        rtac refl 1;
    1.50      fun map_cong0_tac {context = ctxt, prems = _} =
    1.51        mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
    1.52 -    val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf));
    1.53 +    val set_map_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map_of_bnf bnf));
    1.54      fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
    1.55      fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
    1.56      val set_bd_tacs =
    1.57 @@ -348,7 +348,7 @@
    1.58          rtac thm 1
    1.59        end;
    1.60  
    1.61 -    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
    1.62 +    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
    1.63        bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
    1.64  
    1.65      val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
    1.66 @@ -405,12 +405,12 @@
    1.67        rtac refl 1;
    1.68      fun map_cong0_tac {context = ctxt, prems = _} =
    1.69        rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
    1.70 -    val set_natural_tacs =
    1.71 +    val set_map_tacs =
    1.72        if ! quick_and_dirty then
    1.73          replicate (n + live) (K all_tac)
    1.74        else
    1.75          replicate n (K empty_natural_tac) @
    1.76 -        map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf);
    1.77 +        map (fn thm => fn _ => rtac thm 1) (set_map_of_bnf bnf);
    1.78      fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
    1.79      fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
    1.80      val set_bd_tacs =
    1.81 @@ -435,7 +435,7 @@
    1.82      fun srel_O_Gr_tac _ =
    1.83        mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
    1.84  
    1.85 -    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
    1.86 +    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
    1.87        bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
    1.88  
    1.89      val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
    1.90 @@ -490,7 +490,7 @@
    1.91      fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
    1.92      fun map_cong0_tac {context = ctxt, prems = _} =
    1.93        rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
    1.94 -    val set_natural_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf));
    1.95 +    val set_map_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map_of_bnf bnf));
    1.96      fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
    1.97      fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
    1.98      val set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
    1.99 @@ -512,7 +512,7 @@
   1.100      fun srel_O_Gr_tac _ =
   1.101        mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
   1.102  
   1.103 -    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
   1.104 +    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
   1.105        bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
   1.106  
   1.107      val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   1.108 @@ -653,7 +653,7 @@
   1.109        SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
   1.110  
   1.111      val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
   1.112 -      (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
   1.113 +      (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf))
   1.114        (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
   1.115        (mk_tac (map_wpull_of_bnf bnf))
   1.116        (mk_tac (unfold_thms lthy [srel_def_of_bnf bnf] (srel_O_Gr_of_bnf bnf)));