# HG changeset patch # User Cezary Kaliszyk # Date 1267797379 -3600 # Node ID 39e687a99549c8fa8aef1f17da5770ce1a269cba # Parent 8d2667ebe26c964e69daca2dac46f5afde91a8e3# Parent 998b1bde64e7bc730de9c2282ea0ed1c446e41ad merge diff -r 998b1bde64e7 -r 39e687a99549 Nominal/LFex.thy --- a/Nominal/LFex.thy Fri Mar 05 14:55:21 2010 +0100 +++ b/Nominal/LFex.thy Fri Mar 05 14:56:19 2010 +0100 @@ -50,11 +50,9 @@ (t3 \tr s3 \ (p \ t3) \tr (p \ 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: + "(\x. Z x \ Q) = (Q \ (\x. Z x))" + "(\x. Q \ Z x) = (Q \ (\x. Z x))" + "(\x. P x \ Q \ Z x) = (Q \ (\x. P x \ Z x))" + "(\x. Q \ P x \ Z x) = (Q \ (\x. P x \ Z x))" +apply (blast)+ +done + lemma supp_eqs: "supp TYP = {}" "supp rkind = fv_kind rkind \ supp (KPI rty name rkind) = supp rty \ supp (Abs {atom name} rkind)" @@ -170,13 +176,15 @@ "supp (VAR x) = {atom x}" "supp (APP M N) = supp M \ supp N" "supp rtrm = fv_trm rtrm \ supp (LAM rty name rtrm) = supp rty \ 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" diff -r 998b1bde64e7 -r 39e687a99549 Nominal/Term1.thy --- a/Nominal/Term1.thy Fri Mar 05 14:55:21 2010 +0100 +++ b/Nominal/Term1.thy Fri Mar 05 14:56:19 2010 +0100 @@ -138,14 +138,18 @@ apply(simp_all add: supp_atom) done -instance trm1 :: fs +instance trm1 and bp :: fs apply default -apply (rule rtrm1_bp_fs(1)) +apply (rule rtrm1_bp_fs)+ +done +lemma fv_eq_bv_pre: "fv_bp bp = bv1 bp" +apply(induct bp rule: trm1_bp_inducts(2)) +apply(simp_all) done -lemma fv_eq_bv: "fv_bp bp = bv1 bp" -apply(induct bp rule: trm1_bp_inducts(2)) -apply(simp_all) +lemma fv_eq_bv: "fv_bp = bv1" +apply(rule ext) +apply(rule fv_eq_bv_pre) done lemma helper2: "{b. \pi. pi \ (a \ b) \ bp \ bp} = {}" @@ -165,6 +169,35 @@ apply (rule alpha_bp_eq_eq) done +lemma ex_out: + "(\x. Z x \ Q) = (Q \ (\x. Z x))" + "(\x. Q \ Z x) = (Q \ (\x. Z x))" + "(\x. P x \ Q \ Z x) = (Q \ (\x. P x \ Z x))" + "(\x. Q \ P x \ Z x) = (Q \ (\x. P x \ Z x))" + "(\x. Q \ P x \ Z x \ W x) = (Q \ (\x. P x \ Z x \ W x))" +apply (blast)+ +done + +lemma "(Abs bs (x, x') = Abs cs (y, y')) = (\p. (bs, x) \gen op = supp p (cs, y) \ (bs, x') \gen op = supp p (cs, y'))" +thm Abs_eq_iff +apply (simp add: Abs_eq_iff) +apply (rule arg_cong[of _ _ "Ex"]) +apply (rule ext) +apply (simp only: alpha_gen) +apply (simp only: supp_Pair eqvts) +apply rule +apply (erule conjE)+ +oops + +lemma "(f (p \ bp), p \ bp) \gen op = f pi (f bp, bp) = False" +apply (simp add: alpha_gen fresh_star_def) +oops + +(* TODO: permute_ABS should be in eqvt? *) + +lemma Collect_neg_conj: "{x. \(P x \ Q x)} = {x. \(P x)} \ {x. \(Q x)}" +by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) + lemma supp_fv: "supp t = fv_trm1 t" "supp b = fv_bp b" @@ -173,7 +206,7 @@ apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) apply(simp only: supp_at_base[simplified supp_def]) apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) -apply(simp add: Collect_imp_eq Collect_neg_eq) +apply(simp add: Collect_imp_eq Collect_neg_eq Un_commute) apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)") apply(simp add: supp_Abs fv_trm1) apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1) @@ -181,21 +214,31 @@ apply(simp add: Abs_eq_iff) apply(simp add: alpha_gen.simps) apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) -apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \ supp (Abs (bv1 bp) rtrm12)") -apply(simp add: supp_Abs fv_trm1 fv_eq_bv) -apply(simp (no_asm) add: supp_def permute_trm1) -apply(simp add: alpha1_INJ alpha_bp_eq) -apply(simp add: Abs_eq_iff) -apply(simp add: alpha_gen) -apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) -apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2) +defer apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) apply(simp (no_asm) add: supp_def eqvts) apply(fold supp_def) apply(simp add: supp_at_base) apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq) apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric]) -done +apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (rtrm12)) \ supp(rtrm11)") +(*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (bp, rtrm12)) \ supp(rtrm11)")*) +apply(simp add: supp_Abs fv_trm1 supp_Pair Un_Diff Un_assoc fv_eq_bv) +apply(blast) (* Un_commute in a good place *) +apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1) +apply(simp only: alpha1_INJ permute_ABS permute_prod.simps Abs_eq_iff) +apply(simp only: ex_out) +apply(simp only: Un_commute) +apply(simp only: alpha_bp_eq fv_eq_bv) +apply(simp only: alpha_gen fv_eq_bv supp_Pair) +apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) +apply(simp only: ex_out) +apply(simp only: Collect_neg_conj finite_Un Diff_cancel) +apply(simp) +apply(simp add: Collect_imp_eq) +apply(simp add: Collect_neg_eq[symmetric] fresh_star_def) +apply(fold supp_def) +sorry lemma trm1_supp: "supp (Vr1 x) = {atom x}"