# Theory Subst

Up to index of Isabelle/HOL/Subst

theory Subst
imports AList UTerm
begin

    (*  Title:      Subst/Subst.thy
        ID:         $Id: Subst.thy,v 1.11 2005/04/01 19:04:00 paulson Exp $
        Author:     Martin Coen, Cambridge University Computer Laboratory
        Copyright   1993  University of Cambridge
    *)

    header{*Substitutions on uterms*}

    theory Subst
    imports AList UTerm
    begin

    consts

      "=$="  ::  "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52)
      "<|"   ::  "'a uterm => ('a * 'a uterm) list => 'a uterm"        (infixl 55)
      "<>"   ::  "[('a*('a uterm)) list, ('a*('a uterm)) list]
                     => ('a*('a uterm)) list"                          (infixl 56)
      sdom   ::  "('a*('a uterm)) list => 'a set"
      srange ::  "('a*('a uterm)) list => 'a set"

    syntax (xsymbols)
      "op =$=" :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool"
                  (infixr "\<doteq>" 52)
      "op <|" :: "'a uterm => ('a * 'a uterm) list => 'a uterm" (infixl "\<lhd>" 55)
      "op <>" :: "[('a*('a uterm)) list, ('a*('a uterm)) list]
                     => ('a*('a uterm)) list"                   (infixl "◊" 56)

    primrec
      subst_Var:      "(Var v \<lhd> s) = assoc v (Var v) s"
      subst_Const:  "(Const c \<lhd> s) = Const c"
      subst_Comb:  "(Comb M N \<lhd> s) = Comb (M \<lhd> s) (N \<lhd> s)"

    defs

      subst_eq_def:  "r =$= s == ALL t. t \<lhd> r = t \<lhd> s"

      comp_def:    "al ◊ bl == alist_rec al bl (%x y xs g. (x,y \<lhd> bl)#g)"

      sdom_def:
      "sdom(al) == alist_rec al {}
                    (%x y xs g. if Var(x)=y then g - {x} else g Un {x})"

      srange_def:
       "srange(al) == Union({y. ∃x ∈ sdom(al). y = vars_of(Var(x) \<lhd> al)})"

    subsection{*Basic Laws*}

    lemma subst_Nil [simp]: "t \<lhd> [] = t"
    by (induct_tac "t", auto)

    lemma subst_mono [rule_format]: "t \<prec> u --> t \<lhd> s \<prec> u \<lhd> s"
    by (induct_tac "u", auto)

    lemma Var_not_occs [rule_format]:
         "~ (Var(v) \<prec> t) --> t \<lhd> (v,t \<lhd> s) # s = t \<lhd> s"
    apply (case_tac "t = Var v")
    apply (erule_tac [2] rev_mp)
    apply (rule_tac [2] P =
             "%x. x ≠ Var v --> ~(Var v \<prec> x) --> x \<lhd> (v,t\<lhd>s) #s = x\<lhd>s"
           in uterm.induct)
    apply auto
    done

    lemma agreement: "(t\<lhd>r = t\<lhd>s) = (∀v ∈ vars_of t. Var v \<lhd> r = Var v \<lhd> s)"
    by (induct_tac "t", auto)

    lemma repl_invariance: "~ v: vars_of(t) ==> t \<lhd> (v,u)#s = t \<lhd> s"
    by (simp add: agreement)

    lemma Var_in_subst [rule_format]:
         "v ∈ vars_of(t) --> w ∈ vars_of(t \<lhd> (v,Var(w))#s)"
    by (induct_tac "t", auto)

    subsection{*Equality between Substitutions*}

    lemma subst_eq_iff: "r \<doteq> s = (∀t. t \<lhd> r = t \<lhd> s)"
    by (simp add: subst_eq_def)

    lemma subst_refl [iff]: "r \<doteq> r"
    by (simp add: subst_eq_iff)

    lemma subst_sym: "r \<doteq> s ==> s \<doteq> r"
    by (simp add: subst_eq_iff)

    lemma subst_trans: "[| q \<doteq> r; r \<doteq> s |] ==> q \<doteq> s"
    by (simp add: subst_eq_iff)

    lemma subst_subst2:
        "[| r \<doteq> s; P (t \<lhd> r) (u \<lhd> r) |] ==> P (t \<lhd> s) (u \<lhd> s)"
    by (simp add: subst_eq_def)

    lemmas ssubst_subst2 = subst_sym [THEN subst_subst2]

    subsection{*Composition of Substitutions*}

    lemma [simp]:
         "[] ◊ bl = bl"
         "((a,b)#al) ◊ bl = (a,b \<lhd> bl) # (al ◊ bl)"
         "sdom([]) = {}"
         "sdom((a,b)#al) = (if Var(a)=b then (sdom al) - {a} else sdom al Un {a})"
    by (simp_all add: comp_def sdom_def)

    lemma comp_Nil [simp]: "s ◊ [] = s"
    by (induct "s", auto)

    lemma subst_comp_Nil: "s \<doteq> s ◊ []"
    by simp

    lemma subst_comp [simp]: "(t \<lhd> r ◊ s) = (t \<lhd> r \<lhd> s)"
    apply (induct_tac "t")
    apply (simp_all (no_asm_simp))
    apply (induct "r", auto)
    done

    lemma comp_assoc: "(q ◊ r) ◊ s \<doteq> q ◊ (r ◊ s)"
    by (simp add: subst_eq_iff)

    lemma subst_cong:
         "[| theta \<doteq> theta1; sigma \<doteq> sigma1|]
          ==> (theta ◊ sigma) \<doteq> (theta1 ◊ sigma1)"
    by (simp add: subst_eq_def)

    lemma Cons_trivial: "(w, Var(w) \<lhd> s) # s \<doteq> s"
    apply (simp add: subst_eq_iff)
    apply (rule allI)
    apply (induct_tac "t", simp_all)
    done

    lemma comp_subst_subst: "q ◊ r \<doteq> s ==>  t \<lhd> q \<lhd> r = t \<lhd> s"
    by (simp add: subst_eq_iff)

    subsection{*Domain and range of Substitutions*}

    lemma sdom_iff: "(v ∈ sdom(s)) = (Var(v) \<lhd> s ~= Var(v))"
    apply (induct "s")
    apply (case_tac [2] a, auto)
    done

    lemma srange_iff:
       "v ∈ srange(s) = (∃w. w ∈ sdom(s) & v ∈ vars_of(Var(w) \<lhd> s))"
    by (auto simp add: srange_def)

    lemma empty_iff_all_not: "(A = {}) = (ALL a.~ a:A)"
    by (unfold empty_def, blast)

    lemma invariance: "(t \<lhd> s = t) = (sdom(s) Int vars_of(t) = {})"
    apply (induct_tac "t")
    apply (auto simp add: empty_iff_all_not sdom_iff)
    done

    lemma Var_in_srange [rule_format]:
         "v ∈ sdom(s) -->  v ∈ vars_of(t \<lhd> s) --> v ∈ srange(s)"
    apply (induct_tac "t")
    apply (case_tac "a ∈ sdom s")
    apply (auto simp add: sdom_iff srange_iff)
    done

    lemma Var_elim: "[| v ∈ sdom(s); v ∉ srange(s) |] ==>  v ∉ vars_of(t \<lhd> s)"
    by (blast intro: Var_in_srange)

    lemma Var_intro [rule_format]:
         "v ∈ vars_of(t \<lhd> s) --> v ∈ srange(s) | v ∈ vars_of(t)"
    apply (induct_tac "t")
    apply (auto simp add: sdom_iff srange_iff)
    apply (rule_tac x=a in exI, auto)
    done

    lemma srangeD: "v ∈ srange(s) ==> ∃w. w ∈ sdom(s) & v ∈ vars_of(Var(w) \<lhd> s)"
    by (simp add: srange_iff)

    lemma dom_range_disjoint:
         "sdom(s) Int srange(s) = {} = (∀t. sdom(s) Int vars_of(t \<lhd> s) = {})"
    apply (simp add: empty_iff_all_not)
    apply (force intro: Var_in_srange dest: srangeD)
    done

    lemma subst_not_empty: "~ u \<lhd> s = u ==> (∃x. x ∈ sdom(s))"
    by (auto simp add: empty_iff_all_not invariance)

    lemma id_subst_lemma [simp]: "(M \<lhd> [(x, Var x)]) = M"
    by (induct_tac "M", auto)

    end

