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 \\<^sub>a R"
  shows "(\M'. R = Cut .M' (x).N \ M \\<^sub>a M') \
         (∃N'. R = Cut .M (x).N' ∧ N ⟶🚫a N') \
         (Cut <a>.M (x).N ⟶🚫c R) ∨
         (Cut <a>.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 \\<^sub>c R"
  shows "(R = M{a:=(x).N} \ \fic M a) \
         (R = N{x:=<a>.M} ∧ ¬fin N x)"
  using a
  apply(erule_tac c_redu.cases)
   apply(simp_all)
   apply(simp_all add: trm.inject)
   apply(rule disjI1)
   apply(auto simp add: alpha)[1]
       apply(simp add: subst_rename fresh_atm)
      apply(simp add: subst_rename fresh_atm)
     apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
     apply(perm_simp)
    apply(simp add: subst_rename fresh_atm fresh_prod)
   apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
   apply(perm_simp)
  apply(rule disjI2)
  apply(auto simp add: alpha)[1]
      apply(simp add: subst_rename fresh_atm)
     apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
     apply(perm_simp)
    apply(simp add: subst_rename fresh_atm fresh_prod)
   apply(simp add: subst_rename fresh_atm fresh_prod)
  apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
  apply(perm_simp)
  done

lemma not_fic_crename_aux:
  assumes a: "fic M c" "c\(a,b)"
  shows "fic (M[a\c>b]) c"
  using a
  apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
             apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
  done

lemma not_fic_crename:
  assumes a: "\(fic (M[a\c>b]) c)" "c\(a,b)"
  shows "\(fic M c)"
  using a
  apply(auto dest:  not_fic_crename_aux)
  done

lemma not_fin_crename_aux:
  assumes a: "fin M y"
  shows "fin (M[a\c>b]) y"
  using a
  apply(nominal_induct M avoiding: a b rule: trm.strong_induct)
             apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
  done

lemma not_fin_crename:
  assumes a: "\(fin (M[a\c>b]) y)"
  shows "\(fin M y)"
  using a
  apply(auto dest:  not_fin_crename_aux)
  done

lemma crename_fresh_interesting1:
  fixes c::"coname"
  assumes a: "c\(M[a\c>b])" "c\(a,b)"
  shows "c\M"
  using a
  apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
             apply(auto split: if_splits simp add: abs_fresh)
  done

lemma crename_fresh_interesting2:
  fixes x::"name"
  assumes a: "x\(M[a\c>b])"
  shows "x\M"
  using a
  apply(nominal_induct M avoiding: x a b rule: trm.strong_induct)
             apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp fresh_atm)
  done

lemma fic_crename:
  assumes a: "fic (M[a\c>b]) c" "c\(a,b)"
  shows "fic M c"
  using a
  apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
             apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
      split: if_splits)
       apply(auto dest: crename_fresh_interesting1 simp add: fresh_prod fresh_atm)
  done

lemma fin_crename:
  assumes a: "fin (M[a\c>b]) x"
  shows "fin M x"
  using a
  apply(nominal_induct M avoiding: x a b rule: trm.strong_induct)
             apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
      split: if_splits)
        apply(auto dest: crename_fresh_interesting2 simp add: fresh_prod fresh_atm)
  done

