# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1267449974 -3600
# Node ID 8557af71724e066dd9c615392d6a4f3c8954d26a
# Parent  87894b5156f41d357e77ef3c218f369e959c8ee2
slight simplification of the raw-decl generation

diff -r 87894b5156f4 -r 8557af71724e Nominal/Parser.thy
--- a/Nominal/Parser.thy	Mon Mar 01 11:40:48 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 01 14:26:14 2010 +0100
@@ -126,14 +126,11 @@
 fun raw_dts_decl dt_names dts lthy =
 let
   val thy = ProofContext.theory_of lthy
-  val conf = Datatype.default_config
-
-  val dt_names' = add_raws dt_names
   val dt_full_names = map (Sign.full_bname thy) dt_names 
-  val dts' = raw_dts dt_full_names dts
+  val raw_dts = raw_dts dt_full_names dts
+  val raw_dt_names = add_raws dt_names
 in
-  lthy
-  |> Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts')
+  (raw_dt_names, raw_dts)
 end 
 *}
 
@@ -171,10 +168,14 @@
 ML {* 
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 let
+  val conf = Datatype.default_config
   val dts_names = map (fn (_, s, _, _) => Binding.name_of s) dts
+
+  val (raw_dt_names, raw_dts) = raw_dts_decl dts_names dts lthy
+
 in
   lthy
-  |> raw_dts_decl dts_names dts
+  |> Local_Theory.theory_result (Datatype.add_datatype conf raw_dt_names raw_dts)
   ||>> raw_bn_fun_decl dts_names dts bn_funs bn_eqs
 end
 *}
@@ -242,6 +243,7 @@
 *}
 
 ML {*
+(* associates every SOME with the index in the list *)
 fun mk_env xs =
   let
     fun mapp (_: int) [] = []
@@ -256,14 +258,16 @@
 fun env_lookup xs x =
   case AList.lookup (op =) xs x of
     SOME x => x
-  | NONE => error ("cannot find " ^ x ^ " in the binding specification.")  
+  | NONE => error ("cannot find " ^ x ^ " in the binding specification.");
 *}
 
+
+
 ML {*
 fun prepare_binds dt_strs lthy = 
 let
-  fun extract_cnstrs dt_strs =
-    map ((map (fn (_, antys, _, bns) => (antys, bns))) o forth) dt_strs
+  fun extract_annos_binds dt_strs =
+    map ((map (fn (_, antys, _, bns) => (map fst antys, bns))) o forth) dt_strs
 
   fun prep_bn env bn_str =
     case (Syntax.read_term lthy bn_str) of
@@ -271,20 +275,23 @@
      | Const (a, T) $ Free (x, _) => (env_lookup env x, SOME (Const (a, T)))
      | _ => error (bn_str ^ " not allowed as binding specification.");  
  
-  fun prep_typ env (opt_name, _) = 
+  fun prep_typ env opt_name = 
     case opt_name of
       NONE => []
     | SOME x => find_all (op=) env x;
         
-  fun prep_binds (anno_tys, bind_strs) = 
+  (* annos - list of annotation for each type (either NONE or SOME fo a type *)
+  
+  fun prep_binds (annos, bind_strs) = 
   let
-    val env = mk_env (map fst anno_tys)
+    val env = mk_env annos (* for ever label the index *)
     val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs  
   in
-    map (prep_typ binds) anno_tys
+    map (prep_typ binds) annos
   end
+
 in
-  map (map prep_binds) (extract_cnstrs dt_strs)
+  map (map prep_binds) (extract_annos_binds dt_strs)
 end
 *}
 
diff -r 87894b5156f4 -r 8557af71724e Nominal/Term5.thy
--- a/Nominal/Term5.thy	Mon Mar 01 11:40:48 2010 +0100
+++ b/Nominal/Term5.thy	Mon Mar 01 14:26:14 2010 +0100
@@ -173,10 +173,13 @@
 done
 
 lemma lets_ok3:
-  "(Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
-   (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+  assumes a: "distinct [x, y]"
+  shows "(Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
+         (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
 apply (subst alpha5_INJ)
 apply (rule conjI)
+apply (simp add: alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def)
 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply (simp only: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def)
diff -r 87894b5156f4 -r 8557af71724e Nominal/Test.thy
--- a/Nominal/Test.thy	Mon Mar 01 11:40:48 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 01 14:26:14 2010 +0100
@@ -7,9 +7,9 @@
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"
-| LET bp::"bp" t::"lam"   bind "bi bp" in t ("Let _ in _" [100,100] 100)
+| LET bp::"bp" t::"lam"   bind "bi bp" in t
 and bp = 
-  BP "name" "lam"  ("_ ::= _" [100,100] 100)
+  BP "name" "lam" 
 binder
   bi::"bp \<Rightarrow> name set"
 where