Unary Substitution

Tools/mrbnf_sugar.ML

@@ -79,7 +79,7 @@ fun create_binder_type (fp : MRBNF_Util.fp_kind) (spec : spec) lthy =
     val ((mrsbnf, (Ds, absinfo)), lthy) = MRSBNF_Comp.seal_mrsbnf I (bmv_unfolds
       @ BMV_Monad_Def.unfolds_of_bmv_monad (MRSBNF_Def.bmv_monad_of_mrsbnf mrsbnf), snd accum)
       (Binding.name pre_name) (#vars spec) tys mrsbnf NONE lthy;
-    
+
     val mrbnf = hd (MRSBNF_Def.mrbnfs_of_mrsbnf mrsbnf);
 
     val FVars_names = case #set_bs spec of
@@ -1146,7 +1146,7 @@ fun create_binder_datatype co (spec : spec) lthy =
         (single o HOLogic.mk_Trueprop o mk_bij) bounds mapx tac
       end;
 
-    val (lthy, tvsubst_opt) = if not (null (map_filter I (#etas tvsubst_model))) andalso not co then
+    val (tvsubst_opt, lthy) = if not (null (map_filter I (#etas tvsubst_model))) andalso not co then
       let
         val recursor_result = #recursor_result (the vvsubst_res_opt);
         val rec_mrbnf = #rec_mrbnf (the vvsubst_res_opt);
@@ -1257,8 +1257,32 @@ fun create_binder_datatype co (spec : spec) lthy =
           in map (Local_Defs.unfold0 lthy bmv_unfolds) (
             mk_map_simps lthy false true Sbs plives (fs @ rhos) mk_supp_bound mk_imsupp (K []) [] (#tvsubst tvsubst_res) tac
           ) end;
-        in (lthy, SOME (tvsubst_res, tvsubst_simps)) end
-      else (lthy, NONE);
+
+        in (SOME (tvsubst_res, tvsubst_simps), lthy) end
+      else (NONE, lthy);
+
+    val (tvsubst1_opt, lthy) = (case tvsubst_opt of
+        NONE => (NONE, lthy)
+      | SOME tvsubst =>
+        let
+          (* prepare spec (we need the original tv names for RVrs) *)
+          val ctor_Ts = map snd (#ctors spec);
+
+          fun is_RVr (NT, x) =
+            let
+              val (Inj_count, arity) = fold (fn Ts => fn (cnt, arity) =>
+                (if member (op=) Ts (TFree NT)
+                  then (1 + cnt, arity orelse length Ts > 1)
+                  else (cnt, arity))
+              ) ctor_Ts (0, false);
+            in x = Free_Var andalso (Inj_count <> 1 orelse arity) end;
+
+          val RVr_Ns = filter is_RVr (#vars spec)
+            |> map ((fn N => String.extract (N, 1, NONE)) o fst o fst);
+        in
+          TVSubst.create_tvsubst1_of_result (#tvsubst_b spec, RVr_Ns) tvsubst lthy
+          |> apfst SOME
+        end);
 
     val simp = @{attributes [simp]}
     val induct_attrib = Attrib.internal Position.none (K (Induct.induct_type (fst (dest_Type qT))))
@@ -1339,7 +1363,9 @@ fun create_binder_datatype co (spec : spec) lthy =
         ("IImsupp_permute_commute", #IImsupp_permute_commutes res, []),
         ("IImsupp_Diff", #IImsupp_Diffs res, []),
         ("tvsubst_permute", [#tvsubst_permute res], [])
-      ]) tvsubst_opt))
+      ]) tvsubst_opt) @ the_default [] (Option.map (map (fn (N, tvsubst1_simps) =>
+        (N, tvsubst1_simps, simp)
+      )) tvsubst1_opt))
         |> filter_out (null o #2)
         |> (map (fn (thmN, thms, attrs) =>
         ((Binding.qualify true (Binding.name_of (#fp_b spec)) (Binding.name thmN), attrs), [(thms, [])])

Tools/tvsubst.ML

@@ -29,6 +29,9 @@ sig
     -> MRSBNF_Def.mrsbnf -> MRBNF_Def.mrbnf -> thm -> thm -> thm list -> binding
     -> (Proof.context -> tactic) eta_model option list -> string -> local_theory
     -> tvsubst_result * local_theory
+
+  val create_tvsubst1_of_result: binding * string list -> tvsubst_result * thm list -> local_theory
+    -> (string * thm list) list * local_theory
 end
 
 structure TVSubst : TVSUBST =
@@ -2495,4 +2498,159 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
     }: tvsubst_result;
 
   in (result, lthy) end;
+
+local
+  fun mk_Free N T lthy' = mk_Frees N [T] lthy' |>> the_single;
+
+  fun drop_at j xs = (take j xs, drop (j+1) xs);
+
+  (* |Inj x| <o |UNIV| \<mapsto> (Inj, x) *)
+  fun dest_set_bd_UNIV (Trueprop $ (member $ (Pair $ (card_of $ (set $ x)) $ card_of_top) $ ordLess)) = (set, x)
+    | dest_set_bd_UNIV t = raise TERM("dest_set_bd_UNIV", [t])
+in
+fun create_tvsubst1_of_result (tvsubst_b, RVr_Ns) (result, simps) lthy =
+  let
+    val Sb as Const (_, Sb_T) = #tvsubst result;
+
+    val mrsbnf = #mrsbnf result;
+    val mrbnf  = hd (MRSBNF_Def.mrbnfs_of_mrsbnf mrsbnf);
+
+    val bmv = MRSBNF_Def.bmv_monad_of_mrsbnf mrsbnf;
+
+    val RVrs = hd (BMV_Monad_Def.RVrs_of_bmv_monad bmv);
+    val Injs = hd (BMV_Monad_Def.Injs_of_bmv_monad bmv);
+
+    val n = length RVrs + length Injs;
+
+    val (delta_Ts, _) = fastype_of Sb |> binder_types |> split_last;
+    val (id_Ts, Inj_Ts) = partition (op= o dest_funT) delta_Ts;
+
+    (* map Set to fact "|Set ?x| <o |UNIV|" *)
+    val set_bd_UNIV_tab = MRBNF_Def.set_bd_UNIV_of_mrbnf mrbnf
+      |> map (`(Thm.prop_of #> dest_set_bd_UNIV #> fst #> dest_Const_name));
+
+    (* construct the identities for RVrs and their respective unary Sb bindings *)
+    val ids = map2 (fn T => fn N => (N, Const ("Fun.id", T)))
+      id_Ts (take (length id_Ts) RVr_Ns);
+
+    (* construct the Injection ctors and their respective bindings *)
+    val Injs = map2 (fn T => dest_Const #> (fn (N, _) =>
+      (Long_Name.base_name N, Const (N, T)))
+    ) Inj_Ts Injs;
+
+    (* all together *)
+    val (Ns, trms) = split_list (ids @ Injs);
+
+    (* accumulate simplification theorems by index, name, and term: *)
+    fun alg k N trm (acc, lthy) =
+      let
+        val (_, lthy) = Local_Theory.begin_nested lthy;
+        val b = Binding.map_name (fn str => str ^ "_" ^ N) tvsubst_b;
+
+        (* "pure" terms surrounding the current delta term *)
+        val (pre, post) = drop_at k trms;
+
+        val (v_T, t_T) = fastype_of trm |> dest_funT;
+        val (t, (v, names_lthy)) = mk_Free "t" t_T lthy ||> mk_Free "v" v_T;
+
+        (* construct unary Sb definition: subst id... X{k}(v := t) Inj... *)
+        val upd = Quickcheck_Common.mk_fun_upd v_T t_T (v, t) trm;
+
+        val deltas  = pre @ upd :: post;
+        val cdeltas = map (SOME o Thm.cterm_of lthy) deltas;
+
+        val def = list_comb (Sb, deltas)
+          |> Term.absfree (dest_Free t)
+          |> Term.absfree (dest_Free v);
+
+        val ((_, (_, def_thm)), lthy) = Local_Theory.define
+          ((b, NoSyn), ((Thm.def_binding b, []), def)) lthy;
+
+        (* expand definition thm to make the Local_Defs.fold go through *)
+        val def_expanded = def_thm
+          RS @{thm meta_fun_cong} (* v *)
+          RS @{thm meta_fun_cong} (* t *)
+          RS @{thm meta_fun_cong} (* x *);
+
+        (* map trivial premise to theorem that discharge it *)
+        fun trivial_fact prem = case prem |> HOLogic.dest_Trueprop of
+          (* |?A| <o |UNIV| *)
+          Const (@{const_name "Set.member"}, _) $
+            (Const (@{const_name "Pair"}, _) $
+              (Const (@{const_name "card_of"}, _) $ A) $
+              (Const (@{const_name "card_of"}, _) $ Const (@{const_name "top"}, _))) $
+            Const (@{const_name "ordLess"}, _) =>
+          (case A of
+            (* {} *)
+            Const (@{const_name "bot"}, _) => @{thm emp_bound}
+            (* supp (id(v := t)) *)
+          | Const (@{const_name "supp"}, _) $
+              (Const (@{const_name "fun_upd"}, _) $ Const (@{const_name "id"}, _) $ _ $ _) =>
+            @{thm supp_fun_upd_var}
+            (* SSupp Inj (Inj(v := t)) *)
+          | Const (@{const_name "SSupp"}, _) $ _ $ (Const (@{const_name "fun_upd"}, _) $ _ $ _ $ _) =>
+            @{thm SSupp_fun_upd_Inj_bound}
+            (* IImsupp Inj ?Set (Inj(v := t) *)
+          | Const (@{const_name "IImsupp"}, _) $ _ $ Set $
+              (Const (@{const_name "fun_upd"}, _) $ _ $ _ $ _) =>
+            the (AList.lookup op= set_bd_UNIV_tab (dest_Const_name Set)) RS
+            @{thm IImsupp_fun_upd_Inj_bound}
+            (* fallback (skip) *)
+          | _ => @{thm asm_rl}
+          )
+        (* ?x \<notin> {} *)
+        | Const (@{const_name "Not"}, _) $ (Const (@{const_name "Set.member"}, _) $
+            _ $ Const (@{const_name "bot"}, _)) =>
+          @{thm empty_iff[symmetric, unfolded simp_thms(13)]}
+        (* fallback (skip) *)
+        | _ => @{thm asm_rl};
+
+        fun discharge_trivial simp_thm =
+          let
+            (* discharge premises (reverse order in case we don't fully resolve it) *)
+            val iprems = Thm.prop_of simp_thm
+              |> Logic.strip_imp_prems
+              |> map_index (fn (i, prem) => (i+1, trivial_fact prem));
+          in fold_rev (fn (i,P) => fn thm => P RSN (i, thm)) iprems simp_thm end;
+
+        (* get rid of all SSupp, IImssupp, SSupp, and imsupp mentions: *)
+        val tidy =
+          (* unfold "x \<notin> {IImssupp,SSupp,imsupp} .." \<leadsto> "t = Var v \<or> ..." *)
+          Local_Defs.unfold lthy @{thms not_in_SSupp_fun_upd_Inj_iff not_in_IImsupp_fun_upd_Inj_iff not_in_imsupp_fun_upd_id_iff}
+          (* rewrite \<lbrakk> t = Var v \<or> ?A1; t = Var v \<or> ?A2 ... \<rbrakk> \<leadsto> \<lbrakk> t = Var \<or> (?A1 \<and> ...); ... \<rbrakk> *)
+          #> Local_Defs.unfold lthy @{thms atomize_conjL}
+          (* tidy up a bit *)
+          #> Local_Defs.unfold lthy @{thms int_SSupp_fun_upd_iff int_imsupp_id_fun_upd_iff int_IImsupp_fun_upd_iff Int_empty_right simp_thms(6) simp_thms(21,22) True_implies_equals}
+          #> (
+            let
+              fun RS_tac thm = TRY (fn thm' => Seq.single (thm RS thm') handle THM _ => Seq.empty)
+
+              val tac = EVERY
+                [REPEAT (CHANGED (Local_Defs.fold_tac lthy @{thms conj_assoc disj_conj_distribL})),
+                 Local_Defs.unfold_tac lthy @{thms conj_assoc},
+                 RS_tac @{thm disjI2},
+                 RS_tac @{thm conjI}]
+            in REPEAT (CHANGED tac) #> Seq.hd end
+          );
+
+        (* adapt the simp theorems to the unary case: *)
+        val adapt = map (
+          (* specialize the simps with unary Sb *)
+          Drule.infer_instantiate' lthy cdeltas
+          #> Local_Defs.fold lthy [def_expanded]
+          (* unfold trivial/unary supports *)
+          #> Local_Defs.unfold lthy @{thms SSupp_Inj IImsupp_Inj supp_id imsupp_id}
+          (* discharge premises like "|{}| <o |UNIV|" etc. and tidy up *)
+          #> discharge_trivial
+          #> tidy
+          #> singleton (Variable.export names_lthy lthy)
+        );
+        val (lthy, old_lthy) = `Local_Theory.end_nested lthy;
+        val phi = Proof_Context.export_morphism old_lthy lthy;
+
+      in (("subst_" ^ N, adapt simps |> Morphism.fact phi) :: acc, lthy) end;
+
+  in @{fold 3} alg (0 upto n-1) Ns trms ([], lthy) end;
+end;
+
 end

tests/Regression_Tests.thy

@@ -7,6 +7,9 @@ binder_datatype 'a trm =
   Var 'a
 | Abs x::'a t::"'a trm" binds x in t
 
+thm trm.subst
+thm trm.subst_Var
+
 (* #69 *)
 binder_datatype 'a LLC =
   Var 'a

thys/Classes.thy

@@ -114,14 +114,19 @@ lemma IImsupp_Inj_comp_bound1: "inj Inj \<Longrightarrow> |supp (f::'a::var \<Ri
 
 lemma IImsupp_Inj_comp_bound2: "(\<And>a. Vrs (Inj a) = {}) \<Longrightarrow> |IImsupp Inj Vrs (Inj \<circ> f)| <o |UNIV::'a set|"
   by (auto simp: IImsupp_def)
+
 lemmas IImsupp_Inj_comp_bound = IImsupp_Inj_comp_bound1 IImsupp_Inj_comp_bound2
 
 lemma SSupp_fun_upd_bound_UNIV[simp]: "|SSupp Inj (f(x := t))| <o |UNIV::'a::var set| \<longleftrightarrow> |SSupp Inj f| <o |UNIV::'a set|"
   by (simp add: UNIV_cinfinite)
 
 lemma SSupp_fun_upd_Inj_bound[simp]: "|SSupp Inj (Inj(x := t))| <o |UNIV::'a::var set|"
   by simp
+
 lemma IImsupp_fun_upd_Inj_bound[simp, intro!]: "(\<And>x. |Vrs x| <o |UNIV::'a::var set| ) \<Longrightarrow> |IImsupp Inj Vrs (Inj(x := t))| <o |UNIV::'a::var set|"
   unfolding IImsupp_def by (meson SSupp_fun_upd_Inj_bound UN_bound)
 
+lemma supp_fun_upd_var: "|supp (id(v::'a::var := t))| <o |UNIV::'a set|"
+  by (simp add: supp_def)
+
 end

thys/Support.thy

@@ -86,6 +86,31 @@ lemma IImsupp_type_copy: "type_definition Rep Abs UNIV \<Longrightarrow> IImsupp
 lemma notin_SSupp: "a \<notin> SSupp Inj f \<Longrightarrow> f a = Inj a"
   unfolding SSupp_def by blast
 
+lemma not_in_SSupp_fun_upd_Inj_iff:
+  \<open>u \<notin> SSupp Inj (Inj(v := t)) \<longleftrightarrow> t = Inj v \<or> u \<noteq> v\<close>
+  by (simp add: SSupp_def)
+
+lemma not_in_IImsupp_fun_upd_Inj_iff:
+  \<open>u \<notin> IImsupp Inj Set (Inj(v := t)) \<longleftrightarrow> t = Inj v \<or> u \<notin> Set t\<close>
+  by (simp add: IImsupp_def SSupp_def)
+
+lemma not_in_imsupp_fun_upd_id_iff:
+  \<open>u \<notin> imsupp (id(v := t)) \<longleftrightarrow> t = v \<or> (u \<noteq> v \<and> u \<noteq> t)\<close>
+  by (auto simp: imsupp_def supp_def)
+
+lemma int_SSupp_fun_upd_iff:
+  \<open>A \<inter> SSupp Inj (Inj(v := t)) = {} \<longleftrightarrow> t = Inj v \<or> v \<notin> A\<close>
+  by (auto simp: SSupp_def)
+
+lemma int_imsupp_id_fun_upd_iff:
+  \<open>A \<inter> imsupp (id(v := t)) = {} \<longleftrightarrow> t = v \<or> v \<notin> A \<and> t \<notin> A\<close>
+  by (simp add: imsupp_id_fun_upd)
+
+lemma int_IImsupp_fun_upd_iff:
+  \<open>A \<inter> IImsupp Inj Vrs (Inj(v := t)) = {} \<longleftrightarrow>
+   t = Inj v \<or> A \<inter> Vrs t = {}\<close>
+  by (simp add: IImsupp_def SSupp_def)
+
 lemma IImsupp_chain1:
   assumes "\<And>a. Vrs2 (Inj2 a) = {a}" "\<rho>1 = \<rho>' \<or> \<rho>1 = \<rho>2"
   shows "(\<Union>x\<in>SSupp Inj2 \<rho>1. \<Union>x\<in>Vrs2 (\<rho>' x). Vrs2 (\<rho>2 x)) \<subseteq> IImsupp Inj2 Vrs2 \<rho>2 \<union> IImsupp Inj2 Vrs2 \<rho>'"