--- a/Nominal/Fv.thy	Mon Mar 08 15:01:01 2010 +0100
+++ b/Nominal/Fv.thy	Mon Mar 08 15:01:26 2010 +0100
@@ -2,14 +2,15 @@
 imports "Nominal2_Atoms" "Abs" "Perm" "Rsp"
 begin
 
-(* Bindings are given as a list which has a length being equal
-   to the length of the number of constructors.
+(* Bindings are a list of lists of lists of triples.
 
-   Each element is a list whose length is equal to the number
-   of arguents.
+   The first list represents the datatypes defined.
+   The second list represents the constructors.
+   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
@@ -21,12 +22,12 @@
 yields:
 [
  [],
- [[], [], [(NONE, 0)]],
- [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]]
+ [(NONE, 0, 2)],
+ [(SOME (Const f), 0, 2), (Some (Const g), 1, 2)]]
 
-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.
+A SOME binding has to have a function which takes an appropriate
+argument and returns an atom set. 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,
@@ -52,15 +53,50 @@
     (* 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' *)
@@ -110,7 +146,6 @@
 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, _) =>
@@ -128,7 +163,9 @@
       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);
@@ -178,14 +215,14 @@
               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_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"})
+(*              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"}) *)
             in
-              (*if length pi_supps > 1 then
-                HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) alpha_gen
+              (*if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*)
+              alpha_gen
             (* TODO Add some test that is makes sense *)
             end else @{term "True"}
         end
@@ -198,7 +235,7 @@
       (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)
@@ -236,7 +273,7 @@
 
 (* to be given by the user *)
 
-primrec 
+primrec
   bv1
 where
   "bv1 (BUnit) = {}"

--- a/Nominal/LFex.thy	Mon Mar 08 15:01:01 2010 +0100
+++ b/Nominal/LFex.thy	Mon Mar 08 15:01:26 2010 +0100
@@ -5,7 +5,7 @@
 atom_decl name
 atom_decl ident
 
-ML {* restricted_nominal := false *}
+ML {* restricted_nominal := 2 *}
 
 nominal_datatype kind =
     Type

--- a/Nominal/Parser.thy	Mon Mar 08 15:01:01 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 08 15:01:26 2010 +0100
@@ -223,7 +223,7 @@
 end
 *}
 
-ML {* val restricted_nominal=ref true *}
+ML {* val restricted_nominal=ref 0 *}
 
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
@@ -269,7 +269,7 @@
   val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
 in
-if !restricted_nominal then
+if !restricted_nominal = 0 then
   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
 else
 let
@@ -299,6 +299,11 @@
           typ_of_dtyp descr sorts (DtRec i))) l) descr);
   val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7;
   val (consts, const_defs) = split_list consts_defs;
+in
+if !restricted_nominal = 1 then
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy8)
+else
+let
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t]
       (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8;
@@ -341,6 +346,7 @@
   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20)
 end
 end
+end
 *}
 
 ML {* 

--- a/Nominal/Term1.thy	Mon Mar 08 15:01:01 2010 +0100
+++ b/Nominal/Term1.thy	Mon Mar 08 15:01:26 2010 +0100
@@ -232,6 +232,7 @@
 apply(simp only: Un_commute)
 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
 apply(simp only: Collect_disj_eq[symmetric] inf_or)
+apply(simp only: HOL.imp_disj2[symmetric] HOL.not_ex[symmetric] HOL.disj_not1[symmetric] HOL.de_Morgan_conj[symmetric])
 sorry
 
 lemma supp_fv:

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Term5a.thy	Mon Mar 08 15:01:26 2010 +0100
@@ -0,0 +1,38 @@
+theory Term5
+imports "Parser"
+begin
+
+atom_decl name
+
+ML {* restricted_nominal := 2 *}
+
+nominal_datatype trm5 =
+  Vr5 "name"
+| Ap5 "trm5" "trm5"
+| Lt5 l::"lts" t::"trm5"  bind "bv5 l" in t
+and lts =
+  Lnil
+| Lcons "name" "trm5" "lts"
+binder
+  bv5
+where
+  "bv5 Lnil = {}"
+| "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
+
+lemma lets_ok:
+  "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
+apply (simp add: trm5_lts_inject)
+apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply (simp_all add: alpha_gen)
+apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn)
+done
+
+lemma lets_nok:
+  "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons y (Vr5 x) Lnil) (Vr5 y))"
+apply (simp only: trm5_lts_inject not_ex)
+apply (rule allI)
+apply (simp add: alpha_gen)
+apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn trm5_lts_inject)
+done
+
+end

--- a/Nominal/Test.thy	Mon Mar 08 15:01:01 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 08 15:01:26 2010 +0100
@@ -499,8 +499,8 @@
   "bp (PVar x) = {atom x}"
 | "bp (PUnit) = {}"
 | "bp (PPair p1 p2) = bp p1 \<union> bp p2"
+thm alpha_exp_raw_alpha_pat_raw.intros
 
-thm quot_respect
 (* example 6 from Peter Sewell's bestiary *)
 nominal_datatype exp6 =
   EVar name
@@ -516,6 +516,7 @@
   "bp6 (PVar' x) = {atom x}"
 | "bp6 (PUnit') = {}"
 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
+thm alpha_exp6_raw_alpha_pat6_raw.intros
 
 (* example 7 from Peter Sewell's bestiary *)
 nominal_datatype exp7 =
@@ -535,6 +536,7 @@
   "b7 (Assign x e) = {atom x}"
 | "b7s (Single a) = b7 a"
 | "b7s (More a as) = (b7 a) \<union> (b7s as)"
+thm alpha_exp7_raw_alpha_lrb_raw_alpha_lrbs_raw.intros
 
 (* example 8 from Peter Sewell's bestiary *)
 nominal_datatype exp8 =
@@ -572,6 +574,7 @@
 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
 | "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"
 | "b_fnclause (K x pat exp8) = {atom x}"
+thm alpha_exp8_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb8_raw_alpha_lrbs8_raw_alpha_pat8_raw.intros