lemma crename_Cut:
  assumes a: "R[a\c>b] = Cut .M (x).N" "c\(a,b,N,R)" "x\(M,R)"
  shows "\M' N'. R = Cut .M' (x).N' \ M'[a\c>b] = M \ N'[a\c>b] = N \ c\N' \ x\M'"
  using a
  apply(nominal_induct R avoiding: a b c x M N rule: trm.strong_induct)
             apply(auto split: if_splits)
  apply(simp add: trm.inject)
  apply(auto simp add: alpha)
    apply(rule_tac x="[(name,x)]\trm2" in exI)
    apply(perm_simp)
    apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
    apply(drule sym)
    apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
    apply(simp add: eqvts calc_atm)
   apply(rule_tac x="[(coname,c)]\trm1" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
   apply(auto simp add: fresh_atm)[1]
  apply(rule_tac x="[(coname,c)]\trm1" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(rule_tac x="[(name,x)]\trm2" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  apply(auto simp add: fresh_atm)[1]
   apply(drule sym)
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_NotR:
  assumes a: "R[a\c>b] = NotR (x).N c" "x\R" "c\(a,b)"
  shows "\N'. (R = NotR (x).N' c) \ N'[a\c>b] = N"
  using a
  apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(name,x)]\trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_NotR':
  assumes a: "R[a\c>b] = NotR (x).N c" "x\R" "c\a"
  shows "(\N'. (R = NotR (x).N' c) \ N'[a\c>b] = N) \ (\N'. (R = NotR (x).N' a) \ b=c \ N'[a\c>b] = N)"
  using a
  apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
   apply(rule_tac x="[(name,x)]\trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(name,x)]\trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_NotR_aux:
  assumes a: "R[a\c>b] = NotR (x).N c"
  shows "(a=c \ a=b) \ (a\c)"
  using a
  apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_NotL:
  assumes a: "R[a\c>b] = NotL .N y" "c\(R,a,b)"
  shows "\N'. (R = NotL .N' y) \ N'[a\c>b] = N"
  using a
  apply(nominal_induct R avoiding: a b c y N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(coname,c)]\trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_AndL1:
  assumes a: "R[a\c>b] = AndL1 (x).N y" "x\R"
  shows "\N'. (R = AndL1 (x).N' y) \ N'[a\c>b] = N"
  using a
  apply(nominal_induct R avoiding: a b x y N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(name1,x)]\trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_AndL2:
  assumes a: "R[a\c>b] = AndL2 (x).N y" "x\R"
  shows "\N'. (R = AndL2 (x).N' y) \ N'[a\c>b] = N"
  using a
  apply(nominal_induct R avoiding: a b x y N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(name1,x)]\trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_AndR_aux:
  assumes a: "R[a\c>b] = AndR .M .N e"
  shows "(a=e \ a=b) \ (a\e)"
  using a
  apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_AndR:
  assumes a: "R[a\c>b] = AndR .M .N e" "c\(a,b,d,e,N,R)" "d\(a,b,c,e,M,R)" "e\(a,b)"
  shows "\M' N'. R = AndR .M' .N' e \ M'[a\c>b] = M \ N'[a\c>b] = N \ c\N' \ d\M'"
  using a
  apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: trm.inject alpha)
        apply(simp add: fresh_atm fresh_prod)
       apply(rule_tac x="[(coname2,d)]\trm2" in exI)
       apply(perm_simp)
       apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
      apply(rule_tac x="[(coname1,c)]\trm1" in exI)
      apply(perm_simp)
      apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
     apply(rule_tac x="[(coname1,c)]\trm1" in exI)
     apply(perm_simp)
     apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
    apply(rule_tac x="[(coname2,d)]\trm2" in exI)
    apply(perm_simp)
    apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(rule_tac x="[(coname1,c)]\trm1" in exI)
   apply(perm_simp)
   apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(coname1,c)]\trm1" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(coname2,d)]\trm2" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule_tac s="trm2[a\c>b]" in  sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_AndR':
  assumes a: "R[a\c>b] = AndR .M .N e" "c\(a,b,d,e,N,R)" "d\(a,b,c,e,M,R)" "e\a"
  shows "(\M' N'. R = AndR .M' .N' e \ M'[a\c>b] = M \ N'[a\c>b] = N \ c\N' \ d\M') \
         (∃M' N'. R = AndR <c>.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 a
  apply(nominal_induct R avoiding: a b c e M rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_OrR1:
  assumes a: "R[a\c>b] = OrR1 .N d" "c\(R,a,b)" "d\(a,b)"
  shows "\N'. (R = OrR1 .N' d) \ N'[a\c>b] = N"
  using a
  apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(coname1,c)]\trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_OrR1':
  assumes a: "R[a\c>b] = OrR1 .N d" "c\(R,a,b)" "d\a"
  shows "(\N'. (R = OrR1 .N' d) \ N'[a\c>b] = N) \
         (∃N'. (R = OrR1 .N' a) ∧ b=d ∧ N'[a\c>b] = N)"
  using a
  apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
   apply(rule_tac x="[(coname1,c)]\trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(coname1,c)]\trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_OrR2_aux:
  assumes a: "R[a\c>b] = OrR2 .M e"
  shows "(a=e \ a=b) \ (a\e)"
  using a
  apply(nominal_induct R avoiding: a b c e M rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_OrR2:
  assumes a: "R[a\c>b] = OrR2 .N d" "c\(R,a,b)" "d\(a,b)"
  shows "\N'. (R = OrR2 .N' d) \ N'[a\c>b] = N"
  using a
  apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  apply(rule_tac x="[(coname1,c)]\trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_OrR2':
  assumes a: "R[a\c>b] = OrR2 .N d" "c\(R,a,b)" "d\a"
  shows "(\N'. (R = OrR2 .N' d) \ N'[a\c>b] = N) \
         (∃N'. (R = OrR2 .N' a) ∧ b=d ∧ N'[a\c>b] = N)"
  using a
  apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
   apply(rule_tac x="[(coname1,c)]\trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(coname1,c)]\trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_OrL:
  assumes a: "R[a\c>b] = OrL (x).M (y).N z" "x\(y,z,N,R)" "y\(x,z,M,R)"
  shows "\M' N'. R = OrL (x).M' (y).N' z \ M'[a\c>b] = M \ N'[a\c>b] = N \ x\N' \ y\M'"
  using a
  apply(nominal_induct R avoiding: a b x y z M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: trm.inject alpha)
    apply(rule_tac x="[(name2,y)]\trm2" in exI)
    apply(perm_simp)
    apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(rule_tac x="[(name1,x)]\trm1" in exI)
   apply(perm_simp)
   apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(name1,x)]\trm1" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(name2,y)]\trm2" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule_tac s="trm2[a\c>b]" in  sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_ImpL:
  assumes a: "R[a\c>b] = ImpL .M (y).N z" "c\(a,b,N,R)" "y\(z,M,R)"
  shows "\M' N'. R = ImpL .M' (y).N' z \ M'[a\c>b] = M \ N'[a\c>b] = N \ c\N' \ y\M'"
  using a
  apply(nominal_induct R avoiding: a b c y z M N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: trm.inject alpha)
    apply(rule_tac x="[(name1,y)]\trm2" in exI)
    apply(perm_simp)
    apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(rule_tac x="[(coname,c)]\trm1" in exI)
   apply(perm_simp)
   apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(coname,c)]\trm1" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
  apply(rule_tac x="[(name1,y)]\trm2" in exI)
  apply(perm_simp)
  apply(auto simp add: abs_fresh fresh_left calc_atm fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(simp add: eqvts calc_atm)
  apply(drule_tac s="trm2[a\c>b]" in  sym)
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_ImpR_aux:
  assumes a: "R[a\c>b] = ImpR (x)..M e"
  shows "(a=e \ a=b) \ (a\e)"
  using a
  apply(nominal_induct R avoiding: x a b c e M rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
  done

lemma crename_ImpR:
  assumes a: "R[a\c>b] = ImpR (x)..N d" "c\(R,a,b)" "d\(a,b)" "x\R"
  shows "\N'. (R = ImpR (x)..N' d) \ N'[a\c>b] = N"
  using a
  apply(nominal_induct R avoiding: a b x c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_perm alpha abs_fresh trm.inject)
   apply(rule_tac x="[(name,x)]\trm" in exI)
   apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod)
  apply(rule_tac x="[(name,x)]\[(coname1, c)]\trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_supp fin_supp abs_fresh fresh_left calc_atm fresh_prod)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_ImpR':
  assumes a: "R[a\c>b] = ImpR (x)..N d" "c\(R,a,b)" "x\R" "d\a"
  shows "(\N'. (R = ImpR (x)..N' d) \ N'[a\c>b] = N) \
         (∃N'. (R = ImpR (x)..N' a) ∧ b=d ∧ N'[a\c>b] = N)"
  using a
  apply(nominal_induct R avoiding: x a b c d N rule: trm.strong_induct)
             apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject abs_perm calc_atm)
   apply(rule_tac x="[(name,x)]\[(coname1,c)]\trm" in exI)
   apply(perm_simp)
   apply(simp add: abs_fresh fresh_left calc_atm fresh_prod abs_supp fin_supp)
   apply(drule sym)
   apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
   apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
   apply(simp add: eqvts calc_atm)
  apply(rule_tac x="[(name,x)]\[(coname1,c)]\trm" in exI)
  apply(perm_simp)
  apply(simp add: abs_fresh fresh_left calc_atm fresh_prod abs_supp fin_supp)
  apply(drule sym)
  apply(drule pt_bij1[OF pt_coname_inst,OF at_coname_inst])
  apply(drule pt_bij1[OF pt_name_inst,OF at_name_inst])
  apply(simp add: eqvts calc_atm)
  done

lemma crename_ax2:
  assumes a: "N[a\c>b] = Ax x c"
  shows "\d. N = Ax x d"
  using a
  apply(nominal_induct N avoiding: a b rule: trm.strong_induct)
             apply(auto split: if_splits)
  apply(simp add: trm.inject)
  done

lemma crename_interesting1:
  assumes a: "distinct [a,b,c]"
  shows "M[a\c>c][c\c>b] = M[c\c>b][a\c>b]"
  using a
  apply(nominal_induct M avoiding: a c b rule: trm.strong_induct)
             apply(auto simp add: rename_fresh simp add: trm.inject alpha)
     apply(blast)
    apply(rotate_tac 12)
    apply(drule_tac x="a" in meta_spec)
    apply(rotate_tac 15)
    apply(drule_tac x="c" in meta_spec)
    apply(rotate_tac 15)
    apply(drule_tac x="b" in meta_spec)
    apply(blast)
   apply(blast)
  apply(blast)
  done

lemma crename_interesting2:
  assumes a: "a\c" "a\d" "a\b" "c\d" "b\c"
  shows "M[a\c>b][c\c>d] = M[c\c>d][a\c>b]"
  using a
  apply(nominal_induct M avoiding: a c b d rule: trm.strong_induct)
             apply(auto simp add: rename_fresh simp add: trm.inject alpha)
  done

lemma crename_interesting3:
  shows "M[a\c>c][x\n>y] = M[x\n>y][a\c>c]"
  apply(nominal_induct M avoiding: a c x y rule: trm.strong_induct)
             apply(auto simp add: rename_fresh simp add: trm.inject alpha)
  done

lemma crename_credu:
  assumes a: "(M[a\c>b]) \\<^sub>c M'"
  shows "\M0. M0[a\c>b]=M' \ M \\<^sub>c M0"
  using a
  apply(nominal_induct M≡"M[a\c>b]" M' avoiding: M a b rule: c_redu.strong_induct)
   apply(drule sym)
   apply(drule crename_Cut)
     apply(simp)
    apply(simp)
   apply(auto)
   apply(rule_tac x="M'{a:=(x).N'}" in exI)
   apply(rule conjI)
    apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod)
   apply(rule c_redu.intros)
     apply(auto dest: not_fic_crename)[1]
    apply(simp add: abs_fresh)
   apply(simp add: abs_fresh)
  apply(drule sym)
  apply(drule crename_Cut)
    apply(simp)
   apply(simp)
  apply(auto)
  apply(rule_tac x="N'{x:=.M'}" in exI)
  apply(rule conjI)
   apply(simp add: fresh_atm abs_fresh subst_comm fresh_prod)
  apply(rule c_redu.intros)
    apply(auto dest: not_fin_crename)[1]
   apply(simp add: abs_fresh)
  apply(simp add: abs_fresh)
  done

lemma crename_lredu:
  assumes a: "(M[a\c>b]) \\<^sub>l M'"
  shows "\M0. M0[a\c>b]=M' \ M \\<^sub>l M0"
  using a
  apply(nominal_induct M≡"M[a\c>b]" M' avoiding: M a b rule: l_redu.strong_induct)
         apply(drule sym)
         apply(drule crename_Cut)
           apply(simp add: fresh_prod fresh_atm)
          apply(simp)
         apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
         apply(case_tac "aa=ba")
          apply(simp add: crename_id)
          apply(rule l_redu.intros)
            apply(simp)
           apply(simp add: fresh_atm)
          apply(assumption)
         apply(frule crename_ax2)
         apply(auto)[1]
         apply(case_tac "d=aa")
          apply(simp add: trm.inject)
          apply(rule_tac x="M'[a\c>aa]" in exI)
          apply(rule conjI)
           apply(rule crename_interesting1)
           apply(simp)
          apply(rule l_redu.intros)
            apply(simp)
           apply(simp add: fresh_atm)
          apply(auto dest: fic_crename simp add: fresh_prod fresh_atm)[1]
         apply(simp add: trm.inject)
         apply(rule_tac x="M'[a\c>b]" in exI)
         apply(rule conjI)
          apply(rule crename_interesting2)
              apply(simp)
             apply(simp)
            apply(simp)
           apply(simp)
          apply(simp)
         apply(rule l_redu.intros)
           apply(simp)
          apply(simp add: fresh_atm)
         apply(auto dest: fic_crename simp add: fresh_prod fresh_atm)[1]
        apply(drule sym)
        apply(drule crename_Cut)
          apply(simp add: fresh_prod fresh_atm)
         apply(simp add: fresh_prod fresh_atm)
        apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
        apply(case_tac "aa=b")
         apply(simp add: crename_id)
         apply(rule l_redu.intros)
           apply(simp)
          apply(simp add: fresh_atm)
         apply(assumption)
        apply(frule crename_ax2)
        apply(auto)[1]
        apply(case_tac "d=aa")
         apply(simp add: trm.inject)
        apply(simp add: trm.inject)
        apply(rule_tac x="N'[x\n>y]" in exI)
        apply(rule conjI)
         apply(rule sym)
         apply(rule crename_interesting3)
        apply(rule l_redu.intros)
          apply(simp)
         apply(simp add: fresh_atm)
        apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
    (* LNot *)
       apply(drule sym)
       apply(drule crename_Cut)
         apply(simp add: fresh_prod abs_fresh fresh_atm)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
       apply(drule crename_NotR)
         apply(simp add: fresh_prod abs_fresh fresh_atm)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
       apply(drule crename_NotL)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
       apply(rule_tac x="Cut .N'b (x).N'a" in exI)
       apply(simp add: fresh_atm)[1]
       apply(rule l_redu.intros)
            apply(auto simp add: fresh_prod intro: crename_fresh_interesting2)[1]
           apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
          apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
         apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
        apply(simp add: fresh_atm)
       apply(simp add: fresh_atm)
    (* LAnd1 *)
      apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
      apply(drule sym)
      apply(drule crename_Cut)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(auto)[1]
      apply(drule crename_AndR)
         apply(simp add: fresh_prod abs_fresh fresh_atm)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
      apply(drule crename_AndL1)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
      apply(rule_tac x="Cut .M'a (x).N'a" in exI)
      apply(simp add: fresh_atm)[1]
      apply(rule l_redu.intros)
           apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
          apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
         apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
        apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
       apply(simp add: fresh_atm)
      apply(simp add: fresh_atm)
    (* LAnd2 *)
     apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
     apply(drule sym)
     apply(drule crename_Cut)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(auto)[1]
     apply(drule crename_AndR)
        apply(simp add: fresh_prod abs_fresh fresh_atm)
       apply(simp add: fresh_prod abs_fresh fresh_atm)
      apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
     apply(drule crename_AndL2)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
     apply(rule_tac x="Cut .N'b (x).N'a" in exI)
     apply(simp add: fresh_atm)[1]
     apply(rule l_redu.intros)
          apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
         apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
        apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
       apply(auto simp add: fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
      apply(simp add: fresh_atm)
     apply(simp add: fresh_atm)
    (* LOr1 *)
    apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
    apply(drule sym)
    apply(drule crename_Cut)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(auto)[1]
    apply(drule crename_OrL)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
    apply(drule crename_OrR1)
      apply(simp add: fresh_prod abs_fresh fresh_atm)
     apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
    apply(auto)
    apply(rule_tac x="Cut .N' (x1).M'a" in exI)
    apply(rule conjI)
     apply(simp add: abs_fresh fresh_atm)[1]
    apply(rule l_redu.intros)
         apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
        apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
       apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
      apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
     apply(simp add: fresh_atm)
    apply(simp add: fresh_atm)
    (* LOr2 *)
   apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
   apply(drule sym)
   apply(drule crename_Cut)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(auto)[1]
   apply(drule crename_OrL)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
   apply(drule crename_OrR2)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
   apply(auto)
   apply(rule_tac x="Cut .N' (x2).N'a" in exI)
   apply(rule conjI)
    apply(simp add: abs_fresh fresh_atm)[1]
   apply(rule l_redu.intros)
        apply(auto simp add: fresh_atm abs_fresh fresh_prod intro: crename_fresh_interesting1)[1]
       apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting2)[1]
      apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
     apply(auto simp add: abs_fresh fresh_atm fresh_prod intro: crename_fresh_interesting1)[1]
    apply(simp add: fresh_atm)
   apply(simp add: fresh_atm)
    (* ImpL *)
  apply(auto dest: fin_crename simp add: fresh_prod fresh_atm)[1]
  apply(drule sym)
  apply(drule crename_Cut)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(simp add: fresh_prod abs_fresh fresh_atm abs_supp fin_supp)
  apply(auto)[1]
  apply(drule crename_ImpL)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(simp add: fresh_prod abs_fresh fresh_atm)
  apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
  apply(drule crename_ImpR)
     apply(simp add: fresh_prod abs_fresh fresh_atm)
    apply(simp add: fresh_prod abs_fresh fresh_atm)
   apply(simp)
  apply(auto simp add: abs_fresh fresh_prod fresh_atm)[1]
  apply(rule_tac x="Cut .(Cut .M'a (x).N') (y).N'a" in exI)
  apply(rule conjI)
   apply(simp add: abs_fresh abs_supp fin_supp fresh_atm)[1]
  apply(rule l_redu.intros)
       apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp fresh_prod intro: crename_fresh_interesting2)[1]
      apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
     apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting2)[1]
    apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
   apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
  apply(auto simp add: abs_fresh fresh_atm abs_supp fin_supp fresh_prod intro: crename_fresh_interesting1)[1]
  done

lemma crename_aredu:
  assumes a: "(M[a\c>b]) \\<^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) \
         (∃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 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

--> --------------------

Messung V0.5

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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 und die Messung sind noch experimentell.