theory Fv+
−
imports "Nominal2_Atoms" "Abs"+
−
begin+
−
+
−
(* Bindings are given as a list which has a length being equal+
−
   to the length of the number of constructors.+
−
+
−
   Each element is a list whose length is equal to the number+
−
   of arguents.+
−
+
−
   Every element specifies bindings of this argument given as+
−
   a tuple: function, bound argument.+
−
+
−
  Eg:+
−
nominal_datatype+
−
+
−
   C1+
−
 | C2 x y z bind x in z+
−
 | C3 x y z bind f x in z bind g y in z+
−
+
−
yields:+
−
[+
−
 [],+
−
 [[], [], [(NONE, 0)]],+
−
 [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]]+
−
+
−
A SOME binding has to have a function returning an atom set,+
−
and a NONE binding has to be on an argument that is an atom+
−
or an atom set.+
−
+
−
How the procedure works:+
−
  For each of the defined datatypes,+
−
  For each of the constructors,+
−
  It creates a union of free variables for each argument.+
−
+
−
  For an argument the free variables are the variables minus+
−
  bound variables.+
−
+
−
  The variables are:+
−
    For an atom, a singleton set with the atom itself.+
−
    For an atom set, the atom set itself.+
−
    For a recursive argument, the appropriate fv function applied to it.+
−
    (* TODO: This one is not implemented *)+
−
    For other arguments it should be an appropriate fv function stored+
−
      in the database.+
−
  The bound variables are a union of results of all bindings that+
−
  involve the given argument. For a paricular binding the result is:+
−
    For a function applied to an argument this function with the argument.+
−
    For an atom, a singleton set with the atom itself.+
−
    For an atom set, the atom set itself.+
−
    For a recursive argument, the appropriate fv function applied to it.+
−
    (* TODO: This one is not implemented *)+
−
    For other arguments it should be an appropriate fv function stored+
−
      in the database.+
−
*)+
−
+
−
ML {*+
−
  open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);+
−
  (* TODO: It is the same as one in 'nominal_atoms' *)+
−
  fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom});+
−
  val noatoms = @{term "{} :: atom set"};+
−
  fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x];+
−
  fun mk_union sets =+
−
    fold (fn a => fn b =>+
−
      if a = noatoms then b else+
−
      if b = noatoms then a else+
−
      HOLogic.mk_binop @{const_name union} (a, b)) (rev sets) noatoms;+
−
  fun mk_diff a b =+
−
    if b = noatoms then a else+
−
    if b = a then noatoms else+
−
    HOLogic.mk_binop @{const_name minus} (a, b);+
−
  fun mk_atoms t =+
−
    let+
−
      val ty = fastype_of t;+
−
      val atom_ty = HOLogic.dest_setT ty --> @{typ atom};+
−
      val img_ty = atom_ty --> ty --> @{typ "atom set"};+
−
    in+
−
      (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t)+
−
    end;+
−
  (* Copy from Term *)+
−
  fun is_funtype (Type ("fun", [_, _])) = true+
−
    | is_funtype _ = false;+
−
  (* Similar to one in USyntax *)+
−
  fun mk_pair (fst, snd) =+
−
    let val ty1 = fastype_of fst+
−
      val ty2 = fastype_of snd+
−
      val c = HOLogic.pair_const ty1 ty2+
−
    in c $ fst $ snd+
−
    end;+
−
+
−
*}+
−
+
−
ML {*+
−
(* Currently needs just one full_tname to access Datatype *)+
−
fun define_fv_alpha full_tname bindsall lthy =+
−
let+
−
  val thy = ProofContext.theory_of lthy;+
−
  val {descr, ...} = Datatype.the_info thy full_tname;+
−
  val sorts = []; (* TODO *)+
−
  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);+
−
  val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>+
−
    "fv_" ^ name_of_typ (nth_dtyp i)) descr);+
−
  val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr;+
−
  val fv_frees = map Free (fv_names ~~ fv_types);+
−
  val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>+
−
    "alpha_" ^ name_of_typ (nth_dtyp i)) descr);+
−
  val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;+
−
  val alpha_frees = map Free (alpha_names ~~ alpha_types);+
−
  fun fv_alpha_constr i (cname, dts) bindcs =+
−
    let+
−
      val Ts = map (typ_of_dtyp descr sorts) dts;+
−
      val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);+
−
      val args = map Free (names ~~ Ts);+
−
      val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);+
−
      val args2 = map Free (names2 ~~ Ts);+
−
      val c = Const (cname, Ts ---> (nth_dtyp i));+
−
      val fv_c = nth fv_frees i;+
−
      val alpha = nth alpha_frees i;+
−
      fun fv_bind args (NONE, i) =+
−
            if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else+
−
            (* TODO we assume that all can be 'atomized' *)+
−
            if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else+
−
            mk_single_atom (nth args i)+
