# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267018671 -3600
# Node ID 845bf16eee18a66480fac4928ad96dda192cc041
# Parent  18310dff4e3a9a23172a023041acce912856b17f
Regularize finite support proof for trm1

diff -r 18310dff4e3a -r 845bf16eee18 Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Wed Feb 24 14:09:34 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 14:37:51 2010 +0100
@@ -157,9 +157,12 @@
 
 end
 
-lemmas ALPHA_kind_ALPHA_ty_ALPHA_trm_inducts = alpha_rkind_alpha_rty_alpha_rtrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+(*
+Lifts, but slow and not needed?.
+lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+*)
 
-lemmas kind_ty_trm_INJECT = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+lemmas kind_ty_trm_inj = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted]
 
@@ -207,7 +210,7 @@
   "supp (APP M N) = supp M \<union> supp N"
   "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)"
   apply(simp_all (no_asm) add: supp_def)
-  apply(simp_all only: kind_ty_trm_INJECT Abs_eq_iff alpha_gen)
+  apply(simp_all only: kind_ty_trm_inj Abs_eq_iff alpha_gen)
   apply(simp_all only: insert_eqvt empty_eqvt atom_eqvt supp_eqvt[symmetric] fv_eqvt[symmetric])
   apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Set.Un_commute)
   apply(simp_all add: supp_at_base[simplified supp_def])
diff -r 18310dff4e3a -r 845bf16eee18 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 24 14:09:34 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 24 14:37:51 2010 +0100
@@ -173,44 +173,32 @@
 and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted]
 and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
-lemma lm1_supp_pre:
-  shows "(supp (atom x, t)) supports (Lm1 x t) "
-apply(simp add: supports_def)
-apply(fold fresh_def)
-apply(simp add: fresh_Pair swap_fresh_fresh)
-apply(clarify)
-apply(subst swap_at_base_simps(3))
+lemma supports:
+  "(supp (atom x)) supports (Vr1 x)"
+  "(supp t \<union> supp s) supports (Ap1 t s)"
+  "(supp (atom x) \<union> supp t) supports (Lm1 x t)"
+  "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)"
+  "{} supports BUnit"
+  "(supp (atom x)) supports (BVr x)"
+  "(supp a \<union> supp b) supports (BPr a b)"
+apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh)
+apply(rule_tac [!] allI)+
+apply(rule_tac [!] impI)
+apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})
 apply(simp_all add: fresh_atom)
 done
 
-lemma lt1_supp_pre:
-  shows "(supp (x, t, s)) supports (Lt1 t x s) "
-apply(simp add: supports_def)
-apply(fold fresh_def)
-apply(simp add: fresh_Pair swap_fresh_fresh)
-done
-
-lemma bp_supp: "finite (supp (bp :: bp))"
-  apply (induct bp)
-  apply(simp_all add: supp_def)
-  apply(simp add: supp_at_base supp_def[symmetric])
-  apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric] supp_def)
+lemma rtrm1_bp_fs:
+  "finite (supp (x :: trm1))"
+  "finite (supp (b :: bp))"
+  apply (induct x and b rule: trm1_bp_inducts)
+  apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})
+  apply(simp_all add: supp_atom)
   done
 
 instance trm1 :: fs
 apply default
-apply(induct_tac x rule: trm1_bp_inducts(1))
-apply(simp_all)
-apply(simp add: supp_def alpha1_INJ eqvts)
-apply(simp add: supp_def[symmetric] supp_at_base)
-apply(simp only: supp_def alpha1_INJ eqvts permute_trm1)
-apply(simp add: Collect_imp_eq Collect_neg_eq)
-apply(rule supports_finite)
-apply(rule lm1_supp_pre)
-apply(simp add: supp_Pair supp_atom)
-apply(rule supports_finite)
-apply(rule lt1_supp_pre)
-apply(simp add: supp_Pair supp_atom bp_supp)
+apply (rule rtrm1_bp_fs(1))
 done
 
 lemma fv_eq_bv: "fv_bp bp = bv1 bp"