theory Class3
imports Class2
begin
text \<open>3rd Main Lemma\<close>
lemma Cut_a_redu_elim:
assumes a: "Cut .M (x).N \\<^sub>a R"
shows "(\M'. R = Cut .M' (x).N \ M \\<^sub>a M') \
(\<exists>N'. R = Cut <a>.M (x).N' \<and> N \<longrightarrow>\<^sub>a N') \<or>
(Cut <a>.M (x).N \<longrightarrow>\<^sub>c R) \<or>
(Cut <a>.M (x).N \<longrightarrow>\<^sub>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 \\<^sub>c R"
shows "(R = M{a:=(x).N} \ \fic M a) \
(R = N{x:=<a>.M} \<and> \<not>fin N x)"
using a
apply(erule_tac c_redu.cases)
apply(simp_all)
apply(simp_all add: trm.inject)
apply(rule disjI1)
apply(auto simp add: alpha)[1]
apply(simp add: subst_rename fresh_atm)
apply(simp add: subst_rename fresh_atm)
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
apply(perm_simp)
apply(simp add: subst_rename fresh_atm fresh_prod)
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
apply(perm_simp)
apply(rule disjI2)
apply(auto simp add: alpha)[1]
apply(simp add: subst_rename fresh_atm)
apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
apply(perm_simp)
apply(simp add: subst_rename fresh_atm fresh_prod)
apply(simp add: subst_rename fresh_atm fresh_prod)
apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
apply(perm_simp)
done
lemma not_fic_crename_aux:
assumes a: "fic M c" "c\(a,b)"
shows "fic (M[a\c>b]) c"
using a
apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
done
lemma not_fic_crename:
assumes a: "\(fic (M[a\c>b]) c)" "c\(a,b)"
shows "\(fic M c)"
using a
apply(auto dest: not_fic_crename_aux)
done
lemma not_fin_crename_aux:
assumes a: "fin M y"
shows "fin (M[a\c>b]) y"
using a
apply(nominal_induct M avoiding: a b rule: trm.strong_induct)
apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
done
lemma not_fin_crename:
assumes a: "\(fin (M[a\c>b]) y)"
shows "\(fin M y)"
using a
apply(auto dest: not_fin_crename_aux)
done
lemma crename_fresh_interesting1:
fixes c::"coname"
assumes a: "c\(M[a\c>b])" "c\(a,b)"
shows "c\M"
using a
apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
apply(auto split: if_splits simp add: abs_fresh)
done
lemma crename_fresh_interesting2:
fixes x::"name"
assumes a: "x\(M[a\c>b])"
shows "x\M"
using a
apply(nominal_induct M avoiding: x a b rule: trm.strong_induct)
apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp fresh_atm)
done
lemma fic_crename:
assumes a: "fic (M[a\c>b]) c" "c\(a,b)"
shows "fic M c"
using a
apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
split: if_splits)
apply(auto dest: crename_fresh_interesting1 simp add: fresh_prod fresh_atm)
done
lemma fin_crename:
assumes a: "fin (M[a\c>b]) x"
shows "fin M x"
using a
apply(nominal_induct M avoiding: x a b rule: trm.strong_induct)
apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
split: if_splits)
apply(auto dest: crename_fresh_interesting2 simp add: fresh_prod fresh_atm)
done
lemma crename_Cut:
assumes a: "R[a\c>b] = Cut .M (x).N" "c\(a,b,N,R)" "x\(M,R)"
shows "\M' N'. R = Cut .M' (x).N' \ M'[a\c>b] = M \ N'[a\c>b] = N \ c\N' \ x\M'"
using a
apply(nominal_induct R avoiding: a b c x M N rule: trm.strong_induct)
apply(auto split: if_splits)
apply(simp add: trm.inject)
apply(auto simp add: alpha)
apply(rule_tac x="[(name,x)]\trm2" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
apply(rule_tac x="[(coname,c)]\trm1" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
apply(auto simp add: fresh_atm)[1]
apply(rule_tac x="[(coname,c)]\trm1" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(rule_tac x="[(name,x)]\trm2" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
apply(auto simp add: fresh_atm)[1]
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma crename_NotR:
assumes a: "R[a\c>b] = NotR (x).N c" "x\R" "c\(a,b)"
shows "\N'. (R = NotR (x).N' c) \ N'[a\c>b] = N"
using a
apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
apply(rule_tac x="[(name,x)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma crename_NotR':
assumes a: "R[a\c>b] = NotR (x).N c" "x\R" "c\a"
shows "(\N'. (R = NotR (x).N' c) \ N'[a\c>b] = N) \ (\N'. (R = NotR (x).N' a) \ b=c \ N'[a\c>b] = N)"
using a
apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
apply(rule_tac x="[(name,x)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
apply(rule_tac x="[(name,x)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma crename_NotR_aux:
assumes a: "R[a\c>b] = NotR (x).N c"
shows "(a=c \ a=b) \ (a\c)"
using a
apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
done
lemma crename_NotL:
assumes a: "R[a\c>b] = NotL .N y" "c\(R,a,b)"
shows "\N'. (R = NotL .N' y) \ N'[a\c>b] = N"
using a
apply(nominal_induct R avoiding: a b c y N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
apply(rule_tac x="[(coname,c)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
done
lemma crename_AndL1:
assumes a: "R[a\c>b] = AndL1 (x).N y" "x\R"
shows "\N'. (R = AndL1 (x).N' y) \ N'[a\c>b] = N"
using a
apply(nominal_induct R avoiding: a b x y N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
apply(rule_tac x="[(name1,x)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma crename_AndL2:
assumes a: "R[a\c>b] = AndL2 (x).N y" "x\R"
shows "\N'. (R = AndL2 (x).N' y) \ N'[a\c>b] = N"
using a
apply(nominal_induct R avoiding: a b x y N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
apply(rule_tac x="[(name1,x)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma crename_AndR_aux:
assumes a: "R[a\c>b] = AndR .M .N e"
shows "(a=e \ a=b) \ (a\e)"
using a
apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
done
lemma crename_AndR:
assumes a: "R[a\c>b] = AndR .M .N e" "c\(a,b,d,e,N,R)" "d\(a,b,c,e,M,R)" "e\(a,b)"
shows "\M' N'. R = AndR .M' .N' e \ M'[a\c>b] = M \ N'[a\c>b] = N \ c\N' \ d\M'"
using a
apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
apply(auto split: if_splits simp add: trm.inject alpha)
apply(simp add: fresh_atm fresh_prod)
apply(rule_tac x="[(coname2,d)]\trm2" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(rule_tac x="[(coname1,c)]\trm1" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(rule_tac x="[(coname1,c)]\trm1" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(rule_tac x="[(coname2,d)]\trm2" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(rule_tac x="[(coname1,c)]\trm1" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(rule_tac x="[(coname1,c)]\trm1" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(rule_tac x="[(coname2,d)]\trm2" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
apply(drule_tac s="trm2[a\c>b]" in sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
done
lemma crename_AndR':
assumes a: "R[a\c>b] = AndR .M .N e" "c\(a,b,d,e,N,R)" "d\(a,b,c,e,M,R)" "e\a"
shows "(\M' N'. R = AndR .M' .N' e \ M'[a\c>b] = M \ N'[a\c>b] = N \ c\N' \ d\M') \
(\<exists>M' N'. R = AndR <c>.M' <d>.N' a \<and> b=e \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> c\<sharp>N' \<and> d\<sharp>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 a
apply(nominal_induct R avoiding: a b c e M rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
done
lemma crename_OrR1:
assumes a: "R[a\c>b] = OrR1 .N d" "c\(R,a,b)" "d\(a,b)"
shows "\N'. (R = OrR1 .N' d) \ N'[a\c>b] = N"
using a
apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
apply(rule_tac x="[(coname1,c)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
done
lemma crename_OrR1':
assumes a: "R[a\c>b] = OrR1 .N d" "c\(R,a,b)" "d\a"
shows "(\N'. (R = OrR1 .N' d) \ N'[a\c>b] = N) \
(\<exists>N'. (R = OrR1 <c>.N' a) \<and> b=d \<and> N'[a\<turnstile>c>b] = N)"
using a
apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
apply(rule_tac x="[(coname1,c)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
apply(rule_tac x="[(coname1,c)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
done
lemma crename_OrR2_aux:
assumes a: "R[a\c>b] = OrR2 .M e"
shows "(a=e \ a=b) \ (a\e)"
using a
apply(nominal_induct R avoiding: a b c e M rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
done
lemma crename_OrR2:
assumes a: "R[a\c>b] = OrR2 .N d" "c\(R,a,b)" "d\(a,b)"
shows "\N'. (R = OrR2 .N' d) \ N'[a\c>b] = N"
using a
apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
apply(rule_tac x="[(coname1,c)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
done
lemma crename_OrR2':
assumes a: "R[a\c>b] = OrR2 .N d" "c\(R,a,b)" "d\a"
shows "(\N'. (R = OrR2 .N' d) \ N'[a\c>b] = N) \
(\<exists>N'. (R = OrR2 <c>.N' a) \<and> b=d \<and> N'[a\<turnstile>c>b] = N)"
using a
apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
apply(rule_tac x="[(coname1,c)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
apply(rule_tac x="[(coname1,c)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
done
lemma crename_OrL:
assumes a: "R[a\c>b] = OrL (x).M (y).N z" "x\(y,z,N,R)" "y\(x,z,M,R)"
shows "\M' N'. R = OrL (x).M' (y).N' z \ M'[a\c>b] = M \ N'[a\c>b] = N \ x\N' \ y\M'"
using a
apply(nominal_induct R avoiding: a b x y z M N rule: trm.strong_induct)
apply(auto split: if_splits simp add: trm.inject alpha)
apply(rule_tac x="[(name2,y)]\trm2" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(rule_tac x="[(name1,x)]\trm1" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(rule_tac x="[(name1,x)]\trm1" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(rule_tac x="[(name2,y)]\trm2" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
apply(drule_tac s="trm2[a\c>b]" in sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma crename_ImpL:
assumes a: "R[a\c>b] = ImpL .M (y).N z" "c\(a,b,N,R)" "y\(z,M,R)"
shows "\M' N'. R = ImpL .M' (y).N' z \ M'[a\c>b] = M \ N'[a\c>b] = N \ c\N' \ y\M'"
using a
apply(nominal_induct R avoiding: a b c y z M N rule: trm.strong_induct)
apply(auto split: if_splits simp add: trm.inject alpha)
apply(rule_tac x="[(name1,y)]\trm2" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(rule_tac x="[(coname,c)]\trm1" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(rule_tac x="[(coname,c)]\trm1" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(rule_tac x="[(name1,y)]\trm2" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
apply(drule_tac s="trm2[a\c>b]" in sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma crename_ImpR_aux:
assumes a: "R[a\c>b] = ImpR (x)..M e"
shows "(a=e \ a=b) \ (a\e)"
using a
apply(nominal_induct R avoiding: x a b c e M rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
done
lemma crename_ImpR:
assumes a: "R[a\c>b] = ImpR (x)..N d" "c\(R,a,b)" "d\(a,b)" "x\R"
shows "\N'. (R = ImpR (x)..N' d) \ N'[a\c>b] = N"
using a
apply(nominal_induct R avoiding: a b x c d N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_perm alpha abs_fresh trm.inject)
apply(rule_tac x="[(name,x)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(rule_tac x="[(name,x)]\[(coname1, c)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_supp fin_supp abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma crename_ImpR':
assumes a: "R[a\c>b] = ImpR (x)..N d" "c\(R,a,b)" "x\R" "d\a"
shows "(\N'. (R = ImpR (x)..N' d) \ N'[a\c>b] = N) \
(\<exists>N'. (R = ImpR (x).<c>.N' a) \<and> b=d \<and> N'[a\<turnstile>c>b] = N)"
using a
apply(nominal_induct R avoiding: x a b c d N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject abs_perm calc_atm)
apply(rule_tac x="[(name,x)]\[(coname1,c)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod abs_supp fin_supp)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
apply(rule_tac x="[(name,x)]\[(coname1,c)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod abs_supp fin_supp)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma crename_ax2:
assumes a: "N[a\c>b] = Ax x c"
shows "\d. N = Ax x d"
using a
apply(nominal_induct N avoiding: a b rule: trm.strong_induct)
apply(auto split: if_splits)
apply(simp add: trm.inject)
done
lemma crename_interesting1:
assumes a: "distinct [a,b,c]"
shows "M[a\c>c][c\c>b] = M[c\c>b][a\c>b]"
using a
apply(nominal_induct M avoiding: a c b rule: trm.strong_induct)
apply(auto simp add: rename_fresh simp add: trm.inject alpha)
apply(blast)
apply(rotate_tac 12)
apply(drule_tac x="a" in meta_spec)
apply(rotate_tac 15)
apply(drule_tac x="c" in meta_spec)
apply(rotate_tac 15)
apply(drule_tac x="b" in meta_spec)
apply(blast)
apply(blast)
apply(blast)
done
lemma crename_interesting2:
assumes a: "a\c" "a\d" "a\b" "c\d" "b\c"
shows "M[a\c>b][c\c>d] = M[c\c>d][a\c>b]"
using a
apply(nominal_induct M avoiding: a c b d rule: trm.strong_induct)
apply(auto simp add: rename_fresh simp add: trm.inject alpha)
done
lemma crename_interesting3:
shows "M[a\c>c][x\n>y] = M[x\n>y][a\c>c]"
apply(nominal_induct M avoiding: a c x y rule: trm.strong_induct)
apply(auto simp add: rename_fresh simp add: trm.inject alpha)
done
lemma crename_credu:
assumes a: "(M[a\c>b]) \\<^sub>c M'"
shows "\M0. M0[a\c>b]=M' \ M \\<^sub>c M0"
using a
apply(nominal_induct M\<equiv>"M[a\<turnstile>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]) \\<^sub>l M'"
shows "\M0. M0[a\c>b]=M' \ M \\<^sub>l M0"
using a
apply(nominal_induct M\<equiv>"M[a\<turnstile>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]) \\<^sub>a M'" "a\b"
shows "\M0. M0[a\c>b]=M' \ M \\<^sub>a M0"
using a
apply(nominal_induct "M[a\c>b]" M' avoiding: M a b rule: a_redu.strong_induct)
apply(drule crename_lredu)
apply(blast)
apply(drule crename_credu)
apply(blast)
(* Cut *)
apply(drule sym)
apply(drule crename_Cut)
apply(simp)
apply(simp)
apply(auto)[1]
apply(drule_tac x="M'a" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(auto)[1]
apply(rule_tac x="Cut .M0 (x).N'" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(rule conjI)
apply(rule trans)
apply(rule crename.simps)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(drule crename_fresh_interesting2)
apply(simp add: fresh_a_redu)
apply(simp)
apply(auto)[1]
apply(drule sym)
apply(drule crename_Cut)
apply(simp)
apply(simp)
apply(auto)[1]
apply(drule_tac x="N'a" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(auto)[1]
apply(rule_tac x="Cut .M' (x).M0" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(rule conjI)
apply(rule trans)
apply(rule crename.simps)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
apply(drule crename_fresh_interesting1)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(simp add: fresh_a_redu)
apply(simp)
apply(simp)
apply(auto)[1]
(* NotL *)
apply(drule sym)
apply(drule crename_NotL)
apply(simp)
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(auto)[1]
apply(rule_tac x="NotL .M0 x" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
(* NotR *)
apply(drule sym)
apply(frule crename_NotR_aux)
apply(erule disjE)
apply(auto)[1]
apply(drule crename_NotR')
apply(simp)
apply(simp add: fresh_atm)
apply(erule disjE)
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(auto)[1]
apply(rule_tac x="NotR (x).M0 a" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="a" in meta_spec)
apply(auto)[1]
apply(rule_tac x="NotR (x).M0 aa" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
(* AndR *)
apply(drule sym)
apply(frule crename_AndR_aux)
apply(erule disjE)
apply(auto)[1]
apply(drule crename_AndR')
apply(simp add: fresh_prod fresh_atm)
apply(simp add: fresh_atm)
apply(simp add: fresh_atm)
apply(erule disjE)
apply(auto)[1]
apply(drule_tac x="M'a" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="ba" in meta_spec)
apply(auto)[1]
apply(rule_tac x="AndR .M0 .N' c" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(rule trans)
apply(rule crename.simps)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto intro: fresh_a_redu)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(drule_tac x="M'a" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(auto)[1]
apply(rule_tac x="AndR .M0 .N' aa" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(rule trans)
apply(rule crename.simps)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto intro: fresh_a_redu)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(drule sym)
apply(frule crename_AndR_aux)
apply(erule disjE)
apply(auto)[1]
apply(drule crename_AndR')
apply(simp add: fresh_prod fresh_atm)
apply(simp add: fresh_atm)
apply(simp add: fresh_atm)
apply(erule disjE)
apply(auto)[1]
apply(drule_tac x="N'a" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="ba" in meta_spec)
apply(auto)[1]
apply(rule_tac x="AndR .M' .M0 c" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(rule trans)
apply(rule crename.simps)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
apply(auto intro: fresh_a_redu)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(drule_tac x="N'a" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(auto)[1]
apply(rule_tac x="AndR .M' .M0 aa" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(rule trans)
apply(rule crename.simps)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
apply(auto intro: fresh_a_redu)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(simp)
(* AndL1 *)
apply(drule sym)
apply(drule crename_AndL1)
apply(simp)
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(auto)[1]
apply(rule_tac x="AndL1 (x).M0 y" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
(* AndL2 *)
apply(drule sym)
apply(drule crename_AndL2)
apply(simp)
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(auto)[1]
apply(rule_tac x="AndL2 (x).M0 y" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
(* OrL *)
apply(drule sym)
apply(drule crename_OrL)
apply(simp)
apply(auto simp add: fresh_atm fresh_prod)[1]
apply(auto simp add: fresh_atm fresh_prod)[1]
apply(auto)[1]
apply(drule_tac x="M'a" in meta_spec)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(auto)[1]
apply(rule_tac x="OrL (x).M0 (y).N' z" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(rule trans)
apply(rule crename.simps)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto intro: fresh_a_redu)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(simp)
apply(drule sym)
apply(drule crename_OrL)
apply(simp)
apply(auto simp add: fresh_atm fresh_prod)[1]
apply(auto simp add: fresh_atm fresh_prod)[1]
apply(auto)[1]
apply(drule_tac x="N'a" in meta_spec)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(auto)[1]
apply(rule_tac x="OrL (x).M' (y).M0 z" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(rule trans)
apply(rule crename.simps)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
apply(auto intro: fresh_a_redu)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(simp)
apply(simp)
(* OrR1 *)
apply(drule sym)
apply(frule crename_OrR1_aux)
apply(erule disjE)
apply(auto)[1]
apply(drule crename_OrR1')
apply(simp)
apply(simp add: fresh_atm)
apply(erule disjE)
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="ba" in meta_spec)
apply(auto)[1]
apply(rule_tac x="OrR1 .M0 b" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(auto)[1]
apply(rule_tac x="OrR1 .M0 aa" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
(* OrR2 *)
apply(drule sym)
apply(frule crename_OrR2_aux)
apply(erule disjE)
apply(auto)[1]
apply(drule crename_OrR2')
apply(simp)
apply(simp add: fresh_atm)
apply(erule disjE)
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="ba" in meta_spec)
apply(auto)[1]
apply(rule_tac x="OrR2 .M0 b" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(auto)[1]
apply(rule_tac x="OrR2 .M0 aa" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
(* ImpL *)
apply(drule sym)
apply(drule crename_ImpL)
apply(simp)
apply(simp)
apply(auto)[1]
apply(drule_tac x="M'a" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(auto)[1]
apply(rule_tac x="ImpL .M0 (x).N' y" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(rule trans)
apply(rule crename.simps)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto intro: fresh_a_redu)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(drule sym)
apply(drule crename_ImpL)
apply(simp)
apply(simp)
apply(auto)[1]
apply(drule_tac x="N'a" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(auto)[1]
apply(rule_tac x="ImpL .M' (x).M0 y" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(rule trans)
apply(rule crename.simps)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm fresh_prod)[1]
apply(auto intro: fresh_a_redu)[1]
apply(simp add: fresh_prod abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(simp)
(* ImpR *)
apply(drule sym)
apply(frule crename_ImpR_aux)
apply(erule disjE)
apply(auto)[1]
apply(drule crename_ImpR')
apply(simp)
apply(simp add: fresh_atm)
apply(simp add: fresh_atm)
apply(erule disjE)
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="ba" in meta_spec)
apply(auto)[1]
apply(rule_tac x="ImpR (x)..M0 b" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
apply(auto)[1]
apply(drule_tac x="N'" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(auto)[1]
apply(rule_tac x="ImpR (x)..M0 aa" in exI)
apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
apply(auto)[1]
done
lemma SNa_preserved_renaming1:
assumes a: "SNa M"
shows "SNa (M[a\c>b])"
using a
apply(induct rule: SNa_induct)
apply(case_tac "a=b")
apply(simp add: crename_id)
apply(rule SNaI)
apply(drule crename_aredu)
apply(blast)+
done
lemma nrename_interesting1:
assumes a: "distinct [x,y,z]"
shows "M[x\n>z][z\n>y] = M[z\n>y][x\n>y]"
using a
apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
apply(auto simp add: rename_fresh simp add: trm.inject alpha)
apply(blast)
apply(blast)
apply(rotate_tac 12)
apply(drule_tac x="x" in meta_spec)
apply(rotate_tac 15)
apply(drule_tac x="y" in meta_spec)
apply(rotate_tac 15)
apply(drule_tac x="z" in meta_spec)
apply(blast)
apply(rotate_tac 11)
apply(drule_tac x="x" in meta_spec)
apply(rotate_tac 14)
apply(drule_tac x="y" in meta_spec)
apply(rotate_tac 14)
apply(drule_tac x="z" in meta_spec)
apply(blast)
done
lemma nrename_interesting2:
assumes a: "x\z" "x\u" "x\y" "z\u" "y\z"
shows "M[x\n>y][z\n>u] = M[z\n>u][x\n>y]"
using a
apply(nominal_induct M avoiding: x y z u rule: trm.strong_induct)
apply(auto simp add: rename_fresh simp add: trm.inject alpha)
done
lemma not_fic_nrename_aux:
assumes a: "fic M c"
shows "fic (M[x\n>y]) c"
using a
apply(nominal_induct M avoiding: c x y rule: trm.strong_induct)
apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
done
lemma not_fic_nrename:
assumes a: "\(fic (M[x\n>y]) c)"
shows "\(fic M c)"
using a
apply(auto dest: not_fic_nrename_aux)
done
lemma fin_nrename:
assumes a: "fin M z" "z\(x,y)"
shows "fin (M[x\n>y]) z"
using a
apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
split: if_splits)
done
lemma nrename_fresh_interesting1:
fixes z::"name"
assumes a: "z\(M[x\n>y])" "z\(x,y)"
shows "z\M"
using a
apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp)
done
lemma nrename_fresh_interesting2:
fixes c::"coname"
assumes a: "c\(M[x\n>y])"
shows "c\M"
using a
apply(nominal_induct M avoiding: x y c rule: trm.strong_induct)
apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp fresh_atm)
done
lemma fin_nrename2:
assumes a: "fin (M[x\n>y]) z" "z\(x,y)"
shows "fin M z"
using a
apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
split: if_splits)
apply(auto dest: nrename_fresh_interesting1 simp add: fresh_atm fresh_prod)
done
lemma nrename_Cut:
assumes a: "R[x\n>y] = Cut .M (z).N" "c\(N,R)" "z\(x,y,M,R)"
shows "\M' N'. R = Cut .M' (z).N' \ M'[x\n>y] = M \ N'[x\n>y] = N \ c\N' \ z\M'"
using a
apply(nominal_induct R avoiding: c y x z M N rule: trm.strong_induct)
apply(auto split: if_splits)
apply(simp add: trm.inject)
apply(auto simp add: alpha fresh_atm)
apply(rule_tac x="[(coname,c)]\trm1" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(rule_tac x="[(name,z)]\trm2" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(rule conjI)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
apply(auto simp add: fresh_atm)[1]
apply(drule sym)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma nrename_NotR:
assumes a: "R[x\n>y] = NotR (z).N c" "z\(R,x,y)"
shows "\N'. (R = NotR (z).N' c) \ N'[x\n>y] = N"
using a
apply(nominal_induct R avoiding: x y c z N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
apply(rule_tac x="[(name,z)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma nrename_NotL:
assumes a: "R[x\n>y] = NotL .N z" "c\R" "z\(x,y)"
shows "\N'. (R = NotL .N' z) \ N'[x\n>y] = N"
using a
apply(nominal_induct R avoiding: x y c z N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
apply(rule_tac x="[(coname,c)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
done
lemma nrename_NotL':
assumes a: "R[x\n>y] = NotL .N u" "c\R" "x\y"
shows "(\N'. (R = NotL .N' u) \ N'[x\n>y] = N) \ (\N'. (R = NotL .N' x) \ y=u \ N'[x\n>y] = N)"
using a
apply(nominal_induct R avoiding: y u c x N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
apply(rule_tac x="[(coname,c)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
apply(rule_tac x="[(coname,c)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
done
lemma nrename_NotL_aux:
assumes a: "R[x\n>y] = NotL .N u"
shows "(x=u \ x=y) \ (x\u)"
using a
apply(nominal_induct R avoiding: y u c x N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
done
lemma nrename_AndL1:
assumes a: "R[x\n>y] = AndL1 (z).N u" "z\(R,x,y)" "u\(x,y)"
shows "\N'. (R = AndL1 (z).N' u) \ N'[x\n>y] = N"
using a
apply(nominal_induct R avoiding: z u x y N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
apply(rule_tac x="[(name1,z)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma nrename_AndL1':
assumes a: "R[x\n>y] = AndL1 (v).N u" "v\(R,u,x,y)" "x\y"
shows "(\N'. (R = AndL1 (v).N' u) \ N'[x\n>y] = N) \ (\N'. (R = AndL1 (v).N' x) \ y=u \ N'[x\n>y] = N)"
using a
apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
apply(rule_tac x="[(name1,v)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
apply(rule_tac x="[(name1,v)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma nrename_AndL1_aux:
assumes a: "R[x\n>y] = AndL1 (v).N u"
shows "(x=u \ x=y) \ (x\u)"
using a
apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
done
lemma nrename_AndL2:
assumes a: "R[x\n>y] = AndL2 (z).N u" "z\(R,x,y)" "u\(x,y)"
shows "\N'. (R = AndL2 (z).N' u) \ N'[x\n>y] = N"
using a
apply(nominal_induct R avoiding: z u x y N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
apply(rule_tac x="[(name1,z)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma nrename_AndL2':
assumes a: "R[x\n>y] = AndL2 (v).N u" "v\(R,u,x,y)" "x\y"
shows "(\N'. (R = AndL2 (v).N' u) \ N'[x\n>y] = N) \ (\N'. (R = AndL2 (v).N' x) \ y=u \ N'[x\n>y] = N)"
using a
apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
apply(rule_tac x="[(name1,v)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
apply(rule_tac x="[(name1,v)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma nrename_AndL2_aux:
assumes a: "R[x\n>y] = AndL2 (v).N u"
shows "(x=u \ x=y) \ (x\u)"
using a
apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
done
lemma nrename_AndR:
assumes a: "R[x\n>y] = AndR .M .N e" "c\(d,e,N,R)" "d\(c,e,M,R)"
shows "\M' N'. R = AndR .M' .N' e \ M'[x\n>y] = M \ N'[x\n>y] = N \ c\N' \ d\M'"
using a
apply(nominal_induct R avoiding: x y c d e M N rule: trm.strong_induct)
apply(auto split: if_splits simp add: trm.inject alpha)
apply(simp add: fresh_atm fresh_prod)
apply(rule_tac x="[(coname1,c)]\trm1" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(rule_tac x="[(coname1,c)]\trm1" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(rule_tac x="[(coname2,d)]\trm2" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
apply(drule_tac s="trm2[x\n>y]" in sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
done
lemma nrename_OrR1:
assumes a: "R[x\n>y] = OrR1 .N d" "c\(R,d)"
shows "\N'. (R = OrR1 .N' d) \ N'[x\n>y] = N"
using a
apply(nominal_induct R avoiding: x y c d N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
apply(rule_tac x="[(coname1,c)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
done
lemma nrename_OrR2:
assumes a: "R[x\n>y] = OrR2 .N d" "c\(R,d)"
shows "\N'. (R = OrR2 .N' d) \ N'[x\n>y] = N"
using a
apply(nominal_induct R avoiding: x y c d N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
apply(rule_tac x="[(coname1,c)]\trm" in exI)
apply(perm_simp)
apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
apply(drule sym)
apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
apply(simp add: eqvts calc_atm)
done
lemma nrename_OrL:
assumes a: "R[u\n>v] = OrL (x).M (y).N z" "x\(y,z,u,v,N,R)" "y\(x,z,u,v,M,R)" "z\(u,v)"
shows "\M' N'. R = OrL (x).M' (y).N' z \ M'[u\n>v] = M \ N'[u\n>v] = N \ x\N' \ y\M'"
using a
apply(nominal_induct R avoiding: u v x y z M N rule: trm.strong_induct)
apply(auto split: if_splits simp add: trm.inject alpha fresh_prod fresh_atm)
apply(rule_tac x="[(name1,x)]\trm1" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(rule_tac x="[(name2,y)]\trm2" in exI)
apply(perm_simp)
apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
apply(drule sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
apply(drule_tac s="trm2[u\n>v]" in sym)
apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
apply(simp add: eqvts calc_atm)
done
lemma nrename_OrL':
assumes a: "R[x\n>y] = OrL (v).M (w).N u" "v\(R,N,u,x,y)" "w\(R,M,u,x,y)" "x\y"
shows "(\M' N'. (R = OrL (v).M' (w).N' u) \ M'[x\n>y] = M \ N'[x\n>y] = N) \
(\<exists>M' N'. (R = OrL (v).M' (w).N' x) \<and> y=u \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>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 a
apply(nominal_induct R avoiding: y x w u v M N rule: trm.strong_induct)
apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
done
lemma nrename_ImpL:
assumes a: "R[x\n>y] = ImpL .M (u).N z" "c\(N,R)" "u\(y,x,z,M,R)" "z\(x,y)"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.63 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
