Unary Substitution

[b4er]

Draft implementation for #19: adds TVSubst.create_tvsubst1_of_result and hooks it up in mrbnf_sugar.ML

1. This implementation picks apart the simp theorem's premises and discharges cardinality assumptions this way. We could use something like

val set_bd_UNIV_tab = MRBNF_Def.set_bd_UNIV_of_mrbnf mrbnf
  |> take (nRVrs + length Vrs)
  |> map (`(Drule.infer_instantiate' lthy [SOME (Thm.cterm_of lthy x)]
    #> Thm.full_prop_of
    #> (dest_set_bd_UNIV #> fst #> fastype_of #> range_type #> HOLogic.dest_setT)
  ));

(* ... *)

val small_support_prems = map2 (fn T => fn i =>
  let
    val typ_equiv = Sign.typ_equiv (Proof_Context.theory_of lthy);
    val (dom_T, range_T) = dest_funT T;

    val bds = filter (fn (T, _) =>
      typ_equiv (range_T, mrbnf_T) andalso not (typ_equiv (dom_T, T))
    ) set_bd_UNIV_tab |> map snd;
  in
    case (i < nRVrs, i = k) of
    (true, true) => (* this RVr is current trm: *) @{thms supp_fun_upd_var} 
  | (true, _) => (* this RVr is id: *) @{thms supp_id_bound}
  | (false, true) => (* this Inj is current trm: *)
      @{thm SSupp_fun_upd_Inj_bound} ::
      map (fn thm => thm RS @{thm IImsupp_fun_upd_Inj_bound}) bds
  | _ => (* this Inj is "pure": *)
    @{thm SSupp_Inj_bound} ::
    map (K @{thm IImsupp_Inj_bound}) bds
  end
) delta_Ts ixs |> flat;

to construct them a priori but this seems brittle against "upstream" changes (the ordering of IImsupp premises is not straight-forward either and unnecessarily complicates things). Matching premises to cardinality theorems (or asm_rl) is much simpler.

2. I also added a tidy pass over the simp theorems (latest commit) which gets rid of all constants from Support.thy (e.g. IImsupp) and yields more familiar theorems. This is a personal choice, open to discussion.