# HG changeset patch
# User blanchet
# Date 1430220628 -7200
# Node ID 81a0900f0ddceb020c642448cb596f878432677c
# Parent  18267ceb10b5d55806af77f89a88ade687e0b10b
allow sorts on dead variables in BNFs

diff -r 18267ceb10b5 -r 81a0900f0ddc src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Tue Apr 28 11:48:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Tue Apr 28 13:30:28 2015 +0200
@@ -149,10 +149,10 @@
   let
     val olive = live_of_bnf outer;
     val onwits = nwits_of_bnf outer;
-    val odead = dead_of_bnf outer;
+    val odeads = deads_of_bnf outer;
     val inner = hd inners;
     val ilive = live_of_bnf inner;
-    val ideads = map dead_of_bnf inners;
+    val ideadss = map deads_of_bnf inners;
     val inwitss = map nwits_of_bnf inners;
 
     (* TODO: check olive = length inners > 0,
@@ -160,9 +160,9 @@
                    forall inner from inners. idead = dead  *)
 
     val (oDs, lthy1) = apfst (map TFree)
-      (Variable.invent_types (replicate odead @{sort type}) lthy);
+      (Variable.invent_types (map Type.sort_of_atyp odeads) lthy);
     val (Dss, lthy2) = apfst (map (map TFree))
-      (fold_map Variable.invent_types (map (fn n => replicate n @{sort type}) ideads) lthy1);
+      (fold_map Variable.invent_types (map (map Type.sort_of_atyp) ideadss) lthy1);
     val (Ass, lthy3) = apfst (replicate ilive o map TFree)
       (Variable.invent_types (replicate ilive @{sort type}) lthy2);
     val As = if ilive > 0 then hd Ass else [];
@@ -379,13 +379,13 @@
   let
     val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf);
     val live = live_of_bnf bnf;
-    val dead = dead_of_bnf bnf;
+    val deads = deads_of_bnf bnf;
     val nwits = nwits_of_bnf bnf;
 
     (* TODO: check 0 < n <= live *)
 
     val (Ds, lthy1) = apfst (map TFree)
-      (Variable.invent_types (replicate dead @{sort type}) lthy);
+      (Variable.invent_types (map Type.sort_of_atyp deads) lthy);
     val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
       (Variable.invent_types (replicate live @{sort type}) lthy1);
     val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
@@ -478,13 +478,13 @@
   let
     val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf);
     val live = live_of_bnf bnf;
-    val dead = dead_of_bnf bnf;
+    val deads = deads_of_bnf bnf;
     val nwits = nwits_of_bnf bnf;
 
     (* TODO: check 0 < n *)
 
     val (Ds, lthy1) = apfst (map TFree)
-      (Variable.invent_types (replicate dead @{sort type}) lthy);
+      (Variable.invent_types (map Type.sort_of_atyp deads) lthy);
     val ((newAs, As), lthy2) = apfst (chop n o map TFree)
       (Variable.invent_types (replicate (n + live) @{sort type}) lthy1);
     val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
@@ -568,14 +568,14 @@
   let
     val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf);
     val live = live_of_bnf bnf;
-    val dead = dead_of_bnf bnf;
+    val deads = deads_of_bnf bnf;
     val nwits = nwits_of_bnf bnf;
 
     fun permute xs = permute_like_unique (op =) src dest xs;
     fun unpermute xs = permute_like_unique (op =) dest src xs;
 
     val (Ds, lthy1) = apfst (map TFree)
-      (Variable.invent_types (replicate dead @{sort type}) lthy);
+      (Variable.invent_types (map Type.sort_of_atyp deads) lthy);
     val (As, lthy2) = apfst (map TFree)
       (Variable.invent_types (replicate live @{sort type}) lthy1);
     val (Bs, _(*lthy3*)) = apfst (map TFree)
diff -r 18267ceb10b5 -r 81a0900f0ddc src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Apr 28 11:48:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Apr 28 13:30:28 2015 +0200
@@ -777,7 +777,7 @@
             Dont_Inline => false
           | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs
           | Smart_Inline => Term.size_of_term rhs <= smart_max_inline_term_size
-          | Do_Inline => true)
+          | Do_Inline => true);
       in
         if inline then
           ((rhs, Drule.reflexive_thm), lthy)
@@ -861,13 +861,16 @@
     fun mk_bnf_t Ds As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As'));
     fun mk_bnf_T Ds As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As'));
 
