# Theory Substitution

Up to index of Isabelle/ZF/Resid

theory Substitution
imports Redex
begin

    (*  Title:      ZF/Resid/Substitution.thy
        ID:         $Id: Substitution.thy,v 1.13 2005/06/17 14:15:11 haftmann Exp $
        Author:     Ole Rasmussen
        Copyright   1995  University of Cambridge
        Logic Image: ZF
    *)

    theory Substitution imports Redex begin

    consts
      lift_aux      :: "i=>i"
      lift          :: "i=>i"
      subst_aux     :: "i=>i"
      "'/"          :: "[i,i]=>i"  (infixl 70)  (*subst*)

    constdefs
      lift_rec      :: "[i,i]=> i"
        "lift_rec(r,k) == lift_aux(r)`k"

      subst_rec     :: "[i,i,i]=> i"        (**NOTE THE ARGUMENT ORDER BELOW**)
        "subst_rec(u,r,k) == subst_aux(r)`u`k"

    translations
      "lift(r)"  == "lift_rec(r,0)"
      "u/v"      == "subst_rec(u,v,0)"

    (** The clumsy _aux functions are required because other arguments vary
        in the recursive calls ***)

    primrec
      "lift_aux(Var(i)) = (λk ∈ nat. if i<k then Var(i) else Var(succ(i)))"

      "lift_aux(Fun(t)) = (λk ∈ nat. Fun(lift_aux(t) ` succ(k)))"

      "lift_aux(App(b,f,a)) = (λk ∈ nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"

    primrec
      "subst_aux(Var(i)) =
         (λr ∈ redexes. λk ∈ nat. if k<i then Var(i #- 1)
                                    else if k=i then r else Var(i))"
      "subst_aux(Fun(t)) =
         (λr ∈ redexes. λk ∈ nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"

      "subst_aux(App(b,f,a)) =
         (λr ∈ redexes. λk ∈ nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"

    (* ------------------------------------------------------------------------- *)
    (*   Arithmetic extensions                                                   *)
    (* ------------------------------------------------------------------------- *)

    lemma gt_not_eq: "p < n ==> n≠p"
    by blast

    lemma succ_pred [rule_format, simp]: "j ∈ nat ==> i < j --> succ(j #- 1) = j"
    by (induct_tac "j", auto)

    lemma lt_pred: "[|succ(x)<n; n ∈ nat|] ==> x < n #- 1 "
    apply (rule succ_leE)
    apply (simp add: succ_pred)
    done

    lemma gt_pred: "[|n < succ(x); p<n; n ∈ nat|] ==> n #- 1 < x "
    apply (rule succ_leE)
    apply (simp add: succ_pred)
    done

    declare not_lt_iff_le [simp] if_P [simp] if_not_P [simp]

    (* ------------------------------------------------------------------------- *)
    (*     lift_rec equality rules                                               *)
    (* ------------------------------------------------------------------------- *)
    lemma lift_rec_Var:
         "n ∈ nat ==> lift_rec(Var(i),n) = (if i<n then Var(i) else Var(succ(i)))"
    by (simp add: lift_rec_def)

    lemma lift_rec_le [simp]:
         "[|i ∈ nat; k≤i|] ==> lift_rec(Var(i),k) = Var(succ(i))"
    by (simp add: lift_rec_def le_in_nat)

    lemma lift_rec_gt [simp]: "[| k ∈ nat; i<k |] ==> lift_rec(Var(i),k) = Var(i)"
    by (simp add: lift_rec_def)

    lemma lift_rec_Fun [simp]:
         "k ∈ nat ==> lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))"
    by (simp add: lift_rec_def)

    lemma lift_rec_App [simp]:
         "k ∈ nat ==> lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))"
    by (simp add: lift_rec_def)

    (* ------------------------------------------------------------------------- *)
    (*    substitution quality rules                                             *)
    (* ------------------------------------------------------------------------- *)

    lemma subst_Var:
         "[|k ∈ nat; u ∈ redexes|]
          ==> subst_rec(u,Var(i),k) =
              (if k<i then Var(i #- 1) else if k=i then u else Var(i))"
    by (simp add: subst_rec_def gt_not_eq leI)

    lemma subst_eq [simp]:
         "[|n ∈ nat; u ∈ redexes|] ==> subst_rec(u,Var(n),n) = u"
    by (simp add: subst_rec_def)

    lemma subst_gt [simp]:
         "[|u ∈ redexes; p ∈ nat; p<n|] ==> subst_rec(u,Var(n),p) = Var(n #- 1)"
    by (simp add: subst_rec_def)

    lemma subst_lt [simp]:
         "[|u ∈ redexes; p ∈ nat; n<p|] ==> subst_rec(u,Var(n),p) = Var(n)"
    by (simp add: subst_rec_def gt_not_eq leI lt_nat_in_nat)

    lemma subst_Fun [simp]:
         "[|p ∈ nat; u ∈ redexes|]
          ==> subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) "
    by (simp add: subst_rec_def)

    lemma subst_App [simp]:
         "[|p ∈ nat; u ∈ redexes|]
          ==> subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))"
    by (simp add: subst_rec_def)

    lemma lift_rec_type [rule_format, simp]:
         "u ∈ redexes ==> ∀k ∈ nat. lift_rec(u,k) ∈ redexes"
    apply (erule redexes.induct)
    apply (simp_all add: lift_rec_Var lift_rec_Fun lift_rec_App)
    done

    lemma subst_type [rule_format, simp]:
         "v ∈ redexes ==>  ∀n ∈ nat. ∀u ∈ redexes. subst_rec(u,v,n) ∈ redexes"
    apply (erule redexes.induct)
    apply (simp_all add: subst_Var lift_rec_type)
    done

    (* ------------------------------------------------------------------------- *)
    (*    lift and  substitution proofs                                          *)
    (* ------------------------------------------------------------------------- *)

    (*The i∈nat is redundant*)
    lemma lift_lift_rec [rule_format]:
         "u ∈ redexes
          ==> ∀n ∈ nat. ∀i ∈ nat. i≤n -->
               (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))"
    apply (erule redexes.induct, auto)
    apply (case_tac "n < i")
    apply (frule lt_trans2, assumption)
    apply (simp_all add: lift_rec_Var leI)
    done

    lemma lift_lift:
         "[|u ∈ redexes; n ∈ nat|]
          ==> lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"
    by (simp add: lift_lift_rec)

    lemma lt_not_m1_lt: "[|m < n; n ∈ nat; m ∈ nat|]==> ~ n #- 1 < m"
    by (erule natE, auto)

    lemma lift_rec_subst_rec [rule_format]:
         "v ∈ redexes ==>
           ∀n ∈ nat. ∀m ∈ nat. ∀u ∈ redexes. n≤m-->
              lift_rec(subst_rec(u,v,n),m) =
                   subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"
    apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift)
    apply safe
    apply (rename_tac n n' m u)
    apply (case_tac "n < n'")
     apply (frule_tac j = n' in lt_trans2, assumption)
     apply (simp add: leI, simp)
    apply (erule_tac j=n in leE)
    apply (auto simp add: lift_rec_Var subst_Var leI lt_not_m1_lt)
    done

    lemma lift_subst:
         "[|v ∈ redexes; u ∈ redexes; n ∈ nat|]
          ==> lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))"
    by (simp add: lift_rec_subst_rec)

    lemma lift_rec_subst_rec_lt [rule_format]:
         "v ∈ redexes ==>
           ∀n ∈ nat. ∀m ∈ nat. ∀u ∈ redexes. m≤n-->
              lift_rec(subst_rec(u,v,n),m) =
                   subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))"
    apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift)
    apply safe
    apply (rename_tac n n' m u)
    apply (case_tac "n < n'")
    apply (case_tac "n < m")
    apply (simp_all add: leI)
    apply (erule_tac i=n' in leE)
    apply (frule lt_trans1, assumption)
    apply (simp_all add: succ_pred leI gt_pred)
    done

    lemma subst_rec_lift_rec [rule_format]:
         "u ∈ redexes ==>
            ∀n ∈ nat. ∀v ∈ redexes. subst_rec(v,lift_rec(u,n),n) = u"
    apply (erule redexes.induct, auto)
    apply (case_tac "n < na", auto)
    done

    lemma subst_rec_subst_rec [rule_format]:
         "v ∈ redexes ==>
            ∀m ∈ nat. ∀n ∈ nat. ∀u ∈ redexes. ∀w ∈ redexes. m≤n -->
              subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m) =
              subst_rec(w,subst_rec(u,v,m),n)"
    apply (erule redexes.induct)
    apply (simp_all add: lift_lift [symmetric] lift_rec_subst_rec_lt, safe)
    apply (rename_tac n' u w)
    apply (case_tac "n ≤ succ(n') ")
     apply (erule_tac i = n in leE)
     apply (simp_all add: succ_pred subst_rec_lift_rec leI)
     apply (case_tac "n < m")
      apply (frule lt_trans2, assumption, simp add: gt_pred)
     apply simp
     apply (erule_tac j = n in leE, simp add: gt_pred)
     apply (simp add: subst_rec_lift_rec)
    (*final case*)
    apply (frule nat_into_Ord [THEN le_refl, THEN lt_trans], assumption)
    apply (erule leE)
     apply (frule succ_leI [THEN lt_trans], assumption)
     apply (frule_tac i = m in nat_into_Ord [THEN le_refl, THEN lt_trans],
            assumption)
     apply (simp_all add: succ_pred lt_pred)
    done

    lemma substitution:
         "[|v ∈ redexes; u ∈ redexes; w ∈ redexes; n ∈ nat|]
          ==> subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)"
    by (simp add: subst_rec_subst_rec)

    (* ------------------------------------------------------------------------- *)
    (*          Preservation lemmas                                              *)
    (*          Substitution preserves comp and regular                          *)
    (* ------------------------------------------------------------------------- *)

    lemma lift_rec_preserve_comp [rule_format, simp]:
         "u ~ v ==> ∀m ∈ nat. lift_rec(u,m) ~ lift_rec(v,m)"
    by (erule Scomp.induct, simp_all add: comp_refl)

    lemma subst_rec_preserve_comp [rule_format, simp]:
         "u2 ~ v2 ==> ∀m ∈ nat. ∀u1 ∈ redexes. ∀v1 ∈ redexes.
                      u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)"
    by (erule Scomp.induct,
        simp_all add: subst_Var lift_rec_preserve_comp comp_refl)

    lemma lift_rec_preserve_reg [simp]:
         "regular(u) ==> ∀m ∈ nat. regular(lift_rec(u,m))"
    by (erule Sreg.induct, simp_all add: lift_rec_Var)

    lemma subst_rec_preserve_reg [simp]:
         "regular(v) ==>
            ∀m ∈ nat. ∀u ∈ redexes. regular(u)-->regular(subst_rec(u,v,m))"
    by (erule Sreg.induct, simp_all add: subst_Var lift_rec_preserve_reg)

    end