−
        | fv_bind args (SOME f, i) = f $ (nth args i);+
−
      fun fv_arg ((dt, x), bindxs) =+
−
        let+
−
          val arg =+
−
            if is_rec_type dt then nth fv_frees (body_index dt) $ x else+
−
            (* TODO: we just assume everything can be 'atomized' *)+
−
            if (is_funtype o fastype_of) x then mk_atoms x else+
−
            HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x]+
−
          val sub = mk_union (map (fv_bind args) bindxs)+
−
        in+
−
          mk_diff arg sub+
−
        end;+
−
      val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq+
−
        (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))+
−
      val alpha_rhs =+
−
        HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));+
−
      fun alpha_arg ((dt, bindxs), (arg, arg2)) =+
−
        if bindxs = [] then (+
−
          if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)+
−
          else (HOLogic.mk_eq (arg, arg2)))+
−
        else+
−
          if is_rec_type dt then let+
−
            (* THE HARD CASE *)+
−
            val lhs_binds = mk_union (map (fv_bind args) bindxs);+
−
            val lhs = mk_pair (lhs_binds, arg);+
−
            val rhs_binds = mk_union (map (fv_bind args2) bindxs);+
−
            val rhs = mk_pair (rhs_binds, arg2);+
−
            val alpha = nth alpha_frees (body_index dt);+
−
            val fv = nth fv_frees (body_index dt);+
−
            val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ (Free ("pi", @{typ perm})) $ rhs;+
−
            val alpha_gen_t = Syntax.check_term lthy alpha_gen_pre+
−
          in+
−
            HOLogic.mk_exists ("pi", @{typ perm}, alpha_gen_t)+
−
          (* TODO Add some test that is makes sense *)+
−
          end else @{term "True"}+
−
      val alpha_lhss = map (HOLogic.mk_Trueprop o alpha_arg) (dts ~~ bindcs ~~ (args ~~ args2))+
−
      val alpha_eq = Logic.list_implies (alpha_lhss, alpha_rhs)+
−
    in+
−
      (fv_eq, alpha_eq)+
−
    end;+
−
  fun fv_alpha_eq (i, (_, _, constrs)) binds = map2 (fv_alpha_constr i) constrs binds;+
−
  val (fv_eqs, alpha_eqs) = split_list (flat (map2 fv_alpha_eq descr bindsall))+
−
  val add_binds = map (fn x => (Attrib.empty_binding, x))+
−
  val (fvs, lthy') = (Primrec.add_primrec+
−
    (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy)+
−
  val (alphas, lthy'') = (Inductive.add_inductive_i+
−
     {quiet_mode = false, verbose = true, alt_name = Binding.empty,+
−
      coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}+
−
     (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) []+
−
     (add_binds alpha_eqs) [] lthy')+
−
in+
−
  ((fvs, alphas), lthy'')+
−
end+
−
*}+
−
+
−
(* tests+
−
atom_decl name+
−
+
−
datatype ty =+
−
  Var "name set"+
−
+
−
ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *}+
−
+
−
local_setup {* define_fv_alpha "Fv.ty" [[[[]]]] *}+
−
print_theorems+
−
+
−
+
−
datatype rtrm1 =+
−
  rVr1 "name"+
−
| rAp1 "rtrm1" "rtrm1"+
−
| rLm1 "name" "rtrm1"        --"name is bound in trm1"+
−
| rLt1 "bp" "rtrm1" "rtrm1"   --"all variables in bp are bound in the 2nd trm1"+
−
and bp =+
−
  BUnit+
−
| BVr "name"+
−
| BPr "bp" "bp"+
−
+
−
(* to be given by the user *)+
−
+
−
primrec +
−
  bv1+
−
where+
−
  "bv1 (BUnit) = {}"+
−
| "bv1 (BVr x) = {atom x}"+
−
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"+
−
+
−
setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Fv.rtrm1", "Fv.bp"] *}+
−
+
−
local_setup {* define_fv_alpha "Fv.rtrm1"+
−
  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],+
−
   [[], [[]], [[], []]]] *}+
−
print_theorems+
−
*)+
−
+
−
ML {*+
−
fun build_alpha_inj_gl thms ctxt =+
−
let+
−
  (* TODO: use the context for export *)+
−
  val ((_, thms_imp), ctxt') = Variable.import false thms ctxt;+
−
  fun inj_thm thm_imp =+
−
    let+
−
      val prop = prop_of thm_imp;+
−
      val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);+
−
      val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);+
−
      fun list_conj l = foldr1 HOLogic.mk_conj l;+
−
    in+
−
      if hyps = [] then concl+
−
      else HOLogic.mk_eq (concl, list_conj hyps)+
−
    end;+
−
in+
−
  Logic.mk_conjunction_list (map (HOLogic.mk_Trueprop o inj_thm) thms_imp)+
−
end+
−
*}+
−
+
−
end+
−