diff -r 92011cc923f5 -r 9be4ab2acc13 src/HOL/Nominal/Examples/Class3.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nominal/Examples/Class3.thy Thu Apr 22 22:01:06 2010 +0200 @@ -0,0 +1,6506 @@ +theory Class3 +imports Class2 +begin + +text {* 3rd Main Lemma *} + +lemma Cut_a_redu_elim: + assumes a: "Cut .M (x).N \\<^isub>a R" + shows "(\M'. R = Cut .M' (x).N \ M \\<^isub>a M') \ + (\N'. R = Cut .M (x).N' \ N \\<^isub>a N') \ + (Cut .M (x).N \\<^isub>c R) \ + (Cut .M (x).N \\<^isub>l R)" +using a +apply(erule_tac a_redu.cases) +apply(simp_all) +apply(simp_all add: trm.inject) +apply(rule disjI1) +apply(auto simp add: alpha)[1] +apply(rule_tac x="[(a,aa)]\M'" in exI) +apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu) +apply(rule_tac x="[(a,aa)]\M'" in exI) +apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu) +apply(rule disjI2) +apply(rule disjI1) +apply(auto simp add: alpha)[1] +apply(rule_tac x="[(x,xa)]\N'" in exI) +apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu) +apply(rule_tac x="[(x,xa)]\N'" in exI) +apply(perm_simp add: fresh_left calc_atm a_redu.eqvt fresh_a_redu) +done + +lemma Cut_c_redu_elim: + assumes a: "Cut .M (x).N \\<^isub>c R" + shows "(R = M{a:=(x).N} \ \fic M a) \ + (R = N{x:=.M} \ \fin N x)" +using a +apply(erule_tac c_redu.cases) +apply(simp_all) +apply(simp_all add: trm.inject) +apply(rule disjI1) +apply(auto simp add: alpha)[1] +apply(simp add: subst_rename fresh_atm) +apply(simp add: subst_rename fresh_atm) +apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2)) +apply(perm_simp) +apply(simp add: subst_rename fresh_atm fresh_prod) +apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2)) +apply(perm_simp) +apply(rule disjI2) +apply(auto simp add: alpha)[1] +apply(simp add: subst_rename fresh_atm) +apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1)) +apply(perm_simp) +apply(simp add: subst_rename fresh_atm fresh_prod) +apply(simp add: subst_rename fresh_atm fresh_prod) +apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1)) +apply(perm_simp) +done + +lemma not_fic_crename_aux: + assumes a: "fic M c" "c\(a,b)" + shows "fic (M[a\c>b]) c" +using a +apply(nominal_induct M avoiding: c a b rule: trm.strong_induct) +apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh) +done + +lemma not_fic_crename: + assumes a: "\(fic (M[a\c>b]) c)" "c\(a,b)" + shows "\(fic M c)" +using a +apply(auto dest: not_fic_crename_aux) +done + +lemma not_fin_crename_aux: + assumes a: "fin M y" + shows "fin (M[a\c>b]) y" +using a +apply(nominal_induct M avoiding: a b rule: trm.strong_induct) +apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh) +done + +lemma not_fin_crename: + assumes a: "\(fin (M[a\c>b]) y)" + shows "\(fin M y)" +using a +apply(auto dest: not_fin_crename_aux) +done + +lemma crename_fresh_interesting1: + fixes c::"coname" + assumes a: "c\(M[a\c>b])" "c\(a,b)" + shows "c\M" +using a +apply(nominal_induct M avoiding: c a b rule: trm.strong_induct) +apply(auto split: if_splits simp add: abs_fresh) +done + +lemma crename_fresh_interesting2: + fixes x::"name" + assumes a: "x\(M[a\c>b])" + shows "x\M" +using a +apply(nominal_induct M avoiding: x a b rule: trm.strong_induct) +apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp fresh_atm) +done + + +lemma fic_crename: + assumes a: "fic (M[a\c>b]) c" "c\(a,b)" + shows "fic M c" +using a +apply(nominal_induct M avoiding: c a b rule: trm.strong_induct) +apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh + split: if_splits) +apply(auto dest: crename_fresh_interesting1 simp add: fresh_prod fresh_atm) +done + +lemma fin_crename: + assumes a: "fin (M[a\c>b]) x" + shows "fin M x" +using a +apply(nominal_induct M avoiding: x a b rule: trm.strong_induct) +apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh + split: if_splits) +apply(auto dest: crename_fresh_interesting2 simp add: fresh_prod fresh_atm) +done + +lemma crename_Cut: + assumes a: "R[a\c>b] = Cut .M (x).N" "c\(a,b,N,R)" "x\(M,R)" + shows "\M' N'. R = Cut .M' (x).N' \ M'[a\c>b] = M \ N'[a\c>b] = N \ c\N' \ x\M'" +using a +apply(nominal_induct R avoiding: a b c x M N rule: trm.strong_induct) +apply(auto split: if_splits) +apply(simp add: trm.inject) +apply(auto simp add: alpha) +apply(rule_tac x="[(name,x)]\trm2" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +apply(rule_tac x="[(coname,c)]\trm1" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(auto simp add: fresh_atm)[1] +apply(rule_tac x="[(coname,c)]\trm1" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(rule_tac x="[(name,x)]\trm2" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(auto simp add: fresh_atm)[1] +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma crename_NotR: + assumes a: "R[a\c>b] = NotR (x).N c" "x\R" "c\(a,b)" + shows "\N'. (R = NotR (x).N' c) \ N'[a\c>b] = N" +using a +apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +apply(rule_tac x="[(name,x)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma crename_NotR': + assumes a: "R[a\c>b] = NotR (x).N c" "x\R" "c\a" + shows "(\N'. (R = NotR (x).N' c) \ N'[a\c>b] = N) \ (\N'. (R = NotR (x).N' a) \ b=c \ N'[a\c>b] = N)" +using a +apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject) +apply(rule_tac x="[(name,x)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +apply(rule_tac x="[(name,x)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma crename_NotR_aux: + assumes a: "R[a\c>b] = NotR (x).N c" + shows "(a=c \ a=b) \ (a\c)" +using a +apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +done + +lemma crename_NotL: + assumes a: "R[a\c>b] = NotL .N y" "c\(R,a,b)" + shows "\N'. (R = NotL .N' y) \ N'[a\c>b] = N" +using a +apply(nominal_induct R avoiding: a b c y N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +apply(rule_tac x="[(coname,c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma crename_AndL1: + assumes a: "R[a\c>b] = AndL1 (x).N y" "x\R" + shows "\N'. (R = AndL1 (x).N' y) \ N'[a\c>b] = N" +using a +apply(nominal_induct R avoiding: a b x y N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +apply(rule_tac x="[(name1,x)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma crename_AndL2: + assumes a: "R[a\c>b] = AndL2 (x).N y" "x\R" + shows "\N'. (R = AndL2 (x).N' y) \ N'[a\c>b] = N" +using a +apply(nominal_induct R avoiding: a b x y N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +apply(rule_tac x="[(name1,x)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma crename_AndR_aux: + assumes a: "R[a\c>b] = AndR .M .N e" + shows "(a=e \ a=b) \ (a\e)" +using a +apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +done + +lemma crename_AndR: + assumes a: "R[a\c>b] = AndR .M .N e" "c\(a,b,d,e,N,R)" "d\(a,b,c,e,M,R)" "e\(a,b)" + shows "\M' N'. R = AndR .M' .N' e \ M'[a\c>b] = M \ N'[a\c>b] = N \ c\N' \ d\M'" +using a +apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct) +apply(auto split: if_splits simp add: trm.inject alpha) +apply(simp add: fresh_atm fresh_prod) +apply(rule_tac x="[(coname2,d)]\trm2" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(coname1,c)]\trm1" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(coname1,c)]\trm1" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(coname2,d)]\trm2" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(coname1,c)]\trm1" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(coname1,c)]\trm1" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(coname2,d)]\trm2" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(drule_tac s="trm2[a\c>b]" in sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma crename_AndR': + assumes a: "R[a\c>b] = AndR .M .N e" "c\(a,b,d,e,N,R)" "d\(a,b,c,e,M,R)" "e\a" + shows "(\M' N'. R = AndR .M' .N' e \ M'[a\c>b] = M \ N'[a\c>b] = N \ c\N' \ d\M') \ + (\M' N'. R = AndR .M' .N' a \ b=e \ M'[a\c>b] = M \ N'[a\c>b] = N \ c\N' \ d\M')" +using a +apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct) +apply(auto split: if_splits simp add: trm.inject alpha)[1] +apply(auto split: if_splits simp add: trm.inject alpha)[1] +apply(auto split: if_splits simp add: trm.inject alpha)[1] +apply(auto split: if_splits simp add: trm.inject alpha)[1] +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm trm.inject alpha)[1] +apply(case_tac "coname3=a") +apply(simp) +apply(rule_tac x="[(coname1,c)]\trm1" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(coname2,d)]\trm2" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm trm.inject alpha split: if_splits)[1] +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(drule_tac s="trm2[a\c>e]" in sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(simp) +apply(rule_tac x="[(coname1,c)]\trm1" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(rule_tac x="[(coname2,d)]\trm2" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm trm.inject alpha split: if_splits)[1] +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(drule_tac s="trm2[a\c>b]" in sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +done + +lemma crename_OrR1_aux: + assumes a: "R[a\c>b] = OrR1 .M e" + shows "(a=e \ a=b) \ (a\e)" +using a +apply(nominal_induct R avoiding: a b c e M rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +done + +lemma crename_OrR1: + assumes a: "R[a\c>b] = OrR1 .N d" "c\(R,a,b)" "d\(a,b)" + shows "\N'. (R = OrR1 .N' d) \ N'[a\c>b] = N" +using a +apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +apply(rule_tac x="[(coname1,c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma crename_OrR1': + assumes a: "R[a\c>b] = OrR1 .N d" "c\(R,a,b)" "d\a" + shows "(\N'. (R = OrR1 .N' d) \ N'[a\c>b] = N) \ + (\N'. (R = OrR1 .N' a) \ b=d \ N'[a\c>b] = N)" +using a +apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +apply(rule_tac x="[(coname1,c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(rule_tac x="[(coname1,c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma crename_OrR2_aux: + assumes a: "R[a\c>b] = OrR2 .M e" + shows "(a=e \ a=b) \ (a\e)" +using a +apply(nominal_induct R avoiding: a b c e M rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +done + +lemma crename_OrR2: + assumes a: "R[a\c>b] = OrR2 .N d" "c\(R,a,b)" "d\(a,b)" + shows "\N'. (R = OrR2 .N' d) \ N'[a\c>b] = N" +using a +apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +apply(rule_tac x="[(coname1,c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma crename_OrR2': + assumes a: "R[a\c>b] = OrR2 .N d" "c\(R,a,b)" "d\a" + shows "(\N'. (R = OrR2 .N' d) \ N'[a\c>b] = N) \ + (\N'. (R = OrR2 .N' a) \ b=d \ N'[a\c>b] = N)" +using a +apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +apply(rule_tac x="[(coname1,c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(rule_tac x="[(coname1,c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma crename_OrL: + assumes a: "R[a\c>b] = OrL (x).M (y).N z" "x\(y,z,N,R)" "y\(x,z,M,R)" + shows "\M' N'. R = OrL (x).M' (y).N' z \ M'[a\c>b] = M \ N'[a\c>b] = N \ x\N' \ y\M'" +using a +apply(nominal_induct R avoiding: a b x y z M N rule: trm.strong_induct) +apply(auto split: if_splits simp add: trm.inject alpha) +apply(rule_tac x="[(name2,y)]\trm2" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(name1,x)]\trm1" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(name1,x)]\trm1" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(name2,y)]\trm2" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +apply(drule_tac s="trm2[a\c>b]" in sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma crename_ImpL: + assumes a: "R[a\c>b] = ImpL .M (y).N z" "c\(a,b,N,R)" "y\(z,M,R)" + shows "\M' N'. R = ImpL .M' (y).N' z \ M'[a\c>b] = M \ N'[a\c>b] = N \ c\N' \ y\M'" +using a +apply(nominal_induct R avoiding: a b c y z M N rule: trm.strong_induct) +apply(auto split: if_splits simp add: trm.inject alpha) +apply(rule_tac x="[(name1,y)]\trm2" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(coname,c)]\trm1" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(coname,c)]\trm1" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(name1,y)]\trm2" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(drule_tac s="trm2[a\c>b]" in sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma crename_ImpR_aux: + assumes a: "R[a\c>b] = ImpR (x)..M e" + shows "(a=e \ a=b) \ (a\e)" +using a +apply(nominal_induct R avoiding: x a b c e M rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +done + +lemma crename_ImpR: + assumes a: "R[a\c>b] = ImpR (x)..N d" "c\(R,a,b)" "d\(a,b)" "x\R" + shows "\N'. (R = ImpR (x)..N' d) \ N'[a\c>b] = N" +using a +apply(nominal_induct R avoiding: a b x c d N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_perm alpha abs_fresh trm.inject) +apply(rule_tac x="[(name,x)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(rule_tac x="[(name,x)]\[(coname1, c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_supp fin_supp abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma crename_ImpR': + assumes a: "R[a\c>b] = ImpR (x)..N d" "c\(R,a,b)" "x\R" "d\a" + shows "(\N'. (R = ImpR (x)..N' d) \ N'[a\c>b] = N) \ + (\N'. (R = ImpR (x)..N' a) \ b=d \ N'[a\c>b] = N)" +using a +apply(nominal_induct R avoiding: x a b c d N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject abs_perm calc_atm) +apply(rule_tac x="[(name,x)]\[(coname1,c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod abs_supp fin_supp) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +apply(rule_tac x="[(name,x)]\[(coname1,c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod abs_supp fin_supp) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma crename_ax2: + assumes a: "N[a\c>b] = Ax x c" + shows "\d. N = Ax x d" +using a +apply(nominal_induct N avoiding: a b rule: trm.strong_induct) +apply(auto split: if_splits) +apply(simp add: trm.inject) +done + +lemma crename_interesting1: + assumes a: "distinct [a,b,c]" + shows "M[a\c>c][c\c>b] = M[c\c>b][a\c>b]" +using a +apply(nominal_induct M avoiding: a c b rule: trm.strong_induct) +apply(auto simp add: rename_fresh simp add: trm.inject alpha) +apply(blast) +apply(rotate_tac 12) +apply(drule_tac x="a" in meta_spec) +apply(rotate_tac 15) +apply(drule_tac x="c" in meta_spec) +apply(rotate_tac 15) +apply(drule_tac x="b" in meta_spec) +apply(blast) +apply(blast) +apply(blast) +done + +lemma crename_interesting2: + assumes a: "a\c" "a\d" "a\b" "c\d" "b\c" + shows "M[a\c>b][c\c>d] = M[c\c>d][a\c>b]" +using a +apply(nominal_induct M avoiding: a c b d rule: trm.strong_induct) +apply(auto simp add: rename_fresh simp add: trm.inject alpha) +done + +lemma crename_interesting3: + shows "M[a\c>c][x\n>y] = M[x\n>y][a\c>c]" +apply(nominal_induct M avoiding: a c x y rule: trm.strong_induct) +apply(auto simp add: rename_fresh simp add: trm.inject alpha) +done + +lemma crename_credu: + assumes a: "(M[a\c>b]) \\<^isub>c M'" + shows "\M0. M0[a\c>b]=M' \ M \\<^isub>c M0" +using a +apply(nominal_induct M\"M[a\c>b]" M' avoiding: M a b rule: c_redu.strong_induct) +apply(drule sym) +apply(drule crename_Cut) +apply(simp) +apply(simp) +apply(auto) +apply(rule_tac x="M'{a:=(x).N'}" in exI) +apply(rule conjI) +apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod) +apply(rule c_redu.intros) +apply(auto dest: not_fic_crename)[1] +apply(simp add: abs_fresh) +apply(simp add: abs_fresh) +apply(drule sym) +apply(drule crename_Cut) +apply(simp) +apply(simp) +apply(auto) +apply(rule_tac x="N'{x:=.M'}" in exI) +apply(rule conjI) +apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod) +apply(rule c_redu.intros) +apply(auto dest: not_fin_crename)[1] +apply(simp add: abs_fresh) +apply(simp add: abs_fresh) +done + +lemma crename_lredu: + assumes a: "(M[a\c>b]) \\<^isub>l M'" + shows "\M0. M0[a\c>b]=M' \ M \\<^isub>l M0" +using a +apply(nominal_induct M\"M[a\c>b]" M' avoiding: M a b rule: l_redu.strong_induct) +apply(drule sym) +apply(drule crename_Cut) +apply(simp add: fresh_prod fresh_atm) +apply(simp) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(case_tac "aa=ba") +apply(simp add: crename_id) +apply(rule l_redu.intros) +apply(simp) +apply(simp add: fresh_atm) +apply(assumption) +apply(frule crename_ax2) +apply(auto)[1] +apply(case_tac "d=aa") +apply(simp add: trm.inject) +apply(rule_tac x="M'[a\c>aa]" in exI) +apply(rule conjI) +apply(rule crename_interesting1) +apply(simp) +apply(rule l_redu.intros) +apply(simp) +apply(simp add: fresh_atm) +apply(auto dest: fic_crename simp add: fresh_prod fresh_atm)[1] +apply(simp add: trm.inject) +apply(rule_tac x="M'[a\c>b]" in exI) +apply(rule conjI) +apply(rule crename_interesting2) +apply(simp) +apply(simp) +apply(simp) +apply(simp) +apply(simp) +apply(rule l_redu.intros) +apply(simp) +apply(simp add: fresh_atm) +apply(auto dest: fic_crename simp add: fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule crename_Cut) +apply(simp add: fresh_prod fresh_atm) +apply(simp add: fresh_prod fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(case_tac "aa=b") +apply(simp add: crename_id) +apply(rule l_redu.intros) +apply(simp) +apply(simp add: fresh_atm) +apply(assumption) +apply(frule crename_ax2) +apply(auto)[1] +apply(case_tac "d=aa") +apply(simp add: trm.inject) +apply(simp add: trm.inject) +apply(rule_tac x="N'[x\n>y]" in exI) +apply(rule conjI) +apply(rule sym) +apply(rule crename_interesting3) +apply(rule l_redu.intros) +apply(simp) +apply(simp add: fresh_atm) +apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1] +(* LNot *) +apply(drule sym) +apply(drule crename_Cut) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(drule crename_NotR) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(drule crename_NotL) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(rule_tac x="Cut .N'b (x).N'a" in exI) +apply(simp add: fresh_atm)[1] +apply(rule l_redu.intros) +apply(auto simp add: fresh_prod intro: crename_fresh_interesting2)[1] +apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting2)[1] +apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1] +apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1] +apply(simp add: fresh_atm) +apply(simp add: fresh_atm) +(* LAnd1 *) +apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule crename_Cut) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto)[1] +apply(drule crename_AndR) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(drule crename_AndL1) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(rule_tac x="Cut .M'a (x).N'a" in exI) +apply(simp add: fresh_atm)[1] +apply(rule l_redu.intros) +apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1] +apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1] +apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1] +apply(simp add: fresh_atm) +apply(simp add: fresh_atm) +(* LAnd2 *) +apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule crename_Cut) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto)[1] +apply(drule crename_AndR) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(drule crename_AndL2) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(rule_tac x="Cut .N'b (x).N'a" in exI) +apply(simp add: fresh_atm)[1] +apply(rule l_redu.intros) +apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1] +apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1] +apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1] +apply(simp add: fresh_atm) +apply(simp add: fresh_atm) +(* LOr1 *) +apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule crename_Cut) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto)[1] +apply(drule crename_OrL) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(drule crename_OrR1) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(auto) +apply(rule_tac x="Cut .N' (x1).M'a" in exI) +apply(rule conjI) +apply(simp add: abs_fresh fresh_atm)[1] +apply(rule l_redu.intros) +apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1] +apply(simp add: fresh_atm) +apply(simp add: fresh_atm) +(* LOr2 *) +apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule crename_Cut) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto)[1] +apply(drule crename_OrL) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(drule crename_OrR2) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(auto) +apply(rule_tac x="Cut .N' (x2).N'a" in exI) +apply(rule conjI) +apply(simp add: abs_fresh fresh_atm)[1] +apply(rule l_redu.intros) +apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1] +apply(simp add: fresh_atm) +apply(simp add: fresh_atm) +(* ImpL *) +apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule crename_Cut) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm abs_supp fin_supp) +apply(auto)[1] +apply(drule crename_ImpL) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(drule crename_ImpR) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(rule_tac x="Cut .(Cut .M'a (x).N') (y).N'a" in exI) +apply(rule conjI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(rule l_redu.intros) +apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp fresh_prod intro: crename_fresh_interesting2)[1] +apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1] +apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting2)[1] +apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1] +apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1] +apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1] +done + +lemma crename_aredu: + assumes a: "(M[a\c>b]) \\<^isub>a M'" "a\b" + shows "\M0. M0[a\c>b]=M' \ M \\<^isub>a M0" +using a +apply(nominal_induct "M[a\c>b]" M' avoiding: M a b rule: a_redu.strong_induct) +apply(drule crename_lredu) +apply(blast) +apply(drule crename_credu) +apply(blast) +(* Cut *) +apply(drule sym) +apply(drule crename_Cut) +apply(simp) +apply(simp) +apply(auto)[1] +apply(drule_tac x="M'a" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(auto)[1] +apply(rule_tac x="Cut .M0 (x).N'" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(rule conjI) +apply(rule trans) +apply(rule crename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(drule crename_fresh_interesting2) +apply(simp add: fresh_a_redu) +apply(simp) +apply(auto)[1] +apply(drule sym) +apply(drule crename_Cut) +apply(simp) +apply(simp) +apply(auto)[1] +apply(drule_tac x="N'a" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(auto)[1] +apply(rule_tac x="Cut .M' (x).M0" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(rule conjI) +apply(rule trans) +apply(rule crename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1] +apply(drule crename_fresh_interesting1) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_a_redu) +apply(simp) +apply(simp) +apply(auto)[1] +(* NotL *) +apply(drule sym) +apply(drule crename_NotL) +apply(simp) +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(auto)[1] +apply(rule_tac x="NotL .M0 x" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +(* NotR *) +apply(drule sym) +apply(frule crename_NotR_aux) +apply(erule disjE) +apply(auto)[1] +apply(drule crename_NotR') +apply(simp) +apply(simp add: fresh_atm) +apply(erule disjE) +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(auto)[1] +apply(rule_tac x="NotR (x).M0 a" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="a" in meta_spec) +apply(auto)[1] +apply(rule_tac x="NotR (x).M0 aa" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +(* AndR *) +apply(drule sym) +apply(frule crename_AndR_aux) +apply(erule disjE) +apply(auto)[1] +apply(drule crename_AndR') +apply(simp add: fresh_prod fresh_atm) +apply(simp add: fresh_atm) +apply(simp add: fresh_atm) +apply(erule disjE) +apply(auto)[1] +apply(drule_tac x="M'a" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="ba" in meta_spec) +apply(auto)[1] +apply(rule_tac x="AndR .M0 .N' c" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule crename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(drule_tac x="M'a" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="c" in meta_spec) +apply(auto)[1] +apply(rule_tac x="AndR .M0 .N' aa" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule crename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(drule sym) +apply(frule crename_AndR_aux) +apply(erule disjE) +apply(auto)[1] +apply(drule crename_AndR') +apply(simp add: fresh_prod fresh_atm) +apply(simp add: fresh_atm) +apply(simp add: fresh_atm) +apply(erule disjE) +apply(auto)[1] +apply(drule_tac x="N'a" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="ba" in meta_spec) +apply(auto)[1] +apply(rule_tac x="AndR .M' .M0 c" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule crename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(drule_tac x="N'a" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="c" in meta_spec) +apply(auto)[1] +apply(rule_tac x="AndR .M' .M0 aa" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule crename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp) +(* AndL1 *) +apply(drule sym) +apply(drule crename_AndL1) +apply(simp) +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(auto)[1] +apply(rule_tac x="AndL1 (x).M0 y" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +(* AndL2 *) +apply(drule sym) +apply(drule crename_AndL2) +apply(simp) +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(auto)[1] +apply(rule_tac x="AndL2 (x).M0 y" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +(* OrL *) +apply(drule sym) +apply(drule crename_OrL) +apply(simp) +apply(auto simp add: fresh_atm fresh_prod)[1] +apply(auto simp add: fresh_atm fresh_prod)[1] +apply(auto)[1] +apply(drule_tac x="M'a" in meta_spec) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(auto)[1] +apply(rule_tac x="OrL (x).M0 (y).N' z" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule crename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp) +apply(drule sym) +apply(drule crename_OrL) +apply(simp) +apply(auto simp add: fresh_atm fresh_prod)[1] +apply(auto simp add: fresh_atm fresh_prod)[1] +apply(auto)[1] +apply(drule_tac x="N'a" in meta_spec) +apply(drule_tac x="a" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(auto)[1] +apply(rule_tac x="OrL (x).M' (y).M0 z" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule crename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp) +apply(simp) +(* OrR1 *) +apply(drule sym) +apply(frule crename_OrR1_aux) +apply(erule disjE) +apply(auto)[1] +apply(drule crename_OrR1') +apply(simp) +apply(simp add: fresh_atm) +apply(erule disjE) +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="ba" in meta_spec) +apply(auto)[1] +apply(rule_tac x="OrR1 .M0 b" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(auto)[1] +apply(rule_tac x="OrR1 .M0 aa" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +(* OrR2 *) +apply(drule sym) +apply(frule crename_OrR2_aux) +apply(erule disjE) +apply(auto)[1] +apply(drule crename_OrR2') +apply(simp) +apply(simp add: fresh_atm) +apply(erule disjE) +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="ba" in meta_spec) +apply(auto)[1] +apply(rule_tac x="OrR2 .M0 b" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(auto)[1] +apply(rule_tac x="OrR2 .M0 aa" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +(* ImpL *) +apply(drule sym) +apply(drule crename_ImpL) +apply(simp) +apply(simp) +apply(auto)[1] +apply(drule_tac x="M'a" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(auto)[1] +apply(rule_tac x="ImpL .M0 (x).N' y" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule crename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(drule sym) +apply(drule crename_ImpL) +apply(simp) +apply(simp) +apply(auto)[1] +apply(drule_tac x="N'a" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(auto)[1] +apply(rule_tac x="ImpL .M' (x).M0 y" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule crename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp) +(* ImpR *) +apply(drule sym) +apply(frule crename_ImpR_aux) +apply(erule disjE) +apply(auto)[1] +apply(drule crename_ImpR') +apply(simp) +apply(simp add: fresh_atm) +apply(simp add: fresh_atm) +apply(erule disjE) +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="ba" in meta_spec) +apply(auto)[1] +apply(rule_tac x="ImpR (x)..M0 b" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="aa" in meta_spec) +apply(drule_tac x="b" in meta_spec) +apply(auto)[1] +apply(rule_tac x="ImpR (x)..M0 aa" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +done + +lemma SNa_preserved_renaming1: + assumes a: "SNa M" + shows "SNa (M[a\c>b])" +using a +apply(induct rule: SNa_induct) +apply(case_tac "a=b") +apply(simp add: crename_id) +apply(rule SNaI) +apply(drule crename_aredu) +apply(blast)+ +done + +lemma nrename_interesting1: + assumes a: "distinct [x,y,z]" + shows "M[x\n>z][z\n>y] = M[z\n>y][x\n>y]" +using a +apply(nominal_induct M avoiding: x y z rule: trm.strong_induct) +apply(auto simp add: rename_fresh simp add: trm.inject alpha) +apply(blast) +apply(blast) +apply(rotate_tac 12) +apply(drule_tac x="x" in meta_spec) +apply(rotate_tac 15) +apply(drule_tac x="y" in meta_spec) +apply(rotate_tac 15) +apply(drule_tac x="z" in meta_spec) +apply(blast) +apply(rotate_tac 11) +apply(drule_tac x="x" in meta_spec) +apply(rotate_tac 14) +apply(drule_tac x="y" in meta_spec) +apply(rotate_tac 14) +apply(drule_tac x="z" in meta_spec) +apply(blast) +done + +lemma nrename_interesting2: + assumes a: "x\z" "x\u" "x\y" "z\u" "y\z" + shows "M[x\n>y][z\n>u] = M[z\n>u][x\n>y]" +using a +apply(nominal_induct M avoiding: x y z u rule: trm.strong_induct) +apply(auto simp add: rename_fresh simp add: trm.inject alpha) +done + +lemma not_fic_nrename_aux: + assumes a: "fic M c" + shows "fic (M[x\n>y]) c" +using a +apply(nominal_induct M avoiding: c x y rule: trm.strong_induct) +apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh) +done + +lemma not_fic_nrename: + assumes a: "\(fic (M[x\n>y]) c)" + shows "\(fic M c)" +using a +apply(auto dest: not_fic_nrename_aux) +done + +lemma fin_nrename: + assumes a: "fin M z" "z\(x,y)" + shows "fin (M[x\n>y]) z" +using a +apply(nominal_induct M avoiding: x y z rule: trm.strong_induct) +apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh + split: if_splits) +done + +lemma nrename_fresh_interesting1: + fixes z::"name" + assumes a: "z\(M[x\n>y])" "z\(x,y)" + shows "z\M" +using a +apply(nominal_induct M avoiding: x y z rule: trm.strong_induct) +apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp) +done + +lemma nrename_fresh_interesting2: + fixes c::"coname" + assumes a: "c\(M[x\n>y])" + shows "c\M" +using a +apply(nominal_induct M avoiding: x y c rule: trm.strong_induct) +apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp fresh_atm) +done + +lemma fin_nrename2: + assumes a: "fin (M[x\n>y]) z" "z\(x,y)" + shows "fin M z" +using a +apply(nominal_induct M avoiding: x y z rule: trm.strong_induct) +apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh + split: if_splits) +apply(auto dest: nrename_fresh_interesting1 simp add: fresh_atm fresh_prod) +done + +lemma nrename_Cut: + assumes a: "R[x\n>y] = Cut .M (z).N" "c\(N,R)" "z\(x,y,M,R)" + shows "\M' N'. R = Cut .M' (z).N' \ M'[x\n>y] = M \ N'[x\n>y] = N \ c\N' \ z\M'" +using a +apply(nominal_induct R avoiding: c y x z M N rule: trm.strong_induct) +apply(auto split: if_splits) +apply(simp add: trm.inject) +apply(auto simp add: alpha fresh_atm) +apply(rule_tac x="[(coname,c)]\trm1" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(rule_tac x="[(name,z)]\trm2" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(rule conjI) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(auto simp add: fresh_atm)[1] +apply(drule sym) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma nrename_NotR: + assumes a: "R[x\n>y] = NotR (z).N c" "z\(R,x,y)" + shows "\N'. (R = NotR (z).N' c) \ N'[x\n>y] = N" +using a +apply(nominal_induct R avoiding: x y c z N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +apply(rule_tac x="[(name,z)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma nrename_NotL: + assumes a: "R[x\n>y] = NotL .N z" "c\R" "z\(x,y)" + shows "\N'. (R = NotL .N' z) \ N'[x\n>y] = N" +using a +apply(nominal_induct R avoiding: x y c z N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +apply(rule_tac x="[(coname,c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma nrename_NotL': + assumes a: "R[x\n>y] = NotL .N u" "c\R" "x\y" + shows "(\N'. (R = NotL .N' u) \ N'[x\n>y] = N) \ (\N'. (R = NotL .N' x) \ y=u \ N'[x\n>y] = N)" +using a +apply(nominal_induct R avoiding: y u c x N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject) +apply(rule_tac x="[(coname,c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(rule_tac x="[(coname,c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma nrename_NotL_aux: + assumes a: "R[x\n>y] = NotL .N u" + shows "(x=u \ x=y) \ (x\u)" +using a +apply(nominal_induct R avoiding: y u c x N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +done + +lemma nrename_AndL1: + assumes a: "R[x\n>y] = AndL1 (z).N u" "z\(R,x,y)" "u\(x,y)" + shows "\N'. (R = AndL1 (z).N' u) \ N'[x\n>y] = N" +using a +apply(nominal_induct R avoiding: z u x y N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +apply(rule_tac x="[(name1,z)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma nrename_AndL1': + assumes a: "R[x\n>y] = AndL1 (v).N u" "v\(R,u,x,y)" "x\y" + shows "(\N'. (R = AndL1 (v).N' u) \ N'[x\n>y] = N) \ (\N'. (R = AndL1 (v).N' x) \ y=u \ N'[x\n>y] = N)" +using a +apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject) +apply(rule_tac x="[(name1,v)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +apply(rule_tac x="[(name1,v)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma nrename_AndL1_aux: + assumes a: "R[x\n>y] = AndL1 (v).N u" + shows "(x=u \ x=y) \ (x\u)" +using a +apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +done + +lemma nrename_AndL2: + assumes a: "R[x\n>y] = AndL2 (z).N u" "z\(R,x,y)" "u\(x,y)" + shows "\N'. (R = AndL2 (z).N' u) \ N'[x\n>y] = N" +using a +apply(nominal_induct R avoiding: z u x y N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +apply(rule_tac x="[(name1,z)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma nrename_AndL2': + assumes a: "R[x\n>y] = AndL2 (v).N u" "v\(R,u,x,y)" "x\y" + shows "(\N'. (R = AndL2 (v).N' u) \ N'[x\n>y] = N) \ (\N'. (R = AndL2 (v).N' x) \ y=u \ N'[x\n>y] = N)" +using a +apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject) +apply(rule_tac x="[(name1,v)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +apply(rule_tac x="[(name1,v)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma nrename_AndL2_aux: + assumes a: "R[x\n>y] = AndL2 (v).N u" + shows "(x=u \ x=y) \ (x\u)" +using a +apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +done + +lemma nrename_AndR: + assumes a: "R[x\n>y] = AndR .M .N e" "c\(d,e,N,R)" "d\(c,e,M,R)" + shows "\M' N'. R = AndR .M' .N' e \ M'[x\n>y] = M \ N'[x\n>y] = N \ c\N' \ d\M'" +using a +apply(nominal_induct R avoiding: x y c d e M N rule: trm.strong_induct) +apply(auto split: if_splits simp add: trm.inject alpha) +apply(simp add: fresh_atm fresh_prod) +apply(rule_tac x="[(coname1,c)]\trm1" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(coname1,c)]\trm1" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(coname2,d)]\trm2" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(drule_tac s="trm2[x\n>y]" in sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma nrename_OrR1: + assumes a: "R[x\n>y] = OrR1 .N d" "c\(R,d)" + shows "\N'. (R = OrR1 .N' d) \ N'[x\n>y] = N" +using a +apply(nominal_induct R avoiding: x y c d N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +apply(rule_tac x="[(coname1,c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma nrename_OrR2: + assumes a: "R[x\n>y] = OrR2 .N d" "c\(R,d)" + shows "\N'. (R = OrR2 .N' d) \ N'[x\n>y] = N" +using a +apply(nominal_induct R avoiding: x y c d N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +apply(rule_tac x="[(coname1,c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma nrename_OrL: + assumes a: "R[u\n>v] = OrL (x).M (y).N z" "x\(y,z,u,v,N,R)" "y\(x,z,u,v,M,R)" "z\(u,v)" + shows "\M' N'. R = OrL (x).M' (y).N' z \ M'[u\n>v] = M \ N'[u\n>v] = N \ x\N' \ y\M'" +using a +apply(nominal_induct R avoiding: u v x y z M N rule: trm.strong_induct) +apply(auto split: if_splits simp add: trm.inject alpha fresh_prod fresh_atm) +apply(rule_tac x="[(name1,x)]\trm1" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(name2,y)]\trm2" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +apply(drule_tac s="trm2[u\n>v]" in sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma nrename_OrL': + assumes a: "R[x\n>y] = OrL (v).M (w).N u" "v\(R,N,u,x,y)" "w\(R,M,u,x,y)" "x\y" + shows "(\M' N'. (R = OrL (v).M' (w).N' u) \ M'[x\n>y] = M \ N'[x\n>y] = N) \ + (\M' N'. (R = OrL (v).M' (w).N' x) \ y=u \ M'[x\n>y] = M \ N'[x\n>y] = N)" +using a +apply(nominal_induct R avoiding: y x u v w M N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject) +apply(rule_tac x="[(name1,v)]\trm1" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(rule_tac x="[(name2,w)]\trm2" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(rule conjI) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +apply(drule_tac s="trm2[x\n>u]" in sym) +apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +apply(rule_tac x="[(name1,v)]\trm1" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(rule_tac x="[(name2,w)]\trm2" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(rule conjI) +apply(drule sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +apply(drule_tac s="trm2[x\n>y]" in sym) +apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma nrename_OrL_aux: + assumes a: "R[x\n>y] = OrL (v).M (w).N u" + shows "(x=u \ x=y) \ (x\u)" +using a +apply(nominal_induct R avoiding: y x w u v M N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +done + +lemma nrename_ImpL: + assumes a: "R[x\n>y] = ImpL .M (u).N z" "c\(N,R)" "u\(y,x,z,M,R)" "z\(x,y)" + shows "\M' N'. R = ImpL .M' (u).N' z \ M'[x\n>y] = M \ N'[x\n>y] = N \ c\N' \ u\M'" +using a +apply(nominal_induct R avoiding: u x c y z M N rule: trm.strong_induct) +apply(auto split: if_splits simp add: trm.inject alpha fresh_prod fresh_atm) +apply(rule_tac x="[(coname,c)]\trm1" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(rule_tac x="[(name1,u)]\trm2" in exI) +apply(perm_simp) +apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(drule_tac s="trm2[x\n>y]" in sym) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm fresh_prod fresh_atm) +done + +lemma nrename_ImpL': + assumes a: "R[x\n>y] = ImpL .M (w).N u" "c\(R,N)" "w\(R,M,u,x,y)" "x\y" + shows "(\M' N'. (R = ImpL .M' (w).N' u) \ M'[x\n>y] = M \ N'[x\n>y] = N) \ + (\M' N'. (R = ImpL .M' (w).N' x) \ y=u \ M'[x\n>y] = M \ N'[x\n>y] = N)" +using a +apply(nominal_induct R avoiding: y x u c w M N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject) +apply(rule_tac x="[(coname,c)]\trm1" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(rule_tac x="[(name1,w)]\trm2" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(rule conjI) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(drule_tac s="trm2[x\n>u]" in sym) +apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +apply(rule_tac x="[(coname,c)]\trm1" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(rule_tac x="[(name1,w)]\trm2" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(rule conjI) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(simp add: eqvts calc_atm) +apply(drule_tac s="trm2[x\n>y]" in sym) +apply(drule_tac pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma nrename_ImpL_aux: + assumes a: "R[x\n>y] = ImpL .M (w).N u" + shows "(x=u \ x=y) \ (x\u)" +using a +apply(nominal_induct R avoiding: y x w u c M N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject) +done + +lemma nrename_ImpR: + assumes a: "R[u\n>v] = ImpR (x)..N d" "c\(R,d)" "x\(R,u,v)" + shows "\N'. (R = ImpR (x)..N' d) \ N'[u\n>v] = N" +using a +apply(nominal_induct R avoiding: u v x c d N rule: trm.strong_induct) +apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_perm alpha abs_fresh trm.inject) +apply(rule_tac x="[(name,x)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_fresh fresh_left calc_atm fresh_prod) +apply(rule_tac x="[(name,x)]\[(coname1, c)]\trm" in exI) +apply(perm_simp) +apply(simp add: abs_supp fin_supp abs_fresh fresh_left calc_atm fresh_prod) +apply(drule sym) +apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst]) +apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst]) +apply(simp add: eqvts calc_atm) +done + +lemma nrename_credu: + assumes a: "(M[x\n>y]) \\<^isub>c M'" + shows "\M0. M0[x\n>y]=M' \ M \\<^isub>c M0" +using a +apply(nominal_induct M\"M[x\n>y]" M' avoiding: M x y rule: c_redu.strong_induct) +apply(drule sym) +apply(drule nrename_Cut) +apply(simp) +apply(simp) +apply(auto) +apply(rule_tac x="M'{a:=(x).N'}" in exI) +apply(rule conjI) +apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod) +apply(rule c_redu.intros) +apply(auto dest: not_fic_nrename)[1] +apply(simp add: abs_fresh) +apply(simp add: abs_fresh) +apply(drule sym) +apply(drule nrename_Cut) +apply(simp) +apply(simp) +apply(auto) +apply(rule_tac x="N'{x:=.M'}" in exI) +apply(rule conjI) +apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod) +apply(rule c_redu.intros) +apply(auto) +apply(drule_tac x="xa" and y="y" in fin_nrename) +apply(auto simp add: fresh_prod abs_fresh) +done + +lemma nrename_ax2: + assumes a: "N[x\n>y] = Ax z c" + shows "\z. N = Ax z c" +using a +apply(nominal_induct N avoiding: x y rule: trm.strong_induct) +apply(auto split: if_splits) +apply(simp add: trm.inject) +done + +lemma fic_nrename: + assumes a: "fic (M[x\n>y]) c" + shows "fic M c" +using a +apply(nominal_induct M avoiding: c x y rule: trm.strong_induct) +apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh + split: if_splits) +apply(auto dest: nrename_fresh_interesting2 simp add: fresh_prod fresh_atm) +done + +lemma nrename_lredu: + assumes a: "(M[x\n>y]) \\<^isub>l M'" + shows "\M0. M0[x\n>y]=M' \ M \\<^isub>l M0" +using a +apply(nominal_induct M\"M[x\n>y]" M' avoiding: M x y rule: l_redu.strong_induct) +apply(drule sym) +apply(drule nrename_Cut) +apply(simp add: fresh_prod fresh_atm) +apply(simp) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(case_tac "xa=y") +apply(simp add: nrename_id) +apply(rule l_redu.intros) +apply(simp) +apply(simp add: fresh_atm) +apply(assumption) +apply(frule nrename_ax2) +apply(auto)[1] +apply(case_tac "z=xa") +apply(simp add: trm.inject) +apply(simp) +apply(rule_tac x="M'[a\c>b]" in exI) +apply(rule conjI) +apply(rule crename_interesting3) +apply(rule l_redu.intros) +apply(simp) +apply(simp add: fresh_atm) +apply(auto dest: fic_nrename simp add: fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule nrename_Cut) +apply(simp add: fresh_prod fresh_atm) +apply(simp add: fresh_prod fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(case_tac "xa=ya") +apply(simp add: nrename_id) +apply(rule l_redu.intros) +apply(simp) +apply(simp add: fresh_atm) +apply(assumption) +apply(frule nrename_ax2) +apply(auto)[1] +apply(case_tac "z=xa") +apply(simp add: trm.inject) +apply(rule_tac x="N'[x\n>xa]" in exI) +apply(rule conjI) +apply(rule nrename_interesting1) +apply(auto)[1] +apply(rule l_redu.intros) +apply(simp) +apply(simp add: fresh_atm) +apply(auto dest: fin_nrename2 simp add: fresh_prod fresh_atm)[1] +apply(simp add: trm.inject) +apply(rule_tac x="N'[x\n>y]" in exI) +apply(rule conjI) +apply(rule nrename_interesting2) +apply(simp_all) +apply(rule l_redu.intros) +apply(simp) +apply(simp add: fresh_atm) +apply(auto dest: fin_nrename2 simp add: fresh_prod fresh_atm)[1] +(* LNot *) +apply(drule sym) +apply(drule nrename_Cut) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(drule nrename_NotR) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(drule nrename_NotL) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(rule_tac x="Cut .N'b (x).N'a" in exI) +apply(simp add: fresh_atm)[1] +apply(rule l_redu.intros) +apply(auto simp add: fresh_prod fresh_atm intro: nrename_fresh_interesting1)[1] +apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1] +apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting2)[1] +apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting2)[1] +apply(simp add: fresh_atm) +apply(simp add: fresh_atm) +(* LAnd1 *) +apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule nrename_Cut) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto)[1] +apply(drule nrename_AndR) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(drule nrename_AndL1) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(rule_tac x="Cut .M'a (x).N'b" in exI) +apply(simp add: fresh_atm)[1] +apply(rule l_redu.intros) +apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1] +apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1] +apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1] +apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1] +apply(simp add: fresh_atm) +(* LAnd2 *) +apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule nrename_Cut) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto)[1] +apply(drule nrename_AndR) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(drule nrename_AndL2) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(rule_tac x="Cut .N'a (x).N'b" in exI) +apply(simp add: fresh_atm)[1] +apply(rule l_redu.intros) +apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1] +apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1] +apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1] +apply(auto simp add: fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1] +apply(simp add: fresh_atm) +(* LOr1 *) +apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule nrename_Cut) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto)[1] +apply(drule nrename_OrL) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(drule nrename_OrR1) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(rule_tac x="Cut .N' (x1).M'a" in exI) +apply(rule conjI) +apply(simp add: abs_fresh fresh_atm)[1] +apply(rule l_redu.intros) +apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1] +apply(simp add: fresh_atm) +apply(simp add: fresh_atm) +(* LOr2 *) +apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule nrename_Cut) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto)[1] +apply(drule nrename_OrL) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(drule nrename_OrR2) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(rule_tac x="Cut .N' (x2).N'a" in exI) +apply(rule conjI) +apply(simp add: abs_fresh fresh_atm)[1] +apply(rule l_redu.intros) +apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: nrename_fresh_interesting2)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1] +apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: nrename_fresh_interesting1)[1] +apply(simp add: fresh_atm) +apply(simp add: fresh_atm) +(* ImpL *) +apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1] +apply(drule sym) +apply(drule nrename_Cut) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm abs_supp fin_supp) +apply(auto)[1] +apply(drule nrename_ImpL) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(drule nrename_ImpR) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(simp add: fresh_prod abs_fresh fresh_atm) +apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1] +apply(rule_tac x="Cut .(Cut .M'a (x).N') (y).N'a" in exI) +apply(rule conjI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(rule l_redu.intros) +apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting1)[1] +apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1] +apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting1)[1] +apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1] +apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1] +apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: nrename_fresh_interesting2)[1] +done + +lemma nrename_aredu: + assumes a: "(M[x\n>y]) \\<^isub>a M'" "x\y" + shows "\M0. M0[x\n>y]=M' \ M \\<^isub>a M0" +using a +apply(nominal_induct "M[x\n>y]" M' avoiding: M x y rule: a_redu.strong_induct) +apply(drule nrename_lredu) +apply(blast) +apply(drule nrename_credu) +apply(blast) +(* Cut *) +apply(drule sym) +apply(drule nrename_Cut) +apply(simp) +apply(simp) +apply(auto)[1] +apply(drule_tac x="M'a" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(auto)[1] +apply(rule_tac x="Cut .M0 (x).N'" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(rule conjI) +apply(rule trans) +apply(rule nrename.simps) +apply(drule nrename_fresh_interesting2) +apply(simp add: fresh_a_redu) +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(drule nrename_fresh_interesting1) +apply(simp add: fresh_prod fresh_atm) +apply(simp add: fresh_a_redu) +apply(simp) +apply(auto)[1] +apply(drule sym) +apply(drule nrename_Cut) +apply(simp) +apply(simp) +apply(auto)[1] +apply(drule_tac x="N'a" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(auto)[1] +apply(rule_tac x="Cut .M' (x).M0" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(rule conjI) +apply(rule trans) +apply(rule nrename.simps) +apply(simp add: fresh_a_redu) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1] +apply(simp) +apply(auto)[1] +(* NotL *) +apply(drule sym) +apply(frule nrename_NotL_aux) +apply(erule disjE) +apply(auto)[1] +apply(drule nrename_NotL') +apply(simp) +apply(simp add: fresh_atm) +apply(erule disjE) +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(auto)[1] +apply(rule_tac x="NotL .M0 x" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="x" in meta_spec) +apply(auto)[1] +apply(rule_tac x="NotL .M0 xa" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +(* NotR *) +apply(drule sym) +apply(drule nrename_NotR) +apply(simp) +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(auto)[1] +apply(rule_tac x="NotR (x).M0 a" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +(* AndR *) +apply(drule sym) +apply(drule nrename_AndR) +apply(simp) +apply(auto simp add: fresh_atm fresh_prod)[1] +apply(auto simp add: fresh_atm fresh_prod)[1] +apply(auto)[1] +apply(drule_tac x="M'a" in meta_spec) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(auto)[1] +apply(rule_tac x="AndR .M0 .N' c" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule nrename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp) +apply(drule sym) +apply(drule nrename_AndR) +apply(simp) +apply(auto simp add: fresh_atm fresh_prod)[1] +apply(auto simp add: fresh_atm fresh_prod)[1] +apply(auto)[1] +apply(drule_tac x="N'a" in meta_spec) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(auto)[1] +apply(rule_tac x="AndR .M' .M0 c" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule nrename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp) +apply(simp) +(* AndL1 *) +apply(drule sym) +apply(frule nrename_AndL1_aux) +apply(erule disjE) +apply(auto)[1] +apply(drule nrename_AndL1') +apply(simp) +apply(simp add: fresh_atm) +apply(erule disjE) +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="ya" in meta_spec) +apply(auto)[1] +apply(rule_tac x="AndL1 (x).M0 y" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(auto)[1] +apply(rule_tac x="AndL1 (x).M0 xa" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +(* AndL2 *) +apply(drule sym) +apply(frule nrename_AndL2_aux) +apply(erule disjE) +apply(auto)[1] +apply(drule nrename_AndL2') +apply(simp) +apply(simp add: fresh_atm) +apply(erule disjE) +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="ya" in meta_spec) +apply(auto)[1] +apply(rule_tac x="AndL2 (x).M0 y" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(auto)[1] +apply(rule_tac x="AndL2 (x).M0 xa" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +(* OrL *) +apply(drule sym) +apply(frule nrename_OrL_aux) +apply(erule disjE) +apply(auto)[1] +apply(drule nrename_OrL') +apply(simp add: fresh_prod fresh_atm) +apply(simp add: fresh_atm) +apply(simp add: fresh_atm) +apply(erule disjE) +apply(auto)[1] +apply(drule_tac x="M'a" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="ya" in meta_spec) +apply(auto)[1] +apply(rule_tac x="OrL (x).M0 (y).N' z" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule nrename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(drule_tac x="M'a" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="z" in meta_spec) +apply(auto)[1] +apply(rule_tac x="OrL (x).M0 (y).N' xa" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule nrename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(drule sym) +apply(frule nrename_OrL_aux) +apply(erule disjE) +apply(auto)[1] +apply(drule nrename_OrL') +apply(simp add: fresh_prod fresh_atm) +apply(simp add: fresh_atm) +apply(simp add: fresh_atm) +apply(erule disjE) +apply(auto)[1] +apply(drule_tac x="N'a" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="ya" in meta_spec) +apply(auto)[1] +apply(rule_tac x="OrL (x).M' (y).M0 z" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule nrename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(drule_tac x="N'a" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="z" in meta_spec) +apply(auto)[1] +apply(rule_tac x="OrL (x).M' (y).M0 xa" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule nrename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp) +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +(* OrR1 *) +apply(drule sym) +apply(drule nrename_OrR1) +apply(simp) +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(auto)[1] +apply(rule_tac x="OrR1 .M0 b" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +(* OrR2 *) +apply(drule sym) +apply(drule nrename_OrR2) +apply(simp) +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="x" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(auto)[1] +apply(rule_tac x="OrR2 .M0 b" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +(* ImpL *) +apply(drule sym) +apply(frule nrename_ImpL_aux) +apply(erule disjE) +apply(auto)[1] +apply(drule nrename_ImpL') +apply(simp add: fresh_prod fresh_atm) +apply(simp add: fresh_atm) +apply(simp add: fresh_atm) +apply(erule disjE) +apply(auto)[1] +apply(drule_tac x="M'a" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="ya" in meta_spec) +apply(auto)[1] +apply(rule_tac x="ImpL .M0 (x).N' y" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule nrename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(drule_tac x="M'a" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(auto)[1] +apply(rule_tac x="ImpL .M0 (x).N' xa" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule nrename.simps) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(drule sym) +apply(frule nrename_ImpL_aux) +apply(erule disjE) +apply(auto)[1] +apply(drule nrename_ImpL') +apply(simp add: fresh_prod fresh_atm) +apply(simp add: fresh_atm) +apply(simp add: fresh_atm) +apply(erule disjE) +apply(auto)[1] +apply(drule_tac x="N'a" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="ya" in meta_spec) +apply(auto)[1] +apply(rule_tac x="ImpL .M' (x).M0 y" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule nrename.simps) +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(drule_tac x="N'a" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(auto)[1] +apply(rule_tac x="ImpL .M' (x).M0 xa" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +apply(rule trans) +apply(rule nrename.simps) +apply(auto intro: fresh_a_redu)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1] +(* ImpR *) +apply(drule sym) +apply(drule nrename_ImpR) +apply(simp) +apply(simp) +apply(auto)[1] +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="xa" in meta_spec) +apply(drule_tac x="y" in meta_spec) +apply(auto)[1] +apply(rule_tac x="ImpR (x)..M0 b" in exI) +apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1] +apply(auto)[1] +done + +lemma SNa_preserved_renaming2: + assumes a: "SNa N" + shows "SNa (N[x\n>y])" +using a +apply(induct rule: SNa_induct) +apply(case_tac "x=y") +apply(simp add: nrename_id) +apply(rule SNaI) +apply(drule nrename_aredu) +apply(blast)+ +done + +text {* helper-stuff to set up the induction *} + +abbreviation + SNa_set :: "trm set" +where + "SNa_set \ {M. SNa M}" + +abbreviation + A_Redu_set :: "(trm\trm) set" +where + "A_Redu_set \ {(N,M)| M N. M \\<^isub>a N}" + +lemma SNa_elim: + assumes a: "SNa M" + shows "(\M. (\N. M \\<^isub>a N \ P N)\ P M) \ P M" +using a +by (induct rule: SNa.induct) (blast) + +lemma wf_SNa_restricted: + shows "wf (A_Redu_set \ (UNIV <*> SNa_set))" +apply(unfold wf_def) +apply(intro strip) +apply(case_tac "SNa x") +apply(simp (no_asm_use)) +apply(drule_tac P="P" in SNa_elim) +apply(erule mp) +apply(blast) +(* other case *) +apply(drule_tac x="x" in spec) +apply(erule mp) +apply(fast) +done + +definition SNa_Redu :: "(trm \ trm) set" where + "SNa_Redu \ A_Redu_set \ (UNIV <*> SNa_set)" + +lemma wf_SNa_Redu: + shows "wf SNa_Redu" +apply(unfold SNa_Redu_def) +apply(rule wf_SNa_restricted) +done + +lemma wf_measure_triple: +shows "wf ((measure size) <*lex*> SNa_Redu <*lex*> SNa_Redu)" +by (auto intro: wf_SNa_Redu) + +lemma my_wf_induct_triple: + assumes a: " wf(r1 <*lex*> r2 <*lex*> r3)" + and b: "\x. \\y. ((fst y,fst (snd y),snd (snd y)),(fst x,fst (snd x), snd (snd x))) + \ (r1 <*lex*> r2 <*lex*> r3) \ P y\ \ P x" + shows "P x" +using a +apply(induct x rule: wf_induct_rule) +apply(rule b) +apply(simp) +done + +lemma my_wf_induct_triple': + assumes a: " wf(r1 <*lex*> r2 <*lex*> r3)" + and b: "\x1 x2 x3. \\y1 y2 y3. ((y1,y2,y3),(x1,x2,x3)) \ (r1 <*lex*> r2 <*lex*> r3) \ P (y1,y2,y3)\ + \ P (x1,x2,x3)" + shows "P (x1,x2,x3)" +apply(rule_tac my_wf_induct_triple[OF a]) +apply(case_tac x rule: prod.exhaust) +apply(simp) +apply(case_tac b) +apply(simp) +apply(rule b) +apply(blast) +done + +lemma my_wf_induct_triple'': + assumes a: " wf(r1 <*lex*> r2 <*lex*> r3)" + and b: "\x1 x2 x3. \\y1 y2 y3. ((y1,y2,y3),(x1,x2,x3)) \ (r1 <*lex*> r2 <*lex*> r3) \ P y1 y2 y3\ + \ P x1 x2 x3" + shows "P x1 x2 x3" +apply(rule_tac my_wf_induct_triple'[where P="\(x1,x2,x3). P x1 x2 x3", simplified]) +apply(rule a) +apply(rule b) +apply(auto) +done + +lemma excluded_m: + assumes a: ":M \ (\\)" "(x):N \ (\(B)\)" + shows "(:M \ BINDINGc B (\(B)\) \ (x):N \ BINDINGn B (\\)) + \\(:M \ BINDINGc B (\(B)\) \ (x):N \ BINDINGn B (\\))" +by (blast) + +lemma tricky_subst: + assumes a1: "b\(c,N)" + and a2: "z\(x,P)" + and a3: "M\Ax z b" + shows "(Cut .N (z).M){b:=(x).P} = Cut .N (z).(M{b:=(x).P})" +using a1 a2 a3 +apply - +apply(generate_fresh "coname") +apply(subgoal_tac "Cut .N (z).M = Cut .([(ca,c)]\N) (z).M") +apply(simp) +apply(rule trans) +apply(rule better_Cut_substc) +apply(simp) +apply(simp add: abs_fresh) +apply(simp) +apply(subgoal_tac "b\([(ca,c)]\N)") +apply(simp add: forget) +apply(simp add: trm.inject) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(simp add: trm.inject) +apply(rule sym) +apply(simp add: alpha fresh_prod fresh_atm) +done + +text {* 3rd lemma *} + +lemma CUT_SNa_aux: + assumes a1: ":M \ (\\)" + and a2: "SNa M" + and a3: "(x):N \ (\(B)\)" + and a4: "SNa N" + shows "SNa (Cut .M (x).N)" +using a1 a2 a3 a4 +apply(induct B M N arbitrary: a x rule: my_wf_induct_triple''[OF wf_measure_triple]) +apply(rule SNaI) +apply(drule Cut_a_redu_elim) +apply(erule disjE) +(* left-inner reduction *) +apply(erule exE) +apply(erule conjE)+ +apply(simp) +apply(drule_tac x="x1" in meta_spec) +apply(drule_tac x="M'a" in meta_spec) +apply(drule_tac x="x3" in meta_spec) +apply(drule conjunct2) +apply(drule mp) +apply(rule conjI) +apply(simp) +apply(rule disjI1) +apply(simp add: SNa_Redu_def) +apply(drule_tac x="a" in spec) +apply(drule mp) +apply(simp add: CANDs_preserved_single) +apply(drule mp) +apply(simp add: a_preserves_SNa) +apply(drule_tac x="x" in spec) +apply(simp) +apply(erule disjE) +(* right-inner reduction *) +apply(erule exE) +apply(erule conjE)+ +apply(simp) +apply(drule_tac x="x1" in meta_spec) +apply(drule_tac x="x2" in meta_spec) +apply(drule_tac x="N'" in meta_spec) +apply(drule conjunct2) +apply(drule mp) +apply(rule conjI) +apply(simp) +apply(rule disjI2) +apply(simp add: SNa_Redu_def) +apply(drule_tac x="a" in spec) +apply(drule mp) +apply(simp add: CANDs_preserved_single) +apply(drule mp) +apply(assumption) +apply(drule_tac x="x" in spec) +apply(drule mp) +apply(simp add: CANDs_preserved_single) +apply(drule mp) +apply(simp add: a_preserves_SNa) +apply(assumption) +apply(erule disjE) +(******** c-reduction *********) +apply(drule Cut_c_redu_elim) +(* c-left reduction*) +apply(erule disjE) +apply(erule conjE) +apply(frule_tac B="x1" in fic_CANDS) +apply(simp) +apply(erule disjE) +(* in AXIOMSc *) +apply(simp add: AXIOMSc_def) +apply(erule exE)+ +apply(simp add: ctrm.inject) +apply(simp add: alpha) +apply(erule disjE) +apply(simp) +apply(rule impI) +apply(simp) +apply(subgoal_tac "fic (Ax y b) b")(*A*) +apply(simp) +(*A*) +apply(auto)[1] +apply(simp) +apply(rule impI) +apply(simp) +apply(subgoal_tac "fic (Ax ([(a,aa)]\y) a) a")(*B*) +apply(simp) +(*B*) +apply(auto)[1] +(* in BINDINGc *) +apply(simp) +apply(drule BINDINGc_elim) +apply(simp) +(* c-right reduction*) +apply(erule conjE) +apply(frule_tac B="x1" in fin_CANDS) +apply(simp) +apply(erule disjE) +(* in AXIOMSc *) +apply(simp add: AXIOMSn_def) +apply(erule exE)+ +apply(simp add: ntrm.inject) +apply(simp add: alpha) +apply(erule disjE) +apply(simp) +apply(rule impI) +apply(simp) +apply(subgoal_tac "fin (Ax xa b) xa")(*A*) +apply(simp) +(*A*) +apply(auto)[1] +apply(simp) +apply(rule impI) +apply(simp) +apply(subgoal_tac "fin (Ax x ([(x,xa)]\b)) x")(*B*) +apply(simp) +(*B*) +apply(auto)[1] +(* in BINDINGc *) +apply(simp) +apply(drule BINDINGn_elim) +apply(simp) +(*********** l-reductions ************) +apply(drule Cut_l_redu_elim) +apply(erule disjE) +(* ax1 *) +apply(erule exE) +apply(simp) +apply(simp add: SNa_preserved_renaming1) +apply(erule disjE) +(* ax2 *) +apply(erule exE) +apply(simp add: SNa_preserved_renaming2) +apply(erule disjE) +(* LNot *) +apply(erule exE)+ +apply(auto)[1] +apply(frule_tac excluded_m) +apply(assumption) +apply(erule disjE) +(* one of them in BINDING *) +apply(erule disjE) +apply(drule fin_elims) +apply(drule fic_elims) +apply(simp) +apply(drule BINDINGc_elim) +apply(drule_tac x="x" in spec) +apply(drule_tac x="NotL .N' x" in spec) +apply(simp) +apply(simp add: better_NotR_substc) +apply(generate_fresh "coname") +apply(subgoal_tac "fresh_fun (\a'. Cut .NotR (y).M'a a' (x).NotL .N' x) + = Cut .NotR (y).M'a c (x).NotL .N' x") +apply(simp) +apply(subgoal_tac "Cut .NotR (y).M'a c (x).NotL .N' x \\<^isub>a Cut .N' (y).M'a") +apply(simp only: a_preserves_SNa) +apply(rule al_redu) +apply(rule better_LNot_intro) +apply(simp) +apply(simp) +apply(fresh_fun_simp (no_asm)) +apply(simp) +(* other case of in BINDING *) +apply(drule fin_elims) +apply(drule fic_elims) +apply(simp) +apply(drule BINDINGn_elim) +apply(drule_tac x="a" in spec) +apply(drule_tac x="NotR (y).M'a a" in spec) +apply(simp) +apply(simp add: better_NotL_substn) +apply(generate_fresh "name") +apply(subgoal_tac "fresh_fun (\x'. Cut .NotR (y).M'a a (x').NotL .N' x') + = Cut .NotR (y).M'a a (c).NotL .N' c") +apply(simp) +apply(subgoal_tac "Cut .NotR (y).M'a a (c).NotL .N' c \\<^isub>a Cut .N' (y).M'a") +apply(simp only: a_preserves_SNa) +apply(rule al_redu) +apply(rule better_LNot_intro) +apply(simp) +apply(simp) +apply(fresh_fun_simp (no_asm)) +apply(simp) +(* none of them in BINDING *) +apply(simp) +apply(erule conjE) +apply(frule CAND_NotR_elim) +apply(assumption) +apply(erule exE) +apply(frule CAND_NotL_elim) +apply(assumption) +apply(erule exE) +apply(simp only: ty.inject) +apply(drule_tac x="B'" in meta_spec) +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="M'a" in meta_spec) +apply(erule conjE)+ +apply(drule mp) +apply(simp) +apply(drule_tac x="b" in spec) +apply(rotate_tac 13) +apply(drule mp) +apply(assumption) +apply(rotate_tac 13) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(drule_tac x="y" in spec) +apply(rotate_tac 13) +apply(drule mp) +apply(assumption) +apply(rotate_tac 13) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(assumption) +(* LAnd1 case *) +apply(erule disjE) +apply(erule exE)+ +apply(auto)[1] +apply(frule_tac excluded_m) +apply(assumption) +apply(erule disjE) +(* one of them in BINDING *) +apply(erule disjE) +apply(drule fin_elims) +apply(drule fic_elims) +apply(simp) +apply(drule BINDINGc_elim) +apply(drule_tac x="x" in spec) +apply(drule_tac x="AndL1 (y).N' x" in spec) +apply(simp) +apply(simp add: better_AndR_substc) +apply(generate_fresh "coname") +apply(subgoal_tac "fresh_fun (\a'. Cut .AndR .M1 .M2 a' (x).AndL1 (y).N' x) + = Cut .AndR .M1 .M2 ca (x).AndL1 (y).N' x") +apply(simp) +apply(subgoal_tac "Cut .AndR .M1 .M2 ca (x).AndL1 (y).N' x \\<^isub>a Cut .M1 (y).N'") +apply(auto intro: a_preserves_SNa)[1] +apply(rule al_redu) +apply(rule better_LAnd1_intro) +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(simp) +apply(fresh_fun_simp (no_asm)) +apply(simp) +(* other case of in BINDING *) +apply(drule fin_elims) +apply(drule fic_elims) +apply(simp) +apply(drule BINDINGn_elim) +apply(drule_tac x="a" in spec) +apply(drule_tac x="AndR .M1 .M2 a" in spec) +apply(simp) +apply(simp add: better_AndL1_substn) +apply(generate_fresh "name") +apply(subgoal_tac "fresh_fun (\z'. Cut .AndR .M1 .M2 a (z').AndL1 (y).N' z') + = Cut .AndR .M1 .M2 a (ca).AndL1 (y).N' ca") +apply(simp) +apply(subgoal_tac "Cut .AndR .M1 .M2 a (ca).AndL1 (y).N' ca \\<^isub>a Cut .M1 (y).N'") +apply(auto intro: a_preserves_SNa)[1] +apply(rule al_redu) +apply(rule better_LAnd1_intro) +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(fresh_fun_simp (no_asm)) +apply(simp) +(* none of them in BINDING *) +apply(simp) +apply(erule conjE) +apply(frule CAND_AndR_elim) +apply(assumption) +apply(erule exE) +apply(frule CAND_AndL1_elim) +apply(assumption) +apply(erule exE)+ +apply(simp only: ty.inject) +apply(drule_tac x="B1" in meta_spec) +apply(drule_tac x="M1" in meta_spec) +apply(drule_tac x="N'" in meta_spec) +apply(erule conjE)+ +apply(drule mp) +apply(simp) +apply(drule_tac x="b" in spec) +apply(rotate_tac 14) +apply(drule mp) +apply(assumption) +apply(rotate_tac 14) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(drule_tac x="y" in spec) +apply(rotate_tac 15) +apply(drule mp) +apply(assumption) +apply(rotate_tac 15) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(assumption) +(* LAnd2 case *) +apply(erule disjE) +apply(erule exE)+ +apply(auto)[1] +apply(frule_tac excluded_m) +apply(assumption) +apply(erule disjE) +(* one of them in BINDING *) +apply(erule disjE) +apply(drule fin_elims) +apply(drule fic_elims) +apply(simp) +apply(drule BINDINGc_elim) +apply(drule_tac x="x" in spec) +apply(drule_tac x="AndL2 (y).N' x" in spec) +apply(simp) +apply(simp add: better_AndR_substc) +apply(generate_fresh "coname") +apply(subgoal_tac "fresh_fun (\a'. Cut .AndR .M1 .M2 a' (x).AndL2 (y).N' x) + = Cut .AndR .M1 .M2 ca (x).AndL2 (y).N' x") +apply(simp) +apply(subgoal_tac "Cut .AndR .M1 .M2 ca (x).AndL2 (y).N' x \\<^isub>a Cut .M2 (y).N'") +apply(auto intro: a_preserves_SNa)[1] +apply(rule al_redu) +apply(rule better_LAnd2_intro) +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(simp) +apply(fresh_fun_simp (no_asm)) +apply(simp) +(* other case of in BINDING *) +apply(drule fin_elims) +apply(drule fic_elims) +apply(simp) +apply(drule BINDINGn_elim) +apply(drule_tac x="a" in spec) +apply(drule_tac x="AndR .M1 .M2 a" in spec) +apply(simp) +apply(simp add: better_AndL2_substn) +apply(generate_fresh "name") +apply(subgoal_tac "fresh_fun (\z'. Cut .AndR .M1 .M2 a (z').AndL2 (y).N' z') + = Cut .AndR .M1 .M2 a (ca).AndL2 (y).N' ca") +apply(simp) +apply(subgoal_tac "Cut .AndR .M1 .M2 a (ca).AndL2 (y).N' ca \\<^isub>a Cut .M2 (y).N'") +apply(auto intro: a_preserves_SNa)[1] +apply(rule al_redu) +apply(rule better_LAnd2_intro) +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(fresh_fun_simp (no_asm)) +apply(simp) +(* none of them in BINDING *) +apply(simp) +apply(erule conjE) +apply(frule CAND_AndR_elim) +apply(assumption) +apply(erule exE) +apply(frule CAND_AndL2_elim) +apply(assumption) +apply(erule exE)+ +apply(simp only: ty.inject) +apply(drule_tac x="B2" in meta_spec) +apply(drule_tac x="M2" in meta_spec) +apply(drule_tac x="N'" in meta_spec) +apply(erule conjE)+ +apply(drule mp) +apply(simp) +apply(drule_tac x="c" in spec) +apply(rotate_tac 14) +apply(drule mp) +apply(assumption) +apply(rotate_tac 14) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(drule_tac x="y" in spec) +apply(rotate_tac 15) +apply(drule mp) +apply(assumption) +apply(rotate_tac 15) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(assumption) +(* LOr1 case *) +apply(erule disjE) +apply(erule exE)+ +apply(auto)[1] +apply(frule_tac excluded_m) +apply(assumption) +apply(erule disjE) +(* one of them in BINDING *) +apply(erule disjE) +apply(drule fin_elims) +apply(drule fic_elims) +apply(simp) +apply(drule BINDINGc_elim) +apply(drule_tac x="x" in spec) +apply(drule_tac x="OrL (z).M1 (y).M2 x" in spec) +apply(simp) +apply(simp add: better_OrR1_substc) +apply(generate_fresh "coname") +apply(subgoal_tac "fresh_fun (\a'. Cut .OrR1 .N' a' (x).OrL (z).M1 (y).M2 x) + = Cut .OrR1 .N' c (x).OrL (z).M1 (y).M2 x") +apply(simp) +apply(subgoal_tac "Cut .OrR1 .N' c (x).OrL (z).M1 (y).M2 x \\<^isub>a Cut .N' (z).M1") +apply(auto intro: a_preserves_SNa)[1] +apply(rule al_redu) +apply(rule better_LOr1_intro) +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(simp add: abs_fresh) +apply(fresh_fun_simp (no_asm)) +apply(simp) +(* other case of in BINDING *) +apply(drule fin_elims) +apply(drule fic_elims) +apply(simp) +apply(drule BINDINGn_elim) +apply(drule_tac x="a" in spec) +apply(drule_tac x="OrR1 .N' a" in spec) +apply(simp) +apply(simp add: better_OrL_substn) +apply(generate_fresh "name") +apply(subgoal_tac "fresh_fun (\z'. Cut .OrR1 .N' a (z').OrL (z).M1 (y).M2 z') + = Cut .OrR1 .N' a (c).OrL (z).M1 (y).M2 c") +apply(simp) +apply(subgoal_tac "Cut .OrR1 .N' a (c).OrL (z).M1 (y).M2 c \\<^isub>a Cut .N' (z).M1") +apply(auto intro: a_preserves_SNa)[1] +apply(rule al_redu) +apply(rule better_LOr1_intro) +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(fresh_fun_simp (no_asm)) +apply(simp) +(* none of them in BINDING *) +apply(simp) +apply(erule conjE) +apply(frule CAND_OrR1_elim) +apply(assumption) +apply(erule exE)+ +apply(frule CAND_OrL_elim) +apply(assumption) +apply(erule exE)+ +apply(simp only: ty.inject) +apply(drule_tac x="B1" in meta_spec) +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="M1" in meta_spec) +apply(erule conjE)+ +apply(drule mp) +apply(simp) +apply(drule_tac x="b" in spec) +apply(rotate_tac 15) +apply(drule mp) +apply(assumption) +apply(rotate_tac 15) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(drule_tac x="z" in spec) +apply(rotate_tac 15) +apply(drule mp) +apply(assumption) +apply(rotate_tac 15) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(assumption) +(* LOr2 case *) +apply(erule disjE) +apply(erule exE)+ +apply(auto)[1] +apply(frule_tac excluded_m) +apply(assumption) +apply(erule disjE) +(* one of them in BINDING *) +apply(erule disjE) +apply(drule fin_elims) +apply(drule fic_elims) +apply(simp) +apply(drule BINDINGc_elim) +apply(drule_tac x="x" in spec) +apply(drule_tac x="OrL (z).M1 (y).M2 x" in spec) +apply(simp) +apply(simp add: better_OrR2_substc) +apply(generate_fresh "coname") +apply(subgoal_tac "fresh_fun (\a'. Cut .OrR2 .N' a' (x).OrL (z).M1 (y).M2 x) + = Cut .OrR2 .N' c (x).OrL (z).M1 (y).M2 x") +apply(simp) +apply(subgoal_tac "Cut .OrR2 .N' c (x).OrL (z).M1 (y).M2 x \\<^isub>a Cut .N' (y).M2") +apply(auto intro: a_preserves_SNa)[1] +apply(rule al_redu) +apply(rule better_LOr2_intro) +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(simp add: abs_fresh) +apply(fresh_fun_simp (no_asm)) +apply(simp) +(* other case of in BINDING *) +apply(drule fin_elims) +apply(drule fic_elims) +apply(simp) +apply(drule BINDINGn_elim) +apply(drule_tac x="a" in spec) +apply(drule_tac x="OrR2 .N' a" in spec) +apply(simp) +apply(simp add: better_OrL_substn) +apply(generate_fresh "name") +apply(subgoal_tac "fresh_fun (\z'. Cut .OrR2 .N' a (z').OrL (z).M1 (y).M2 z') + = Cut .OrR2 .N' a (c).OrL (z).M1 (y).M2 c") +apply(simp) +apply(subgoal_tac "Cut .OrR2 .N' a (c).OrL (z).M1 (y).M2 c \\<^isub>a Cut .N' (y).M2") +apply(auto intro: a_preserves_SNa)[1] +apply(rule al_redu) +apply(rule better_LOr2_intro) +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(fresh_fun_simp (no_asm)) +apply(simp) +(* none of them in BINDING *) +apply(simp) +apply(erule conjE) +apply(frule CAND_OrR2_elim) +apply(assumption) +apply(erule exE)+ +apply(frule CAND_OrL_elim) +apply(assumption) +apply(erule exE)+ +apply(simp only: ty.inject) +apply(drule_tac x="B2" in meta_spec) +apply(drule_tac x="N'" in meta_spec) +apply(drule_tac x="M2" in meta_spec) +apply(erule conjE)+ +apply(drule mp) +apply(simp) +apply(drule_tac x="b" in spec) +apply(rotate_tac 15) +apply(drule mp) +apply(assumption) +apply(rotate_tac 15) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(drule_tac x="y" in spec) +apply(rotate_tac 15) +apply(drule mp) +apply(assumption) +apply(rotate_tac 15) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(assumption) +(* LImp case *) +apply(erule exE)+ +apply(auto)[1] +apply(frule_tac excluded_m) +apply(assumption) +apply(erule disjE) +(* one of them in BINDING *) +apply(erule disjE) +apply(drule fin_elims) +apply(drule fic_elims) +apply(simp) +apply(drule BINDINGc_elim) +apply(drule_tac x="x" in spec) +apply(drule_tac x="ImpL .N1 (y).N2 x" in spec) +apply(simp) +apply(simp add: better_ImpR_substc) +apply(generate_fresh "coname") +apply(subgoal_tac "fresh_fun (\a'. Cut .ImpR (z)..M'a a' (x).ImpL .N1 (y).N2 x) + = Cut .ImpR (z)..M'a ca (x).ImpL .N1 (y).N2 x") +apply(simp) +apply(subgoal_tac "Cut .ImpR (z)..M'a ca (x).ImpL .N1 (y).N2 x \\<^isub>a + Cut .Cut .N1 (z).M'a (y).N2") +apply(auto intro: a_preserves_SNa)[1] +apply(rule al_redu) +apply(rule better_LImp_intro) +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(simp add: abs_fresh) +apply(simp) +apply(fresh_fun_simp (no_asm)) +apply(simp) +(* other case of in BINDING *) +apply(drule fin_elims) +apply(drule fic_elims) +apply(simp) +apply(drule BINDINGn_elim) +apply(drule_tac x="a" in spec) +apply(drule_tac x="ImpR (z)..M'a a" in spec) +apply(simp) +apply(simp add: better_ImpL_substn) +apply(generate_fresh "name") +apply(subgoal_tac "fresh_fun (\z'. Cut .ImpR (z)..M'a a (z').ImpL .N1 (y).N2 z') + = Cut .ImpR (z)..M'a a (ca).ImpL .N1 (y).N2 ca") +apply(simp) +apply(subgoal_tac "Cut .ImpR (z)..M'a a (ca).ImpL .N1 (y).N2 ca \\<^isub>a + Cut .Cut .N1 (z).M'a (y).N2") +apply(auto intro: a_preserves_SNa)[1] +apply(rule al_redu) +apply(rule better_LImp_intro) +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(simp) +apply(fresh_fun_simp (no_asm)) +apply(simp add: abs_fresh abs_supp fin_supp) +apply(simp add: abs_fresh abs_supp fin_supp) +apply(simp) +(* none of them in BINDING *) +apply(erule conjE) +apply(frule CAND_ImpL_elim) +apply(assumption) +apply(erule exE)+ +apply(frule CAND_ImpR_elim) (* check here *) +apply(assumption) +apply(erule exE)+ +apply(erule conjE)+ +apply(simp only: ty.inject) +apply(erule conjE)+ +apply(case_tac "M'a=Ax z b") +(* case Ma = Ax z b *) +apply(rule_tac t="Cut .(Cut .N1 (z).M'a) (y).N2" and s="Cut .(M'a{z:=.N1}) (y).N2" in subst) +apply(simp) +apply(drule_tac x="c" in spec) +apply(drule_tac x="N1" in spec) +apply(drule mp) +apply(simp) +apply(drule_tac x="B2" in meta_spec) +apply(drule_tac x="M'a{z:=.N1}" in meta_spec) +apply(drule_tac x="N2" in meta_spec) +apply(drule conjunct1) +apply(drule mp) +apply(simp) +apply(rotate_tac 17) +apply(drule_tac x="b" in spec) +apply(drule mp) +apply(assumption) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(rotate_tac 17) +apply(drule_tac x="y" in spec) +apply(drule mp) +apply(assumption) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(assumption) +(* case Ma \ Ax z b *) +apply(subgoal_tac ":Cut .N1 (z).M'a \ \\") (* lemma *) +apply(frule_tac meta_spec) +apply(drule_tac x="B2" in meta_spec) +apply(drule_tac x="Cut .N1 (z).M'a" in meta_spec) +apply(drule_tac x="N2" in meta_spec) +apply(erule conjE)+ +apply(drule mp) +apply(simp) +apply(rotate_tac 20) +apply(drule_tac x="b" in spec) +apply(rotate_tac 20) +apply(drule mp) +apply(assumption) +apply(rotate_tac 20) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(rotate_tac 20) +apply(drule_tac x="y" in spec) +apply(rotate_tac 20) +apply(drule mp) +apply(assumption) +apply(rotate_tac 20) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(assumption) +(* lemma *) +apply(subgoal_tac ":Cut .N1 (z).M'a \ BINDINGc B2 (\(B2)\)") (* second lemma *) +apply(simp add: BINDING_implies_CAND) +(* second lemma *) +apply(simp (no_asm) add: BINDINGc_def) +apply(rule exI)+ +apply(rule conjI) +apply(rule refl) +apply(rule allI)+ +apply(rule impI) +apply(generate_fresh "name") +apply(rule_tac t="Cut .N1 (z).M'a" and s="Cut .N1 (ca).([(ca,z)]\M'a)" in subst) +apply(simp add: trm.inject alpha fresh_prod fresh_atm) +apply(rule_tac t="(Cut .N1 (ca).([(ca,z)]\M'a)){b:=(xa).P}" + and s="Cut .N1 (ca).(([(ca,z)]\M'a){b:=(xa).P})" in subst) +apply(rule sym) +apply(rule tricky_subst) +apply(simp) +apply(simp) +apply(clarify) +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm) +apply(drule_tac x="B1" in meta_spec) +apply(drule_tac x="N1" in meta_spec) +apply(drule_tac x="([(ca,z)]\M'a){b:=(xa).P}" in meta_spec) +apply(drule conjunct1) +apply(drule mp) +apply(simp) +apply(rotate_tac 19) +apply(drule_tac x="c" in spec) +apply(drule mp) +apply(assumption) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(rotate_tac 19) +apply(drule_tac x="ca" in spec) +apply(subgoal_tac "(ca):([(ca,z)]\M'a){b:=(xa).P} \ \(B1)\")(*A*) +apply(drule mp) +apply(assumption) +apply(drule mp) +apply(simp add: CANDs_imply_SNa) +apply(assumption) +(*A*) +apply(drule_tac x="[(ca,z)]\xa" in spec) +apply(drule_tac x="[(ca,z)]\P" in spec) +apply(rotate_tac 19) +apply(simp add: fresh_prod fresh_left) +apply(drule mp) +apply(rule conjI) +apply(auto simp add: calc_atm)[1] +apply(rule conjI) +apply(auto simp add: calc_atm)[1] +apply(drule_tac pi="[(ca,z)]" and x="(xa):P" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name) +apply(drule_tac pi="[(ca,z)]" and X="\(B1)\" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(simp add: CAND_eqvt_name csubst_eqvt) +apply(perm_simp) +done + + +(* parallel substitution *) + + +lemma CUT_SNa: + assumes a1: ":M \ (\\)" + and a2: "(x):N \ (\(B)\)" + shows "SNa (Cut .M (x).N)" +using a1 a2 +apply - +apply(rule CUT_SNa_aux[OF a1]) +apply(simp_all add: CANDs_imply_SNa) +done + + +fun + findn :: "(name\coname\trm) list\name\(coname\trm) option" +where + "findn [] x = None" +| "findn ((y,c,P)#\n) x = (if y=x then Some (c,P) else findn \n x)" + +lemma findn_eqvt[eqvt]: + fixes pi1::"name prm" + and pi2::"coname prm" + shows "(pi1\findn \n x) = findn (pi1\\n) (pi1\x)" + and "(pi2\findn \n x) = findn (pi2\\n) (pi2\x)" +apply(induct \n) +apply(auto simp add: perm_bij) +done + +lemma findn_fresh: + assumes a: "x\\n" + shows "findn \n x = None" +using a +apply(induct \n) +apply(auto simp add: fresh_list_cons fresh_atm fresh_prod) +done + +fun + findc :: "(coname\name\trm) list\coname\(name\trm) option" +where + "findc [] x = None" +| "findc ((c,y,P)#\c) a = (if a=c then Some (y,P) else findc \c a)" + +lemma findc_eqvt[eqvt]: + fixes pi1::"name prm" + and pi2::"coname prm" + shows "(pi1\findc \c a) = findc (pi1\\c) (pi1\a)" + and "(pi2\findc \c a) = findc (pi2\\c) (pi2\a)" +apply(induct \c) +apply(auto simp add: perm_bij) +done + +lemma findc_fresh: + assumes a: "a\\c" + shows "findc \c a = None" +using a +apply(induct \c) +apply(auto simp add: fresh_list_cons fresh_atm fresh_prod) +done + +abbreviation + nmaps :: "(name\coname\trm) list \ name \ (coname\trm) option \ bool" ("_ nmaps _ to _" [55,55,55] 55) +where + "\n nmaps x to P \ (findn \n x) = P" + +abbreviation + cmaps :: "(coname\name\trm) list \ coname \ (name\trm) option \ bool" ("_ cmaps _ to _" [55,55,55] 55) +where + "\c cmaps a to P \ (findc \c a) = P" + +lemma nmaps_fresh: + shows "\n nmaps x to Some (c,P) \ a\\n \ a\(c,P)" +apply(induct \n) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm) +apply(case_tac "aa=x") +apply(auto) +apply(case_tac "aa=x") +apply(auto) +done + +lemma cmaps_fresh: + shows "\c cmaps a to Some (y,P) \ x\\c \ x\(y,P)" +apply(induct \c) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm) +apply(case_tac "a=aa") +apply(auto) +apply(case_tac "a=aa") +apply(auto) +done + +lemma nmaps_false: + shows "\n nmaps x to Some (c,P) \ x\\n \ False" +apply(induct \n) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm) +done + +lemma cmaps_false: + shows "\c cmaps c to Some (x,P) \ c\\c \ False" +apply(induct \c) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm) +done + +fun + lookupa :: "name\coname\(coname\name\trm) list\trm" +where + "lookupa x a [] = Ax x a" +| "lookupa x a ((c,y,P)#\c) = (if a=c then Cut .Ax x a (y).P else lookupa x a \c)" + +lemma lookupa_eqvt[eqvt]: + fixes pi1::"name prm" + and pi2::"coname prm" + shows "(pi1\(lookupa x a \c)) = lookupa (pi1\x) (pi1\a) (pi1\\c)" + and "(pi2\(lookupa x a \c)) = lookupa (pi2\x) (pi2\a) (pi2\\c)" +apply - +apply(induct \c) +apply(auto simp add: eqvts) +apply(induct \c) +apply(auto simp add: eqvts) +done + +lemma lookupa_fire: + assumes a: "\c cmaps a to Some (y,P)" + shows "(lookupa x a \c) = Cut .Ax x a (y).P" +using a +apply(induct \c arbitrary: x a y P) +apply(auto) +done + +fun + lookupb :: "name\coname\(coname\name\trm) list\coname\trm\trm" +where + "lookupb x a [] c P = Cut .P (x).Ax x a" +| "lookupb x a ((d,y,N)#\c) c P = (if a=d then Cut .P (y).N else lookupb x a \c c P)" + +lemma lookupb_eqvt[eqvt]: + fixes pi1::"name prm" + and pi2::"coname prm" + shows "(pi1\(lookupb x a \c c P)) = lookupb (pi1\x) (pi1\a) (pi1\\c) (pi1\c) (pi1\P)" + and "(pi2\(lookupb x a \c c P)) = lookupb (pi2\x) (pi2\a) (pi2\\c) (pi2\c) (pi2\P)" +apply - +apply(induct \c) +apply(auto simp add: eqvts) +apply(induct \c) +apply(auto simp add: eqvts) +done + +fun + lookup :: "name\coname\(name\coname\trm) list\(coname\name\trm) list\trm" +where + "lookup x a [] \c = lookupa x a \c" +| "lookup x a ((y,c,P)#\n) \c = (if x=y then (lookupb x a \c c P) else lookup x a \n \c)" + +lemma lookup_eqvt[eqvt]: + fixes pi1::"name prm" + and pi2::"coname prm" + shows "(pi1\(lookup x a \n \c)) = lookup (pi1\x) (pi1\a) (pi1\\n) (pi1\\c)" + and "(pi2\(lookup x a \n \c)) = lookup (pi2\x) (pi2\a) (pi2\\n) (pi2\\c)" +apply - +apply(induct \n) +apply(auto simp add: eqvts) +apply(induct \n) +apply(auto simp add: eqvts) +done + +fun + lookupc :: "name\coname\(name\coname\trm) list\trm" +where + "lookupc x a [] = Ax x a" +| "lookupc x a ((y,c,P)#\n) = (if x=y then P[c\c>a] else lookupc x a \n)" + +lemma lookupc_eqvt[eqvt]: + fixes pi1::"name prm" + and pi2::"coname prm" + shows "(pi1\(lookupc x a \n)) = lookupc (pi1\x) (pi1\a) (pi1\\n)" + and "(pi2\(lookupc x a \n)) = lookupc (pi2\x) (pi2\a) (pi2\\n)" +apply - +apply(induct \n) +apply(auto simp add: eqvts) +apply(induct \n) +apply(auto simp add: eqvts) +done + +fun + lookupd :: "name\coname\(coname\name\trm) list\trm" +where + "lookupd x a [] = Ax x a" +| "lookupd x a ((c,y,P)#\c) = (if a=c then P[y\n>x] else lookupd x a \c)" + +lemma lookupd_eqvt[eqvt]: + fixes pi1::"name prm" + and pi2::"coname prm" + shows "(pi1\(lookupd x a \n)) = lookupd (pi1\x) (pi1\a) (pi1\\n)" + and "(pi2\(lookupd x a \n)) = lookupd (pi2\x) (pi2\a) (pi2\\n)" +apply - +apply(induct \n) +apply(auto simp add: eqvts) +apply(induct \n) +apply(auto simp add: eqvts) +done + +lemma lookupa_fresh: + assumes a: "a\\c" + shows "lookupa y a \c = Ax y a" +using a +apply(induct \c) +apply(auto simp add: fresh_prod fresh_list_cons fresh_atm) +done + +lemma lookupa_csubst: + assumes a: "a\\c" + shows "Cut .Ax y a (x).P = (lookupa y a \c){a:=(x).P}" +using a by (simp add: lookupa_fresh) + +lemma lookupa_freshness: + fixes a::"coname" + and x::"name" + shows "a\(\c,c) \ a\lookupa y c \c" + and "x\(\c,y) \ x\lookupa y c \c" +apply(induct \c) +apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm) +done + +lemma lookupa_unicity: + assumes a: "lookupa x a \c= Ax y b" "b\\c" "y\\c" + shows "x=y \ a=b" +using a +apply(induct \c) +apply(auto simp add: trm.inject fresh_list_cons fresh_prod fresh_atm) +apply(case_tac "a=aa") +apply(auto) +apply(case_tac "a=aa") +apply(auto) +done + +lemma lookupb_csubst: + assumes a: "a\(\c,c,N)" + shows "Cut .N (x).P = (lookupb y a \c c N){a:=(x).P}" +using a +apply(induct \c) +apply(auto simp add: fresh_list_cons fresh_atm fresh_prod) +apply(rule sym) +apply(generate_fresh "name") +apply(generate_fresh "coname") +apply(subgoal_tac "Cut .N (y).Ax y a = Cut .([(caa,c)]\N) (ca).Ax ca a") +apply(simp) +apply(rule trans) +apply(rule better_Cut_substc) +apply(simp) +apply(simp add: abs_fresh) +apply(simp) +apply(subgoal_tac "a\([(caa,c)]\N)") +apply(simp add: forget) +apply(simp add: trm.inject) +apply(simp add: fresh_left calc_atm fresh_prod fresh_atm) +apply(simp add: trm.inject) +apply(rule conjI) +apply(rule sym) +apply(simp add: alpha fresh_prod fresh_atm) +apply(simp add: alpha calc_atm fresh_prod fresh_atm) +done + +lemma lookupb_freshness: + fixes a::"coname" + and x::"name" + shows "a\(\c,c,b,P) \ a\lookupb y c \c b P" + and "x\(\c,y,P) \ x\lookupb y c \c b P" +apply(induct \c) +apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm) +done + +lemma lookupb_unicity: + assumes a: "lookupb x a \c c P = Ax y b" "b\(\c,c,P)" "y\\c" + shows "x=y \ a=b" +using a +apply(induct \c) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm) +apply(case_tac "a=aa") +apply(auto) +apply(case_tac "a=aa") +apply(auto) +done + +lemma lookupb_lookupa: + assumes a: "x\\c" + shows "lookupb x c \c a P = (lookupa x c \c){x:=.P}" +using a +apply(induct \c) +apply(auto simp add: fresh_list_cons fresh_prod) +apply(generate_fresh "coname") +apply(generate_fresh "name") +apply(subgoal_tac "Cut .Ax x c (aa).b = Cut .Ax x ca (caa).([(caa,aa)]\b)") +apply(simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn) +apply(simp add: abs_fresh) +apply(simp) +apply(simp) +apply(subgoal_tac "x\([(caa,aa)]\b)") +apply(simp add: forget) +apply(simp add: trm.inject) +apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(simp add: trm.inject) +apply(rule conjI) +apply(simp add: alpha calc_atm fresh_atm fresh_prod) +apply(rule sym) +apply(simp add: alpha calc_atm fresh_atm fresh_prod) +done + +lemma lookup_csubst: + assumes a: "a\(\n,\c)" + shows "lookup y c \n ((a,x,P)#\c) = (lookup y c \n \c){a:=(x).P}" +using a +apply(induct \n) +apply(auto simp add: fresh_prod fresh_list_cons) +apply(simp add: lookupa_csubst) +apply(simp add: lookupa_freshness forget fresh_atm fresh_prod) +apply(rule lookupb_csubst) +apply(simp) +apply(auto simp add: lookupb_freshness forget fresh_atm fresh_prod) +done + +lemma lookup_fresh: + assumes a: "x\(\n,\c)" + shows "lookup x c \n \c = lookupa x c \c" +using a +apply(induct \n) +apply(auto simp add: fresh_prod fresh_list_cons fresh_atm) +done + +lemma lookup_unicity: + assumes a: "lookup x a \n \c= Ax y b" "b\(\c,\n)" "y\(\c,\n)" + shows "x=y \ a=b" +using a +apply(induct \n) +apply(auto simp add: trm.inject fresh_list_cons fresh_prod fresh_atm) +apply(drule lookupa_unicity) +apply(simp)+ +apply(drule lookupa_unicity) +apply(simp)+ +apply(case_tac "x=aa") +apply(auto) +apply(drule lookupb_unicity) +apply(simp add: fresh_atm) +apply(simp) +apply(simp) +apply(case_tac "x=aa") +apply(auto) +apply(drule lookupb_unicity) +apply(simp add: fresh_atm) +apply(simp) +apply(simp) +done + +lemma lookup_freshness: + fixes a::"coname" + and x::"name" + shows "a\(c,\c,\n) \ a\lookup y c \n \c" + and "x\(y,\c,\n) \ x\lookup y c \n \c" +apply(induct \n) +apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm) +apply(simp add: fresh_atm fresh_prod lookupa_freshness) +apply(simp add: fresh_atm fresh_prod lookupa_freshness) +apply(simp add: fresh_atm fresh_prod lookupb_freshness) +apply(simp add: fresh_atm fresh_prod lookupb_freshness) +done + +lemma lookupc_freshness: + fixes a::"coname" + and x::"name" + shows "a\(\c,c) \ a\lookupc y c \c" + and "x\(\c,y) \ x\lookupc y c \c" +apply(induct \c) +apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm) +apply(rule rename_fresh) +apply(simp add: fresh_atm) +apply(rule rename_fresh) +apply(simp add: fresh_atm) +done + +lemma lookupc_fresh: + assumes a: "y\\n" + shows "lookupc y a \n = Ax y a" +using a +apply(induct \n) +apply(auto simp add: fresh_prod fresh_list_cons fresh_atm) +done + +lemma lookupc_nmaps: + assumes a: "\n nmaps x to Some (c,P)" + shows "lookupc x a \n = P[c\c>a]" +using a +apply(induct \n) +apply(auto) +done + +lemma lookupc_unicity: + assumes a: "lookupc y a \n = Ax x b" "x\\n" + shows "y=x" +using a +apply(induct \n) +apply(auto simp add: trm.inject fresh_list_cons fresh_prod) +apply(case_tac "y=aa") +apply(auto) +apply(subgoal_tac "x\(ba[aa\c>a])") +apply(simp add: fresh_atm) +apply(rule rename_fresh) +apply(simp) +done + +lemma lookupd_fresh: + assumes a: "a\\c" + shows "lookupd y a \c = Ax y a" +using a +apply(induct \c) +apply(auto simp add: fresh_prod fresh_list_cons fresh_atm) +done + +lemma lookupd_unicity: + assumes a: "lookupd y a \c = Ax y b" "b\\c" + shows "a=b" +using a +apply(induct \c) +apply(auto simp add: trm.inject fresh_list_cons fresh_prod) +apply(case_tac "a=aa") +apply(auto) +apply(subgoal_tac "b\(ba[aa\n>y])") +apply(simp add: fresh_atm) +apply(rule rename_fresh) +apply(simp) +done + +lemma lookupd_freshness: + fixes a::"coname" + and x::"name" + shows "a\(\c,c) \ a\lookupd y c \c" + and "x\(\c,y) \ x\lookupd y c \c" +apply(induct \c) +apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm) +apply(rule rename_fresh) +apply(simp add: fresh_atm) +apply(rule rename_fresh) +apply(simp add: fresh_atm) +done + +lemma lookupd_cmaps: + assumes a: "\c cmaps a to Some (x,P)" + shows "lookupd y a \c = P[x\n>y]" +using a +apply(induct \c) +apply(auto) +done + +nominal_primrec (freshness_context: "\n::(name\coname\trm)") + stn :: "trm\(name\coname\trm) list\trm" +where + "stn (Ax x a) \n = lookupc x a \n" +| "\a\(N,\n);x\(M,\n)\ \ stn (Cut .M (x).N) \n = (Cut .M (x).N)" +| "x\\n \ stn (NotR (x).M a) \n = (NotR (x).M a)" +| "a\\n \stn (NotL .M x) \n = (NotL .M x)" +| "\a\(N,d,b,\n);b\(M,d,a,\n)\ \ stn (AndR .M .N d) \n = (AndR .M .N d)" +| "x\(z,\n) \ stn (AndL1 (x).M z) \n = (AndL1 (x).M z)" +| "x\(z,\n) \ stn (AndL2 (x).M z) \n = (AndL2 (x).M z)" +| "a\(b,\n) \ stn (OrR1 .M b) \n = (OrR1 .M b)" +| "a\(b,\n) \ stn (OrR2 .M b) \n = (OrR2 .M b)" +| "\x\(N,z,u,\n);u\(M,z,x,\n)\ \ stn (OrL (x).M (u).N z) \n = (OrL (x).M (u).N z)" +| "\a\(b,\n);x\\n\ \ stn (ImpR (x)..M b) \n = (ImpR (x)..M b)" +| "\a\(N,\n);x\(M,z,\n)\ \ stn (ImpL .M (x).N z) \n = (ImpL .M (x).N z)" +apply(finite_guess)+ +apply(rule TrueI)+ +apply(simp add: abs_fresh abs_supp fin_supp)+ +apply(fresh_guess)+ +done + +nominal_primrec (freshness_context: "\c::(coname\name\trm)") + stc :: "trm\(coname\name\trm) list\trm" +where + "stc (Ax x a) \c = lookupd x a \c" +| "\a\(N,\c);x\(M,\c)\ \ stc (Cut .M (x).N) \c = (Cut .M (x).N)" +| "x\\c \ stc (NotR (x).M a) \c = (NotR (x).M a)" +| "a\\c \ stc (NotL .M x) \c = (NotL .M x)" +| "\a\(N,d,b,\c);b\(M,d,a,\c)\ \ stc (AndR .M .N d) \c = (AndR .M .N d)" +| "x\(z,\c) \ stc (AndL1 (x).M z) \c = (AndL1 (x).M z)" +| "x\(z,\c) \ stc (AndL2 (x).M z) \c = (AndL2 (x).M z)" +| "a\(b,\c) \ stc (OrR1 .M b) \c = (OrR1 .M b)" +| "a\(b,\c) \ stc (OrR2 .M b) \c = (OrR2 .M b)" +| "\x\(N,z,u,\c);u\(M,z,x,\c)\ \ stc (OrL (x).M (u).N z) \c = (OrL (x).M (u).N z)" +| "\a\(b,\c);x\\c\ \ stc (ImpR (x)..M b) \c = (ImpR (x)..M b)" +| "\a\(N,\c);x\(M,z,\c)\ \ stc (ImpL .M (x).N z) \c = (ImpL .M (x).N z)" +apply(finite_guess)+ +apply(rule TrueI)+ +apply(simp add: abs_fresh abs_supp fin_supp)+ +apply(fresh_guess)+ +done + +lemma stn_eqvt[eqvt]: + fixes pi1::"name prm" + and pi2::"coname prm" + shows "(pi1\(stn M \n)) = stn (pi1\M) (pi1\\n)" + and "(pi2\(stn M \n)) = stn (pi2\M) (pi2\\n)" +apply - +apply(nominal_induct M avoiding: \n rule: trm.strong_induct) +apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm) +apply(nominal_induct M avoiding: \n rule: trm.strong_induct) +apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm) +done + +lemma stc_eqvt[eqvt]: + fixes pi1::"name prm" + and pi2::"coname prm" + shows "(pi1\(stc M \c)) = stc (pi1\M) (pi1\\c)" + and "(pi2\(stc M \c)) = stc (pi2\M) (pi2\\c)" +apply - +apply(nominal_induct M avoiding: \c rule: trm.strong_induct) +apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm) +apply(nominal_induct M avoiding: \c rule: trm.strong_induct) +apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm) +done + +lemma stn_fresh: + fixes a::"coname" + and x::"name" + shows "a\(\n,M) \ a\stn M \n" + and "x\(\n,M) \ x\stn M \n" +apply(nominal_induct M avoiding: \n a x rule: trm.strong_induct) +apply(auto simp add: abs_fresh fresh_prod fresh_atm) +apply(rule lookupc_freshness) +apply(simp add: fresh_atm) +apply(rule lookupc_freshness) +apply(simp add: fresh_atm) +done + +lemma stc_fresh: + fixes a::"coname" + and x::"name" + shows "a\(\c,M) \ a\stc M \c" + and "x\(\c,M) \ x\stc M \c" +apply(nominal_induct M avoiding: \c a x rule: trm.strong_induct) +apply(auto simp add: abs_fresh fresh_prod fresh_atm) +apply(rule lookupd_freshness) +apply(simp add: fresh_atm) +apply(rule lookupd_freshness) +apply(simp add: fresh_atm) +done + +lemma option_case_eqvt1[eqvt_force]: + fixes pi1::"name prm" + and pi2::"coname prm" + and B::"(name\trm) option" + and r::"trm" + shows "(pi1\(case B of Some (x,P) \ s x P | None \ r)) = + (case (pi1\B) of Some (x,P) \ (pi1\s) x P | None \ (pi1\r))" + and "(pi2\(case B of Some (x,P) \ s x P| None \ r)) = + (case (pi2\B) of Some (x,P) \ (pi2\s) x P | None \ (pi2\r))" +apply(cases "B") +apply(auto) +apply(perm_simp) +apply(cases "B") +apply(auto) +apply(perm_simp) +done + +lemma option_case_eqvt2[eqvt_force]: + fixes pi1::"name prm" + and pi2::"coname prm" + and B::"(coname\trm) option" + and r::"trm" + shows "(pi1\(case B of Some (x,P) \ s x P | None \ r)) = + (case (pi1\B) of Some (x,P) \ (pi1\s) x P | None \ (pi1\r))" + and "(pi2\(case B of Some (x,P) \ s x P| None \ r)) = + (case (pi2\B) of Some (x,P) \ (pi2\s) x P | None \ (pi2\r))" +apply(cases "B") +apply(auto) +apply(perm_simp) +apply(cases "B") +apply(auto) +apply(perm_simp) +done + +nominal_primrec (freshness_context: "(\n::(name\coname\trm) list,\c::(coname\name\trm) list)") + psubst :: "(name\coname\trm) list\(coname\name\trm) list\trm\trm" ("_,_<_>" [100,100,100] 100) +where + "\n,\c = lookup x a \n \c" +| "\a\(N,\n,\c);x\(M,\n,\c)\ \ \n,\c.M (x).N> = + Cut .(if \x. M=Ax x a then stn M \n else \n,\c) + (x).(if \a. N=Ax x a then stc N \c else \n,\c)" +| "x\(\n,\c) \ \n,\c = + (case (findc \c a) of + Some (u,P) \ fresh_fun (\a'. Cut .NotR (x).(\n,\c) a' (u).P) + | None \ NotR (x).(\n,\c) a)" +| "a\(\n,\c) \ \n,\c.M x> = + (case (findn \n x) of + Some (c,P) \ fresh_fun (\x'. Cut .P (x').(NotL .(\n,\c) x')) + | None \ NotL .(\n,\c) x)" +| "\a\(N,c,\n,\c);b\(M,c,\n,\c);b\a\ \ (\n,\c.M .N c>) = + (case (findc \c c) of + Some (x,P) \ fresh_fun (\a'. Cut .(AndR .(\n,\c) .(\n,\c) a') (x).P) + | None \ AndR .(\n,\c) .(\n,\c) c)" +| "x\(z,\n,\c) \ (\n,\c) = + (case (findn \n z) of + Some (c,P) \ fresh_fun (\z'. Cut .P (z').AndL1 (x).(\n,\c) z') + | None \ AndL1 (x).(\n,\c) z)" +| "x\(z,\n,\c) \ (\n,\c) = + (case (findn \n z) of + Some (c,P) \ fresh_fun (\z'. Cut .P (z').AndL2 (x).(\n,\c) z') + | None \ AndL2 (x).(\n,\c) z)" +| "\x\(N,z,\n,\c);u\(M,z,\n,\c);x\u\ \ (\n,\c) = + (case (findn \n z) of + Some (c,P) \ fresh_fun (\z'. Cut .P (z').OrL (x).(\n,\c) (u).(\n,\c) z') + | None \ OrL (x).(\n,\c) (u).(\n,\c) z)" +| "a\(b,\n,\c) \ (\n,\c.M b>) = + (case (findc \c b) of + Some (x,P) \ fresh_fun (\a'. Cut .OrR1 .(\n,\c) a' (x).P) + | None \ OrR1 .(\n,\c) b)" +| "a\(b,\n,\c) \ (\n,\c.M b>) = + (case (findc \c b) of + Some (x,P) \ fresh_fun (\a'. Cut .OrR2 .(\n,\c) a' (x).P) + | None \ OrR2 .(\n,\c) b)" +| "\a\(b,\n,\c); x\(\n,\c)\ \ (\n,\c.M b>) = + (case (findc \c b) of + Some (z,P) \ fresh_fun (\a'. Cut .ImpR (x)..(\n,\c) a' (z).P) + | None \ ImpR (x)..(\n,\c) b)" +| "\a\(N,\n,\c); x\(z,M,\n,\c)\ \ (\n,\c.M (x).N z>) = + (case (findn \n z) of + Some (c,P) \ fresh_fun (\z'. Cut .P (z').ImpL .(\n,\c) (x).(\n,\c) z') + | None \ ImpL .(\n,\c) (x).(\n,\c) z)" +apply(finite_guess)+ +apply(rule TrueI)+ +apply(simp add: abs_fresh stc_fresh) +apply(simp add: abs_fresh stn_fresh) +apply(case_tac "findc \c x3") +apply(simp add: abs_fresh) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp (no_asm)) +apply(drule cmaps_fresh) +apply(auto simp add: fresh_prod)[1] +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(case_tac "findn \n x3") +apply(simp add: abs_fresh) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp (no_asm)) +apply(drule nmaps_fresh) +apply(auto simp add: fresh_prod)[1] +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(case_tac "findc \c x5") +apply(simp add: abs_fresh) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp (no_asm)) +apply(drule cmaps_fresh) +apply(auto simp add: fresh_prod)[1] +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(case_tac "findc \c x5") +apply(simp add: abs_fresh) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp (no_asm)) +apply(drule_tac x="x3" in cmaps_fresh) +apply(auto simp add: fresh_prod)[1] +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(case_tac "findn \n x3") +apply(simp add: abs_fresh) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp (no_asm)) +apply(drule nmaps_fresh) +apply(auto simp add: fresh_prod)[1] +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(case_tac "findn \n x3") +apply(simp add: abs_fresh) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp (no_asm)) +apply(drule nmaps_fresh) +apply(auto simp add: fresh_prod)[1] +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(case_tac "findc \c x3") +apply(simp add: abs_fresh) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp (no_asm)) +apply(drule cmaps_fresh) +apply(auto simp add: fresh_prod)[1] +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(case_tac "findc \c x3") +apply(simp add: abs_fresh) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp (no_asm)) +apply(drule cmaps_fresh) +apply(auto simp add: fresh_prod)[1] +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(case_tac "findn \n x5") +apply(simp add: abs_fresh) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp (no_asm)) +apply(drule nmaps_fresh) +apply(auto simp add: fresh_prod)[1] +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(case_tac "findn \n x5") +apply(simp add: abs_fresh) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp (no_asm)) +apply(drule_tac a="x3" in nmaps_fresh) +apply(auto simp add: fresh_prod)[1] +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(case_tac "findc \c x4") +apply(simp add: abs_fresh abs_supp fin_supp) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp (no_asm)) +apply(drule cmaps_fresh) +apply(auto simp add: fresh_prod)[1] +apply(simp add: abs_fresh fresh_prod fresh_atm abs_supp fin_supp) +apply(case_tac "findc \c x4") +apply(simp add: abs_fresh abs_supp fin_supp) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp (no_asm)) +apply(drule_tac x="x2" in cmaps_fresh) +apply(auto simp add: fresh_prod)[1] +apply(simp add: abs_fresh fresh_prod fresh_atm abs_supp fin_supp) +apply(case_tac "findn \n x5") +apply(simp add: abs_fresh) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp (no_asm)) +apply(drule nmaps_fresh) +apply(auto simp add: fresh_prod)[1] +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(case_tac "findn \n x5") +apply(simp add: abs_fresh) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp (no_asm)) +apply(drule_tac a="x3" in nmaps_fresh) +apply(auto simp add: fresh_prod)[1] +apply(simp add: abs_fresh fresh_prod fresh_atm) +apply(fresh_guess)+ +done + +lemma case_cong: + assumes a: "B1=B2" "x1=x2" "y1=y2" + shows "(case B1 of None \ x1 | Some (x,P) \ y1 x P) = (case B2 of None \ x2 | Some (x,P) \ y2 x P)" +using a +apply(auto) +done + +lemma find_maps: + shows "\c cmaps a to (findc \c a)" + and "\n nmaps x to (findn \n x)" +apply(auto) +done + +lemma psubst_eqvt[eqvt]: + fixes pi1::"name prm" + and pi2::"coname prm" + shows "pi1\(\n,\c) = (pi1\\n),(pi1\\c)<(pi1\M)>" + and "pi2\(\n,\c) = (pi2\\n),(pi2\\c)<(pi2\M)>" +apply(nominal_induct M avoiding: \n \c rule: trm.strong_induct) +apply(auto simp add: eq_bij fresh_bij eqvts perm_pi_simp) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +apply(rule case_cong) +apply(rule find_maps) +apply(simp) +apply(perm_simp add: eqvts) +done + +lemma ax_psubst: + assumes a: "\n,\c = Ax x a" + and b: "a\(\n,\c)" "x\(\n,\c)" + shows "M = Ax x a" +using a b +apply(nominal_induct M avoiding: \n \c rule: trm.strong_induct) +apply(auto) +apply(drule lookup_unicity) +apply(simp)+ +apply(case_tac "findc \c coname") +apply(simp) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(simp) +apply(case_tac "findn \n name") +apply(simp) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(simp) +apply(case_tac "findc \c coname3") +apply(simp) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(simp) +apply(case_tac "findn \n name2") +apply(simp) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(simp) +apply(case_tac "findn \n name2") +apply(simp) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(simp) +apply(case_tac "findc \c coname2") +apply(simp) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(simp) +apply(case_tac "findc \c coname2") +apply(simp) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(simp) +apply(case_tac "findn \n name3") +apply(simp) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(simp) +apply(case_tac "findc \c coname2") +apply(simp) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(simp) +apply(case_tac "findn \n name2") +apply(simp) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(simp) +done + +lemma better_Cut_substc1: + assumes a: "a\(P,b)" "b\N" + shows "(Cut .M (x).N){b:=(y).P} = Cut .(M{b:=(y).P}) (x).N" +using a +apply - +apply(generate_fresh "coname") +apply(generate_fresh "name") +apply(subgoal_tac "Cut .M (x).N = Cut .([(c,a)]\M) (ca).([(ca,x)]\N)") +apply(simp) +apply(rule trans) +apply(rule better_Cut_substc) +apply(simp) +apply(simp add: abs_fresh) +apply(auto)[1] +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm fresh_atm) +apply(subgoal_tac"b\([(ca,x)]\N)") +apply(simp add: forget) +apply(simp add: trm.inject) +apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1] +apply(perm_simp) +apply(simp add: fresh_left calc_atm) +apply(simp add: trm.inject) +apply(rule conjI) +apply(rule sym) +apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1] +apply(rule sym) +apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1] +done + +lemma better_Cut_substc2: + assumes a: "x\(y,P)" "b\(a,M)" "N\Ax x b" + shows "(Cut .M (x).N){b:=(y).P} = Cut .M (x).(N{b:=(y).P})" +using a +apply - +apply(generate_fresh "coname") +apply(generate_fresh "name") +apply(subgoal_tac "Cut .M (x).N = Cut .([(c,a)]\M) (ca).([(ca,x)]\N)") +apply(simp) +apply(rule trans) +apply(rule better_Cut_substc) +apply(simp) +apply(simp add: abs_fresh) +apply(auto)[1] +apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst]) +apply(simp add: calc_atm fresh_atm fresh_prod) +apply(subgoal_tac"b\([(c,a)]\M)") +apply(simp add: forget) +apply(simp add: trm.inject) +apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1] +apply(perm_simp) +apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(simp add: trm.inject) +apply(rule conjI) +apply(rule sym) +apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1] +apply(rule sym) +apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1] +done + +lemma better_Cut_substn1: + assumes a: "y\(x,N)" "a\(b,P)" "M\Ax y a" + shows "(Cut .M (x).N){y:=.P} = Cut .(M{y:=.P}) (x).N" +using a +apply - +apply(generate_fresh "coname") +apply(generate_fresh "name") +apply(subgoal_tac "Cut .M (x).N = Cut .([(c,a)]\M) (ca).([(ca,x)]\N)") +apply(simp) +apply(rule trans) +apply(rule better_Cut_substn) +apply(simp add: abs_fresh) +apply(simp add: abs_fresh) +apply(auto)[1] +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm fresh_atm fresh_prod) +apply(subgoal_tac"y\([(ca,x)]\N)") +apply(simp add: forget) +apply(simp add: trm.inject) +apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1] +apply(perm_simp) +apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] +apply(simp add: trm.inject) +apply(rule conjI) +apply(rule sym) +apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1] +apply(rule sym) +apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1] +done + +lemma better_Cut_substn2: + assumes a: "x\(P,y)" "y\M" + shows "(Cut .M (x).N){y:=.P} = Cut .M (x).(N{y:=.P})" +using a +apply - +apply(generate_fresh "coname") +apply(generate_fresh "name") +apply(subgoal_tac "Cut .M (x).N = Cut .([(c,a)]\M) (ca).([(ca,x)]\N)") +apply(simp) +apply(rule trans) +apply(rule better_Cut_substn) +apply(simp add: abs_fresh) +apply(simp add: abs_fresh) +apply(auto)[1] +apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst]) +apply(simp add: calc_atm fresh_atm) +apply(subgoal_tac"y\([(c,a)]\M)") +apply(simp add: forget) +apply(simp add: trm.inject) +apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1] +apply(perm_simp) +apply(simp add: fresh_left calc_atm) +apply(simp add: trm.inject) +apply(rule conjI) +apply(rule sym) +apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1] +apply(rule sym) +apply(simp add: alpha eqvts calc_atm fresh_prod fresh_atm subst_fresh)[1] +done + +lemma psubst_fresh_name: + fixes x::"name" + assumes a: "x\\n" "x\\c" "x\M" + shows "x\\n,\c" +using a +apply(nominal_induct M avoiding: x \n \c rule: trm.strong_induct) +apply(simp add: lookup_freshness) +apply(auto simp add: abs_fresh)[1] +apply(simp add: lookupc_freshness) +apply(simp add: lookupc_freshness) +apply(simp add: lookupc_freshness) +apply(simp add: lookupd_freshness) +apply(simp add: lookupd_freshness) +apply(simp add: lookupc_freshness) +apply(simp) +apply(case_tac "findc \c coname") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh) +apply(simp) +apply(case_tac "findn \n name") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh) +apply(simp) +apply(case_tac "findc \c coname3") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh) +apply(simp) +apply(case_tac "findn \n name2") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh) +apply(simp) +apply(case_tac "findn \n name2") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh) +apply(simp) +apply(case_tac "findc \c coname2") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh) +apply(simp) +apply(case_tac "findc \c coname2") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh) +apply(simp) +apply(case_tac "findn \n name3") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh) +apply(simp) +apply(case_tac "findc \c coname2") +apply(auto simp add: abs_fresh abs_supp fin_supp)[1] +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(simp add: abs_fresh abs_supp fin_supp fresh_prod fresh_atm cmaps_fresh) +apply(simp) +apply(case_tac "findn \n name2") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh) +done + +lemma psubst_fresh_coname: + fixes a::"coname" + assumes a: "a\\n" "a\\c" "a\M" + shows "a\\n,\c" +using a +apply(nominal_induct M avoiding: a \n \c rule: trm.strong_induct) +apply(simp add: lookup_freshness) +apply(auto simp add: abs_fresh)[1] +apply(simp add: lookupd_freshness) +apply(simp add: lookupd_freshness) +apply(simp add: lookupc_freshness) +apply(simp add: lookupd_freshness) +apply(simp add: lookupc_freshness) +apply(simp add: lookupd_freshness) +apply(simp) +apply(case_tac "findc \c coname") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh) +apply(simp) +apply(case_tac "findn \n name") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh) +apply(simp) +apply(case_tac "findc \c coname3") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh) +apply(simp) +apply(case_tac "findn \n name2") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh) +apply(simp) +apply(case_tac "findn \n name2") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh) +apply(simp) +apply(case_tac "findc \c coname2") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh) +apply(simp) +apply(case_tac "findc \c coname2") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh) +apply(simp) +apply(case_tac "findn \n name3") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh) +apply(simp) +apply(case_tac "findc \c coname2") +apply(auto simp add: abs_fresh abs_supp fin_supp)[1] +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(simp add: abs_fresh abs_supp fin_supp fresh_prod fresh_atm cmaps_fresh) +apply(simp) +apply(case_tac "findn \n name2") +apply(auto simp add: abs_fresh)[1] +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh) +done + +lemma psubst_csubst: + assumes a: "a\(\n,\c)" + shows "\n,((a,x,P)#\c) = ((\n,\c){a:=(x).P})" +using a +apply(nominal_induct M avoiding: a x \n \c P rule: trm.strong_induct) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(simp add: lookup_csubst) +apply(simp add: fresh_list_cons fresh_prod) +apply(auto)[1] +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc) +apply(simp) +apply(simp add: abs_fresh fresh_atm) +apply(simp add: lookupd_fresh) +apply(subgoal_tac "a\lookupc xa coname \n") +apply(simp add: forget) +apply(simp add: trm.inject) +apply(rule sym) +apply(simp add: alpha nrename_swap fresh_atm) +apply(rule lookupc_freshness) +apply(simp add: fresh_atm) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc) +apply(simp) +apply(simp add: abs_fresh fresh_atm) +apply(simp) +apply(rule conjI) +apply(rule impI) +apply(simp add: lookupd_unicity) +apply(rule impI) +apply(subgoal_tac "a\lookupc xa coname \n") +apply(subgoal_tac "a\lookupd name aa \c") +apply(simp add: forget) +apply(rule lookupd_freshness) +apply(simp add: fresh_atm) +apply(rule lookupc_freshness) +apply(simp add: fresh_atm) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc) +apply(simp) +apply(simp add: abs_fresh fresh_atm) +apply(simp) +apply(rule conjI) +apply(rule impI) +apply(drule ax_psubst) +apply(simp) +apply(simp) +apply(blast) +apply(rule impI) +apply(subgoal_tac "a\lookupc xa coname \n") +apply(simp add: forget) +apply(rule lookupc_freshness) +apply(simp add: fresh_atm) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc) +apply(simp) +apply(simp add: abs_fresh fresh_atm) +apply(simp) +apply(rule conjI) +apply(rule impI) +apply(simp add: trm.inject) +apply(rule sym) +apply(simp add: alpha) +apply(simp add: alpha nrename_swap fresh_atm) +apply(simp add: lookupd_fresh) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc) +apply(simp) +apply(simp add: abs_fresh fresh_atm) +apply(simp) +apply(rule conjI) +apply(rule impI) +apply(simp add: lookupd_unicity) +apply(rule impI) +apply(subgoal_tac "a\lookupd name aa \c") +apply(simp add: forget) +apply(rule lookupd_freshness) +apply(simp add: fresh_atm) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc) +apply(simp) +apply(simp add: abs_fresh fresh_atm) +apply(simp) +apply(rule impI) +apply(drule ax_psubst) +apply(simp) +apply(simp) +apply(blast) +(* NotR *) +apply(simp) +apply(case_tac "findc \c coname") +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(drule cmaps_false) +apply(assumption) +apply(simp) +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc1) +apply(simp) +apply(simp add: cmaps_fresh) +apply(auto simp add: fresh_prod fresh_atm)[1] +(* NotL *) +apply(simp) +apply(case_tac "findn \n name") +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(drule_tac a="a" in nmaps_fresh) +apply(assumption) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc2) +apply(simp) +apply(simp) +apply(simp) +apply(simp) +(* AndR *) +apply(simp) +apply(case_tac "findc \c coname3") +apply(simp) +apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(drule cmaps_false) +apply(assumption) +apply(simp) +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc1) +apply(simp) +apply(simp add: cmaps_fresh) +apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1] +(* AndL1 *) +apply(simp) +apply(case_tac "findn \n name2") +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(drule_tac a="a" in nmaps_fresh) +apply(assumption) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc2) +apply(simp) +apply(simp) +apply(simp) +apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1] +(* AndL2 *) +apply(simp) +apply(case_tac "findn \n name2") +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(drule_tac a="a" in nmaps_fresh) +apply(assumption) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc2) +apply(simp) +apply(simp) +apply(simp) +apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1] +(* OrR1 *) +apply(simp) +apply(case_tac "findc \c coname2") +apply(simp) +apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(drule cmaps_false) +apply(assumption) +apply(simp) +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc1) +apply(simp) +apply(simp add: cmaps_fresh) +apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1] +(* OrR2 *) +apply(simp) +apply(case_tac "findc \c coname2") +apply(simp) +apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(drule cmaps_false) +apply(assumption) +apply(simp) +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc1) +apply(simp) +apply(simp add: cmaps_fresh) +apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1] +(* OrL *) +apply(simp) +apply(case_tac "findn \n name3") +apply(simp) +apply(auto simp add: fresh_list_cons psubst_fresh_name fresh_atm fresh_prod)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(drule_tac a="a" in nmaps_fresh) +apply(assumption) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc2) +apply(simp) +apply(simp) +apply(simp) +apply(auto simp add: psubst_fresh_name fresh_prod fresh_atm)[1] +(* ImpR *) +apply(simp) +apply(case_tac "findc \c coname2") +apply(simp) +apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(drule cmaps_false) +apply(assumption) +apply(simp) +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc1) +apply(simp) +apply(simp add: cmaps_fresh) +apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1] +(* ImpL *) +apply(simp) +apply(case_tac "findn \n name2") +apply(simp) +apply(auto simp add: fresh_list_cons psubst_fresh_coname psubst_fresh_name fresh_atm fresh_prod)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(simp add: abs_fresh subst_fresh) +apply(drule_tac a="a" in nmaps_fresh) +apply(assumption) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substc2) +apply(simp) +apply(simp) +apply(simp) +apply(auto simp add: psubst_fresh_coname psubst_fresh_name fresh_prod fresh_atm)[1] +done + +lemma psubst_nsubst: + assumes a: "x\(\n,\c)" + shows "((x,a,P)#\n),\c = ((\n,\c){x:=.P})" +using a +apply(nominal_induct M avoiding: a x \n \c P rule: trm.strong_induct) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(simp add: lookup_fresh) +apply(rule lookupb_lookupa) +apply(simp) +apply(rule sym) +apply(rule forget) +apply(rule lookup_freshness) +apply(simp add: fresh_atm) +apply(auto simp add: lookupc_freshness fresh_list_cons fresh_prod)[1] +apply(simp add: lookupc_fresh) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn) +apply(simp add: abs_fresh) +apply(simp add: abs_fresh fresh_atm) +apply(simp add: lookupd_fresh) +apply(subgoal_tac "x\lookupd name aa \c") +apply(simp add: forget) +apply(simp add: trm.inject) +apply(rule sym) +apply(simp add: alpha crename_swap fresh_atm) +apply(rule lookupd_freshness) +apply(simp add: fresh_atm) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn) +apply(simp add: abs_fresh) +apply(simp add: abs_fresh fresh_atm) +apply(simp) +apply(rule conjI) +apply(rule impI) +apply(simp add: lookupc_unicity) +apply(rule impI) +apply(subgoal_tac "x\lookupc xa coname \n") +apply(subgoal_tac "x\lookupd name aa \c") +apply(simp add: forget) +apply(rule lookupd_freshness) +apply(simp add: fresh_atm) +apply(rule lookupc_freshness) +apply(simp add: fresh_atm) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn) +apply(simp add: abs_fresh) +apply(simp add: abs_fresh fresh_atm) +apply(simp) +apply(rule conjI) +apply(rule impI) +apply(simp add: trm.inject) +apply(rule sym) +apply(simp add: alpha crename_swap fresh_atm) +apply(rule impI) +apply(simp add: lookupc_fresh) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn) +apply(simp add: abs_fresh) +apply(simp add: abs_fresh fresh_atm) +apply(simp) +apply(rule conjI) +apply(rule impI) +apply(simp add: lookupc_unicity) +apply(rule impI) +apply(subgoal_tac "x\lookupc xa coname \n") +apply(simp add: forget) +apply(rule lookupc_freshness) +apply(simp add: fresh_prod fresh_atm) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn) +apply(simp add: abs_fresh) +apply(simp add: abs_fresh fresh_atm) +apply(simp) +apply(rule conjI) +apply(rule impI) +apply(drule ax_psubst) +apply(simp) +apply(simp) +apply(simp) +apply(blast) +apply(rule impI) +apply(subgoal_tac "x\lookupd name aa \c") +apply(simp add: forget) +apply(rule lookupd_freshness) +apply(simp add: fresh_atm) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn) +apply(simp add: abs_fresh) +apply(simp add: abs_fresh fresh_atm) +apply(simp) +apply(rule impI) +apply(drule ax_psubst) +apply(simp) +apply(simp) +apply(blast) +(* NotR *) +apply(simp) +apply(case_tac "findc \c coname") +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn1) +apply(simp add: cmaps_fresh) +apply(simp) +apply(simp) +apply(simp) +(* NotL *) +apply(simp) +apply(case_tac "findn \n name") +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(drule nmaps_false) +apply(simp) +apply(simp) +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn2) +apply(simp) +apply(simp add: nmaps_fresh) +apply(simp add: fresh_prod fresh_atm) +(* AndR *) +apply(simp) +apply(case_tac "findc \c coname3") +apply(simp) +apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn1) +apply(simp add: cmaps_fresh) +apply(simp) +apply(simp) +apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1] +(* AndL1 *) +apply(simp) +apply(case_tac "findn \n name2") +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(drule nmaps_false) +apply(simp) +apply(simp) +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn2) +apply(simp) +apply(simp add: nmaps_fresh) +apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1] +(* AndL2 *) +apply(simp) +apply(case_tac "findn \n name2") +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(drule nmaps_false) +apply(simp) +apply(simp) +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn2) +apply(simp) +apply(simp add: nmaps_fresh) +apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1] +(* OrR1 *) +apply(simp) +apply(case_tac "findc \c coname2") +apply(simp) +apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn1) +apply(simp add: cmaps_fresh) +apply(simp) +apply(simp) +apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1] +(* OrR2 *) +apply(simp) +apply(case_tac "findc \c coname2") +apply(simp) +apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn1) +apply(simp add: cmaps_fresh) +apply(simp) +apply(simp) +apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1] +(* OrL *) +apply(simp) +apply(case_tac "findn \n name3") +apply(simp) +apply(auto simp add: fresh_list_cons psubst_fresh_name fresh_atm fresh_prod)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(drule nmaps_false) +apply(simp) +apply(simp) +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn2) +apply(simp) +apply(simp add: nmaps_fresh) +apply(auto simp add: psubst_fresh_name fresh_prod fresh_atm)[1] +(* ImpR *) +apply(simp) +apply(case_tac "findc \c coname2") +apply(simp) +apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn1) +apply(simp add: cmaps_fresh) +apply(simp) +apply(simp) +apply(auto simp add: psubst_fresh_coname fresh_prod fresh_atm)[1] +(* ImpL *) +apply(simp) +apply(case_tac "findn \n name2") +apply(simp) +apply(auto simp add: fresh_list_cons psubst_fresh_coname psubst_fresh_name fresh_atm fresh_prod)[1] +apply(simp) +apply(auto simp add: fresh_list_cons fresh_prod)[1] +apply(drule nmaps_false) +apply(simp) +apply(simp) +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(fresh_fun_simp) +apply(rule sym) +apply(rule trans) +apply(rule better_Cut_substn2) +apply(simp) +apply(simp add: nmaps_fresh) +apply(auto simp add: psubst_fresh_coname psubst_fresh_name fresh_prod fresh_atm)[1] +done + +definition + ncloses :: "(name\coname\trm) list\(name\ty) list \ bool" ("_ ncloses _" [55,55] 55) +where + "\n ncloses \ \ \x B. ((x,B) \ set \ \ (\c P. \n nmaps x to Some (c,P) \ :P \ (\\)))" + +definition + ccloses :: "(coname\name\trm) list\(coname\ty) list \ bool" ("_ ccloses _" [55,55] 55) +where + "\c ccloses \ \ \a B. ((a,B) \ set \ \ (\x P. \c cmaps a to Some (x,P) \ (x):P \ (\(B)\)))" + +lemma ncloses_elim: + assumes a: "(x,B) \ set \" + and b: "\n ncloses \" + shows "\c P. \n nmaps x to Some (c,P) \ :P \ (\\)" +using a b by (auto simp add: ncloses_def) + +lemma ccloses_elim: + assumes a: "(a,B) \ set \" + and b: "\c ccloses \" + shows "\x P. \c cmaps a to Some (x,P) \ (x):P \ (\(B)\)" +using a b by (auto simp add: ccloses_def) + +lemma ncloses_subset: + assumes a: "\n ncloses \" + and b: "set \' \ set \" + shows "\n ncloses \'" +using a b by (auto simp add: ncloses_def) + +lemma ccloses_subset: + assumes a: "\c ccloses \" + and b: "set \' \ set \" + shows "\c ccloses \'" +using a b by (auto simp add: ccloses_def) + +lemma validc_fresh: + fixes a::"coname" + and \::"(coname\ty) list" + assumes a: "a\\" + shows "\(\B. (a,B)\set \)" +using a +apply(induct \) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm) +done + +lemma validn_fresh: + fixes x::"name" + and \::"(name\ty) list" + assumes a: "x\\" + shows "\(\B. (x,B)\set \)" +using a +apply(induct \) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm) +done + +lemma ccloses_extend: + assumes a: "\c ccloses \" "a\\" "a\\c" "(x):P\\(B)\" + shows "(a,x,P)#\c ccloses (a,B)#\" +using a +apply(simp add: ccloses_def) +apply(drule validc_fresh) +apply(auto) +done + +lemma ncloses_extend: + assumes a: "\n ncloses \" "x\\" "x\\n" ":P\\\" + shows "(x,a,P)#\n ncloses (x,B)#\" +using a +apply(simp add: ncloses_def) +apply(drule validn_fresh) +apply(auto) +done + + +text {* typing relation *} + +inductive + typing :: "ctxtn \ trm \ ctxtc \ bool" ("_ \ _ \ _" [100,100,100] 100) +where + TAx: "\validn \;validc \; (x,B)\set \; (a,B)\set \\ \ \ \ Ax x a \ \" +| TNotR: "\x\\; ((x,B)#\) \ M \ \; set \' = {(a,NOT B)}\set \; validc \'\ + \ \ \ NotR (x).M a \ \'" +| TNotL: "\a\\; \ \ M \ ((a,B)#\); set \' = {(x,NOT B)} \ set \; validn \'\ + \ \' \ NotL .M x \ \" +| TAndL1: "\x\(\,y); ((x,B1)#\) \ M \ \; set \' = {(y,B1 AND B2)} \ set \; validn \'\ + \ \' \ AndL1 (x).M y \ \" +| TAndL2: "\x\(\,y); ((x,B2)#\) \ M \ \; set \' = {(y,B1 AND B2)} \ set \; validn \'\ + \ \' \ AndL2 (x).M y \ \" +| TAndR: "\a\(\,N,c); b\(\,M,c); a\b; \ \ M \ ((a,B)#\); \ \ N \ ((b,C)#\); + set \' = {(c,B AND C)}\set \; validc \'\ + \ \ \ AndR .M .N c \ \'" +| TOrL: "\x\(\,N,z); y\(\,M,z); x\y; ((x,B)#\) \ M \ \; ((y,C)#\) \ N \ \; + set \' = {(z,B OR C)} \ set \; validn \'\ + \ \' \ OrL (x).M (y).N z \ \" +| TOrR1: "\a\(\,b); \ \ M \ ((a,B1)#\); set \' = {(b,B1 OR B2)}\set \; validc \'\ + \ \ \ OrR1 .M b \ \'" +| TOrR2: "\a\(\,b); \ \ M \ ((a,B2)#\); set \' = {(b,B1 OR B2)}\set \; validc \'\ + \ \ \ OrR2 .M b \ \'" +| TImpL: "\a\(\,N); x\(\,M,y); \ \ M \ ((a,B)#\); ((x,C)#\) \ N \ \; + set \' = {(y,B IMP C)} \ set \; validn \'\ + \ \' \ ImpL .M (x).N y \ \" +| TImpR: "\a\(\,b); x\\; ((x,B)#\) \ M \ ((a,C)#\); set \' = {(b,B IMP C)}\set \; validc \'\ + \ \ \ ImpR (x)..M b \ \'" +| TCut: "\a\(\,N); x\(\,M); \ \ M \ ((a,B)#\); ((x,B)#\) \ N \ \\ + \ \ \ Cut .M (x).N \ \" + +equivariance typing + +lemma fresh_set_member: + fixes x::"name" + and a::"coname" + shows "x\L \ e\set L \ x\e" + and "a\L \ e\set L \ a\e" +by (induct L) (auto simp add: fresh_list_cons) + +lemma fresh_subset: + fixes x::"name" + and a::"coname" + shows "x\L \ set L' \ set L \ x\L'" + and "a\L \ set L' \ set L \ a\L'" +apply(induct L' arbitrary: L) +apply(auto simp add: fresh_list_cons fresh_list_nil intro: fresh_set_member) +done + +lemma fresh_subset_ext: + fixes x::"name" + and a::"coname" + shows "x\L \ x\e \ set L' \ set (e#L) \ x\L'" + and "a\L \ a\e \ set L' \ set (e#L) \ a\L'" +apply(induct L' arbitrary: L) +apply(auto simp add: fresh_list_cons fresh_list_nil intro: fresh_set_member) +done + +lemma fresh_under_insert: + fixes x::"name" + and a::"coname" + and \::"ctxtn" + and \::"ctxtc" + shows "x\\ \ x\y \ set \' = insert (y,B) (set \) \ x\\'" + and "a\\ \ a\c \ set \' = insert (c,B) (set \) \ a\\'" +apply(rule fresh_subset_ext(1)) +apply(auto simp add: fresh_prod fresh_atm fresh_ty) +apply(rule fresh_subset_ext(2)) +apply(auto simp add: fresh_prod fresh_atm fresh_ty) +done + +nominal_inductive typing + apply (simp_all add: abs_fresh fresh_atm fresh_list_cons fresh_prod fresh_ty fresh_ctxt + fresh_list_append abs_supp fin_supp) + apply(auto intro: fresh_under_insert) + done + +lemma validn_elim: + assumes a: "validn ((x,B)#\)" + shows "validn \ \ x\\" +using a +apply(erule_tac validn.cases) +apply(auto) +done + +lemma validc_elim: + assumes a: "validc ((a,B)#\)" + shows "validc \ \ a\\" +using a +apply(erule_tac validc.cases) +apply(auto) +done + +lemma context_fresh: + fixes x::"name" + and a::"coname" + shows "x\\ \ \(\B. (x,B)\set \)" + and "a\\ \ \(\B. (a,B)\set \)" +apply - +apply(induct \) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm) +apply(induct \) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm) +done + +lemma typing_implies_valid: + assumes a: "\ \ M \ \" + shows "validn \ \ validc \" +using a +apply(nominal_induct rule: typing.strong_induct) +apply(auto dest: validn_elim validc_elim) +done + +lemma ty_perm: + fixes pi1::"name prm" + and pi2::"coname prm" + and B::"ty" + shows "pi1\B=B" and "pi2\B=B" +apply(nominal_induct B rule: ty.strong_induct) +apply(auto simp add: perm_string) +done + +lemma ctxt_perm: + fixes pi1::"name prm" + and pi2::"coname prm" + and \::"ctxtn" + and \::"ctxtc" + shows "pi2\\=\" and "pi1\\=\" +apply - +apply(induct \) +apply(auto simp add: calc_atm ty_perm) +apply(induct \) +apply(auto simp add: calc_atm ty_perm) +done + +lemma typing_Ax_elim1: + assumes a: "\ \ Ax x a \ ((a,B)#\)" + shows "(x,B)\set \" +using a +apply(erule_tac typing.cases) +apply(simp_all add: trm.inject) +apply(auto) +apply(auto dest: validc_elim context_fresh) +done + +lemma typing_Ax_elim2: + assumes a: "((x,B)#\) \ Ax x a \ \" + shows "(a,B)\set \" +using a +apply(erule_tac typing.cases) +apply(simp_all add: trm.inject) +apply(auto dest!: validn_elim context_fresh) +done + +lemma psubst_Ax_aux: + assumes a: "\c cmaps a to Some (y,N)" + shows "lookupb x a \c c P = Cut .P (y).N" +using a +apply(induct \c) +apply(auto) +done + +lemma psubst_Ax: + assumes a: "\n nmaps x to Some (c,P)" + and b: "\c cmaps a to Some (y,N)" + shows "\n,\c = Cut .P (y).N" +using a b +apply(induct \n) +apply(auto simp add: psubst_Ax_aux) +done + +lemma psubst_Cut: + assumes a: "\x. M\Ax x c" + and b: "\a. N\Ax x a" + and c: "c\(\n,\c,N)" "x\(\n,\c,M)" + shows "\n,\c.M (x).N> = Cut .(\n,\c) (x).(\n,\c)" +using a b c +apply(simp) +done + +lemma all_CAND: + assumes a: "\ \ M \ \" + and b: "\n ncloses \" + and c: "\c ccloses \" + shows "SNa (\n,\c)" +using a b c +proof(nominal_induct avoiding: \n \c rule: typing.strong_induct) + case (TAx \ \ x B a \n \c) + then show ?case + apply - + apply(drule ncloses_elim) + apply(assumption) + apply(drule ccloses_elim) + apply(assumption) + apply(erule exE)+ + apply(erule conjE)+ + apply(rule_tac s="Cut .P (xa).Pa" and t="\n,\c" in subst) + apply(rule sym) + apply(simp only: psubst_Ax) + apply(simp add: CUT_SNa) + done +next + case (TNotR x \ B M \ \' a \n \c) + then show ?case + apply(simp) + apply(subgoal_tac "(a,NOT B) \ set \'") + apply(drule ccloses_elim) + apply(assumption) + apply(erule exE)+ + apply(simp) + apply(generate_fresh "coname") + apply(fresh_fun_simp) + apply(rule_tac B="NOT B" in CUT_SNa) + apply(simp) + apply(rule disjI2) + apply(rule disjI2) + apply(rule_tac x="c" in exI) + apply(rule_tac x="x" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp) + apply(rule conjI) + apply(rule fic.intros) + apply(rule psubst_fresh_coname) + apply(simp) + apply(simp) + apply(simp) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGn_def) + apply(simp) + apply(rule_tac x="x" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp) + apply(rule allI)+ + apply(rule impI) + apply(simp add: psubst_nsubst[symmetric]) + apply(drule_tac x="(x,aa,Pa)#\n" in meta_spec) + apply(drule_tac x="\c" in meta_spec) + apply(drule meta_mp) + apply(rule ncloses_extend) + apply(assumption) + apply(assumption) + apply(assumption) + apply(assumption) + apply(drule meta_mp) + apply(rule ccloses_subset) + apply(assumption) + apply(blast) + apply(assumption) + apply(simp) + apply(blast) + done +next + case (TNotL a \ \ M B \' x \n \c) + then show ?case + apply(simp) + apply(subgoal_tac "(x,NOT B) \ set \'") + apply(drule ncloses_elim) + apply(assumption) + apply(erule exE)+ + apply(simp del: NEGc.simps) + apply(generate_fresh "name") + apply(fresh_fun_simp) + apply(rule_tac B="NOT B" in CUT_SNa) + apply(simp) + apply(rule NEG_intro) + apply(simp (no_asm)) + apply(rule disjI2) + apply(rule disjI2) + apply(rule_tac x="a" in exI) + apply(rule_tac x="ca" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp del: NEGc.simps) + apply(rule conjI) + apply(rule fin.intros) + apply(rule psubst_fresh_name) + apply(simp) + apply(simp) + apply(simp) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGc_def) + apply(simp (no_asm)) + apply(rule_tac x="a" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp (no_asm)) + apply(rule allI)+ + apply(rule impI) + apply(simp del: NEGc.simps add: psubst_csubst[symmetric]) + apply(drule_tac x="\n" in meta_spec) + apply(drule_tac x="(a,xa,Pa)#\c" in meta_spec) + apply(drule meta_mp) + apply(rule ncloses_subset) + apply(assumption) + apply(blast) + apply(drule meta_mp) + apply(rule ccloses_extend) + apply(assumption) + apply(assumption) + apply(assumption) + apply(assumption) + apply(assumption) + apply(blast) + done +next + case (TAndL1 x \ y B1 M \ \' B2 \n \c) + then show ?case + apply(simp) + apply(subgoal_tac "(y,B1 AND B2) \ set \'") + apply(drule ncloses_elim) + apply(assumption) + apply(erule exE)+ + apply(simp del: NEGc.simps) + apply(generate_fresh "name") + apply(fresh_fun_simp) + apply(rule_tac B="B1 AND B2" in CUT_SNa) + apply(simp) + apply(rule NEG_intro) + apply(simp (no_asm)) + apply(rule disjI2) + apply(rule disjI2) + apply(rule disjI1) + apply(rule_tac x="x" in exI) + apply(rule_tac x="ca" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp del: NEGc.simps) + apply(rule conjI) + apply(rule fin.intros) + apply(simp del: NEGc.simps add: abs_fresh fresh_prod fresh_atm) + apply(rule psubst_fresh_name) + apply(simp) + apply(simp) + apply(simp) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGn_def) + apply(simp (no_asm)) + apply(rule_tac x="x" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp (no_asm)) + apply(rule allI)+ + apply(rule impI) + apply(simp del: NEGc.simps add: psubst_nsubst[symmetric]) + apply(drule_tac x="(x,a,Pa)#\n" in meta_spec) + apply(drule_tac x="\c" in meta_spec) + apply(drule meta_mp) + apply(rule ncloses_extend) + apply(rule ncloses_subset) + apply(assumption) + apply(blast) + apply(simp) + apply(simp) + apply(simp) + apply(drule meta_mp) + apply(assumption) + apply(assumption) + apply(blast) + done +next + case (TAndL2 x \ y B2 M \ \' B1 \n \c) + then show ?case + apply(simp) + apply(subgoal_tac "(y,B1 AND B2) \ set \'") + apply(drule ncloses_elim) + apply(assumption) + apply(erule exE)+ + apply(simp del: NEGc.simps) + apply(generate_fresh "name") + apply(fresh_fun_simp) + apply(rule_tac B="B1 AND B2" in CUT_SNa) + apply(simp) + apply(rule NEG_intro) + apply(simp (no_asm)) + apply(rule disjI2) + apply(rule disjI2) + apply(rule disjI2) + apply(rule_tac x="x" in exI) + apply(rule_tac x="ca" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp del: NEGc.simps) + apply(rule conjI) + apply(rule fin.intros) + apply(simp del: NEGc.simps add: abs_fresh fresh_prod fresh_atm) + apply(rule psubst_fresh_name) + apply(simp) + apply(simp) + apply(simp) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGn_def) + apply(simp (no_asm)) + apply(rule_tac x="x" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp (no_asm)) + apply(rule allI)+ + apply(rule impI) + apply(simp del: NEGc.simps add: psubst_nsubst[symmetric]) + apply(drule_tac x="(x,a,Pa)#\n" in meta_spec) + apply(drule_tac x="\c" in meta_spec) + apply(drule meta_mp) + apply(rule ncloses_extend) + apply(rule ncloses_subset) + apply(assumption) + apply(blast) + apply(simp) + apply(simp) + apply(simp) + apply(drule meta_mp) + apply(assumption) + apply(assumption) + apply(blast) + done +next + case (TAndR a \ N c b M \ B C \' \n \c) + then show ?case + apply(simp) + apply(subgoal_tac "(c,B AND C) \ set \'") + apply(drule ccloses_elim) + apply(assumption) + apply(erule exE)+ + apply(simp) + apply(generate_fresh "coname") + apply(fresh_fun_simp) + apply(rule_tac B="B AND C" in CUT_SNa) + apply(simp) + apply(rule disjI2) + apply(rule disjI2) + apply(rule_tac x="ca" in exI) + apply(rule_tac x="a" in exI) + apply(rule_tac x="b" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp) + apply(rule conjI) + apply(rule fic.intros) + apply(simp add: abs_fresh fresh_prod fresh_atm) + apply(rule psubst_fresh_coname) + apply(simp) + apply(simp) + apply(simp) + apply(simp add: abs_fresh fresh_prod fresh_atm) + apply(rule psubst_fresh_coname) + apply(simp) + apply(simp) + apply(simp) + apply(rule conjI) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGc_def) + apply(simp) + apply(rule_tac x="a" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp) + apply(rule allI)+ + apply(rule impI) + apply(simp add: psubst_csubst[symmetric]) + apply(drule_tac x="\n" in meta_spec) + apply(drule_tac x="(a,xa,Pa)#\c" in meta_spec) + apply(drule meta_mp) + apply(assumption) + apply(drule meta_mp) + apply(rule ccloses_extend) + apply(rule ccloses_subset) + apply(assumption) + apply(blast) + apply(simp) + apply(simp) + apply(assumption) + apply(assumption) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGc_def) + apply(simp) + apply(rule_tac x="b" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp) + apply(rule allI)+ + apply(rule impI) + apply(simp add: psubst_csubst[symmetric]) + apply(rotate_tac 14) + apply(drule_tac x="\n" in meta_spec) + apply(drule_tac x="(b,xa,Pa)#\c" in meta_spec) + apply(drule meta_mp) + apply(assumption) + apply(drule meta_mp) + apply(rule ccloses_extend) + apply(rule ccloses_subset) + apply(assumption) + apply(blast) + apply(simp) + apply(simp) + apply(assumption) + apply(assumption) + apply(simp) + apply(blast) + done +next + case (TOrL x \ N z y M B \ C \' \n \c) + then show ?case + apply(simp) + apply(subgoal_tac "(z,B OR C) \ set \'") + apply(drule ncloses_elim) + apply(assumption) + apply(erule exE)+ + apply(simp del: NEGc.simps) + apply(generate_fresh "name") + apply(fresh_fun_simp) + apply(rule_tac B="B OR C" in CUT_SNa) + apply(simp) + apply(rule NEG_intro) + apply(simp (no_asm)) + apply(rule disjI2) + apply(rule disjI2) + apply(rule_tac x="x" in exI) + apply(rule_tac x="y" in exI) + apply(rule_tac x="ca" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp del: NEGc.simps) + apply(rule conjI) + apply(rule fin.intros) + apply(simp del: NEGc.simps add: abs_fresh fresh_prod fresh_atm) + apply(rule psubst_fresh_name) + apply(simp) + apply(simp) + apply(simp) + apply(simp del: NEGc.simps add: abs_fresh fresh_prod fresh_atm) + apply(rule psubst_fresh_name) + apply(simp) + apply(simp) + apply(simp) + apply(rule conjI) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGn_def) + apply(simp del: NEGc.simps) + apply(rule_tac x="x" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp del: NEGc.simps) + apply(rule allI)+ + apply(rule impI) + apply(simp del: NEGc.simps add: psubst_nsubst[symmetric]) + apply(drule_tac x="(x,a,Pa)#\n" in meta_spec) + apply(drule_tac x="\c" in meta_spec) + apply(drule meta_mp) + apply(rule ncloses_extend) + apply(rule ncloses_subset) + apply(assumption) + apply(blast) + apply(simp) + apply(simp) + apply(assumption) + apply(drule meta_mp) + apply(assumption) + apply(assumption) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGn_def) + apply(simp del: NEGc.simps) + apply(rule_tac x="y" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp del: NEGc.simps) + apply(rule allI)+ + apply(rule impI) + apply(simp del: NEGc.simps add: psubst_nsubst[symmetric]) + apply(rotate_tac 14) + apply(drule_tac x="(y,a,Pa)#\n" in meta_spec) + apply(drule_tac x="\c" in meta_spec) + apply(drule meta_mp) + apply(rule ncloses_extend) + apply(rule ncloses_subset) + apply(assumption) + apply(blast) + apply(simp) + apply(simp) + apply(assumption) + apply(drule meta_mp) + apply(assumption) + apply(assumption) + apply(blast) + done +next + case (TOrR1 a \ b \ M B1 \' B2 \n \c) + then show ?case + apply(simp) + apply(subgoal_tac "(b,B1 OR B2) \ set \'") + apply(drule ccloses_elim) + apply(assumption) + apply(erule exE)+ + apply(simp del: NEGc.simps) + apply(generate_fresh "coname") + apply(fresh_fun_simp) + apply(rule_tac B="B1 OR B2" in CUT_SNa) + apply(simp) + apply(rule disjI2) + apply(rule disjI2) + apply(rule disjI1) + apply(rule_tac x="a" in exI) + apply(rule_tac x="c" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp) + apply(rule conjI) + apply(rule fic.intros) + apply(simp del: NEGc.simps add: abs_fresh fresh_prod fresh_atm) + apply(rule psubst_fresh_coname) + apply(simp) + apply(simp) + apply(simp) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGc_def) + apply(simp (no_asm)) + apply(rule_tac x="a" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp (no_asm)) + apply(rule allI)+ + apply(rule impI) + apply(simp del: NEGc.simps add: psubst_csubst[symmetric]) + apply(drule_tac x="\n" in meta_spec) + apply(drule_tac x="(a,xa,Pa)#\c" in meta_spec) + apply(drule meta_mp) + apply(assumption) + apply(drule meta_mp) + apply(rule ccloses_extend) + apply(rule ccloses_subset) + apply(assumption) + apply(blast) + apply(simp) + apply(simp) + apply(simp) + apply(assumption) + apply(simp) + apply(blast) + done +next + case (TOrR2 a \ b \ M B2 \' B1 \n \c) + then show ?case + apply(simp) + apply(subgoal_tac "(b,B1 OR B2) \ set \'") + apply(drule ccloses_elim) + apply(assumption) + apply(erule exE)+ + apply(simp del: NEGc.simps) + apply(generate_fresh "coname") + apply(fresh_fun_simp) + apply(rule_tac B="B1 OR B2" in CUT_SNa) + apply(simp) + apply(rule disjI2) + apply(rule disjI2) + apply(rule disjI2) + apply(rule_tac x="a" in exI) + apply(rule_tac x="c" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp) + apply(rule conjI) + apply(rule fic.intros) + apply(simp del: NEGc.simps add: abs_fresh fresh_prod fresh_atm) + apply(rule psubst_fresh_coname) + apply(simp) + apply(simp) + apply(simp) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGc_def) + apply(simp (no_asm)) + apply(rule_tac x="a" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp (no_asm)) + apply(rule allI)+ + apply(rule impI) + apply(simp del: NEGc.simps add: psubst_csubst[symmetric]) + apply(drule_tac x="\n" in meta_spec) + apply(drule_tac x="(a,xa,Pa)#\c" in meta_spec) + apply(drule meta_mp) + apply(assumption) + apply(drule meta_mp) + apply(rule ccloses_extend) + apply(rule ccloses_subset) + apply(assumption) + apply(blast) + apply(simp) + apply(simp) + apply(simp) + apply(assumption) + apply(simp) + apply(blast) + done +next + case (TImpL a \ N x \ M y B C \' \n \c) + then show ?case + apply(simp) + apply(subgoal_tac "(y,B IMP C) \ set \'") + apply(drule ncloses_elim) + apply(assumption) + apply(erule exE)+ + apply(simp del: NEGc.simps) + apply(generate_fresh "name") + apply(fresh_fun_simp) + apply(rule_tac B="B IMP C" in CUT_SNa) + apply(simp) + apply(rule NEG_intro) + apply(simp (no_asm)) + apply(rule disjI2) + apply(rule disjI2) + apply(rule_tac x="x" in exI) + apply(rule_tac x="a" in exI) + apply(rule_tac x="ca" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp del: NEGc.simps) + apply(rule conjI) + apply(rule fin.intros) + apply(rule psubst_fresh_name) + apply(simp) + apply(simp) + apply(simp) + apply(simp del: NEGc.simps add: abs_fresh fresh_prod fresh_atm) + apply(rule psubst_fresh_name) + apply(simp) + apply(simp) + apply(simp) + apply(rule conjI) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGc_def) + apply(simp del: NEGc.simps) + apply(rule_tac x="a" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp del: NEGc.simps) + apply(rule allI)+ + apply(rule impI) + apply(simp del: NEGc.simps add: psubst_csubst[symmetric]) + apply(drule_tac x="\n" in meta_spec) + apply(drule_tac x="(a,xa,Pa)#\c" in meta_spec) + apply(drule meta_mp) + apply(rule ncloses_subset) + apply(assumption) + apply(blast) + apply(drule meta_mp) + apply(rule ccloses_extend) + apply(assumption) + apply(simp) + apply(simp) + apply(assumption) + apply(assumption) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGn_def) + apply(simp del: NEGc.simps) + apply(rule_tac x="x" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp del: NEGc.simps) + apply(rule allI)+ + apply(rule impI) + apply(simp del: NEGc.simps add: psubst_nsubst[symmetric]) + apply(rotate_tac 12) + apply(drule_tac x="(x,aa,Pa)#\n" in meta_spec) + apply(drule_tac x="\c" in meta_spec) + apply(drule meta_mp) + apply(rule ncloses_extend) + apply(rule ncloses_subset) + apply(assumption) + apply(blast) + apply(simp) + apply(simp) + apply(assumption) + apply(drule meta_mp) + apply(assumption) + apply(assumption) + apply(blast) + done +next + case (TImpR a \ b x \ B M C \' \n \c) + then show ?case + apply(simp) + apply(subgoal_tac "(b,B IMP C) \ set \'") + apply(drule ccloses_elim) + apply(assumption) + apply(erule exE)+ + apply(simp) + apply(generate_fresh "coname") + apply(fresh_fun_simp) + apply(rule_tac B="B IMP C" in CUT_SNa) + apply(simp) + apply(rule disjI2) + apply(rule disjI2) + apply(rule_tac x="x" in exI) + apply(rule_tac x="a" in exI) + apply(rule_tac x="c" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp) + apply(rule conjI) + apply(rule fic.intros) + apply(simp add: abs_fresh fresh_prod fresh_atm) + apply(rule psubst_fresh_coname) + apply(simp) + apply(simp) + apply(simp) + apply(rule conjI) + apply(rule allI)+ + apply(rule impI) + apply(simp add: psubst_csubst[symmetric]) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGn_def) + apply(simp) + apply(rule_tac x="x" in exI) + apply(rule_tac x="\n,((a,z,Pa)#\c)" in exI) + apply(simp) + apply(rule allI)+ + apply(rule impI) + apply(rule_tac t="\n,((a,z,Pa)#\c){x:=.Pb}" and + s="((x,aa,Pb)#\n),((a,z,Pa)#\c)" in subst) + apply(rule psubst_nsubst) + apply(simp add: fresh_prod fresh_atm fresh_list_cons) + apply(drule_tac x="(x,aa,Pb)#\n" in meta_spec) + apply(drule_tac x="(a,z,Pa)#\c" in meta_spec) + apply(drule meta_mp) + apply(rule ncloses_extend) + apply(assumption) + apply(simp) + apply(simp) + apply(simp) + apply(drule meta_mp) + apply(rule ccloses_extend) + apply(rule ccloses_subset) + apply(assumption) + apply(blast) + apply(auto intro: fresh_subset simp del: NEGc.simps)[1] + apply(simp) + apply(simp) + apply(assumption) + apply(rule allI)+ + apply(rule impI) + apply(simp add: psubst_nsubst[symmetric]) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGc_def) + apply(simp) + apply(rule_tac x="a" in exI) + apply(rule_tac x="((x,ca,Q)#\n),\c" in exI) + apply(simp) + apply(rule allI)+ + apply(rule impI) + apply(rule_tac t="((x,ca,Q)#\n),\c{a:=(xaa).Pa}" and + s="((x,ca,Q)#\n),((a,xaa,Pa)#\c)" in subst) + apply(rule psubst_csubst) + apply(simp add: fresh_prod fresh_atm fresh_list_cons) + apply(drule_tac x="(x,ca,Q)#\n" in meta_spec) + apply(drule_tac x="(a,xaa,Pa)#\c" in meta_spec) + apply(drule meta_mp) + apply(rule ncloses_extend) + apply(assumption) + apply(simp) + apply(simp) + apply(simp) + apply(drule meta_mp) + apply(rule ccloses_extend) + apply(rule ccloses_subset) + apply(assumption) + apply(blast) + apply(auto intro: fresh_subset simp del: NEGc.simps)[1] + apply(simp) + apply(simp) + apply(assumption) + apply(simp) + apply(blast) + done +next + case (TCut a \ N x \ M B \n \c) + then show ?case + apply - + apply(case_tac "\y. M\Ax y a") + apply(case_tac "\c. N\Ax x c") + apply(simp) + apply(rule_tac B="B" in CUT_SNa) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGc_def) + apply(simp) + apply(rule_tac x="a" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp) + apply(rule allI) + apply(rule allI) + apply(rule impI) + apply(simp add: psubst_csubst[symmetric]) (*?*) + apply(drule_tac x="\n" in meta_spec) + apply(drule_tac x="(a,xa,P)#\c" in meta_spec) + apply(drule meta_mp) + apply(assumption) + apply(drule meta_mp) + apply(rule ccloses_extend) + apply(assumption) + apply(assumption) + apply(assumption) + apply(assumption) + apply(assumption) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGn_def) + apply(simp) + apply(rule_tac x="x" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp) + apply(rule allI) + apply(rule allI) + apply(rule impI) + apply(simp add: psubst_nsubst[symmetric]) (*?*) + apply(rotate_tac 11) + apply(drule_tac x="(x,aa,P)#\n" in meta_spec) + apply(drule_tac x="\c" in meta_spec) + apply(drule meta_mp) + apply(rule ncloses_extend) + apply(assumption) + apply(assumption) + apply(assumption) + apply(assumption) + apply(drule_tac meta_mp) + apply(assumption) + apply(assumption) + (* cases at least one axiom *) + apply(simp (no_asm_use)) + apply(erule exE) + apply(simp del: psubst.simps) + apply(drule typing_Ax_elim2) + apply(auto simp add: trm.inject)[1] + apply(rule_tac B="B" in CUT_SNa) + (* left term *) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGc_def) + apply(simp) + apply(rule_tac x="a" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp) + apply(rule allI)+ + apply(rule impI) + apply(drule_tac x="\n" in meta_spec) + apply(drule_tac x="(a,xa,P)#\c" in meta_spec) + apply(drule meta_mp) + apply(assumption) + apply(drule meta_mp) + apply(rule ccloses_extend) + apply(assumption) + apply(assumption) + apply(assumption) + apply(assumption) + apply(simp add: psubst_csubst[symmetric]) (*?*) + (* right term -axiom *) + apply(drule ccloses_elim) + apply(assumption) + apply(erule exE)+ + apply(erule conjE) + apply(frule_tac y="x" in lookupd_cmaps) + apply(drule cmaps_fresh) + apply(assumption) + apply(simp) + apply(subgoal_tac "(x):P[xa\n>x] = (xa):P") + apply(simp) + apply(simp add: ntrm.inject) + apply(simp add: alpha fresh_prod fresh_atm) + apply(rule sym) + apply(rule nrename_swap) + apply(simp) + (* M is axiom *) + apply(simp) + apply(auto)[1] + (* both are axioms *) + apply(rule_tac B="B" in CUT_SNa) + apply(drule typing_Ax_elim1) + apply(drule ncloses_elim) + apply(assumption) + apply(erule exE)+ + apply(erule conjE) + apply(frule_tac a="a" in lookupc_nmaps) + apply(drule_tac a="a" in nmaps_fresh) + apply(assumption) + apply(simp) + apply(subgoal_tac ":P[c\c>a] = :P") + apply(simp) + apply(simp add: ctrm.inject) + apply(simp add: alpha fresh_prod fresh_atm) + apply(rule sym) + apply(rule crename_swap) + apply(simp) + apply(drule typing_Ax_elim2) + apply(drule ccloses_elim) + apply(assumption) + apply(erule exE)+ + apply(erule conjE) + apply(frule_tac y="x" in lookupd_cmaps) + apply(drule cmaps_fresh) + apply(assumption) + apply(simp) + apply(subgoal_tac "(x):P[xa\n>x] = (xa):P") + apply(simp) + apply(simp add: ntrm.inject) + apply(simp add: alpha fresh_prod fresh_atm) + apply(rule sym) + apply(rule nrename_swap) + apply(simp) + (* N is not axioms *) + apply(rule_tac B="B" in CUT_SNa) + (* left term *) + apply(drule typing_Ax_elim1) + apply(drule ncloses_elim) + apply(assumption) + apply(erule exE)+ + apply(erule conjE) + apply(frule_tac a="a" in lookupc_nmaps) + apply(drule_tac a="a" in nmaps_fresh) + apply(assumption) + apply(simp) + apply(subgoal_tac ":P[c\c>a] = :P") + apply(simp) + apply(simp add: ctrm.inject) + apply(simp add: alpha fresh_prod fresh_atm) + apply(rule sym) + apply(rule crename_swap) + apply(simp) + apply(rule BINDING_implies_CAND) + apply(unfold BINDINGn_def) + apply(simp) + apply(rule_tac x="x" in exI) + apply(rule_tac x="\n,\c" in exI) + apply(simp) + apply(rule allI) + apply(rule allI) + apply(rule impI) + apply(simp add: psubst_nsubst[symmetric]) (*?*) + apply(rotate_tac 10) + apply(drule_tac x="(x,aa,P)#\n" in meta_spec) + apply(drule_tac x="\c" in meta_spec) + apply(drule meta_mp) + apply(rule ncloses_extend) + apply(assumption) + apply(assumption) + apply(assumption) + apply(assumption) + apply(drule_tac meta_mp) + apply(assumption) + apply(assumption) + done +qed + +consts + "idn" :: "(name\ty) list\coname\(name\coname\trm) list" +primrec + "idn [] a = []" + "idn (p#\) a = ((fst p),a,Ax (fst p) a)#(idn \ a)" + +consts + "idc" :: "(coname\ty) list\name\(coname\name\trm) list" +primrec + "idc [] x = []" + "idc (p#\) x = ((fst p),x,Ax x (fst p))#(idc \ x)" + +lemma idn_eqvt[eqvt]: + fixes pi1::"name prm" + and pi2::"coname prm" + shows "(pi1\(idn \ a)) = idn (pi1\\) (pi1\a)" + and "(pi2\(idn \ a)) = idn (pi2\\) (pi2\a)" +apply(induct \) +apply(auto) +done + +lemma idc_eqvt[eqvt]: + fixes pi1::"name prm" + and pi2::"coname prm" + shows "(pi1\(idc \ x)) = idc (pi1\\) (pi1\x)" + and "(pi2\(idc \ x)) = idc (pi2\\) (pi2\x)" +apply(induct \) +apply(auto) +done + +lemma ccloses_id: + shows "(idc \ x) ccloses \" +apply(induct \) +apply(auto simp add: ccloses_def) +apply(rule Ax_in_CANDs) +apply(rule Ax_in_CANDs) +done + +lemma ncloses_id: + shows "(idn \ a) ncloses \" +apply(induct \) +apply(auto simp add: ncloses_def) +apply(rule Ax_in_CANDs) +apply(rule Ax_in_CANDs) +done + +lemma fresh_idn: + fixes x::"name" + and a::"coname" + shows "x\\ \ x\idn \ a" + and "a\(\,b) \ a\idn \ b" +apply(induct \) +apply(auto simp add: fresh_list_cons fresh_list_nil fresh_atm fresh_prod) +done + +lemma fresh_idc: + fixes x::"name" + and a::"coname" + shows "x\(\,y) \ x\idc \ y" + and "a\\ \ a\idc \ y" +apply(induct \) +apply(auto simp add: fresh_list_cons fresh_list_nil fresh_atm fresh_prod) +done + +lemma idc_cmaps: + assumes a: "idc \ y cmaps b to Some (x,M)" + shows "M=Ax x b" +using a +apply(induct \) +apply(auto) +apply(case_tac "b=a") +apply(auto) +done + +lemma idn_nmaps: + assumes a: "idn \ a nmaps x to Some (b,M)" + shows "M=Ax x b" +using a +apply(induct \) +apply(auto) +apply(case_tac "aa=x") +apply(auto) +done + +lemma lookup1: + assumes a: "x\(idn \ b)" + shows "lookup x a (idn \ b) \c = lookupa x a \c" +using a +apply(induct \) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm) +done + +lemma lookup2: + assumes a: "\(x\(idn \ b))" + shows "lookup x a (idn \ b) \c = lookupb x a \c b (Ax x b)" +using a +apply(induct \) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm fresh_list_nil) +done + +lemma lookup3: + assumes a: "a\(idc \ y)" + shows "lookupa x a (idc \ y) = Ax x a" +using a +apply(induct \) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm) +done + +lemma lookup4: + assumes a: "\(a\(idc \ y))" + shows "lookupa x a (idc \ y) = Cut .(Ax x a) (y).Ax y a" +using a +apply(induct \) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm fresh_list_nil) +done + +lemma lookup5: + assumes a: "a\(idc \ y)" + shows "lookupb x a (idc \ y) c P = Cut .P (x).Ax x a" +using a +apply(induct \) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm fresh_list_nil) +done + +lemma lookup6: + assumes a: "\(a\(idc \ y))" + shows "lookupb x a (idc \ y) c P = Cut .P (y).Ax y a" +using a +apply(induct \) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm fresh_list_nil) +done + +lemma lookup7: + shows "lookupc x a (idn \ b) = Ax x a" +apply(induct \) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm fresh_list_nil) +done + +lemma lookup8: + shows "lookupd x a (idc \ y) = Ax x a" +apply(induct \) +apply(auto simp add: fresh_list_cons fresh_prod fresh_atm fresh_list_nil) +done + +lemma id_redu: + shows "(idn \ x),(idc \ a) \\<^isub>a* M" +apply(nominal_induct M avoiding: \ \ x a rule: trm.strong_induct) +apply(auto) +(* Ax *) +apply(case_tac "name\(idn \ x)") +apply(simp add: lookup1) +apply(case_tac "coname\(idc \ a)") +apply(simp add: lookup3) +apply(simp add: lookup4) +apply(rule a_star_trans) +apply(rule a_starI) +apply(rule al_redu) +apply(rule better_LAxR_intro) +apply(rule fic.intros) +apply(simp) +apply(simp add: lookup2) +apply(case_tac "coname\(idc \ a)") +apply(simp add: lookup5) +apply(rule a_star_trans) +apply(rule a_starI) +apply(rule al_redu) +apply(rule better_LAxR_intro) +apply(rule fic.intros) +apply(simp) +apply(simp add: lookup6) +apply(rule a_star_trans) +apply(rule a_starI) +apply(rule al_redu) +apply(rule better_LAxR_intro) +apply(rule fic.intros) +apply(simp) +(* Cut *) +apply(auto simp add: fresh_idn fresh_idc psubst_fresh_name psubst_fresh_coname fresh_atm fresh_prod )[1] +apply(simp add: lookup7 lookup8) +apply(simp add: lookup7 lookup8) +apply(simp add: a_star_Cut) +apply(simp add: lookup7 lookup8) +apply(simp add: a_star_Cut) +apply(simp add: a_star_Cut) +(* NotR *) +apply(simp add: fresh_idn fresh_idc) +apply(case_tac "findc (idc \ a) coname") +apply(simp) +apply(simp add: a_star_NotR) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(drule idc_cmaps) +apply(simp) +apply(subgoal_tac "c\idn \ x,idc \ a") +apply(rule a_star_trans) +apply(rule a_starI) +apply(rule al_redu) +apply(rule better_LAxR_intro) +apply(rule fic.intros) +apply(assumption) +apply(simp add: crename_fresh) +apply(simp add: a_star_NotR) +apply(rule psubst_fresh_coname) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp) +apply(simp) +(* NotL *) +apply(simp add: fresh_idn fresh_idc) +apply(case_tac "findn (idn \ x) name") +apply(simp) +apply(simp add: a_star_NotL) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(drule idn_nmaps) +apply(simp) +apply(subgoal_tac "c\idn \ x,idc \ a") +apply(rule a_star_trans) +apply(rule a_starI) +apply(rule al_redu) +apply(rule better_LAxL_intro) +apply(rule fin.intros) +apply(assumption) +apply(simp add: nrename_fresh) +apply(simp add: a_star_NotL) +apply(rule psubst_fresh_name) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp) +apply(simp) +(* AndR *) +apply(simp add: fresh_idn fresh_idc) +apply(case_tac "findc (idc \ a) coname3") +apply(simp) +apply(simp add: a_star_AndR) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(drule idc_cmaps) +apply(simp) +apply(subgoal_tac "c\idn \ x,idc \ a") +apply(subgoal_tac "c\idn \ x,idc \ a") +apply(rule a_star_trans) +apply(rule a_starI) +apply(rule al_redu) +apply(rule better_LAxR_intro) +apply(rule fic.intros) +apply(simp add: abs_fresh) +apply(simp add: abs_fresh) +apply(auto simp add: fresh_idn fresh_idc psubst_fresh_name crename_fresh fresh_atm fresh_prod )[1] +apply(rule aux3) +apply(rule crename.simps) +apply(auto simp add: fresh_prod fresh_atm)[1] +apply(rule psubst_fresh_coname) +apply(rule fresh_idn) +apply(simp add: fresh_prod fresh_atm) +apply(rule fresh_idc) +apply(simp) +apply(simp) +apply(auto simp add: fresh_prod fresh_atm)[1] +apply(rule psubst_fresh_coname) +apply(rule fresh_idn) +apply(simp add: fresh_prod fresh_atm) +apply(rule fresh_idc) +apply(simp) +apply(simp) +apply(simp) +apply(simp) +apply(simp add: crename_fresh) +apply(simp add: a_star_AndR) +apply(rule psubst_fresh_coname) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp) +apply(simp) +apply(rule psubst_fresh_coname) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp) +apply(simp) +(* AndL1 *) +apply(simp add: fresh_idn fresh_idc) +apply(case_tac "findn (idn \ x) name2") +apply(simp) +apply(simp add: a_star_AndL1) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(drule idn_nmaps) +apply(simp) +apply(subgoal_tac "c\idn \ x,idc \ a") +apply(rule a_star_trans) +apply(rule a_starI) +apply(rule al_redu) +apply(rule better_LAxL_intro) +apply(rule fin.intros) +apply(simp add: abs_fresh) +apply(rule aux3) +apply(rule nrename.simps) +apply(auto simp add: fresh_prod fresh_atm)[1] +apply(simp) +apply(simp add: nrename_fresh) +apply(simp add: a_star_AndL1) +apply(rule psubst_fresh_name) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp) +apply(simp) +(* AndL2 *) +apply(simp add: fresh_idn fresh_idc) +apply(case_tac "findn (idn \ x) name2") +apply(simp) +apply(simp add: a_star_AndL2) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(drule idn_nmaps) +apply(simp) +apply(subgoal_tac "c\idn \ x,idc \ a") +apply(rule a_star_trans) +apply(rule a_starI) +apply(rule al_redu) +apply(rule better_LAxL_intro) +apply(rule fin.intros) +apply(simp add: abs_fresh) +apply(rule aux3) +apply(rule nrename.simps) +apply(auto simp add: fresh_prod fresh_atm)[1] +apply(simp) +apply(simp add: nrename_fresh) +apply(simp add: a_star_AndL2) +apply(rule psubst_fresh_name) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp) +apply(simp) +(* OrR1 *) +apply(simp add: fresh_idn fresh_idc) +apply(case_tac "findc (idc \ a) coname2") +apply(simp) +apply(simp add: a_star_OrR1) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(drule idc_cmaps) +apply(simp) +apply(subgoal_tac "c\idn \ x,idc \ a") +apply(rule a_star_trans) +apply(rule a_starI) +apply(rule al_redu) +apply(rule better_LAxR_intro) +apply(rule fic.intros) +apply(simp add: abs_fresh) +apply(rule aux3) +apply(rule crename.simps) +apply(auto simp add: fresh_prod fresh_atm)[1] +apply(simp) +apply(simp add: crename_fresh) +apply(simp add: a_star_OrR1) +apply(rule psubst_fresh_coname) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp) +apply(simp) +(* OrR2 *) +apply(simp add: fresh_idn fresh_idc) +apply(case_tac "findc (idc \ a) coname2") +apply(simp) +apply(simp add: a_star_OrR2) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(drule idc_cmaps) +apply(simp) +apply(subgoal_tac "c\idn \ x,idc \ a") +apply(rule a_star_trans) +apply(rule a_starI) +apply(rule al_redu) +apply(rule better_LAxR_intro) +apply(rule fic.intros) +apply(simp add: abs_fresh) +apply(rule aux3) +apply(rule crename.simps) +apply(auto simp add: fresh_prod fresh_atm)[1] +apply(simp) +apply(simp add: crename_fresh) +apply(simp add: a_star_OrR2) +apply(rule psubst_fresh_coname) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp) +apply(simp) +(* OrL *) +apply(simp add: fresh_idn fresh_idc) +apply(case_tac "findn (idn \ x) name3") +apply(simp) +apply(simp add: a_star_OrL) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(drule idn_nmaps) +apply(simp) +apply(subgoal_tac "c\idn \ x,idc \ a") +apply(subgoal_tac "c\idn \ x,idc \ a") +apply(rule a_star_trans) +apply(rule a_starI) +apply(rule al_redu) +apply(rule better_LAxL_intro) +apply(rule fin.intros) +apply(simp add: abs_fresh) +apply(simp add: abs_fresh) +apply(rule aux3) +apply(rule nrename.simps) +apply(auto simp add: fresh_prod fresh_atm)[1] +apply(rule psubst_fresh_name) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp add: fresh_prod fresh_atm) +apply(simp) +apply(auto simp add: fresh_prod fresh_atm)[1] +apply(rule psubst_fresh_name) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp add: fresh_prod fresh_atm) +apply(simp) +apply(simp) +apply(simp) +apply(simp add: nrename_fresh) +apply(simp add: a_star_OrL) +apply(rule psubst_fresh_name) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp) +apply(simp) +apply(rule psubst_fresh_name) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp) +apply(simp) +(* ImpR *) +apply(simp add: fresh_idn fresh_idc) +apply(case_tac "findc (idc \ a) coname2") +apply(simp) +apply(simp add: a_star_ImpR) +apply(auto)[1] +apply(generate_fresh "coname") +apply(fresh_fun_simp) +apply(drule idc_cmaps) +apply(simp) +apply(subgoal_tac "c\idn \ x,idc \ a") +apply(rule a_star_trans) +apply(rule a_starI) +apply(rule al_redu) +apply(rule better_LAxR_intro) +apply(rule fic.intros) +apply(simp add: abs_fresh) +apply(rule aux3) +apply(rule crename.simps) +apply(auto simp add: fresh_prod fresh_atm)[1] +apply(simp) +apply(simp add: crename_fresh) +apply(simp add: a_star_ImpR) +apply(rule psubst_fresh_coname) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp) +apply(simp) +(* ImpL *) +apply(simp add: fresh_idn fresh_idc) +apply(case_tac "findn (idn \ x) name2") +apply(simp) +apply(simp add: a_star_ImpL) +apply(auto)[1] +apply(generate_fresh "name") +apply(fresh_fun_simp) +apply(drule idn_nmaps) +apply(simp) +apply(subgoal_tac "c\idn \ x,idc \ a") +apply(subgoal_tac "c\idn \ x,idc \ a") +apply(rule a_star_trans) +apply(rule a_starI) +apply(rule al_redu) +apply(rule better_LAxL_intro) +apply(rule fin.intros) +apply(simp add: abs_fresh) +apply(simp add: abs_fresh) +apply(rule aux3) +apply(rule nrename.simps) +apply(auto simp add: fresh_prod fresh_atm)[1] +apply(rule psubst_fresh_coname) +apply(rule fresh_idn) +apply(simp add: fresh_atm) +apply(rule fresh_idc) +apply(simp add: fresh_prod fresh_atm) +apply(simp) +apply(auto simp add: fresh_prod fresh_atm)[1] +apply(rule psubst_fresh_name) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp add: fresh_prod fresh_atm) +apply(simp) +apply(simp) +apply(simp add: nrename_fresh) +apply(simp add: a_star_ImpL) +apply(rule psubst_fresh_name) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp) +apply(simp) +apply(rule psubst_fresh_name) +apply(rule fresh_idn) +apply(simp) +apply(rule fresh_idc) +apply(simp) +apply(simp) +done + +theorem ALL_SNa: + assumes a: "\ \ M \ \" + shows "SNa M" +proof - + fix x have "(idc \ x) ccloses \" by (simp add: ccloses_id) + moreover + fix a have "(idn \ a) ncloses \" by (simp add: ncloses_id) + ultimately have "SNa ((idn \ a),(idc \ x))" using a by (simp add: all_CAND) + moreover + have "((idn \ a),(idc \ x)) \\<^isub>a* M" by (simp add: id_redu) + ultimately show "SNa M" by (simp add: a_star_preserves_SNa) +qed + +end