diff -r 515e5496171c -r 07f775729e90 Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Mon Dec 06 16:35:42 2010 +0000
+++ b/Nominal/nominal_dt_quot.ML	Mon Dec 06 17:11:34 2010 +0000
@@ -2,7 +2,8 @@
     Author:     Christian Urban
     Author:     Cezary Kaliszyk
 
-  Performing quotient constructions and lifting theorems
+  Performing quotient constructions, lifting theorems and
+  deriving support propoerties for the quotient types.
 *)
 
 signature NOMINAL_DT_QUOT =
@@ -21,6 +22,20 @@
 
   val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context
 
+  val prove_supports: Proof.context -> thm list -> term list -> thm list  
+  val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list
+
+  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 -> term list -> thm list -> 
+    thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list 
+
+  val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list
+ 
+  val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
+    thm list -> Proof.context -> thm list
+  
 end
 
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -128,5 +143,208 @@
         #> unraw_vars_thm
         #> Drule.zero_var_indexes) thms, ctxt)
 
+
+
+fun mk_supports_goal ctxt qtrm =
+  let  
+    val vs = fresh_args ctxt qtrm
+    val rhs = list_comb (qtrm, vs)
+    val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"}
+      |> mk_supp
+  in
+    mk_supports lhs rhs
+    |> HOLogic.mk_Trueprop
+  end
+
+fun supports_tac ctxt perm_simps =
+  let
+    val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]}
+    val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair}
+  in
+    EVERY' [ simp_tac ss1,
+             Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [],
+             simp_tac ss2 ]
+  end
+
+fun prove_supports_single ctxt perm_simps qtrm =
+  let
+    val goal = mk_supports_goal ctxt qtrm 
+    val ctxt' = Variable.auto_fixes goal ctxt
+  in
+    Goal.prove ctxt' [] [] goal
+      (K (HEADGOAL (supports_tac ctxt perm_simps)))
+    |> singleton (ProofContext.export ctxt' ctxt)
+  end
+
+fun prove_supports ctxt perm_simps qtrms =
+  map (prove_supports_single ctxt perm_simps) qtrms
+
+
+(* finite supp lemmas for qtypes *)
+
+fun prove_fsupp ctxt qtys qinduct qsupports_thms =
+  let
+    val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt
+    val goals = vs ~~ qtys
+      |> map Free
+      |> map (mk_finite o mk_supp)
+      |> foldr1 (HOLogic.mk_conj)
+      |> HOLogic.mk_Trueprop
+
+    val tac = 
+      EVERY' [ rtac @{thm supports_finite},
+               resolve_tac qsupports_thms,
+               asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ]
+  in
+    Goal.prove ctxt' [] [] goals
+      (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac)))
+    |> singleton (ProofContext.export ctxt' ctxt)
+    |> Datatype_Aux.split_conj_thm
+    |> map zero_var_indexes
+  end
+
+
+(* finite supp instances *)
+
+fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy =
+  let
+    val lthy1 = 
+      lthy
+      |> Local_Theory.exit_global
+      |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) 
+  
+    fun tac _ =
+      Class.intro_classes_tac [] THEN
+        (ALLGOALS (resolve_tac qfsupp_thms))
+  in
+    lthy1
+    |> Class.prove_instantiation_exit tac 
+    |> Named_Target.theory_init
+  end
+
+
+(* proves that fv and fv_bn equals supp *)
+
+fun gen_mk_goals fv supp =
+  let
+    val arg_ty = 
+      fastype_of fv
+      |> domain_type
+  in
+    (arg_ty, fn x => HOLogic.mk_eq (fv $ x, supp x))
+  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
+
+fun symmetric thms = 
+  map (fn thm => thm RS @{thm sym}) thms
+
+val supp_Abs_set = @{thms supp_Abs(1)[symmetric]}
+val supp_Abs_res = @{thms supp_Abs(2)[symmetric]}
+val supp_Abs_lst = @{thms supp_Abs(3)[symmetric]}
+
+fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_set 
+  | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_res
+  | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_lst
+
+fun mk_supp_abs_tac ctxt [] = []
+  | 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 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", [trm]))
+
+
+val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc}
+val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un}
+val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def 
+  prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI}
+
+fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps 
+  fv_bn_eqvts qinduct bclausess ctxt =
+  let
+    val goals1 = map mk_fvs_goals fvs
+    val goals2 = map2 mk_fv_bns_goals 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
+    |> map atomize
+    |> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]}))
+  end
+
+
+fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt =
+  let
+    fun mk_goal qbn = 
+      let
+        val arg_ty = domain_type (fastype_of qbn)
+        val finite = @{term "finite :: atom set => bool"}
+      in
+        (arg_ty, fn x => finite $ (to_set (qbn $ x)))
+      end
+
+    val props = map mk_goal qbns
+    val ss_tac = asm_full_simp_tac (HOL_basic_ss addsimps (qbn_simps @ 
+      @{thms set.simps set_append finite_insert finite.emptyI finite_Un}))
+  in
+    induct_prove qtys props qinduct (K ss_tac) ctxt
+  end
+
+fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt =
+  let 
+    val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
+    val p = Free (p, @{typ perm})
+
+    fun mk_goal qperm_bn alpha_bn =
+      let
+        val arg_ty = domain_type (fastype_of alpha_bn)
+      in
+        (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x)
+      end
+
+    val props = map2 mk_goal qperm_bns alpha_bns
+    val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls
+    val ss_tac = asm_full_simp_tac (HOL_ss addsimps ss)
+  in
+    induct_prove qtys props qinduct (K ss_tac) ctxt'
+    |> ProofContext.export ctxt' ctxt
+    |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) 
+  end
+
+
+
 end (* structure *)