--- a/Nominal/Ex/CoreHaskell.thy	Mon Sep 20 21:52:45 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Wed Sep 22 14:19:48 2010 +0800
@@ -8,8 +8,6 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 31]]
-
 nominal_datatype core_haskell: 
  tkind =
   KStar
@@ -97,6 +95,7 @@
 thm core_haskell.eq_iff
 thm core_haskell.fv_bn_eqvt
 thm core_haskell.size_eqvt
+thm core_haskell.supp
 
 (*
 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"

--- a/Nominal/Ex/ExPS7.thy	Mon Sep 20 21:52:45 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-theory ExPS7
-imports "../Nominal2"
-begin
-
-(* example 7 from Peter Sewell's bestiary *)
-
-atom_decl name
-
-declare [[STEPS = 31]]
-
-nominal_datatype exp =
-  Var name
-| Unit
-| Pair exp exp
-| LetRec l::"lrbs" e::"exp"  bind (set) "bs l" in l e
-and lrb =
-  Assign name exp
-and lrbs =
-  Single lrb
-| More lrb lrbs
-binder
-  b :: "lrb \<Rightarrow> atom set" and
-  bs :: "lrbs \<Rightarrow> atom set"
-where
-  "b (Assign x e) = {atom x}"
-| "bs (Single a) = b a"
-| "bs (More a as) = (b a) \<union> (bs as)"
-
-
-
-end
-
-
-

--- a/Nominal/Ex/ExPS8.thy	Mon Sep 20 21:52:45 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-theory ExPS8
-imports "../Nominal2"
-begin
-
-(* example 8 from Peter Sewell's bestiary *)
-
-atom_decl name
-
-declare [[STEPS = 31]]
-
-nominal_datatype fun_pats: exp =
-  EVar name
-| EUnit 
-| EPair exp exp
-| ELetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e
-and fnclause =
-  K x::name p::pat f::exp bind (set) "b_pat p" in f
-and fnclauses =
-  S fnclause
-| ORs fnclause fnclauses
-and lrb =
-  Clause fnclauses
-and lrbs =
-  Single lrb
-| More lrb lrbs
-and pat =
-  PVar name
-| PUnit
-| PPair pat pat
-binder
-  b_lrbs :: "lrbs \<Rightarrow> atom set" and
-  b_pat :: "pat \<Rightarrow> atom set" and
-  b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
-  b_fnclause :: "fnclause \<Rightarrow> atom set" and
-  b_lrb :: "lrb \<Rightarrow> atom set"
-where
-  "b_lrbs (Single l) = b_lrb l"
-| "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls"
-| "b_pat (PVar x) = {atom x}"
-| "b_pat (PUnit) = {}"
-| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
-| "b_fnclauses (S fc) = (b_fnclause fc)"
-| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
-| "b_lrb (Clause fcs) = (b_fnclauses fcs)"
-| "b_fnclause (K x pat exp) = {atom x}"
-
-thm fun_pats.distinct
-thm fun_pats.induct
-thm fun_pats.inducts
-thm fun_pats.exhaust
-thm fun_pats.fv_defs
-thm fun_pats.bn_defs
-thm fun_pats.perm_simps
-thm fun_pats.eq_iff
-thm fun_pats.fv_bn_eqvt
-thm fun_pats.size_eqvt
-thm fun_pats.supports
-thm fun_pats.fsupp
-thm fun_pats.supp
-
-lemma
-  "(fv_exp x = supp x) \<and>
-   (fv_fnclause xa = supp xa \<and> fv_b_lrb xa = supp_rel alpha_b_lrb xa) \<and>
-   (fv_fnclauses xb = supp xb \<and> fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb) \<and>
-   (fv_lrb xc = supp xc \<and> fv_b_fnclause xc = supp_rel alpha_b_fnclause xc) \<and>
-   (fv_lrbs xd = supp xd \<and> fv_b_lrbs xd = supp_rel alpha_b_lrbs xd) \<and>
-   (fv_pat xe = supp xe \<and> fv_b_pat xe = supp_rel alpha_b_pat xe)"
-apply(rule fun_pats.induct)
-apply(tactic {* ALLGOALS (TRY o rtac @{thm conjI})*})
-thm fun_pats.inducts
-oops
-
-
-lemma
-  "fv_exp x = supp x" and
-  "fv_fnclause y = supp y" and
-  "fv_fnclauses xb = supp xb" and
-  "fv_lrb xc = supp xc" and
-  "fv_lrbs xd = supp xd" and
-  "fv_pat xe = supp xe" and
-  "fv_b_lrbs xd = supp_rel alpha_b_lrbs xd" and
-  "fv_b_pat xe = supp_rel alpha_b_pat xe" and
-  "fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb" and 
-  "fv_b_fnclause xc = supp_rel alpha_b_fnclause xc" and
-  "fv_b_lrb y = supp_rel alpha_b_lrb y"
-thm fun_pats.inducts
-apply(induct rule: fun_pats.inducts(1)[where ?exp="x::exp"] 
-                   fun_pats.inducts(2)[where ?fnclause="y"]
-                   fun_pats.inducts(3)[where ?fnclauses="xb"]
-                   fun_pats.inducts(4)[where ?lrb="xc"] 
-                   fun_pats.inducts(5)[where ?lrbs="xd"]
-                   fun_pats.inducts(6)[where ?pat="xe"])
-thm fun_pats.inducts
-oops
-
-end
-
-
-

--- a/Nominal/Ex/Modules.thy	Mon Sep 20 21:52:45 2010 +0800
+++ b/Nominal/Ex/Modules.thy	Wed Sep 22 14:19:48 2010 +0800
@@ -2,14 +2,14 @@
 imports "../Nominal2"
 begin
 
-(* example from Leroy'96 about modules; 
-   see OTT example by Owens *)
+(* 
+   example from Leroy'96 about modules
+
+   see OTT example by Owens 
+*)
 
 atom_decl name
 
-declare [[STEPS = 31]]
-
-
 nominal_datatype modules: 
  mexp =
   Acc "path"
@@ -72,7 +72,7 @@
 thm modules.eq_iff
 thm modules.fv_bn_eqvt
 thm modules.size_eqvt
-
+thm modules.supp
 
 
 end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Multi_Recs.thy	Wed Sep 22 14:19:48 2010 +0800
@@ -0,0 +1,49 @@
+theory Multi_Recs
+imports "../Nominal2"
+begin
+
+(* 
+  multiple recursive binders
+
+  example 7 from Peter Sewell's bestiary 
+
+*)
+
+atom_decl name
+
+nominal_datatype multi_recs: exp =
+  Var name
+| Unit
+| Pair exp exp
+| LetRec l::"lrbs" e::"exp"  bind (set) "bs l" in l e
+and lrb =
+  Assign name exp
+and lrbs =
+  Single lrb
+| More lrb lrbs
+binder
+  b :: "lrb \<Rightarrow> atom set" and
+  bs :: "lrbs \<Rightarrow> atom set"
+where
+  "b (Assign x e) = {atom x}"
+| "bs (Single a) = b a"
+| "bs (More a as) = (b a) \<union> (bs as)"
+
+thm multi_recs.distinct
+thm multi_recs.induct
+thm multi_recs.inducts
+thm multi_recs.exhaust
+thm multi_recs.fv_defs
+thm multi_recs.bn_defs
+thm multi_recs.perm_simps
+thm multi_recs.eq_iff
+thm multi_recs.fv_bn_eqvt
+thm multi_recs.size_eqvt
+thm multi_recs.supports
+thm multi_recs.fsupp
+thm multi_recs.supp
+
+end
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Multi_Recs2.thy	Wed Sep 22 14:19:48 2010 +0800
@@ -0,0 +1,70 @@
+theory Multi_Recs2
+imports "../Nominal2"
+begin
+
+(* 
+  multiple recursive binders - multiple letrecs with multiple 
+  clauses for each functions
+
+  example 8 from Peter Sewell's bestiary (originally due
+  to James Cheney) 
+
+*)
+
+atom_decl name
+
+nominal_datatype fun_recs: exp =
+  Var name
+| Unit 
+| Pair exp exp
+| LetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e
+and fnclause =
+  K x::name p::pat f::exp bind (set) "b_pat p" in f
+and fnclauses =
+  S fnclause
+| ORs fnclause fnclauses
+and lrb =
+  Clause fnclauses
+and lrbs =
+  Single lrb
+| More lrb lrbs
+and pat =
+  PVar name
+| PUnit
+| PPair pat pat
+binder
+  b_lrbs :: "lrbs \<Rightarrow> atom set" and
+  b_pat :: "pat \<Rightarrow> atom set" and
+  b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
+  b_fnclause :: "fnclause \<Rightarrow> atom set" and
+  b_lrb :: "lrb \<Rightarrow> atom set"
+where
+  "b_lrbs (Single l) = b_lrb l"
+| "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls"
+| "b_pat (PVar x) = {atom x}"
+| "b_pat (PUnit) = {}"
+| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
+| "b_fnclauses (S fc) = (b_fnclause fc)"
+| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
+| "b_lrb (Clause fcs) = (b_fnclauses fcs)"
+| "b_fnclause (K x pat exp) = {atom x}"
+
+thm fun_recs.distinct
+thm fun_recs.induct
+thm fun_recs.inducts
+thm fun_recs.exhaust
+thm fun_recs.fv_defs
+thm fun_recs.bn_defs
+thm fun_recs.perm_simps
+thm fun_recs.eq_iff
+thm fun_recs.fv_bn_eqvt
+thm fun_recs.size_eqvt
+thm fun_recs.supports
+thm fun_recs.fsupp
+thm fun_recs.supp
+
+
+end
+
+
+

--- a/Nominal/Nominal2.thy	Mon Sep 20 21:52:45 2010 +0800
+++ b/Nominal/Nominal2.thy	Wed Sep 22 14:19:48 2010 +0800
@@ -563,8 +563,8 @@
   val _ = warning "Proving Equality between fv and supp"
   val qfv_supp_thms = 
     if get_STEPS lthy > 31
-    then prove_fv_supp qtys qfvs qfv_bns qalpha_bns qbn_defs qfv_defs qeq_iffs 
-      qperm_simps qfv_qbn_eqvts qinducts (flat raw_bclauses) lthyC
+    then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qbn_defs qfv_defs qeq_iffs 
+      qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
     else []
 
  

--- a/Nominal/ROOT.ML	Mon Sep 20 21:52:45 2010 +0800
+++ b/Nominal/ROOT.ML	Wed Sep 22 14:19:48 2010 +0800
@@ -3,10 +3,11 @@
 no_document use_thys
    ["Ex/Classical",    
     "Ex/CoreHaskell",
+     Ex/Datatypes",
     "Ex/Ex1",
     "Ex/ExPS3",
-    "Ex/ExPS7",
-    "Ex/ExPS8",
+    "Ex/Multi_Recs",
+    "Ex/Multi_Recs2",
     "Ex/LF",
     "Ex/Lambda",
     "Ex/Let",

--- a/Nominal/nominal_dt_supp.ML	Mon Sep 20 21:52:45 2010 +0800
+++ b/Nominal/nominal_dt_supp.ML	Wed Sep 22 14:19:48 2010 +0800
@@ -13,8 +13,8 @@
   val fs_instance: typ list -> string list -> (string * sort) list -> thm list ->  
     local_theory -> local_theory
 
-  val prove_fv_supp: typ list -> term list -> term list -> term list -> thm list -> thm list -> 
-    thm list -> thm list -> thm list -> thm list -> bclause list list -> Proof.context -> thm list 
+  val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> thm list -> 
+    thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list 
 end
 
 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
@@ -104,27 +104,17 @@
 
 (* proves that fv and fv_bn equals supp *)
 
-fun mk_fvs_goals ty_arg_map fv =
+fun gen_mk_goals fv supp =
   let
-    val arg = fastype_of fv
+    val arg_ty = 
+      fastype_of fv
       |> domain_type
-      |> lookup ty_arg_map
   in
-    (fv $ arg, mk_supp arg)
-      |> HOLogic.mk_eq
-      |> HOLogic.mk_Trueprop 
+    (arg_ty, fn x => HOLogic.mk_eq (fv $ x, supp x))
   end
 
-fun mk_fv_bns_goals ty_arg_map fv_bn alpha_bn =
-  let
-    val arg = fastype_of fv_bn
-      |> domain_type
-      |> lookup ty_arg_map
-  in
-    (fv_bn $ arg, mk_supp_rel alpha_bn arg)
-      |> HOLogic.mk_eq
-      |> HOLogic.mk_Trueprop 
-  end
+fun mk_fvs_goals fv = gen_mk_goals fv mk_supp
+fun mk_fv_bns_goals fv_bn alpha_bn = gen_mk_goals fv_bn (mk_supp_rel alpha_bn)
 
 fun add_ss thms =
   HOL_basic_ss addsimps thms
@@ -144,15 +134,14 @@
   | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs
   | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs
 
-fun mk_bn_supp_abs_tac thm =
-  (prop_of thm)
-  |> HOLogic.dest_Trueprop
-  |> snd o HOLogic.dest_eq
+fun mk_bn_supp_abs_tac trm =
+  trm
   |> fastype_of
+  |> body_type
   |> (fn ty => case ty of
         @{typ "atom set"}  => simp_tac (add_ss supp_abs_set)
       | @{typ "atom list"} => simp_tac (add_ss supp_abs_lst)
-      | _ => raise TERM ("mk_bn_supp_abs_tac", [prop_of thm]))
+      | _ => raise TERM ("mk_bn_supp_abs_tac", [trm]))
 
 
 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc}
@@ -160,32 +149,49 @@
 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def 
   prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI}
 
