# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265019373 -3600
# Node ID 3f227ed7e3e54b6abfe4416fe945231828262302
# Parent  b7d259ded92ee0fae8892f10dfd4db751b1d9aa7
More proofs in the LF example.

diff -r b7d259ded92e -r 3f227ed7e3e5 Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Mon Feb 01 09:56:32 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Mon Feb 01 11:16:13 2010 +0100
@@ -570,23 +570,82 @@
  "(p \<bullet> fv_trm t3) = fv_trm (p \<bullet> t3)"
 by(lifting rfv_eqvt)
 
+lemma supp_kind_ty_trm_easy:
+ "supp TYP = {}"
+ "supp (TCONST i) = {atom i}"
+ "supp (TAPP A M) = supp A \<union> supp M"
+ "supp (CONS i) = {atom i}"
+ "supp (VAR x) = {atom x}"
+ "supp (APP M N) = supp M \<union> supp N"
+apply (simp_all add: supp_def permute_ktt KIND_TY_TRM_INJECT)
+apply (simp_all only: supp_at_base[simplified supp_def])
+apply (simp_all add: Collect_imp_eq Collect_neg_eq)
+done
+
+lemma supp_bind:
+  "(supp (atom na, (ty, ki))) supports (KPI ty na ki)"
+  "(supp (atom na, (ty, ty2))) supports (TPI ty na ty2)"
+  "(supp (atom na, (ty, trm))) supports (LAM ty na trm)"
+apply(simp_all add: supports_def)
+apply(fold fresh_def)
+apply(simp_all add: fresh_Pair swap_fresh_fresh)
+apply(clarify)
+apply(subst swap_at_base_simps(3))
+apply(simp_all add: fresh_atom)
+apply(clarify)
+apply(subst swap_at_base_simps(3))
+apply(simp_all add: fresh_atom)
+apply(clarify)
+apply(subst swap_at_base_simps(3))
+apply(simp_all add: fresh_atom)
+done
+
+lemma KIND_TY_TRM_fs:
+  "finite (supp (x\<Colon>KIND))"
+  "finite (supp (y\<Colon>TY))"
+  "finite (supp (z\<Colon>TRM))"
+apply(induct x and y and z rule: KIND_TY_TRM_inducts)
+apply(simp_all add: supp_kind_ty_trm_easy)
+apply(rule supports_finite)
+apply(rule supp_bind(1))
+apply(simp add: supp_Pair supp_atom)
+apply(rule supports_finite)
+apply(rule supp_bind(2))
+apply(simp add: supp_Pair supp_atom)
+apply(rule supports_finite)
+apply(rule supp_bind(3))
+apply(simp add: supp_Pair supp_atom)
+done
+
+instance KIND and TY and TRM :: fs
+apply(default)
+apply(simp_all only: KIND_TY_TRM_fs)
+done
+
 lemma supp_fv:
  "fv_kind t1 = supp t1"
  "fv_ty t2 = supp t2"
  "fv_trm t3 = supp t3"
 apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts)
+apply (simp_all add: supp_kind_ty_trm_easy)
 apply (simp_all add: fv_kind_ty_trm)
-apply (simp_all add: supp_def)
-sorry
-
-lemma
-"(supp ((a \<rightleftharpoons> b) \<bullet> (K::KIND)) - {atom ((a \<rightleftharpoons> b) \<bullet> (x::name))} = supp K - {atom x} \<longrightarrow>
-(a \<rightleftharpoons> b) \<bullet> A = (A::TY) \<longrightarrow> (\<forall>pi\<Colon>perm. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> K = K \<longrightarrow> (supp K - {atom x}) \<sharp>* pi \<longrightarrow> pi \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> x)) =
-(supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)} = supp K - {atom x} \<and>
-(\<exists>pi\<Colon>perm. (supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)}) \<sharp>* pi \<and> pi \<bullet> (a \<rightleftharpoons> b) \<bullet> K = K) \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> A \<noteq> A)"
-apply (case_tac "(a \<rightleftharpoons> b) \<bullet> A = A")
-apply (case_tac "supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)} = supp K - {atom x}")
-apply simp_all
+apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abst {atom name} kind)")
+apply(simp add: supp_Abst Set.Un_commute)
+apply(simp (no_asm) add: supp_def)
+apply(simp add: KIND_TY_TRM_INJECT)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
+apply(simp add: abs_eq alpha_gen)
+apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
+apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric])
+apply (fold supp_def)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
+apply (rule refl)
+apply(subst Set.Un_commute)
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
+apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
+apply (rule refl)
+prefer 2
+apply(simp add: eqvts supp_eqvt atom_eqvt)
 sorry
 
 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abst {atom x} K)) \<union> supp A"
@@ -600,18 +659,6 @@
 apply (unfold supp_def)
 sorry
 
-lemma KIND_TY_TRM_fs:
-  "finite (supp (x\<Colon>KIND))"
-  "finite (supp (y\<Colon>TY))"
-  "finite (supp (z\<Colon>TRM))"
-apply(induct x and y and z rule: KIND_TY_TRM_inducts)
-sorry
-
-instance KIND and TY and TRM :: fs
-apply(default)
-apply(simp_all only: KIND_TY_TRM_fs)
-done
-
 lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
 apply(subst supp_kpi_pre)
 apply(subst supp_Abst)
@@ -628,18 +675,10 @@
  "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 -
-apply (simp add: supp_def)
+apply (simp_all only: supp_kind_ty_trm_easy)
 apply (simp add: supp_kpi)
-apply (simp add: supp_def KIND_TY_TRM_INJECT) apply (fold supp_def) apply (rule supp_at_base)
-apply (simp add: supp_def permute_ktt KIND_TY_TRM_INJECT Collect_imp_eq Collect_neg_eq)
-defer
-apply (simp add: supp_def KIND_TY_TRM_INJECT) apply (fold supp_def) apply (rule supp_at_base)
-apply (simp add: supp_def KIND_TY_TRM_INJECT) apply (fold supp_def) apply (rule supp_at_base)
-apply (simp add: supp_def permute_ktt KIND_TY_TRM_INJECT Collect_imp_eq Collect_neg_eq)
 sorry
 
-
 end