### Basic Laws

lemma subst_Nil:

      t <| [] = t

lemma subst_mono:

      t <: u ==> t <| s <: u <| s

lemma Var_not_occs:

      ¬ Var v <: t ==> t <| (v, t <| s) # s = t <| s

lemma agreement:

      (t <| r = t <| s) = (∀v∈vars_of t. Var v <| r = Var v <| s)

lemma repl_invariance:

      v ∉ vars_of t ==> t <| (v, u) # s = t <| s

lemma Var_in_subst:

      v ∈ vars_of t ==> w ∈ vars_of (t <| (v, Var w) # s)

### Equality between Substitutions

lemma subst_eq_iff:

      r =$= s = (∀t. t <| r = t <| s)

lemma subst_refl:

      r =$= r

lemma subst_sym:

      r =$= s ==> s =$= r

lemma subst_trans:

      [| q =$= r; r =$= s |] ==> q =$= s

lemma subst_subst2:

      [| r =$= s; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)

lemmas ssubst_subst2:

      [| s =$= r; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)

lemmas ssubst_subst2:

      [| s =$= r; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)

### Composition of Substitutions

lemma

      [] <> bl = bl

      (a, b) # al <> bl = (a, b <| bl) # (al <> bl)

      sdom [] = {}

      sdom ((a, b) # al) = (if Var a = b then sdom al - {a} else sdom al ∪ {a})

lemma comp_Nil:

      s <> [] = s

lemma subst_comp_Nil:

      s =$= s <> []

lemma subst_comp:

      t <| r <> s = t <| r <| s

lemma comp_assoc:

      q <> r <> s =$= q <> (r <> s)

lemma subst_cong:

      [| theta =$= theta1.0; sigma =$= sigma1.0 |]
      ==> theta <> sigma =$= theta1.0 <> sigma1.0

lemma Cons_trivial:

      (w, Var w <| s) # s =$= s

lemma comp_subst_subst:

      q <> r =$= s ==> t <| q <| r = t <| s

### Domain and range of Substitutions

lemma sdom_iff:

      (v ∈ sdom s) = (Var v <| s ≠ Var v)

lemma srange_iff:

      (v ∈ srange s) = (∃w. w ∈ sdom s ∧ v ∈ vars_of (Var w <| s))

lemma empty_iff_all_not:

      (A = {}) = (∀a. a ∉ A)

lemma invariance:

      (t <| s = t) = (sdom s ∩ vars_of t = {})

lemma Var_in_srange:

      [| v ∈ sdom s; v ∈ vars_of (t <| s) |] ==> v ∈ srange s

lemma Var_elim:

      [| v ∈ sdom s; v ∉ srange s |] ==> v ∉ vars_of (t <| s)

lemma Var_intro:

      v ∈ vars_of (t <| s) ==> v ∈ srange s ∨ v ∈ vars_of t

lemma srangeD:

      v ∈ srange s ==> ∃w. w ∈ sdom s ∧ v ∈ vars_of (Var w <| s)

lemma dom_range_disjoint:

      (sdom s ∩ srange s = {}) = (∀t. sdom s ∩ vars_of (t <| s) = {})

lemma subst_not_empty:

      u <| s ≠ u ==> ∃x. x ∈ sdom s

lemma id_subst_lemma:

      M <| [(x, Var x)] = M