-fun ind_tac ctxt qinducts = 
-  let
-    fun CASES_TAC_TO_TAC cases_tac st = Seq.map snd (cases_tac st)
-  in
-    DETERM o (CASES_TAC_TO_TAC o (Induct.induct_tac ctxt false [] [] [] (SOME qinducts) []))
-  end
-
 fun p_tac msg i = 
   if false then print_tac ("ptest: " ^ msg) else all_tac
 
 fun q_tac msg i = 
   if true then print_tac ("qtest: " ^ msg) else all_tac
 
-fun prove_fv_supp qtys fvs fv_bns alpha_bns bn_simps fv_simps eq_iffs perm_simps 
-  fv_bn_eqvts qinducts bclausess ctxt =
+fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns bn_simps fv_simps eq_iffs perm_simps 
+  fv_bn_eqvts qinduct bclausess ctxt =
   let
-    val (arg_names, ctxt') = 
-      Variable.variant_fixes (replicate (length qtys) "x") ctxt 
-    val args = map2 (curry Free) arg_names qtys 
-    val ty_arg_map = qtys ~~ args
-    val ind_args = map SOME arg_names
+    val goals1 = map mk_fvs_goals fvs
+    val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns   
+
+    
 
-    val goals1 = map (mk_fvs_goals ty_arg_map) fvs
-    val goals2 = map2 (mk_fv_bns_goals ty_arg_map) fv_bns alpha_bns
+    fun tac ctxt =
+      SUBGOAL (fn (goal, i) =>
+        let
+          val (fv_fun, arg) = 
+            goal |> Envir.eta_contract
+                 |> Logic.strip_assums_concl
+                 |> HOLogic.dest_Trueprop
+                 |> fst o HOLogic.dest_eq
+                 |> dest_comb
+          val supp_abs_tac = 
+            case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of
+              SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses)
+            | NONE => mk_bn_supp_abs_tac fv_fun
+        in
+          EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)),
+                   TRY o supp_abs_tac,
+                   TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}),
+                   TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], 
+                   TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)),
+                   TRY o asm_full_simp_tac (add_ss thms3),
+                   TRY o simp_tac (add_ss thms2),
+                   TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts)))] i
+        end)
+  in
+    induct_prove qtys (goals1 @ goals2) qinduct tac ctxt
+  end
 
