nominal2: comparison Nominal/Fv.thy

equal deleted inserted replaced

-:f00761b5957e
+:226693549aa0
 theory Fv
 imports "Nominal2_Atoms" "Abs" "Perm" "Rsp"
 begin
-(* Bindings are given as a list which has a length being equal
+(* Bindings are a list of lists of lists of triples.
-to the length of the number of constructors.
+The first list represents the datatypes defined.
-Each element is a list whose length is equal to the number
+The second list represents the constructors.
-of arguents.
+The internal list is a list of all the bndings that
+concern the constructor.
-Every element specifies bindings of this argument given as
-a tuple: function, bound argument.
+Every triple consists of a function, the binding and
+the body.
 Eg:
 nominal_datatype
 C1
 | C3 x y z bind f x in z bind g y in z
 yields:
 [
 [],
-[[], [], [(NONE, 0)]],
+[(NONE, 0, 2)],
-[[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]]
+[(SOME (Const f), 0, 2), (Some (Const g), 1, 2)]]
-A SOME binding has to have a function returning an atom set,
+A SOME binding has to have a function which takes an appropriate
-and a NONE binding has to be on an argument that is an atom
+argument and returns an atom set. A NONE binding has to be on an
-or an atom set.
+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 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.
+For every argument that is a binding, we add a the same binding in its
+body.
 *)
+ML {*
+fun is_atom thy typ =
+Sign.of_sort thy (typ, @{sort at})
+*}
+(* Like map2, only if the second list is empty passes empty lists insted of error *)
 ML {*
 fun map2i _ [] [] = []
 | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys
 | map2i f (x :: xs) [] = f x [] :: map2i f xs []
 | map2i _ _ _ = raise UnequalLengths;
+*}
+(* Finds bindings with the same function and binding, and gathers all
+bodys for such pairs *)
+ML {*
+fun gather_binds binds =
+let
+fun gather_binds_cons binds =
+let
+val common = map (fn (f, bi, _) => (f, bi)) binds
+val nodups = distinct (op =) common
+fun find_bodys (sf, sbi) =
+filter (fn (f, bi, _) => f = sf andalso bi = sbi) binds
+val bodys = map ((map (fn (_, _, bo) => bo)) o find_bodys) nodups
+in
+nodups ~~ bodys
+end
+in
+map (map gather_binds_cons) binds
+end
+*}
+ML {*
+fun un_gather_binds_cons binds =
+flat (map (fn (((f, bi), bos), pi) => map (fn bo => ((f, bi, bo), pi)) bos) binds)
 *}
 ML {*
 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
 (* TODO: It is the same as one in 'nominal_atoms' *)
 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
 ML {*
 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy =
 let
-val thy = ProofContext.theory_of lthy;
 val {descr, sorts, ...} = dt_info;
 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 Ts = map (typ_of_dtyp descr sorts) dts;
 val bindslen = length bindcs
 val pi_strs_same = replicate bindslen "pi"
 val pi_strs = Name.variant_list [] pi_strs_same;
 val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs;
-val bind_pis = bindcs ~~ pis;
+val bind_pis_gath = bindcs ~~ pis;
+val bind_pis = un_gather_binds_cons bind_pis_gath;
+val bindcs = map fst bind_pis;
 val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts);
 val args = map Free (names ~~ Ts);
 val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts);
 val args2 = map Free (names2 ~~ Ts);
 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
 val lhs = mk_pair (lhs_binds, arg);
 val rhs_binds = fv_binds args2 rbinds;
 val rhs = mk_pair (rhs_binds, arg2);
 val alpha = nth alpha_frees (body_index dt);
 val fv = nth fv_frees (body_index dt);
-val pi = foldr1 add_perm rpis;
+val pi = foldr1 add_perm (distinct (op =) rpis);
 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
 val alpha_gen = Syntax.check_term lthy alpha_gen_pre
-val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis;
+(*              val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis;
-val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"})
+val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *)
 in
-(*if length pi_supps > 1 then
+(*if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*)
-HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) alpha_gen
+alpha_gen
 (* TODO Add some test that is makes sense *)
 end else @{term "True"}
 end
 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2))
 val alpha_lhss = mk_conjl alphas
 val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs)
 in
 (fv_eq, alpha_eq)
 end;
 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds;
-val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr bindsall))
+val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr (gather_binds 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 = true, verbose = false, alt_name = Binding.empty,
 | 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)"

changeset 1364	226693549aa0
parent 1362	e72d9d9eada3
child 1366	2bf82fa871e7