# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268326147 -3600
# Node ID 866208388c1dac50d1f6a3802b6f0db412ef4ca3
# Parent  4029105011cab324cb4aec532735eb4c018a5e0e
Finite_support proof no longer needed in LF.

diff -r 4029105011ca -r 866208388c1d Nominal/LFex.thy
--- a/Nominal/LFex.thy	Thu Mar 11 17:47:29 2010 +0100
+++ b/Nominal/LFex.thy	Thu Mar 11 17:49:07 2010 +0100
@@ -5,8 +5,6 @@
 atom_decl name
 atom_decl ident
 
-ML {* restricted_nominal := 2 *}
-
 nominal_datatype kind =
     Type
   | KPi "ty" n::"name" k::"kind" bind n in k
@@ -20,35 +18,6 @@
   | App "trm" "trm"
   | Lam "ty" n::"name" t::"trm" bind n in t
 
-lemma supports:
-  "{} supports Type"
-  "(supp (atom i)) supports (TConst i)"
-  "(supp A \<union> supp M) supports (TApp A M)"
-  "(supp (atom i)) supports (Const i)"
-  "(supp (atom x)) supports (Var x)"
-  "(supp M \<union> supp N) supports (App M N)"
-  "(supp ty \<union> supp (atom na) \<union> supp ki) supports (KPi ty na ki)"
-  "(supp ty \<union> supp (atom na) \<union> supp ty2) supports (TPi ty na ty2)"
-  "(supp ty \<union> supp (atom na) \<union> supp trm) supports (Lam ty na trm)"
-apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh kind_ty_trm_perm)
-apply(rule_tac [!] allI)+
-apply(rule_tac [!] impI)
-apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})
-apply(simp_all add: fresh_atom)
-done
-
-lemma kind_ty_trm_fs:
-  "finite (supp (x\<Colon>kind)) \<and> finite (supp (y\<Colon>ty)) \<and> finite (supp (z\<Colon>trm))"
-apply(induct rule: kind_ty_trm_induct)
-apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})
-apply(simp_all add: supp_atom)
-done
-
-instance kind and ty and trm :: fs
-apply(default)
-apply(simp_all only: kind_ty_trm_fs)
-done
-
 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))"
diff -r 4029105011ca -r 866208388c1d Nominal/Term1.thy
--- a/Nominal/Term1.thy	Thu Mar 11 17:47:29 2010 +0100
+++ b/Nominal/Term1.thy	Thu Mar 11 17:49:07 2010 +0100
@@ -140,13 +140,9 @@
 apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *})
 done
 
-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
+prove rtrm1_bp_fs: {* snd (mk_fs [@{typ trm1}, @{typ bp}]) *}
+apply (tactic {* fs_tac @{thm trm1_bp_induct} @{thms supports} 1 *})
+done
 
 instance trm1 and bp :: fs
 apply default