-    fun fv_tac ctxt bclauses =
+(*
+   fun fv_tac bclauses ctxt =
       SOLVED' (EVERY' [
         (fn i => print_tac ("FV Goal: " ^ string_of_int i ^ "  with  " ^ (@{make_string} bclauses))),
         TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), 
@@ -207,7 +213,12 @@
         (fn i => print_tac ("finished with FV Goal: " ^ string_of_int i))
         ])
     
-    fun bn_tac ctxt bn_simp =
+    fun fv_tacs ctxt = map (fv_tac ctxt) bclausess
+    (*fun bn_tacs ctxt = map (bn_tac ctxt) bn_simps*)
+*)
+
+(*
+  fun bn_tac ctxt bn_simp =
       SOLVED' (EVERY' [
         (fn i => print_tac ("BN Goal: " ^ string_of_int i)),
         TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)),
@@ -227,18 +238,7 @@
         TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))),
         (fn i => print_tac ("finished with BN Goal: " ^ string_of_int i))
         ])
-
-    fun fv_tacs ctxt = map (fv_tac ctxt) bclausess
-    fun bn_tacs ctxt = map (bn_tac ctxt) bn_simps
-    
-  in
-    Goal.prove_multi ctxt' [] [] (goals1 @ goals2)
-     (fn {context as ctxt, ...} => HEADGOAL 
-       (ind_tac ctxt qinducts THEN' RANGE  (fv_tacs ctxt @ bn_tacs ctxt)))
-    |> ProofContext.export ctxt' ctxt
-  end
-
+*)
 
 
 end (* structure *)
-