# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268223000 -3600
# Node ID 08294f4d6c082f90b46361f7c64be777af681e37
# Parent  e81857969443ef683381164aa80037882be058f7
Linked parser to fv and alpha.

diff -r e81857969443 -r 08294f4d6c08 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Wed Mar 10 12:53:44 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 10 13:10:00 2010 +0100
@@ -278,9 +278,10 @@
   val thy_name = Context.theory_name thy
   val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) =
     raw_nominal_decls dts bn_funs bn_eqs binds lthy
-  val bn_funs_decls = [];
+  val morphism_2_1 = ProofContext.export_morphism lthy2 lthy
+  val raw_bns_exp = map (apsnd (map (apfst (Morphism.term morphism_2_1)))) raw_bns;
+  val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
 
-  val morphism_2_1 = ProofContext.export_morphism lthy2 lthy
   val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc
   val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names);
diff -r e81857969443 -r 08294f4d6c08 Nominal/Test.thy
--- a/Nominal/Test.thy	Wed Mar 10 12:53:44 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 10 13:10:00 2010 +0100
@@ -42,7 +42,7 @@
 term Test.BP_raw
 thm bi_raw.simps
 thm permute_lam_raw_permute_bp_raw.simps
-thm alpha_lam_raw_alpha_bp_raw.intros[no_vars]
+thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros[no_vars]
 thm fv_lam_raw_fv_bp_raw.simps[no_vars]
 (*thm lam_bp_induct
 thm lam_bp_perm
@@ -77,7 +77,7 @@
 *)
 
 
-thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars]
+thm alpha_trm'_raw_alpha_pat'_raw_alpha_f_raw.intros[no_vars]
 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]
 thm f_raw.simps
 (*thm trm'_pat'_induct
@@ -167,7 +167,7 @@
 
 
 thm fv_trm2_raw_fv_assign_raw.simps[no_vars]
-thm alpha_trm2_raw_alpha_assign_raw.intros[no_vars]
+thm alpha_trm2_raw_alpha_assign_raw_alpha_bv2_raw.intros[no_vars]
 
 
 
@@ -339,11 +339,11 @@
   "cbinders (Type t T) = {atom t}"
 | "cbinders (Dty t) = {atom t}"
 | "cbinders (DStru x s) = {atom x}"
-| "cbinders (Val v M) = {atom v}"*)
+| "cbinders (Val v M) = {atom v}"
 | "Cbinders (Type1 t) = {atom t}"
 | "Cbinders (Type2 t T) = {atom t}"
 | "Cbinders (SStru x S) = {atom x}"
-| "Cbinders (SVal v T) = {atom v}"  
+| "Cbinders (SVal v T) = {atom v}"
 
 
 (* core haskell *)
@@ -424,18 +424,18 @@
   VarP "name"
 | AppP "exp" "exp"
 | LamP x::"name" e::"exp" bind x in e
-| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1
+| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp' p" in e1
 and pat3 =
   PVar "name"
 | PUnit
 | PPair "pat3" "pat3"
 binder
-  bp :: "pat3 \<Rightarrow> atom set"
+  bp' :: "pat3 \<Rightarrow> atom set"
 where
-  "bp (PVar x) = {atom x}"
-| "bp (PUnit) = {}"
-| "bp (PPair p1 p2) = bp p1 \<union> bp p2"
-thm alpha_exp_raw_alpha_pat3_raw.intros
+  "bp' (PVar x) = {atom x}"
+| "bp' (PUnit) = {}"
+| "bp' (PPair p1 p2) = bp' p1 \<union> bp' p2"
+thm alpha_exp_raw_alpha_pat3_raw_alpha_bp'_raw.intros
 
 (* example 6 from Peter Sewell's bestiary *)
 nominal_datatype exp6 =
@@ -452,7 +452,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
+thm alpha_exp6_raw_alpha_pat6_raw_alpha_bp6_raw.intros
 
 (* example 7 from Peter Sewell's bestiary *)
 nominal_datatype exp7 =