CR from scratch

CR.thy

theory CR
imports "~~/src/HOL/Nominal/Nominal"
begin

atom_decl var

nominal_datatype lambda =
  Var var
| App lambda lambda (infixl "$" 120)
| Abs "«var»lambda" ("lam [_]._" [100,100] 100)

nominal_primrec subst ("_[_::=_]" [100,100,100] 120) where
  "(Var x)[y ::= s] = (if x = y then s else Var x)"
| "(M1 $ M2)[y ::= s] = (M1 [y ::= s]) $ (M2 [y ::= s])"
| "x♯(y,s) ⟹ (lam [x]. M)[y ::= s] = lam [x]. (M[y ::= s])"
apply (finite_guess+, auto)
apply (simp add: abs_fresh)
apply (fresh_guess+)
done

lemma subst_gfresh':
  assumes "x ♯ t" "x ♯ s" "x ≠ y"
  shows "x ♯ t [y ::= s]"
using assms
apply (nominal_induct t avoiding: x y s rule: lambda.strong_induct)
  apply (simp add: assms(2))
  apply simp
  apply (metis abs_fresh(1) fresh_prod lambda.fresh(3) simps(3))
done
  
lemma subst_fresh: "x ♯ s ⟹ x ♯ t[x ::= s]"
apply (nominal_induct t avoiding: x s rule: lambda.strong_induct)
apply (auto simp add: fresh_atm abs_fresh)
done

lemma subst_gfresh:
  fixes x y :: var
  assumes "x ♯ t" "x ♯ s"
  shows "x ♯ t [y ::= s]"
apply (cases "x = y")
  using assms(2) subst_fresh apply blast
  using assms(1) assms(2) subst_gfresh' apply auto
done

lemma no_subst: "x ♯ t ⟹ t[x ::= s] = t"
apply (nominal_induct t avoiding: x s rule: lambda.strong_induct)
  apply (simp add: fresh_atm)
  apply simp
  apply (simp add: abs_fresh(1) fresh_atm)
done

lemma substitution:
  assumes "x ≠ y" "x ♯ L"
  shows "M [x ::= N] [y ::= L] = M [y ::= L] [x ::= N [y ::= L]]"
