--- 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 *)
-