-    val (((As, Bs), Ds), names_lthy) = lthy
+    val (((As, Bs), unsorted_Ds), names_lthy) = lthy
       |> mk_TFrees live
       ||>> mk_TFrees live
       ||>> mk_TFrees (length deads);
+
+    val Ds = map2 (resort_tfree_or_tvar o Type.sort_of_atyp) deads unsorted_Ds;
+
     val RTs = map2 (curry HOLogic.mk_prodT) As Bs;
     val pred2RTs = map2 mk_pred2T As Bs;
-    val (Rs, Rs') = names_lthy |> mk_Frees' "R" pred2RTs |> fst
+    val (Rs, Rs') = names_lthy |> mk_Frees' "R" pred2RTs |> fst;
     val CA = mk_bnf_T Ds As Calpha;
     val CR = mk_bnf_T Ds RTs Calpha;
     val setRs =
@@ -967,7 +970,7 @@
 
     val dead = length deads;
 
-    val (((((((As', Bs'), Cs), Ds), Es), B1Ts), B2Ts), (Ts, T)) = lthy
+    val (((((((As', Bs'), Cs), unsorted_Ds), Es), B1Ts), B2Ts), (Ts, T)) = lthy
       |> mk_TFrees live
       ||>> mk_TFrees live
       ||>> mk_TFrees live
@@ -979,6 +982,8 @@
       ||> the_single
       ||> `(replicate live);
 
+    val Ds = map2 (resort_tfree_or_tvar o Type.sort_of_atyp) deads unsorted_Ds;
+
     val mk_bnf_map = mk_bnf_map_Ds Ds;
     val mk_bnf_t = mk_bnf_t_Ds Ds;
     val mk_bnf_T = mk_bnf_T_Ds Ds;
diff -r 18267ceb10b5 -r 81a0900f0ddc src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Apr 28 11:48:44 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Apr 28 13:30:28 2015 +0200
@@ -102,7 +102,7 @@
     val (((As, Bs), Ds), ctxt) = ctxt
       |> mk_TFrees live
       ||>> mk_TFrees live
-      ||>> mk_TFrees (dead_of_bnf bnf)
+      ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf))
 
     val relator = mk_rel_of_bnf Ds As Bs bnf
     val relsT = map2 mk_pred2T As Bs
@@ -181,7 +181,7 @@
     val Tname = base_name_of_bnf bnf
     val ((As, Ds), lthy) = lthy
       |> mk_TFrees live
-      ||>> mk_TFrees (dead_of_bnf bnf)
+      ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf))
     val T = mk_T_of_bnf Ds As bnf
     val sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf
     val argTs = map mk_pred1T As
@@ -232,7 +232,7 @@
     val (((As, Bs), Ds), ctxt) = ctxt
       |> mk_TFrees live
       ||>> mk_TFrees live
-      ||>> mk_TFrees (dead_of_bnf bnf)
+      ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf))
 
     val relator = mk_rel_of_bnf Ds As Bs bnf
     val relsT = map2 mk_pred2T As Bs
@@ -259,7 +259,7 @@
     val old_ctxt = ctxt
     val ((As, Ds), ctxt) = ctxt
       |> mk_TFrees live
-      ||>> mk_TFrees (dead_of_bnf bnf)
+      ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf))
     val T = mk_T_of_bnf Ds As bnf
     val argTs = map mk_pred1T As
     val (args, ctxt) = mk_Frees "P" argTs ctxt
@@ -334,8 +334,6 @@
     map_filter (uncurry (fn true => SOME | false => K NONE)) (liveness ~~ As)
   end
 
-fun sorts_of_fp fp_sugar = map (snd o Ctr_Sugar_Util.dest_TFree_or_TVar) (lives_of_fp fp_sugar)
-
 fun prove_pred_inject lthy (fp_sugar:fp_sugar) =
   let
     val involved_types = distinct op= (
@@ -344,7 +342,7 @@
       @ map type_name_of_bnf (#bnfs (#fp_res fp_sugar)))
     val eq_onps = map (Transfer.rel_eq_onp o lookup_defined_pred_data lthy) involved_types
     val old_lthy = lthy
-    val (As, lthy) = mk_TFrees' (sorts_of_fp fp_sugar) lthy
+    val (As, lthy) = mk_TFrees' (map Type.sort_of_atyp (lives_of_fp fp_sugar)) lthy
     val predTs = map mk_pred1T As
     val (preds, lthy) = mk_Frees "P" predTs lthy
     val args = map mk_eq_onp preds