using assms 
apply (nominal_induct M avoiding: x y N L rule: lambda.strong_induct)
  apply (simp add: no_subst)
  apply simp
  apply (simp add: fresh_atm subst_gfresh')
done
  
lemma subst_eqvt[eqvt]:
  fixes π :: "var prm"
  shows "π∙(t[x ::= s]) = (π∙t)[(π∙x) ::= (π∙s)]"
apply (nominal_induct t avoiding: x s rule: strong_induct)
apply (simp add: perm_bij)
apply (simp)
apply (simp add: fresh_bij)
done

lemma subst_rename:
  assumes "x ♯ t"
  shows "([(x,y)]∙t) [x ::= s] = t [y ::= s]"
using assms
apply (nominal_induct t avoiding: x y s rule: lambda.strong_induct)
apply (auto simp add: swap_simps fresh_atm abs_fresh)
done

inductive beta (infixl "→β" 50) where
  b_app1: "t1 →β t2 ⟹ t1 $ s →β t2 $ s"
| b_app2: "t1 →β t2 ⟹ s $ t1 →β s $ t2"
| b_abs: "t →β s ⟹ lam[x].t →β lam[x].s"
| b_beta': "x ♯ s ⟹ (lam [x]. t) $ s →β t[x ::= s]"

equivariance beta

nominal_inductive beta
by (simp_all add: abs_fresh subst_fresh)

inductive par_beta (infixl "⇒β" 50) where
  pb_var: "Var x ⇒β Var x"
| pb_app: "⟦ t1 ⇒β t2; s1 ⇒β s2 ⟧ ⟹ t1 $ s1 ⇒β t2 $ s2"
| pb_abs: "t ⇒β s ⟹ lam[x].t ⇒β lam[x].s"
| pb_beta: "⟦ x ♯ (s1,s2); t1 ⇒β t2; s1 ⇒β s2 ⟧ ⟹ (lam [x]. t1) $ s1 ⇒β t2 [x ::= s2]"

equivariance par_beta

nominal_inductive par_beta
by (simp_all add: abs_fresh subst_fresh)

lemma pb_refl: "t ⇒β t"
apply (induction t rule: lambda.induct)
apply (rule, rule, simp, simp, rule, simp)
done

lemma one_to_par: "M →β N ⟹ M ⇒β N"
apply (induction rule: beta.induct)
  apply (rule, simp, rule pb_refl)
  apply (rule, rule pb_refl, simp)
  apply (rule, simp, rule)
  apply (auto simp add: pb_refl)
done

abbreviation long_beta (infixl "⟶β" 50) where
  "long_beta == beta⇧*⇧*"

lemma lb_app1: "t1 ⟶β t2 ⟹ t1 $ s ⟶β t2 $ s"
apply (induction rule: rtranclp_induct)
apply (simp, rule, simp, rule, simp)
done

lemma lb_app2: "s1 ⟶β s2 ⟹ t $ s1 ⟶β t $ s2"
apply (induction rule: rtranclp_induct)
apply (simp, rule, simp, rule, simp)
done

lemma lb_abs: "t ⟶β s ⟹ lam[x].t ⟶β lam[x].s"
apply (induction rule: rtranclp_induct)
apply (simp, rule, simp, rule, simp)
done

lemma perm_fresh_lambda:
  fixes M :: lambda and x y :: var
  assumes "y ♯ (x,M)"
  shows "x ♯ ([(y,x)] ∙ M)"
using assms
apply (nominal_induct M rule: lambda.strong_induct)
  apply (metis fresh_bij fresh_prodD(2) swap_simps(1))
  apply (simp add: fresh_prod)
  apply (metis fresh_bij fresh_prodD(2) swap_simps(1))
done

lemma lb_subst1: "t →β s ⟹ t[x ::= p] ⟶β s[x ::= p]"
apply (nominal_induct avoiding: x p rule: beta.strong_induct, simp_all)
  apply (rule lb_app1, simp, rule lb_app2, simp)
  apply (rule lb_abs, simp)
  apply (rule rtranclp_trans, rule, rule, rule, rule subst_gfresh, simp_all)
  apply (subst substitution [symmetric], auto simp add: fresh_atm)
done

lemma lb_subst: "⟦ t1 ⟶β t2; s1 ⟶β s2 ⟧ ⟹ t1[x ::= s1] ⟶β t2[x ::= s2]"
apply (induction rule: rtranclp_induct)
  apply (nominal_induct t1 avoiding: x s1 s2 rule: lambda.strong_induct)
  apply (simp, simp, rule rtranclp_trans, rule lb_app1)
  defer
  apply (rule lb_app2, simp)
  apply (simp, rule lb_abs, simp)
  apply (auto, rule rtranclp_trans, simp)
  apply (simp add: lb_subst1)
done

lemma par_to_longbeta: "M ⇒β N ⟹ M ⟶β N"
apply (induction rule: par_beta.induct)
  apply (simp)
  apply (rule rtranclp_trans, rule lb_app1, simp, rule lb_app2, simp)
  apply (rule lb_abs, simp)
  apply (rule rtranclp_trans, rule r_into_rtranclp, rule, simp)
  apply (simp add: lb_subst)
done

nominal_primrec nonabs :: "lambda ⇒ bool" where
  "nonabs (lam [_]._) = False"
  | "nonabs (Var _) = True"
  | "nonabs (App _ _) = True"
by (finite_guess+, rule+, fresh_guess+)

lemma nonabs_eqvt[eqvt]:
  fixes π :: "var prm" and M :: lambda
  shows "π ∙ nonabs M = nonabs (π ∙ M)"
by (nominal_induct M rule: lambda.strong_induct, auto)

inductive bstar (infixl "⟶*" 50) where
  bs_var: "Var x ⟶* Var x"
| bs_abs: "M ⟶* M' ⟹ lam [x]. M ⟶* lam [x]. M'"
| bs_app: "⟦ nonabs M1; M1 ⟶* M2; N1 ⟶* N2 ⟧ ⟹ M1 $ N1 ⟶* M2 $ N2"
| bs_beta': "⟦ x ♯ (N1,N2); M1 ⟶* M2; N1 ⟶* N2 ⟧ ⟹ (lam [x]. M1) $ N1 ⟶* M2 [x ::= N2]"

equivariance bstar

nominal_inductive bstar
by (simp_all add: abs_fresh subst_fresh)

lemma bs_beta:
  assumes "M1 ⟶* M2" "N1 ⟶* N2"
  shows "(lam [x]. M1) $ N1 ⟶* M2 [x ::= N2]"
proof-
  obtain y :: var where y: "y ♯ (x,M1,M2,N1,N2)"
    using exists_fresh [of "(x,M1,M2,N1,N2)"]
    using fs_var1 by blast
  have "(lam [x]. M1) $ N1 = (lam [y]. ([(y,x)]∙M1)) $ N1"
    apply (simp add: lambda.inject alpha, rule disjI2, auto)
    using y apply (meson fresh_atm fresh_prodD(1))
    apply (simp add: perm_swap)
    apply (rule perm_fresh_lambda, simp add: y)
    done
  also have "… ⟶* ([(y,x)]∙M2)[y ::= N2]"
    by (rule, simp add: y, simp add: assms bstar.eqvt, rule assms)
  also have "… = M2[x ::= N2]"
    by (auto simp add: subst_rename y)
  finally show "(lam [x]. M1) $ N1 ⟶* M2 [x ::= N2]"
    by simp
qed

lemma elim_pb_var: "Var x ⇒β N ⟹ N = Var x"
by (cases rule: par_beta.cases, auto)

lemma elim_pb_abs:
  assumes "lam [x]. M ⇒β N'" "x ♯ N'"
  obtains N where "M ⇒β N" "N' = lam [x]. N"
using assms
apply (cases rule: par_beta.cases, auto simp add: abs_fresh lambda.inject alpha)
by (metis fresh_bij par_beta.eqvt perm_swap(2) swap_simps(1))

lemma elim_pb_app:
  assumes "M1 $ M2 ⇒β N"
  obtains N1 N2 where "N = N1 $ N2" "M1 ⇒β N1" "M2 ⇒β N2"
     | x P P' L where "M1 = lam[x]. P" "P ⇒β P'" "N = P'[x ::= L]" "M2 ⇒β L" "x ♯ (M2,L)"
using assms
apply (cases rule: par_beta.cases, auto simp add: lambda.inject)
done

lemma elim_pb_app_nonabs:
  assumes "M1 $ M2 ⇒β N" "nonabs M1"
  obtains N1 N2 where "N = N1 $ N2" "M1 ⇒β N1" "M2 ⇒β N2"
using assms
apply (cases rule: par_beta.cases, auto simp add: lambda.inject)
done

lemma elim_pb_app_beta:
  assumes "(lam [x]. M1) $ M2 ⇒β N" "x ♯ (M2,N)"
  obtains N1 N2 where "N = (lam [x]. N1) $ N2" "M1 ⇒β N1" "M2 ⇒β N2"
  | N1 N2 where "N = N1[x ::= N2]" "M1 ⇒β N1" "M2 ⇒β N2"
using assms
apply (cases rule: par_beta.strong_cases [of _ _ _ x x], auto)
apply (auto simp add: lambda.inject)
apply (erule elim_pb_abs, simp add: fresh_prod, simp)
apply (simp add: abs_fresh)
apply (simp add: abs_fresh abs_fun_eq1)
done

lemma pb_subst: "⟦ t1 ⇒β s1; t2 ⇒β s2 ⟧ ⟹ t1 [x ::= t2] ⇒β s1 [x ::= s2]"
apply (nominal_induct avoiding: x t2 s2 rule: par_beta.strong_induct, auto)
  apply (rule, rule, simp, simp)
  apply (rule, simp)
  apply (simp add: fresh_atm pb_beta subst_gfresh' substitution)
done
    
lemma par_to_star: "⟦ t ⟶* t1; t ⇒β t2 ⟧ ⟹ t2 ⇒β t1"
apply (nominal_induct avoiding: t2 rule: bstar.strong_induct)
  using elim_pb_var apply blast
  apply (erule elim_pb_abs, simp, simp, rule, simp)
  apply (erule elim_pb_app, simp, rule, simp, simp, simp)
  apply (erule elim_pb_app_beta, simp, simp, rule, simp, simp, simp)
  apply (simp, rule pb_subst, simp, simp)
done

lemma bstar_fresh:
  fixes x :: var
  assumes "M ⟶* N"
  shows "x ♯ M ⟹ x ♯ N"
using assms apply (nominal_induct rule: bstar.strong_induct, auto)
apply (auto simp add: abs_fresh subst_gfresh)
apply (auto simp add: subst_fresh)
done

lemma elim_bs_abs:
  assumes "lam [x]. t ⟶* s"
  obtains t' where "t ⟶* t'" "s = lam [x]. t'"
proof-
  have Q: "lam [x]. t ⟶* s ⟹ ∃t'. t ⟶* t' ∧ s = lam [x]. t'"
    apply (cases rule: bstar.strong_cases [of _ _ _ x x], auto)
    apply (auto simp add: lambda.inject alpha bstar_fresh abs_fresh)
    done
  show "(⋀t'. t ⟶* t' ⟹ s = lam [x].t' ⟹ thesis) ⟹ thesis"
    using Q [OF assms] by blast
qed

lemma lambda_nonabs_case:
  fixes M :: lambda
  shows "(nonabs M ⟹ thesis) ⟹ (⋀x M'. M = lam [x]. M' ⟹ thesis) ⟹ thesis"
by (nominal_induct M rule: lambda.strong_induct, auto)

lemma star_exist:
  obtains t' where "t ⟶* t'"
proof-
  have "∃t'. t ⟶* t'"
    apply (nominal_induct t rule: lambda.strong_induct, auto)
    apply (rule, rule)
    defer
    apply (rule, rule, simp)
    proof-
      fix M1 M2 N N'
      assume hyp: "M1 ⟶* N" "M2 ⟶* N'"
      show "∃t'. M1 $ M2 ⟶* t'"
        apply (rule_tac lambda_nonabs_case [of M1])
        apply (rule, rule, simp, rule hyp, rule hyp)
        proof-
          fix x M'
          assume M1: "M1 = lam [x].M'"
          then obtain N1 where N1: "N = lam [x].N1" "M' ⟶* N1"
            using elim_bs_abs hyp(1) by blast
          have "M1 $ M2 ⟶* N1 [x ::= N']"
            by (simp add: M1, rule bs_beta, simp add: N1, simp add: hyp)
          thus ?thesis by blast
        qed
    qed
  thus "(⋀t'. t ⟶* t' ⟹ thesis) ⟹ thesis" by blast
qed
  
lemma par_confluent:
  assumes "t ⇒β t1" "t ⇒β t2"
  obtains s where "t1 ⇒β s" "t2 ⇒β s"
proof-
  obtain t' where t': "t ⟶* t'"
    using star_exist by auto 
  have "t1 ⇒β t'" "t2 ⇒β t'"
    using par_to_star [OF t'] assms by auto
  thus "(⋀s. t1 ⇒β s ⟹ t2 ⇒β s ⟹ thesis) ⟹ thesis" by blast
qed

abbreviation long_par_beta (infixl "⟹β" 50) where
  "long_par_beta == par_beta⇧*⇧*"

lemma long_pb_iff_long_b: "t ⟹β s ⟷ t ⟶β s"
apply rule
apply (induct rule: rtranclp_induct)
  apply simp
  apply (rule rtranclp_trans, simp, simp add: par_to_longbeta)
apply (induct rule: rtranclp_induct)
  apply simp
  apply (rule rtranclp_trans, simp, rule r_into_rtranclp, simp add: one_to_par)
done

lemma CR:
  assumes "t ⟶β t1" "t ⟶β t2"
  obtains s where "t1 ⟶β s" "t2 ⟶β s"
proof-
  have CR_one_long: "⋀t t1 t2. ⟦ t ⟹β t2; t ⇒β t1 ⟧ ⟹ ∃s. t1 ⟹β s ∧ t2 ⇒β s"
    proof-
      fix t t1 t2
      show "⟦ t ⟹β t2; t ⇒β t1 ⟧ ⟹ ∃s. t1 ⟹β s ∧ t2 ⇒β s"
        proof (induct arbitrary: t1 rule: rtranclp_induct)
          fix t1 show "t ⇒β t1 ⟹ ∃s. t1 ⟹β s ∧ t ⇒β s"
            by (rule par_confluent, rule pb_refl, simp, blast)
        next
          fix y z t1
          assume t: "t ⟹β y" "y ⇒β z" and hyp: "⋀t1. t ⇒β t1 ⟹ ∃s. t1 ⟹β s ∧ y ⇒β s" and t2: "t ⇒β t1"
          obtain s where s: "t1 ⟹β s" "y ⇒β s" using hyp t t2 by blast
          obtain s' where s': "s ⇒β s'" "z ⇒β s'" using par_confluent [OF t(2) s(2)] by blast
          have "t1 ⟹β s'" "z ⇒β s'"
            by (rule, rule s, rule s', rule s')
          thus "∃s. t1 ⟹β s ∧ z ⇒β s"
            by blast
        qed
    qed

  have CR_long_long: "⟦ t ⟹β t1; t ⟹β t2 ⟧ ⟹ ∃s. t1 ⟹β s ∧ t2 ⟹β s"
    apply (induct arbitrary: t2 rule: rtranclp_induct)
      apply (rule, rule, simp, simp)
      using CR_one_long apply (meson rtranclp.rtrancl_into_rtrancl)
    done

  have "t ⟹β t1" "t ⟹β t2"
    using assms by (simp add: long_pb_iff_long_b, simp add: long_pb_iff_long_b)
  hence "∃s. t1 ⟹β s ∧ t2 ⟹β s"
    by (rule CR_long_long)
  hence "∃s. t1 ⟶β s ∧ t2 ⟶β s"
    by (simp add: long_pb_iff_long_b)
  thus "(⋀s. t1 ⟶β s ⟹ t2 ⟶β s ⟹ thesis) ⟹ thesis"
    by blast
qed

end