Quelle Substitution.thy

Sprache: Isabelle

(*  Title:      ZF/Resid/Substitution.thy
Author: Ole Rasmussen, University of Cambridge
*)

theory Substitution imports Redex begin

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

consts
  lift_aux      :: "i==>i"
primrec
  "lift_aux(Var(i)) = (λk ∈ nat. if 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))"

definition
  lift_rec      :: "[i,i]==> i"  where
    "lift_rec(r,k) ≡ lift_aux(r)`k"

abbreviation
  lift :: "i==>i" where
  "lift(r) ≡ lift_rec(r,0)"

consts
  subst_aux     :: "i==>i"
primrec
  "subst_aux(Var(i)) =
     (λr ∈ redexes. λk ∈ nat. if k
                                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))"

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

abbreviation
  subst :: "[i,i]==>i"  (infixl ‹'/› 70)  where
  "u/v ≡ subst_rec(u,v,0)"

(* ------------------------------------------------------------------------- *)
(*   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)∈ nat] ==> x < n #- 1 "
apply (rule succ_leE)
apply (simp add: succ_pred)
done

lemma gt_pred: "[n < succ(x); p∈ 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
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] ==> 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
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] ==> subst_rec(u,Var(n),p) = Var(n #- 1)"
by (simp add: subst_rec_def)

lemma subst_lt [simp]:
     "[u ∈ redexes; p ∈ nat; n] ==> 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\<in>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

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet am 2026-04-28) ¤

*© 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.