# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1277738548 -3600
# Node ID 1e0b3992189c11e937428c8a5c57a777ba361568
# Parent  e1764a73c2928da1b5f2c7de603c5a381da723fc
more quotient-definitions

diff -r e1764a73c292 -r 1e0b3992189c Nominal/Ex/CoreHaskell.thy
--- a/Nominal/Ex/CoreHaskell.thy	Mon Jun 28 15:23:56 2010 +0100
+++ b/Nominal/Ex/CoreHaskell.thy	Mon Jun 28 16:22:28 2010 +0100
@@ -8,7 +8,7 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 15]]
+declare [[STEPS = 16]]
 
 nominal_datatype tkind =
   KStar
@@ -85,6 +85,10 @@
 | "bv_cvs CvsNil = []"
 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
+
+term TvsNil
+
+
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm
diff -r e1764a73c292 -r 1e0b3992189c Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Mon Jun 28 15:23:56 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Mon Jun 28 16:22:28 2010 +0100
@@ -24,6 +24,8 @@
 term Var 
 term App
 term Baz
+term bn
+term fv_trm
 
 
 typ trm
diff -r e1764a73c292 -r 1e0b3992189c Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Mon Jun 28 15:23:56 2010 +0100
+++ b/Nominal/NewParser.thy	Mon Jun 28 16:22:28 2010 +0100
@@ -425,8 +425,8 @@
   (* defining the quotient type *)
   val _ = warning "Declaring the quotient types"
   val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
-  val qty_binds = map (fn (_, bind, _, _) => bind) dts            (* not used *)
-  val qty_names = map Name.of_binding qty_binds;                  (* not used *)
+  val qty_binds = map (fn (_, bind, _, _) => bind) dts        
+  val qty_names = map Name.of_binding qty_binds;              
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names (* not used *)
   
   val (qty_infos, lthy7) = 
@@ -435,21 +435,28 @@
     else raise TEST lthy6
 
   val qtys = map #qtyp qty_infos
-  val qconstr_descrs = 
+  
+  (* defining of quotient term-constructors, binding functions, free vars functions *)
+  val qconstr_descr = 
     flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts)
     |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs
 
-  val (qconstrs, lthy8) = 
+  val qbns_descr =
+    map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bn_funs
+
+  val qfvs_descr = 
+    map2 (fn n => fn t => (n, t, NoSyn)) qty_names raw_fvs
+
+
+  val (qs, lthy8) = 
     if get_STEPS lthy > 15
-    then qconst_defs qtys qconstr_descrs lthy7
+    then qconst_defs qtys (qconstr_descr @ qbns_descr @ qfvs_descr) lthy7
     else raise TEST lthy7
 
+  val _ = tracing ("raw fvs  " ^ commas (map @{make_string} raw_fvs))
+  val _ = tracing ("raw fv_bns  " ^ commas (map @{make_string} raw_fv_bns))
+
   (* HERE *)
-
-  val _ = tracing ("all_raw_tys: " ^ commas (map @{make_string} all_raw_tys))
-  val _ = tracing ("constrs: " ^ commas (map @{make_string} all_raw_constrs))
-  val _ = tracing ("qtys: " ^ commas (map @{make_string} qtys))
-  val _ = tracing ("qconstrs " ^ commas (map @{make_string} qconstrs))
   
   val _ = 
     if get_STEPS lthy > 16
@@ -498,7 +505,7 @@
       in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
     const_rsp_tac) raw_consts lthy11a
-    val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns)
+  val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns)
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns)
   val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys dd lthy12;
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts;