allow sorts on dead variables in BNFs
authorblanchet
Tue Apr 28 13:30:28 2015 +0200 (2015-04-28)
changeset 6020781a0900f0ddc
parent 60206 18267ceb10b5
child 60208 d72795f401c3
allow sorts on dead variables in BNFs
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/Transfer/transfer_bnf.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Tue Apr 28 11:48:44 2015 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Tue Apr 28 13:30:28 2015 +0200
     1.3 @@ -149,10 +149,10 @@
     1.4    let
     1.5      val olive = live_of_bnf outer;
     1.6      val onwits = nwits_of_bnf outer;
     1.7 -    val odead = dead_of_bnf outer;
     1.8 +    val odeads = deads_of_bnf outer;
     1.9      val inner = hd inners;
    1.10      val ilive = live_of_bnf inner;
    1.11 -    val ideads = map dead_of_bnf inners;
    1.12 +    val ideadss = map deads_of_bnf inners;
    1.13      val inwitss = map nwits_of_bnf inners;
    1.14  
    1.15      (* TODO: check olive = length inners > 0,
    1.16 @@ -160,9 +160,9 @@
    1.17                     forall inner from inners. idead = dead  *)
    1.18  
    1.19      val (oDs, lthy1) = apfst (map TFree)
    1.20 -      (Variable.invent_types (replicate odead @{sort type}) lthy);
    1.21 +      (Variable.invent_types (map Type.sort_of_atyp odeads) lthy);
    1.22      val (Dss, lthy2) = apfst (map (map TFree))
    1.23 -      (fold_map Variable.invent_types (map (fn n => replicate n @{sort type}) ideads) lthy1);
    1.24 +      (fold_map Variable.invent_types (map (map Type.sort_of_atyp) ideadss) lthy1);
    1.25      val (Ass, lthy3) = apfst (replicate ilive o map TFree)
    1.26        (Variable.invent_types (replicate ilive @{sort type}) lthy2);
    1.27      val As = if ilive > 0 then hd Ass else [];
    1.28 @@ -379,13 +379,13 @@
    1.29    let
    1.30      val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf);
    1.31      val live = live_of_bnf bnf;
    1.32 -    val dead = dead_of_bnf bnf;
    1.33 +    val deads = deads_of_bnf bnf;
    1.34      val nwits = nwits_of_bnf bnf;
    1.35  
    1.36      (* TODO: check 0 < n <= live *)
    1.37  
    1.38      val (Ds, lthy1) = apfst (map TFree)
    1.39 -      (Variable.invent_types (replicate dead @{sort type}) lthy);
    1.40 +      (Variable.invent_types (map Type.sort_of_atyp deads) lthy);
    1.41      val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
    1.42        (Variable.invent_types (replicate live @{sort type}) lthy1);
    1.43      val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
    1.44 @@ -478,13 +478,13 @@
    1.45    let
    1.46      val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf);
    1.47      val live = live_of_bnf bnf;
    1.48 -    val dead = dead_of_bnf bnf;
    1.49 +    val deads = deads_of_bnf bnf;
    1.50      val nwits = nwits_of_bnf bnf;
    1.51  
    1.52      (* TODO: check 0 < n *)
    1.53  
    1.54      val (Ds, lthy1) = apfst (map TFree)
    1.55 -      (Variable.invent_types (replicate dead @{sort type}) lthy);
    1.56 +      (Variable.invent_types (map Type.sort_of_atyp deads) lthy);
    1.57      val ((newAs, As), lthy2) = apfst (chop n o map TFree)
    1.58        (Variable.invent_types (replicate (n + live) @{sort type}) lthy1);
    1.59      val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
    1.60 @@ -568,14 +568,14 @@
    1.61    let
    1.62      val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf);
    1.63      val live = live_of_bnf bnf;
    1.64 -    val dead = dead_of_bnf bnf;
    1.65 +    val deads = deads_of_bnf bnf;
    1.66      val nwits = nwits_of_bnf bnf;
    1.67  
    1.68      fun permute xs = permute_like_unique (op =) src dest xs;
    1.69      fun unpermute xs = permute_like_unique (op =) dest src xs;
    1.70  
    1.71      val (Ds, lthy1) = apfst (map TFree)
    1.72 -      (Variable.invent_types (replicate dead @{sort type}) lthy);
    1.73 +      (Variable.invent_types (map Type.sort_of_atyp deads) lthy);
    1.74      val (As, lthy2) = apfst (map TFree)
    1.75        (Variable.invent_types (replicate live @{sort type}) lthy1);
    1.76      val (Bs, _(*lthy3*)) = apfst (map TFree)
     2.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Apr 28 11:48:44 2015 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Apr 28 13:30:28 2015 +0200
     2.3 @@ -777,7 +777,7 @@
     2.4              Dont_Inline => false
     2.5            | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs
     2.6            | Smart_Inline => Term.size_of_term rhs <= smart_max_inline_term_size
     2.7 -          | Do_Inline => true)
     2.8 +          | Do_Inline => true);
     2.9        in
    2.10          if inline then
    2.11            ((rhs, Drule.reflexive_thm), lthy)
    2.12 @@ -861,13 +861,16 @@
    2.13      fun mk_bnf_t Ds As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As'));
    2.14      fun mk_bnf_T Ds As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As'));
    2.15  
    2.16 -    val (((As, Bs), Ds), names_lthy) = lthy
    2.17 +    val (((As, Bs), unsorted_Ds), names_lthy) = lthy
    2.18        |> mk_TFrees live
    2.19        ||>> mk_TFrees live
    2.20        ||>> mk_TFrees (length deads);
    2.21 +
    2.22 +    val Ds = map2 (resort_tfree_or_tvar o Type.sort_of_atyp) deads unsorted_Ds;
    2.23 +
    2.24      val RTs = map2 (curry HOLogic.mk_prodT) As Bs;
    2.25      val pred2RTs = map2 mk_pred2T As Bs;
    2.26 -    val (Rs, Rs') = names_lthy |> mk_Frees' "R" pred2RTs |> fst
    2.27 +    val (Rs, Rs') = names_lthy |> mk_Frees' "R" pred2RTs |> fst;
    2.28      val CA = mk_bnf_T Ds As Calpha;
    2.29      val CR = mk_bnf_T Ds RTs Calpha;
    2.30      val setRs =
    2.31 @@ -967,7 +970,7 @@
    2.32  
    2.33      val dead = length deads;
    2.34  
    2.35 -    val (((((((As', Bs'), Cs), Ds), Es), B1Ts), B2Ts), (Ts, T)) = lthy
    2.36 +    val (((((((As', Bs'), Cs), unsorted_Ds), Es), B1Ts), B2Ts), (Ts, T)) = lthy
    2.37        |> mk_TFrees live
    2.38        ||>> mk_TFrees live
    2.39        ||>> mk_TFrees live
    2.40 @@ -979,6 +982,8 @@
    2.41        ||> the_single
    2.42        ||> `(replicate live);
    2.43  
    2.44 +    val Ds = map2 (resort_tfree_or_tvar o Type.sort_of_atyp) deads unsorted_Ds;
    2.45 +
    2.46      val mk_bnf_map = mk_bnf_map_Ds Ds;
    2.47      val mk_bnf_t = mk_bnf_t_Ds Ds;
    2.48      val mk_bnf_T = mk_bnf_T_Ds Ds;
     3.1 --- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Apr 28 11:48:44 2015 +0200
     3.2 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Apr 28 13:30:28 2015 +0200
     3.3 @@ -102,7 +102,7 @@
     3.4      val (((As, Bs), Ds), ctxt) = ctxt
     3.5        |> mk_TFrees live
     3.6        ||>> mk_TFrees live
     3.7 -      ||>> mk_TFrees (dead_of_bnf bnf)
     3.8 +      ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf))
     3.9  
    3.10      val relator = mk_rel_of_bnf Ds As Bs bnf
    3.11      val relsT = map2 mk_pred2T As Bs
    3.12 @@ -181,7 +181,7 @@
    3.13      val Tname = base_name_of_bnf bnf
    3.14      val ((As, Ds), lthy) = lthy
    3.15        |> mk_TFrees live
    3.16 -      ||>> mk_TFrees (dead_of_bnf bnf)
    3.17 +      ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf))
    3.18      val T = mk_T_of_bnf Ds As bnf
    3.19      val sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf
    3.20      val argTs = map mk_pred1T As
    3.21 @@ -232,7 +232,7 @@
    3.22      val (((As, Bs), Ds), ctxt) = ctxt
    3.23        |> mk_TFrees live
    3.24        ||>> mk_TFrees live
    3.25 -      ||>> mk_TFrees (dead_of_bnf bnf)
    3.26 +      ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf))
    3.27  
    3.28      val relator = mk_rel_of_bnf Ds As Bs bnf
    3.29      val relsT = map2 mk_pred2T As Bs
    3.30 @@ -259,7 +259,7 @@
    3.31      val old_ctxt = ctxt
    3.32      val ((As, Ds), ctxt) = ctxt
    3.33        |> mk_TFrees live
    3.34 -      ||>> mk_TFrees (dead_of_bnf bnf)
    3.35 +      ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf))
    3.36      val T = mk_T_of_bnf Ds As bnf
    3.37      val argTs = map mk_pred1T As
    3.38      val (args, ctxt) = mk_Frees "P" argTs ctxt
    3.39 @@ -334,8 +334,6 @@
    3.40      map_filter (uncurry (fn true => SOME | false => K NONE)) (liveness ~~ As)
    3.41    end
    3.42  
    3.43 -fun sorts_of_fp fp_sugar = map (snd o Ctr_Sugar_Util.dest_TFree_or_TVar) (lives_of_fp fp_sugar)
    3.44 -
    3.45  fun prove_pred_inject lthy (fp_sugar:fp_sugar) =
    3.46    let
    3.47      val involved_types = distinct op= (
    3.48 @@ -344,7 +342,7 @@
    3.49        @ map type_name_of_bnf (#bnfs (#fp_res fp_sugar)))
    3.50      val eq_onps = map (Transfer.rel_eq_onp o lookup_defined_pred_data lthy) involved_types
    3.51      val old_lthy = lthy
    3.52 -    val (As, lthy) = mk_TFrees' (sorts_of_fp fp_sugar) lthy
    3.53 +    val (As, lthy) = mk_TFrees' (map Type.sort_of_atyp (lives_of_fp fp_sugar)) lthy
    3.54      val predTs = map mk_pred1T As
    3.55      val (preds, lthy) = mk_Frees "P" predTs lthy
    3.56      val args = map mk_eq_onp preds