lemma gt_not_eq:

      p < n ==> n ≠ p

lemma succ_pred:

      [| j ∈ nat; i < j |] ==> succ(j #- 1) = j

lemma lt_pred:

      [| succ(x) < n; n ∈ nat |] ==> x < n #- 1

lemma gt_pred:

      [| n ≤ x; p < n; n ∈ nat |] ==> n #- 1 < x

lemma lift_rec_Var:

      n ∈ nat ==> lift_rec(Var(i), n) = (if i < n then Var(i) else Var(succ(i)))

lemma lift_rec_le:

      [| i ∈ nat; k ≤ i |] ==> lift_rec(Var(i), k) = Var(succ(i))

lemma lift_rec_gt:

      [| k ∈ nat; i < k |] ==> lift_rec(Var(i), k) = Var(i)

lemma lift_rec_Fun:

      k ∈ nat ==> lift_rec(Fun(t), k) = Fun(lift_rec(t, succ(k)))

lemma lift_rec_App:

      k ∈ nat ==> lift_rec(App(b, f, a), k) = App(b, lift_rec(f, k), lift_rec(a, k))

lemma subst_Var:

      [| k ∈ nat; u ∈ redexes |]
      ==> subst_rec(u, Var(i), k) =
          (if k < i then Var(i #- 1) else if k = i then u else Var(i))

lemma subst_eq:

      [| n ∈ nat; u ∈ redexes |] ==> subst_rec(u, Var(n), n) = u

lemma subst_gt:

      [| u ∈ redexes; p ∈ nat; p < n |] ==> subst_rec(u, Var(n), p) = Var(n #- 1)

lemma subst_lt:

      [| u ∈ redexes; p ∈ nat; n < p |] ==> subst_rec(u, Var(n), p) = Var(n)

lemma subst_Fun:

      [| p ∈ nat; u ∈ redexes |]
      ==> subst_rec(u, Fun(t), p) = Fun(subst_rec(lift(u), t, succ(p)))

lemma subst_App:

      [| p ∈ nat; u ∈ redexes |]
      ==> subst_rec(u, App(b, f, a), p) =
          App(b, subst_rec(u, f, p), subst_rec(u, a, p))

lemma lift_rec_type:

      [| u ∈ redexes; k ∈ nat |] ==> lift_rec(u, k) ∈ redexes

lemma subst_type:

      [| v ∈ redexes; n ∈ nat; u ∈ redexes |] ==> subst_rec(u, v, n) ∈ redexes

lemma lift_lift_rec:

      [| u ∈ redexes; n ∈ nat; i ∈ nat; i ≤ n |]
      ==> lift_rec(lift_rec(u, i), succ(n)) = lift_rec(lift_rec(u, n), i)

lemma lift_lift:

      [| u ∈ redexes; n ∈ nat |] ==> lift_rec(lift(u), succ(n)) = lift(lift_rec(u, n))

lemma lt_not_m1_lt:

      [| m < n; n ∈ nat; m ∈ nat |] ==> ¬ n #- 1 < m

lemma lift_rec_subst_rec:

      [| v ∈ redexes; n ∈ nat; m ∈ nat; u ∈ redexes; n ≤ m |]
      ==> lift_rec(subst_rec(u, v, n), m) =
          subst_rec(lift_rec(u, m), lift_rec(v, succ(m)), n)

lemma lift_subst:

      [| v ∈ redexes; u ∈ redexes; n ∈ nat |]
      ==> lift_rec(u / v, n) = lift_rec(u, n) / lift_rec(v, succ(n))

lemma lift_rec_subst_rec_lt:

      [| v ∈ redexes; n ∈ nat; m ∈ nat; u ∈ redexes; m ≤ n |]
      ==> lift_rec(subst_rec(u, v, n), m) =
          subst_rec(lift_rec(u, m), lift_rec(v, m), succ(n))

lemma subst_rec_lift_rec:

      [| u ∈ redexes; n ∈ nat; v ∈ redexes |] ==> subst_rec(v, lift_rec(u, n), n) = u

lemma subst_rec_subst_rec:

      [| v ∈ redexes; m ∈ nat; n ∈ nat; u ∈ redexes; w ∈ redexes; m ≤ n |]
      ==> subst_rec(subst_rec(w, u, n), subst_rec(lift_rec(w, m), v, succ(n)), m) =
          subst_rec(w, subst_rec(u, v, m), n)

lemma substitution:

      [| v ∈ redexes; u ∈ redexes; w ∈ redexes; n ∈ nat |]
      ==> subst_rec(w, u, n) / subst_rec(lift(w), v, succ(n)) = subst_rec(w, u / v, n)

lemma lift_rec_preserve_comp:

      [| u ~ v; m ∈ nat |] ==> lift_rec(u, m) ~ lift_rec(v, m)

lemma subst_rec_preserve_comp:

      [| u2.0 ~ v2.0; m ∈ nat; u1.0 ∈ redexes; v1.0 ∈ redexes; u1.0 ~ v1.0 |]
      ==> subst_rec(u1.0, u2.0, m) ~ subst_rec(v1.0, v2.0, m)

lemma lift_rec_preserve_reg:

      regular(u) ==> ∀m∈nat. regular(lift_rec(u, m))

lemma subst_rec_preserve_reg:

      regular(v) ==> ∀m∈nat. ∀u∈redexes. regular(u) --> regular(subst_rec(u, v, m))