# HG changeset patch
# User traytel
# Date 1706803600 -3600
# Node ID 33b10cd883ae8992c44cb17e6acb5099118958c7
# Parent  76ad72736e9ed3f1ee5d76a82383942209211d10
made lift_bnf more robust for abstract types with 'phantom' type variables

diff -r 76ad72736e9e -r 33b10cd883ae src/HOL/Datatype_Examples/Lift_BNF.thy
--- a/src/HOL/Datatype_Examples/Lift_BNF.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Datatype_Examples/Lift_BNF.thy	Thu Feb 01 17:06:40 2024 +0100
@@ -104,6 +104,13 @@
 lift_bnf (dead 'k, 'v) fmap [wits: "Map.empty :: 'k \<Rightarrow> 'v option"]
   by auto
 
+class len = fixes len :: "'a \<Rightarrow> nat"
+typedef (overloaded) ('a, 'b :: len) vec = "{xs :: 'a list. length xs = len (undefined :: 'b)}"
+  by (auto intro!: exI[of _ "replicate _ _"])
+setup_lifting type_definition_vec
+lift_bnf (no_warn_wits) ('a, dead 'b :: len) vec
+  by auto
+
 typedef ('a, 'b) tuple_dead = "UNIV :: ('a \<times> 'b) set" ..
 typedef ('a, 'b) tuple_dead1 = "UNIV :: ('a \<times> 'b) set" ..
 typedef ('a, 'b) tuple_dead2 = "UNIV :: ('a \<times> 'b) set" ..
diff -r 76ad72736e9e -r 33b10cd883ae src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Thu Feb 01 17:06:40 2024 +0100
@@ -203,7 +203,8 @@
     val (pcrel_tm, crel_tm) = apply2 (Thm.prop_of #> Logic.dest_equals #> fst #> head_of)
       (pcrel_def, crel_def);
 
-    val (var_Qs, var_Rs) = fold Variable.declare_typ (#alphas Tss @ #deads Tss) lthy
+    val (var_Qs, var_Rs) = lthy
+      |> fold Variable.declare_typ (#alphas Tss @ Library.union (op =) (#deads Tss) (#Ds0 Tss))
       |> mk_Frees "Q" (map2 mk_relT (#alphas Tss) (#betas Tss))
       ||>> mk_Frees "R" (map2 mk_relT (#gammas Tss) (#deltas Tss))
       |> fst;
@@ -221,11 +222,11 @@
     val (pcrel_a, pcrel_b) = Envir.subst_term (tyenv_match, Vartab.empty) pcrel_tm
       |> `(subst_atomic_types (#alphas Tss @ #betas Tss ~~ #gammas Tss @ #deltas Tss));
 
-    (* match "crel :: {?a F} \<Rightarrow> a G" with "rep_G :: {a F}" *)
+    (* match "crel :: ?a F \<Rightarrow> {a G} \<Rightarrow> bool" with "a G" *)
     val tyenv_match = Vartab.empty |> Sign.typ_match thy
-      (crel_tm |> fastype_of |> binder_types |> hd, #rep Tss);
+      (crel_tm |> fastype_of |> binder_types |> tl |> hd, #abs Tss);
     val crel_b = Envir.subst_term (tyenv_match, Vartab.empty) crel_tm
-      |> subst_atomic_types (#alphas Tss ~~ #betas Tss)
+      |> subst_atomic_types (#alphas Tss ~~ #betas Tss);
     val crel_d = subst_atomic_types (#betas Tss ~~ #deltas Tss) crel_b;
 
     (* instantiate pcrel with Qs and Rs*)
@@ -237,12 +238,11 @@
           | go (_ :: dTs) tms = go dTs tms
           | go _ _ = [];
       in go dead_args end;
-
     val pcrel_Qs = list_comb (pcrel_b, parametrize var_Qs);
     val pcrel_Rs = list_comb (pcrel_a, parametrize var_Rs);
 
     (* get the order of the dead variables right *)
-    val Ds0 = maps the_list dead_args;
+    val Ds0 = Library.union (op =) (maps the_list dead_args) (#Ds0 Tss);
     val permute_Ds = (mk_T_of_bnf Ds0 (#betas Tss) bnf_G, nth (binder_types (type_of pcrel_Qs)) 1)
       |> apply2 (fn Type (_, Ts) => Ts | _ => []) |> op~~ |> typ_subst_atomic;
     val Ds0 = map permute_Ds Ds0;
@@ -287,26 +287,21 @@
           #tac const {Rs=var_Rs,Qs=var_Qs} ctxt);
       in prove lthy vars tm tac end;
     val prove_transfer_thm = prove_transfer_thm' 0;
-
     (* map transfer: "((Q ===> R) ===> pcr_G Q ===> pcr_G R) map_F' map_G" *)
     val map_G = mk_map_of_bnf Ds0 (#betas Tss) (#deltas Tss) bnf_G;
     val map_transfer = prove_transfer_thm (var_Qs @ var_Rs) map_G (#map consts);
-
     (* pred_transfer: "((Q ===> (=)) ===> pcr_G Q ===> (=)) pred_F' pred_G" *)
     val pred_G = mk_pred_of_bnf Ds0 (#betas Tss) bnf_G;
     val pred_transfer = #pred consts |> Option.map (fn p =>
       ("pred", [prove_transfer_thm (var_Qs @ var_Rs) pred_G p]));
-
     (* rel_transfer: "((Q ===> R ===> (=)) ===> pcr_G Q ===> pcr_G R ===> (=)) rel_F' rel_G" *)
     val rel_G = mk_rel_of_bnf Ds0 (#betas Tss) (#deltas Tss) bnf_G;
     val rel_transfer = prove_transfer_thm (var_Qs @ var_Rs) rel_G (#rel consts);
-
     (* set_transfer: "(pcr_G Q ===> rel_set Q) set_F' set_G" *)
     val sets_G = mk_sets_of_bnf (replicate live Ds0) (replicate live (#betas Tss)) bnf_G;
     fun mk_set_transfer i set_G raw tac = prove_transfer_thm' i var_Qs set_G {raw=raw, tac=tac};
     val sets_transfer = @{map 4} mk_set_transfer
       (0 upto (live-1)) sets_G (#raws (#sets consts)) (#tacs (#sets consts));
-
     (* export transfer theorems *)
     val transform = Morphism.thm (Morphism.thm_morphism "BNF" (unfold_thms lthy defs)) |> map;
     val b = Binding.qualified_name name;
@@ -457,7 +452,7 @@
 
     (* state the three required properties *)
     val sorts = map Type.sort_of_atyp alphas;
-    val names_lthy = fold Variable.declare_typ (alphas @ deads) lthy;
+    val names_lthy = fold Variable.declare_typ (alphas @ Library.union (op =) deads (map TFree Ds0)) lthy;
     val (((alphas', betas), betas'), names_lthy) = names_lthy
       |> mk_TFrees' sorts
       ||>> mk_TFrees' sorts