Quelle Class3.thy
Sprache: Isabelle
theory Class3
imports Class2
begin
text ‹ 3rd Main Lemma›
lemma Cut_a_redu_elim:
assumes a:
"Cut .M (x).N ⟶ 🪙 a R"
shows "(∃ M'. R = Cut .M' (x).N ∧ M ⟶ 🪙 a M') ∨
(∃ N'. R = Cut .M (x).N' ∧ N ⟶ 🪙 a N') ∨
(Cut .M (x).N ⟶ 🪙 c R) ∨
(Cut .M (x).N ⟶ 🪙 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 ⟶ 🪙 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_fres
h abs_fresh)done lemma not_fic_crename:assumes a: "¬ (fic (M[a⊨ c>b]) c)" "c♯ (a,b)" shows "¬ (fic M c)" using aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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_freshapply (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 aapply (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_freshapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 [[simproc del: defined_all]]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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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♯ using aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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]) ⟶ 🪙 c M'" shows "∃ M0. M0[a⊨ c>b]=M' ∧ M ⟶ 🪙 c M0" using aapply (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]) ⟶ 🪙 l M'" shows "∃ M0. M0[a⊨ c>b]=M' ∧ M ⟶ 🪙 l M0" using aapply (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]) ⟶ 🪙 a M'" "a≠ b" shows "∃ M0. M0[a⊨ c>b]=M' ∧ M ⟶ 🪙 a M0" using aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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_freshdone lemma nrename_fresh_interesting1:fixes z::"name" assumes a: "z♯ (M[x⊨ n>y])" "z♯ (x,y)" shows "z♯ M" using aapply (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 aapply (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 aapply (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_freshapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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♯ using aapply (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 [[simproc del: defined_all]]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 aapply (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 aapply (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 [[simproc del: defined_all]]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 aapply (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 aapply (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]) ⟶ 🪙 c M'" shows "∃ M0. M0[x⊨ n>y]=M' ∧ M ⟶ 🪙 c M0" using aapply (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 aapply (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 aapply (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_freshapply (auto dest: nrename_fresh_interesting2 simp add: fresh_prod fresh_atm)done lemma nrename_lredu:assumes a: "(M[x⊨ n>y]) ⟶ 🪙 l M'" shows "∃ M0. M0[x⊨ n>y]=M' ∧ M ⟶ 🪙 l M0" using aapply (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]) ⟶ 🪙 a M'" "x≠ y" shows "∃ M0. M0[x⊨ n>y]=M' ∧ M ⟶ 🪙 a M0" using aapply (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 aapply (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 "trm set" where "SNa_set ≡ {M. SNa M}" abbreviation "(trm× trm) set" where "A_Redu_set ≡ {(N,M)| M N. M ⟶ 🪙 a N}" lemma SNa_elim:assumes a: "SNa M" shows "(∀ M. (∀ N. M ⟶ 🪙 a N ⟶ P N)⟶ P M) ⟶ P M" using aby (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: "∧ [ ∧ ) ∈ (r1 <*lex*> r2 <*lex*> r3) ⟶ P y] ==> P x" shows "P x" using aapply (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: "∧ [ ∧ ∈ (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 (rename_tac p a b)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: "∧ [ ∧ ∈ (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)text ‹ The following two simplification rules are necessary because of the new definition of lexicographic ordering › lemma ne_and_SNa_Redu[simp]: "M ≠ x ∧ (M,x) ∈ SNa_Redu ⟷ (M,x) ∈ SNa_Redu" using wf_SNa_Redu by autolemma ne_and_less_size [simp]: "A ≠ B ∧ size A < size B ⟷ size A < size B" by autolemma 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 a3apply -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 [[simproc del: defined_all]]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 ⟶ 🪙 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 ⟶ 🪙 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 ⟶ 🪙 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 ⟶ 🪙 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 ⟶ 🪙 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 ⟶ 🪙 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 ⟶ 🪙 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 ⟶ 🪙 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 ⟶ 🪙 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 ⟶ 🪙 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 ⟶ 🪙 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 ⟶ 🪙 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 \<noteq> 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 a2apply -apply (rule CUT_SNa_aux[OF a1])apply (simp_all add: CANDs_imply_SNa)done fun "(name× coname× trm) list==> ==> × 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 aapply (induct θ_n)apply (auto simp add: fresh_list_cons fresh_atm fresh_prod)done fun "(coname× name× trm) list==> ==> × 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 aapply (induct θ_c)apply (auto simp add: fresh_list_cons fresh_atm fresh_prod)done abbreviation "(name× coname× trm) list ==> ==> × trm) option ==> (‹ _ nmaps _ to _ › [55,55,55] 55) where "θ_n nmaps x to P ≡ (findn θ_n x) = P" abbreviation "(coname× name× trm) list ==> ==> × trm) option ==> (‹ _ 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 "name==> ==> × name× trm) list==> 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 aapply (induct θ_c arbitrary: x a y P)apply (auto)done fun "name==> ==> × name× trm) list==> ==> ==> 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∙ 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 "name==> ==> × coname× trm) list==> × name× trm) list==> 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 "name==> ==> × coname× trm) list==> 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 "name==> ==> × name× trm) list==> 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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (induct θ_n)apply (auto)done lemma lookupc_unicity:assumes a: "lookupc y a θ_n = Ax x b" "x♯ θ_n" shows "y=x" using aapply (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 aapply (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 aapply (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 aapply (induct θ_c)apply (auto)done nominal_primrec (freshness_context: "θ_n::(name× coname× trm)" )"trm==> × coname× trm) list==> 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)" )"trm==> × name× trm) list==> 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 case_option_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) ==> ==> (case (pi1∙ B) of Some (x,P) ==> ∙ s) x P | None ==> ∙ r))" and "(pi2∙ (case B of Some (x,P) ==> ==> (case (pi2∙ B) of Some (x,P) ==> ∙ s) x P | None ==> ∙ r))" apply (cases "B" )apply (auto)apply (perm_simp)apply (cases "B" )apply (auto)apply (perm_simp)done lemma case_option_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) ==> ==> (case (pi1∙ B) of Some (x,P) ==> ∙ s) x P | None ==> ∙ r))" and "(pi2∙ (case B of Some (x,P) ==> ==> (case (pi2∙ B) of Some (x,P) ==> ∙ s) x P | None ==> ∙ 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)" )"(name× coname× trm) list==> × name× trm) list==> ==> (‹ _,_🪙 › [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) ==> .NotR (x).(θ_n,θ_c) a' (u).P) | None ==> ) a)" "a♯ (θ_n,θ_c) ==> θ_n,θ_c.M x> = (case (findn θ_n x) of Some (c,P) ==> .P (x').(NotL .(θ_n,θ_c) x')) | None ==> .(θ_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) ==> .(AndR .(θ_n,θ_c) .(θ_n,θ_c) a') (x).P) | None ==> .(θ_n,θ_c) .(θ_n,θ_c) c)" "x♯ (z,θ_n,θ_c) ==> (θ_n,θ_c) = (case (findn θ_n z) of Some (c,P) ==> .P (z').AndL1 (x).(θ_n,θ_c) z') | None ==> ) z)" "x♯ (z,θ_n,θ_c) ==> (θ_n,θ_c) = (case (findn θ_n z) of Some (c,P) ==> .P (z').AndL2 (x).(θ_n,θ_c) z') | None ==> ) z)" "[ x♯ (N,z,θ_n,θ_c);u♯ (M,z,θ_n,θ_c);x≠ u] ==> (θ_n,θ_c) = (case (findn θ_n z) of Some (c,P) ==> .P (z').OrL (x).(θ_n,θ_c) (u).(θ_n,θ_c) z') | None ==> ) (u).(θ_n,θ_c) z)" "a♯ (b,θ_n,θ_c) ==> (θ_n,θ_c.M b>) = (case (findc θ_c b) of Some (x,P) ==> .OrR1 .(θ_n,θ_c) a' (x).P) | None ==> .(θ_n,θ_c) b)" "a♯ (b,θ_n,θ_c) ==> (θ_n,θ_c.M b>) = (case (findc θ_c b) of Some (x,P) ==> .OrR2 .(θ_n,θ_c) a' (x).P) | None ==> .(θ_n,θ_c) b)" "[ a♯ (b,θ_n,θ_c); x♯ (θ_n,θ_c)] ==> (θ_n,θ_c.M b>) = (case (findc θ_c b) of Some (z,P) ==> .ImpR (x)..(θ_n,θ_c) a' (z).P) | None ==> .(θ_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) ==> .P (z').ImpL .(θ_n,θ_c) (x).(θ_n,θ_c) z') | None ==> .(θ_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 ==> ==> ==> | Some (x,P) ==> using aapply (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 bapply (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 aapply -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 aapply -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 aapply -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 aapply -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 aapply (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 aapply (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 aapply (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 aapply (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 "(name× coname× trm) list==> × ty) list ==> (‹ _ ncloses _› [55,55] 55) where "θ_n ncloses Γ ≡ ∀ x B. ((x,B) ∈ set Γ ⟶ (∃ c P. θ_n nmaps x to Some (c,P) ∧ :P ∈ (∥ ∥ )))" definition "(coname× name× trm) list==> × ty) list ==> (‹ _ ccloses _› [55,55] 55) where "θ_c ccloses Δ ≡ ∀ a B. ((a,B) ∈ set Δ ⟶ (∃ x P. θ_c cmaps a to Some (x,P) ∧ (x):P ∈ (∥ ∥ )))" 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 aapply (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 aapply (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 aapply (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 aapply (simp add: ncloses_def)apply (drule validn_fresh)apply (auto)done text ‹ typing relation› inductive "ctxtn ==> ==> ==> (‹ _ ⊨ _ ⊨ _› [100,100,100] 100)where "[ validn Γ;validc Δ; (x,B)∈ set Γ; (a,B)∈ set Δ] ==> Γ ⊨ Ax x a ⊨ Δ" "[ x♯ Γ; ((x,B)#Γ) ⊨ M ⊨ Δ; set Δ' = {(a,NOT B)}∪ set Δ; validc Δ'] ==> Γ ⊨ NotR (x).M a ⊨ Δ'" "[ a♯ Δ; Γ ⊨ M ⊨ ((a,B)#Δ); set Γ' = {(x,NOT B)} ∪ set Γ; validn Γ'] ==> Γ' ⊨ NotL .M x ⊨ Δ" "[ x♯ (Γ,y); ((x,B1)#Γ) ⊨ M ⊨ Δ; set Γ' = {(y,B1 AND B2)} ∪ set Γ; validn Γ'] ==> Γ' ⊨ AndL1 (x).M y ⊨ Δ" "[ x♯ (Γ,y); ((x,B2)#Γ) ⊨ M ⊨ Δ; set Γ' = {(y,B1 AND B2)} ∪ set Γ; validn Γ'] ==> Γ' ⊨ AndL2 (x).M y ⊨ Δ" "[ 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 ⊨ Δ'" "[ 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 ⊨ Δ" "[ a♯ (Δ,b); Γ ⊨ M ⊨ ((a,B1)#Δ); set Δ' = {(b,B1 OR B2)}∪ set Δ; validc Δ'] ==> Γ ⊨ OrR1 .M b ⊨ Δ'" "[ a♯ (Δ,b); Γ ⊨ M ⊨ ((a,B2)#Δ); set Δ' = {(b,B1 OR B2)}∪ set Δ; validc Δ'] ==> Γ ⊨ OrR2 .M b ⊨ Δ'" "[ a♯ (Δ,N); x♯ (Γ,M,y); Γ ⊨ M ⊨ ((a,B)#Δ); ((x,C)#Γ) ⊨ N ⊨ Δ; set Γ' = {(y,B IMP C)} ∪ set Γ; validn Γ'] ==> Γ' ⊨ ImpL .M (x).N y ⊨ Δ" "[ a♯ (Δ,b); x♯ Γ; ((x,B)#Γ) ⊨ M ⊨ ((a,C)#Δ); set Δ' = {(b,B IMP C)}∪ set Δ; validc Δ'] ==> Γ ⊨ ImpR (x)..M b ⊨ Δ'" "[ a♯ (Δ,N); x♯ (Γ,M); Γ ⊨ M ⊨ ((a,B)#Δ); ((x,B)#Γ) ⊨ N ⊨ Δ] ==> Γ ⊨ Cut .M (x).N ⊨ Δ" equivariance typinglemma 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 typingapply (simp_all add: abs_fresh fresh_atm fresh_list_cons fresh_prod fresh_ty fresh_ctxt apply (auto intro: fresh_under_insert)done lemma validn_elim:assumes a: "validn ((x,B)#Γ)" shows "validn Γ ∧ x♯ Γ" using aapply (erule_tac validn.cases)apply (auto)done lemma validc_elim:assumes a: "validc ((a,B)#Δ)" shows "validc Δ ∧ a♯ Δ" using aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 bapply (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 capply (simp)done lemma all_CAND: assumes a: "Γ ⊨ M ⊨ Δ" and b: "θ_n ncloses Γ" and c: "θ_c ccloses Δ" shows "SNa (θ_n,θ_c)" using a b cproof (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 "((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 "((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 primrec "idn" :: "(name× ty) list==> ==> × coname× trm) list" where "idn [] a = []" "idn (p#Γ) a = ((fst p),a,Ax (fst p) a)#(idn Γ a)" primrec "idc" :: "(coname× ty) list==> ==> × name× trm) list" where "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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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 aapply (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) ⟶ 🪙 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 rtranclp_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 rtranclp_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 rtranclp_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 rtranclp_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 rtranclp_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 rtranclp_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 rtranclp_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 rtranclp_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 rtranclp_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 rtranclp_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 rtranclp_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 rtranclp_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 rtranclp_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)) ⟶ 🪙 a* M" by (simp add: id_redu)ultimately show "SNa M" by (simp add: a_star_preserves_SNa)qed end Messung V0.5 in Prozent C=98 H=98 G=97
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.483Bemerkung:
(vorverarbeitet am 2026-05-03)
¤ *Bot Zugriff
2026-05-26
