# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267781020 -3600
# Node ID b320da14e63cb9bcd765e1ca80c101e30674265b
# Parent  693df83172f09f4fdbd8a09e2e42457cb75a49c9
Fixed LF for one quantifier over 2 premises.

diff -r 693df83172f0 -r b320da14e63c Nominal/LFex.thy
--- a/Nominal/LFex.thy	Fri Mar 05 09:41:22 2010 +0100
+++ b/Nominal/LFex.thy	Fri Mar 05 10:23:40 2010 +0100
@@ -50,11 +50,9 @@
    (t3 \<approx>tr s3 \<longrightarrow> (p \<bullet> t3) \<approx>tr (p \<bullet> s3))"
 apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct)
 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
-apply (erule alpha_gen_compose_eqvt)
-apply (simp_all add: rfv_eqvt eqvts atom_eqvt)
-apply (erule alpha_gen_compose_eqvt)
-apply (simp_all add: rfv_eqvt eqvts atom_eqvt)
-apply (erule alpha_gen_compose_eqvt)
+apply (erule_tac [!] conjE)+
+apply (erule_tac [!] exi[of _ _ "p"])
+apply (erule_tac [!] alpha_gen_compose_eqvt)
 apply (simp_all add: rfv_eqvt eqvts atom_eqvt)
 done
 
@@ -160,6 +158,14 @@
 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))"
+  "(\<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 supp_eqs:
   "supp TYP = {}"
   "supp rkind = fv_kind rkind \<Longrightarrow> supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"
@@ -170,13 +176,15 @@
   "supp (VAR x) = {atom x}"
   "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 (no_asm) add: supp_def permute_set_eq atom_eqvt)
   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])
+  apply(simp_all only:ex_out)
+  apply(simp_all only: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts[symmetric])
+  apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric])
+  apply(simp_all add: supp_at_base[simplified supp_def] Un_commute)
   done
 
+
 lemma supp_fv:
   "supp t1 = fv_kind t1"
   "supp t2 = fv_ty t2"