# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269020577 -3600
# Node ID 4355eb3b7161006487b74047fcfbf0947e12733c
# Parent  74888979e9cd70d2953e0014a014fcf5c427841a
Automatically derive support for datatypes with at-most one binding per constructor.

diff -r 74888979e9cd -r 4355eb3b7161 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Fri Mar 19 15:01:01 2010 +0100
+++ b/Nominal/Fv.thy	Fri Mar 19 18:42:57 2010 +0100
@@ -385,6 +385,7 @@
   val nr_bns = non_rec_binds bindsall;
   val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns;
   val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns);
+  val fvbns = map snd bn_fv_bns;
   val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs;
   val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
     "alpha_" ^ name_of_typ (nth_dtyp i)) descr);
@@ -548,9 +549,11 @@
      (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names)
      (alpha_types @ alpha_bn_types)) []
      (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'')
+  val ordered_fvs = fv_frees @ fvbns;
+  val exported_fvs = map (Morphism.term (ProofContext.export_morphism lthy''' lthy)) ordered_fvs;
   val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2)
 in
-  ((all_fvs, alphas), lthy''')
+  (((all_fvs, ordered_fvs), alphas), lthy''')
 end
 *}
 
@@ -920,4 +923,76 @@
 end
 *}
 
+ML {*
+fun mk_supp x = Const (@{const_name supp}, fastype_of x --> @{typ "atom set"}) $ x;
+
+fun mk_supp_neq arg (fv, alpha) =
+let
+  val collect = Const ("Collect", @{typ "(atom \<Rightarrow> bool) \<Rightarrow> atom \<Rightarrow> bool"});
+  val ty = fastype_of arg;
+  val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty);
+  val finite = @{term "finite :: atom set \<Rightarrow> bool"}
+  val rhs = collect $ Abs ("a", @{typ atom},
+    HOLogic.mk_not (finite $
+      (collect $ Abs ("b", @{typ atom},
+        HOLogic.mk_not (alpha $ (perm $ (@{term swap} $ Bound 1 $ Bound 0) $ arg) $ arg)))))
+in
+  HOLogic.mk_eq (fv $ arg, rhs)
+end;
+
+fun supp_eq fv_alphas_lst =
+let
+  val (fvs_alphas, ls) = split_list fv_alphas_lst;
+  val (fv_ts, _) = split_list fvs_alphas;
+  val tys = map (domain_type o fastype_of) fv_ts;
+  val names = Datatype_Prop.make_tnames tys;
+  val args = map Free (names ~~ tys);
+  fun supp_eq_arg ((fv, arg), l) =
+    mk_conjl
+      ((HOLogic.mk_eq (fv $ arg, mk_supp arg)) ::
+       (map (mk_supp_neq arg) l))
+  val eqs = mk_conjl (map supp_eq_arg ((fv_ts ~~ args) ~~ ls))
+in
+  (names, HOLogic.mk_Trueprop eqs)
 end
+*}
+
+ML {*
+fun combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos =
+if length fv_ts_bn < length alpha_ts_bn then
+  (fv_ts_nobn ~~ alpha_ts_nobn) ~~ (replicate (length fv_ts_nobn) [])
+else let
+  val fv_alpha_nos = 0 upto (length fv_ts_nobn - 1);
+  fun filter_fn i (x, j) = if j = i then SOME x else NONE;
+  val fv_alpha_bn_nos = (fv_ts_bn ~~ alpha_ts_bn) ~~ bn_nos;
+  val fv_alpha_bn_all = map (fn i => map_filter (filter_fn i) fv_alpha_bn_nos) fv_alpha_nos;
+in
+  (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all
+end
+*}
+
+lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
+  apply (simp add: supp_Abs supp_Pair)
+  apply blast
+  done
+
+ML {*
+fun supp_eq_tac ind fv perm eqiff ctxt =
+  ind_tac ind THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_Abs[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps (@{thm permute_ABS} :: perm)) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric] Collect_disj_eq[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW
+  simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
+*}
+
+end
diff -r 74888979e9cd -r 4355eb3b7161 Nominal/LFex.thy
--- a/Nominal/LFex.thy	Fri Mar 19 15:01:01 2010 +0100
+++ b/Nominal/LFex.thy	Fri Mar 19 18:42:57 2010 +0100
@@ -22,57 +22,7 @@
   | App "trm" "trm"
   | Lam "ty" n::"name" t::"trm" bind n in t
 
-lemma ex_out: 
-  "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))"
-  "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))"
-  "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
-  "(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
-apply (blast)+
-done
-
-lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}"
-by (simp add: Collect_imp_eq Collect_neg_eq[symmetric])
-
-lemma supp_eqs:
-  "supp Type = {}"
-  "supp kind = fv_kind kind \<Longrightarrow> supp (KPi ty name kind) = supp ty \<union> supp (Abs {atom name} kind)"
-  "supp (TConst i) = {atom i}"
-  "supp (TApp A M) = supp A \<union> supp M"
-  "supp ty2 = fv_ty ty2 \<Longrightarrow> supp (TPi ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)"
-  "supp (Const i) = {atom i}"
-  "supp (Var x) = {atom x}"
-  "supp (App M N) = supp M \<union> supp N"
-  "supp trm = fv_trm trm \<Longrightarrow> supp (Lam ty name trm) = supp ty \<union> supp (Abs {atom name} trm)"
-  apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt)
-  apply(simp_all only: kind_ty_trm.eq_iff Abs_eq_iff alpha_gen)
-  apply(simp_all only: ex_out)
-  apply(simp_all only: eqvts[symmetric])
-  apply(simp_all only: Collect_neg_conj)
-  apply(simp_all only: supp_at_base[simplified supp_def] Un_commute Un_assoc)
-  apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Un_commute Un_assoc)
-  apply(simp_all add: Un_left_commute)
-  done
-
-lemma supp_fv:
-  "supp t1 = fv_kind t1 \<and> supp t2 = fv_ty t2 \<and> supp t3 = fv_trm t3"
-  apply(induct rule: kind_ty_trm.induct)
-  apply(simp_all (no_asm) only: supp_eqs)
-  apply(simp_all)
-  apply(simp_all add: supp_eqs)
-  apply(simp_all add: supp_Abs)
-  done
-
-lemma supp_kind_ty_trm:
-  "supp Type = {}"
-  "supp (KPi A x K) = supp A \<union> (supp K - {atom x})"
-  "supp (TConst i) = {atom i}"
-  "supp (TApp A M) = supp A \<union> supp M"
-  "supp (TPi A x B) = supp A \<union> (supp B - {atom x})"
-  "supp (Const i) = {atom i}"
-  "supp (Var x) = {atom x}"
-  "supp (App M N) = supp M \<union> supp N"
-  "supp (Lam A x M) = supp A \<union> (supp M - {atom x})"
-apply (simp_all add: supp_fv)
+thm kind_ty_trm.supp
 
 end
 
diff -r 74888979e9cd -r 4355eb3b7161 Nominal/Lift.thy
--- a/Nominal/Lift.thy	Fri Mar 19 15:01:01 2010 +0100
+++ b/Nominal/Lift.thy	Fri Mar 19 18:42:57 2010 +0100
@@ -61,7 +61,7 @@
 ML {*
 fun define_fv_alpha_export dt binds bns ctxt =
 let
-  val (((fv_ts_loc, fv_def_loc), alpha), ctxt') =
+  val ((((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), alpha), ctxt') =
     define_fv_alpha dt binds bns ctxt;
   val alpha_ts_loc = #preds alpha
   val alpha_induct_loc = #induct alpha
@@ -69,13 +69,14 @@
   val alpha_cases_loc = #elims alpha
   val morphism = ProofContext.export_morphism ctxt' ctxt;
   val fv_ts = map (Morphism.term morphism) fv_ts_loc;
+  val ord_fv_ts = map (Morphism.term morphism) ord_fv_ts_loc;
   val fv_def = Morphism.fact morphism fv_def_loc;
   val alpha_ts = map (Morphism.term morphism) alpha_ts_loc;
   val alpha_induct = Morphism.thm morphism alpha_induct_loc;
   val alpha_intros = Morphism.fact morphism alpha_intros_loc
   val alpha_cases = Morphism.fact morphism alpha_cases_loc
 in
-  (((fv_ts, fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt')
+  ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt')
 end;
 *}
 
diff -r 74888979e9cd -r 4355eb3b7161 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Fri Mar 19 15:01:01 2010 +0100
+++ b/Nominal/Parser.thy	Fri Mar 19 18:42:57 2010 +0100
@@ -306,7 +306,7 @@
   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
   val raw_binds_flat = map (map flat) raw_binds;
-  val (((fv_ts, fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) =
+  val ((((fv_ts, ordered_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) =
     define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3;
   val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts;
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
@@ -325,7 +325,7 @@
   val (fv_bn_eqvts, lthy6a) =
     if fv_ts_bn = [] then ([], lthy6) else
     fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) inducts)
-      (fv_ts_bn ~~ (map snd bns)) lthy6;
+      (fv_ts_bn ~~ bn_nos) lthy6;
   val raw_fv_bv_eqvt = flat (map snd bv_eqvts) @ (snd fv_eqvts) @ flat (map snd fv_bn_eqvts)
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
@@ -365,12 +365,13 @@
     else constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp) alpha_equivp 1
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
     const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11
-  val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts
-  val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12;
+  val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts
+  val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12;
+  val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
   val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a;
   val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
-  val (qbn_defs, lthy12c) = fold_map Quotient_Def.quotient_lift_const (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
+  val (qalpha_ts_bn, qbn_defs, lthy12c) = quotient_lift_consts_export (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
   val _ = tracing "Lifting permutations";
   val thy = Local_Theory.exit_global lthy12c;
   val perm_names = map (fn x => "permute_" ^ x) qty_names
@@ -381,6 +382,8 @@
   val _ = tracing "Lifting induction";
   val constr_names = map (Long_Name.base_name o fst o dest_Const) consts;
   val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 induct);
+  fun note_suffix s th ctxt =
+    snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
   fun note_simp_suffix s th ctxt =
     snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
   val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
@@ -413,9 +416,13 @@
   val thy3 = Local_Theory.exit_global lthy20;
   val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3;
   fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))
-  val lthy22 = Class.prove_instantiation_instance tac lthy21 handle _ => lthy20
+  val lthy22 = Class.prove_instantiation_instance tac lthy21
+  val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
+  val (names, supp_eq_t) = supp_eq fv_alpha_all;
+  val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => [];
+  val lthy23 = note_suffix "supp" q_supp lthy22;
 in
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy22)
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy23)
 end
 *}
 
diff -r 74888979e9cd -r 4355eb3b7161 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Fri Mar 19 15:01:01 2010 +0100
+++ b/Nominal/Rsp.thy	Fri Mar 19 18:42:57 2010 +0100
@@ -86,10 +86,12 @@
   (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))))
 *}
 
+
 ML {*
-  fun all_eqvts ctxt =
-    Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
-  val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
+fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt)
+fun all_eqvts ctxt =
+  Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
+val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
 *}
 
 ML {*
diff -r 74888979e9cd -r 4355eb3b7161 Nominal/Test.thy
--- a/Nominal/Test.thy	Fri Mar 19 15:01:01 2010 +0100
+++ b/Nominal/Test.thy	Fri Mar 19 18:42:57 2010 +0100
@@ -13,43 +13,7 @@
 | Ap "lm" "lm"
 | Lm x::"name" l::"lm"  bind x in l
 
-lemma finite_fv:
-  shows "finite (fv_lm t)"
-apply(induct t rule: lm.induct)
-apply(simp_all)
-done
-
-lemma supp_fn:
-  shows "supp t = fv_lm t"
-apply(induct t rule: lm.induct)
-apply(simp_all)
-apply(simp only: supp_def)
-apply(simp only: lm.perm)
-apply(simp only: lm.eq_iff)
-apply(simp only: supp_def[symmetric])
-apply(simp only: supp_at_base)
-apply(simp (no_asm) only: supp_def)
-apply(simp only: lm.perm)
-apply(simp only: lm.eq_iff)
-apply(simp only: de_Morgan_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-apply(simp only: supp_def[symmetric])
-apply(rule_tac t="supp (Lm name lm)" and s="supp (Abs {atom name} lm)" in subst)
-apply(simp (no_asm) only: supp_def)
-apply(simp only: lm.perm)
-apply(simp only: permute_ABS)
-apply(simp only: lm.eq_iff)
-apply(simp only: Abs_eq_iff)
-apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
-apply(simp only: alpha_gen)
-apply(simp only: supp_eqvt[symmetric])
-apply(simp only: eqvts)
-apply(simp only: supp_Abs)
-done
-
-lemmas supp_fn' = lm.fv[simplified supp_fn[symmetric]]
+lemmas supp_fn' = lm.fv[simplified lm.supp]
 
 lemma
   fixes c::"'a::fs"
@@ -67,6 +31,11 @@
     apply(blast)[1]
     apply(assumption)
     apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))")
+    defer
+    apply(simp add: fresh_def)
+    apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base)
+    apply(simp add: supp_Pair finite_supp)
+    apply(blast)
     apply(erule exE)
     apply(rule_tac t="p \<bullet> Lm name lm" and 
                    s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst)
@@ -83,10 +52,6 @@
     apply(simp add: fresh_Pair)
     apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
     apply(simp)
-    apply(simp add: fresh_def)
-    apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base)
-    apply(simp add: supp_Pair finite_supp)
-    apply(blast)
     done
   then have "P c (0 \<bullet> lm)" by blast
   then show "P c lm" by simp
@@ -124,7 +89,6 @@
   then show "P c lm" by simp
 qed
 
-
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"
@@ -138,6 +102,7 @@
   "bi (BP x t) = {atom x}"
 
 thm lam_bp.fv
+thm lam_bp.supp
 thm lam_bp.eq_iff
 thm lam_bp.bn
 thm lam_bp.perm
@@ -145,77 +110,7 @@
 thm lam_bp.inducts
 thm lam_bp.distinct
 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
-
-term "supp (x :: lam)"
-
-lemma bi_eqvt:
-  shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
-  by (rule eqvts)
-
-lemma supp_fv:
-  shows "supp t = fv_lam t" 
-  and "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}"
-apply(induct t and bp rule: lam_bp.inducts)
-apply(simp_all)
-(* VAR case *)
-apply(simp only: supp_def)
-apply(simp only: lam_bp.perm)
-apply(simp only: lam_bp.eq_iff)
-apply(simp only: supp_def[symmetric])
-apply(simp only: supp_at_base)
-(* APP case *)
-apply(simp only: supp_def)
-apply(simp only: lam_bp.perm)
-apply(simp only: lam_bp.eq_iff)
-apply(simp only: de_Morgan_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-(* LAM case *)
-apply(rule_tac t="supp (LAM name lam)" and s="supp (Abs {atom name} lam)" in subst)
-apply(simp (no_asm) only: supp_def)
-apply(simp only: lam_bp.perm)
-apply(simp only: permute_ABS)
-apply(simp only: lam_bp.eq_iff)
-apply(simp only: Abs_eq_iff)
-apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
-apply(simp only: alpha_gen)
-apply(simp only: supp_eqvt[symmetric])
-apply(simp only: eqvts)
-apply(simp only: supp_Abs)
-(* LET case *)
-apply(rule_tac t="supp (LET bp lam)" and s="supp (Abs (bi bp) lam) \<union> fv_bi bp" in subst)
-apply(simp (no_asm) only: supp_def)
-apply(simp only: lam_bp.perm)
-apply(simp only: permute_ABS)
-apply(simp only: lam_bp.eq_iff)
-apply(simp only: eqvts)
-apply(simp only: Abs_eq_iff)
-apply(simp only: ex_simps)
-apply(simp only: de_Morgan_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-apply(simp only: alpha_gen)
-apply(simp only: supp_eqvt[symmetric])
-apply(simp only: eqvts)
-apply(blast)
-apply(simp add: supp_Abs)
-apply(blast)
-(* BP case *)
-apply(simp only: supp_def)
-apply(simp only: lam_bp.perm)
-apply(simp only: lam_bp.eq_iff)
-apply(simp only: de_Morgan_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-apply(simp only: supp_def[symmetric])
-apply(simp only: supp_at_base)
-apply(simp)
-done
-
-thm lam_bp.fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
+thm lam_bp.fv[simplified lam_bp.supp]
 
 ML {* val _ = recursive := true *}
 
@@ -240,69 +135,7 @@
 thm lam'_bp'.distinct
 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
 
-lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
-apply (simp add: supp_Abs supp_Pair)
-apply blast
-done
-
-lemma supp_fv':
-  shows "supp t = fv_lam' t" 
-  and "supp bp = fv_bp' bp"
-apply(induct t and bp rule: lam'_bp'.inducts)
-apply(simp_all)
-(* VAR case *)
-apply(simp only: supp_def)
-apply(simp only: lam'_bp'.perm)
-apply(simp only: lam'_bp'.eq_iff)
-apply(simp only: supp_def[symmetric])
-apply(simp only: supp_at_base)
-(* APP case *)
-apply(simp only: supp_def)
-apply(simp only: lam'_bp'.perm)
-apply(simp only: lam'_bp'.eq_iff)
-apply(simp only: de_Morgan_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-(* LAM case *)
-apply(rule_tac t="supp (LAM' name lam')" and s="supp (Abs {atom name} lam')" in subst)
-apply(simp (no_asm) only: supp_def)
-apply(simp only: lam'_bp'.perm)
-apply(simp only: permute_ABS)
-apply(simp only: lam'_bp'.eq_iff)
-apply(simp only: Abs_eq_iff)
-apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
-apply(simp only: alpha_gen)
-apply(simp only: supp_eqvt[symmetric])
-apply(simp only: eqvts)
-apply(simp only: supp_Abs)
-(* LET case *)
-apply(rule_tac t="supp (LET' bp' lam')" and 
-               s="supp (Abs (bi' bp') (bp', lam'))" in subst)
-apply(simp (no_asm) only: supp_def)
-apply(simp only: lam'_bp'.perm)
-apply(simp only: permute_ABS)
-apply(simp only: lam'_bp'.eq_iff)
-apply(simp only: Abs_eq_iff)
-apply(simp only: alpha_gen)
-apply(simp only: eqvts split_def fst_conv snd_conv)
-apply(simp only: eqvts[symmetric] supp_Pair)
-apply(simp only: eqvts Pair_eq)
-apply(simp add: supp_Abs supp_Pair)
-apply blast
-apply(simp only: supp_def)
-apply(simp only: lam'_bp'.perm)
-apply(simp only: lam'_bp'.eq_iff)
-apply(simp only: de_Morgan_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-apply(simp only: supp_def[symmetric])
-apply(simp only: supp_at_base supp_atom)
-apply simp
-done
-
-thm lam'_bp'.fv[simplified supp_fv'[symmetric]]
+thm lam'_bp'.fv[simplified lam'_bp'.supp]
 
 
 text {* example 2 *}
@@ -330,83 +163,7 @@
 thm trm'_pat'.perm
 thm trm'_pat'.induct
 thm trm'_pat'.distinct
-
-lemma supp_fv_trm'_pat':
-  shows "supp t = fv_trm' t" 
-  and "supp bp = fv_pat' bp \<and> {a. infinite {b. \<not>alpha_f ((a \<rightleftharpoons> b) \<bullet> bp) bp}} = fv_f bp"
-apply(induct t and bp rule: trm'_pat'.inducts)
-apply(simp_all)
-(* VAR case *)
-apply(simp only: supp_def)
-apply(simp only: trm'_pat'.perm)
-apply(simp only: trm'_pat'.eq_iff)
-apply(simp only: supp_def[symmetric])
-apply(simp only: supp_at_base)
-(* APP case *)
-apply(simp only: supp_def)
-apply(simp only: trm'_pat'.perm)
-apply(simp only: trm'_pat'.eq_iff)
-apply(simp only: de_Morgan_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-(* LAM case *)
-apply(rule_tac t="supp (Lam name trm')" and s="supp (Abs {atom name} trm')" in subst)
-apply(simp (no_asm) only: supp_def)
-apply(simp only: trm'_pat'.perm)
-apply(simp only: permute_ABS)
-apply(simp only: trm'_pat'.eq_iff)
-apply(simp only: Abs_eq_iff)
-apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
-apply(simp only: alpha_gen)
-apply(simp only: supp_eqvt[symmetric])
-apply(simp only: eqvts)
-apply(simp only: supp_Abs)
-(* LET case *)
-apply(rule_tac t="supp (Let pat' trm'1 trm'2)" 
-           and s="supp (Abs (f pat') trm'2) \<union> supp trm'1 \<union> fv_f pat'" in subst)
-apply(simp (no_asm) only: supp_def)
-apply(simp only: trm'_pat'.perm)
-apply(simp only: permute_ABS)
-apply(simp only: trm'_pat'.eq_iff)
-apply(simp only: eqvts)
-apply(simp only: Abs_eq_iff)
-apply(simp only: ex_simps)
-apply(simp only: de_Morgan_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-apply(simp only: alpha_gen)
-apply(simp only: supp_eqvt[symmetric])
-apply(simp only: eqvts)
-apply(blast)
-apply(simp add: supp_Abs)
-apply(blast)
-(* PN case *)
-apply(simp only: supp_def)
-apply(simp only: trm'_pat'.perm)
-apply(simp only: trm'_pat'.eq_iff)
-apply(simp)
-(* PS case *)
-apply(simp only: supp_def)
-apply(simp only: trm'_pat'.perm)
-apply(simp only: trm'_pat'.eq_iff)
-apply(simp only: supp_def[symmetric])
-apply(simp only: supp_at_base)
-apply(simp)
-(* PD case *)
-apply(simp only: supp_def)
-apply(simp only: trm'_pat'.perm)
-apply(simp only: trm'_pat'.eq_iff)
-apply(simp only: de_Morgan_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-apply(simp only: supp_def[symmetric])
-apply(simp add: supp_at_base)
-done
-
-thm trm'_pat'.fv[simplified supp_fv_trm'_pat'(1)[symmetric] supp_fv_trm'_pat'(2)[THEN conjunct1, symmetric]]
+thm trm'_pat'.fv[simplified trm'_pat'.supp]
 
 nominal_datatype trm0 =
   Var0 "name"
@@ -430,6 +187,7 @@
 thm trm0_pat0.perm
 thm trm0_pat0.induct
 thm trm0_pat0.distinct
+thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars]
 
 text {* example type schemes *}
 
@@ -445,61 +203,16 @@
 thm t_tyS.perm
 thm t_tyS.induct
 thm t_tyS.distinct
+thm t_tyS.fv[simplified t_tyS.supp]
 
 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *}
 
-lemma finite_fv_t_tyS:
-  fixes T::"t"
-  and   S::"tyS"
-  shows "finite (fv_t T)" 
-  and   "finite (fv_tyS S)"
-apply(induct T and S rule: t_tyS.inducts)
-apply(simp_all add: t_tyS.fv)
-done
 
-lemma supp_fv_t_tyS:
-  shows "supp T = fv_t T" 
-  and   "supp S = fv_tyS S"
-apply(induct T and S rule: t_tyS.inducts)
-apply(simp_all)
-(* VarTS case *)
-apply(simp only: supp_def)
-apply(simp only: t_tyS.perm)
-apply(simp only: t_tyS.eq_iff)
-apply(simp only: supp_def[symmetric])
-apply(simp only: supp_at_base)
-(* FunTS case *)
-apply(simp only: supp_def)
-apply(simp only: t_tyS.perm)
-apply(simp only: t_tyS.eq_iff)
-apply(simp only: de_Morgan_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-(* All case *)
-apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst)
-apply(simp (no_asm) only: supp_def)
-apply(simp only: t_tyS.perm)
-apply(simp only: permute_ABS)
-apply(simp only: t_tyS.eq_iff)
-apply(simp only: Abs_eq_iff)
-apply(simp only: eqvts)
-apply(simp only: alpha_gen)
-apply(simp only: supp_eqvt[symmetric])
-apply(simp only: eqvts eqvts_raw)
-apply(rule trans)
-apply(rule finite_supp_Abs)
-apply(simp add: finite_fv_t_tyS)
-apply(simp)
-done
 
 (* example 1 from Terms.thy *)
 
 
-  
-
-
 nominal_datatype trm1 =
   Vr1 "name"
 | Ap1 "trm1" "trm1"
@@ -522,6 +235,7 @@
 thm trm1_bp1.perm
 thm trm1_bp1.induct
 thm trm1_bp1.distinct
+thm trm1_bp1.fv[simplified trm1_bp1.supp]
 
 text {* example 3 from Terms.thy *}
 
@@ -545,6 +259,7 @@
 thm trm3_rassigns3.perm
 thm trm3_rassigns3.induct
 thm trm3_rassigns3.distinct
+thm trm3_rassigns3.fv[simplified trm3_rassigns3.supp]
 
 (* example 5 from Terms.thy *)
 
@@ -567,47 +282,7 @@
 thm trm5_lts.perm
 thm trm5_lts.induct
 thm trm5_lts.distinct
-
-lemma
-  shows "fv_trm5 t = supp t"
-  and "fv_lts l = supp l \<and> fv_bv5 l = {a. infinite {b. \<not>alpha_bv5 ((a \<rightleftharpoons> b) \<bullet> l) l}}"
-apply(induct t and l rule: trm5_lts.inducts)
-apply(simp_all only: trm5_lts.fv)
-apply(simp_all only: supp_Abs[symmetric])
-(*apply(simp_all only: supp_abs_sum)*)
-apply(simp_all (no_asm) only: supp_def)
-apply(simp_all only: trm5_lts.perm)
-apply(simp_all only: permute_ABS)
-apply(simp_all only: trm5_lts.eq_iff Abs_eq_iff)
-(*apply(simp_all only: alpha_gen2)*)
-apply(simp_all only: alpha_gen)
-apply(simp_all only: eqvts[symmetric] supp_Pair)
-apply(simp_all only: eqvts Pair_eq)
-apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
-apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
-apply(simp_all only: de_Morgan_conj[symmetric])
-apply simp_all
-done
-
-(* example from my PHD *)
-
-atom_decl coname
-
-nominal_datatype phd =
-   Ax "name" "coname"
-|  Cut n::"coname" t1::"phd" c::"coname" t2::"phd"              bind n in t1, bind c in t2
-|  AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname"  bind c1 in t1, bind c2 in t2
-|  AndL1 n::"name" t::"phd" "name"                              bind n in t
-|  AndL2 n::"name" t::"phd" "name"                              bind n in t
-|  ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name"        bind c in t1, bind n in t2
-|  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in t, bind c in t
-
-thm phd.fv
-thm phd.eq_iff
-thm phd.bn
-thm phd.perm
-thm phd.induct
-thm phd.distinct
+thm trm5_lts.fv[simplified trm5_lts.supp]
 
 (* example form Leroy 96 about modules; OTT *)
 
@@ -669,28 +344,30 @@
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp]
 
-lemma
-"fv_mexp j = supp j \<and> fv_body k = supp k \<and> 
-(fv_defn c = supp c \<and> fv_cbinders c = {a. infinite {b. \<not>alpha_cbinders ((a \<rightleftharpoons> b) \<bullet> c) c}}) \<and>
-fv_sexp d = supp d \<and> fv_sbody e = supp e \<and> 
-(fv_spec l = supp l \<and> fv_Cbinders l = {a. infinite {b. \<not>alpha_Cbinders ((a \<rightleftharpoons> b) \<bullet> l) l}}) \<and>
-fv_tyty g = supp g \<and> fv_path h = supp h \<and> fv_trmtrm i = supp i"
-apply(induct rule: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct)
-apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv)
-apply(simp_all only: supp_Abs[symmetric])
-apply(simp_all (no_asm) only: supp_def)
-apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm)
-apply(simp_all only: permute_ABS)
-apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff Abs_eq_iff)
-apply(simp_all only: alpha_gen)
-apply(simp_all only: eqvts[symmetric] supp_Pair)
-apply(simp_all only: eqvts Pair_eq)
-apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
-apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
-apply(simp_all only: de_Morgan_conj[symmetric])
-apply simp_all
-done
+
+(* example from my PHD *)
+
+atom_decl coname
+
+nominal_datatype phd =
+   Ax "name" "coname"
+|  Cut n::"coname" t1::"phd" c::"coname" t2::"phd"              bind n in t1, bind c in t2
+|  AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname"  bind c1 in t1, bind c2 in t2
+|  AndL1 n::"name" t::"phd" "name"                              bind n in t
+|  AndL2 n::"name" t::"phd" "name"                              bind n in t
+|  ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name"        bind c in t1, bind n in t2
+|  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in t, bind c in t
+
+thm phd.fv
+thm phd.eq_iff
+thm phd.bn
+thm phd.perm
+thm phd.induct
+thm phd.distinct
+thm phd.fv[simplified phd.supp]
 
 (* example 3 from Peter Sewell's bestiary *)
 
@@ -716,6 +393,7 @@
 thm exp_pat3.perm
 thm exp_pat3.induct
 thm exp_pat3.distinct
+thm exp_pat3.fv[simplified exp_pat3.supp]
 
 (* example 6 from Peter Sewell's bestiary *)
 nominal_datatype exp6 =
@@ -740,6 +418,7 @@
 thm exp6_pat6.induct
 thm exp6_pat6.distinct
 
+
 (* THE REST ARE NOT SUPPOSED TO WORK YET *)
 
 (* example 7 from Peter Sewell's bestiary *)
diff -r 74888979e9cd -r 4355eb3b7161 Nominal/TySch.thy
--- a/Nominal/TySch.thy	Fri Mar 19 15:01:01 2010 +0100
+++ b/Nominal/TySch.thy	Fri Mar 19 18:42:57 2010 +0100
@@ -22,39 +22,7 @@
 thm t_tyS.distinct
 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
 
-lemma finite_fv_t_tyS:
-  shows "finite (fv_t t)" "finite (fv_tyS ts)"
-  by (induct rule: t_tyS.inducts) (simp_all)
-
-lemma supp_fv_t_tyS:
-  shows "fv_t t = supp t" "fv_tyS ts = supp ts"
-  apply(induct rule: t_tyS.inducts)
-  apply(simp_all only: t_tyS.fv)
-  prefer 3
-  apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst)
-  prefer 2
-  apply(subst finite_supp_Abs)
-  apply(drule sym)
-  apply(simp add: finite_fv_t_tyS(1))
-  apply(simp)
-  apply(simp_all (no_asm) only: supp_def)
-  apply(simp_all only: t_tyS.perm)
-  apply(simp_all only: permute_ABS)
-  apply(simp_all only: t_tyS.eq_iff Abs_eq_iff)
-  apply(simp_all only: alpha_gen)
-  apply(simp_all only: eqvts[symmetric])
-  apply(simp_all only: eqvts eqvts_raw)
-  apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
-  apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
-  apply(simp_all only: de_Morgan_conj[symmetric])
-  done
-
-instance t and tyS :: fs
-  apply default
-  apply (simp_all add: supp_fv_t_tyS[symmetric] finite_fv_t_tyS)
-  done
-
-lemmas t_tyS_supp = t_tyS.fv[simplified supp_fv_t_tyS]
+lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
 
 lemma induct:
   assumes a1: "\<And>name b. P b (Var name)"