# Theory Residuals

Up to index of Isabelle/ZF/Resid

theory Residuals
imports Substitution
begin

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

    *)

    theory Residuals imports Substitution begin

    consts
      Sres          :: "i"
      residuals     :: "[i,i,i]=>i"
      "|>"          :: "[i,i]=>i"     (infixl 70)

    translations
      "residuals(u,v,w)"  == "<u,v,w> ∈ Sres"

    inductive
      domains       "Sres" <= "redexes*redexes*redexes"
      intros
        Res_Var:    "n ∈ nat ==> residuals(Var(n),Var(n),Var(n))"
        Res_Fun:    "[|residuals(u,v,w)|]==>
                         residuals(Fun(u),Fun(v),Fun(w))"
        Res_App:    "[|residuals(u1,v1,w1);
                       residuals(u2,v2,w2); b ∈ bool|]==>
                     residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
        Res_redex:  "[|residuals(u1,v1,w1);
                       residuals(u2,v2,w2); b ∈ bool|]==>
                     residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
      type_intros    subst_type nat_typechecks redexes.intros bool_typechecks

    defs
      res_func_def:  "u |> v == THE w. residuals(u,v,w)"

    subsection{*Setting up rule lists*}

    declare Sres.intros [intro]
    declare Sreg.intros [intro]
    declare subst_type [intro]

    inductive_cases [elim!]:
      "residuals(Var(n),Var(n),v)"
      "residuals(Fun(t),Fun(u),v)"
      "residuals(App(b, u1, u2), App(0, v1, v2),v)"
      "residuals(App(b, u1, u2), App(1, Fun(v1), v2),v)"
      "residuals(Var(n),u,v)"
      "residuals(Fun(t),u,v)"
      "residuals(App(b, u1, u2), w,v)"
      "residuals(u,Var(n),v)"
      "residuals(u,Fun(t),v)"
      "residuals(w,App(b, u1, u2),v)"

    inductive_cases [elim!]:
      "Var(n) <== u"
      "Fun(n) <== u"
      "u <== Fun(n)"
      "App(1,Fun(t),a) <== u"
      "App(0,t,a) <== u"

    inductive_cases [elim!]:
      "Fun(t) ∈ redexes"

    declare Sres.intros [simp]

    subsection{*residuals is a  partial function*}

    lemma residuals_function [rule_format]:
         "residuals(u,v,w) ==> ∀w1. residuals(u,v,w1) --> w1 = w"
    by (erule Sres.induct, force+)

    lemma residuals_intro [rule_format]:
         "u~v ==> regular(v) --> (∃w. residuals(u,v,w))"
    by (erule Scomp.induct, force+)

    lemma comp_resfuncD:
         "[| u~v;  regular(v) |] ==> residuals(u, v, THE w. residuals(u, v, w))"
    apply (frule residuals_intro, assumption, clarify)
    apply (subst the_equality)
    apply (blast intro: residuals_function)+
    done

    subsection{*Residual function*}

    lemma res_Var [simp]: "n ∈ nat ==> Var(n) |> Var(n) = Var(n)"
    by (unfold res_func_def, blast)

    lemma res_Fun [simp]:
        "[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)"
    apply (unfold res_func_def)
    apply (blast intro: comp_resfuncD residuals_function)
    done

    lemma res_App [simp]:
        "[|s~u; regular(u); t~v; regular(v); b ∈ bool|]
         ==> App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)"
    apply (unfold res_func_def)
    apply (blast dest!: comp_resfuncD intro: residuals_function)
    done

    lemma res_redex [simp]:
        "[|s~u; regular(u); t~v; regular(v); b ∈ bool|]
         ==> App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)"
    apply (unfold res_func_def)
    apply (blast elim!: redexes.free_elims dest!: comp_resfuncD
                 intro: residuals_function)
    done

    lemma resfunc_type [simp]:
         "[|s~t; regular(t)|]==> regular(t) --> s |> t ∈ redexes"
      by (erule Scomp.induct, auto)

    subsection{*Commutation theorem*}

    lemma sub_comp [simp]: "u<==v ==> u~v"
    by (erule Ssub.induct, simp_all)

    lemma sub_preserve_reg [rule_format, simp]:
         "u<==v  ==> regular(v) --> regular(u)"
    by (erule Ssub.induct, auto)

    lemma residuals_lift_rec: "[|u~v; k ∈ nat|]==> regular(v)--> (∀n ∈ nat.
             lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))"
    apply (erule Scomp.induct, safe)
    apply (simp_all add: lift_rec_Var subst_Var lift_subst)
    done

    lemma residuals_subst_rec:
         "u1~u2 ==>  ∀v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->
                      (∀n ∈ nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) =
                        subst_rec(v1 |> v2, u1 |> u2,n))"
    apply (erule Scomp.induct, safe)
    apply (simp_all add: lift_rec_Var subst_Var residuals_lift_rec)
    apply (drule_tac psi = "∀x.?P (x) " in asm_rl)
    apply (simp add: substitution)
    done

    lemma commutation [simp]:
         "[|u1~u2; v1~v2; regular(u2); regular(v2)|]
          ==> (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)"
    by (simp add: residuals_subst_rec)

    subsection{*Residuals are comp and regular*}

    lemma residuals_preserve_comp [rule_format, simp]:
         "u~v ==> ∀w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)"
    by (erule Scomp.induct, force+)

    lemma residuals_preserve_reg [rule_format, simp]:
         "u~v ==> regular(u) --> regular(v) --> regular(u|>v)"
    apply (erule Scomp.induct, auto)
    done

    subsection{*Preservation lemma*}

    lemma union_preserve_comp: "u~v ==> v ~ (u un v)"
    by (erule Scomp.induct, simp_all)

    lemma preservation [rule_format]:
         "u ~ v ==> regular(v) --> u|>v = (u un v)|>v"
    apply (erule Scomp.induct, safe)
    apply (drule_tac [3] psi = "Fun (?u) |> ?v = ?w" in asm_rl)
    apply (auto simp add: union_preserve_comp comp_sym_iff)
    done

    declare sub_comp [THEN comp_sym, simp]

    subsection{*Prism theorem*}

    (* Having more assumptions than needed -- removed below  *)
    lemma prism_l [rule_format]:
         "v<==u ==>
           regular(u) --> (∀w. w~v --> w~u -->
                                w |> u = (w|>v) |> (u|>v))"
    by (erule Ssub.induct, force+)

    lemma prism: "[|v <== u; regular(u); w~v|] ==> w |> u = (w|>v) |> (u|>v)"
    apply (rule prism_l)
    apply (rule_tac [4] comp_trans, auto)
    done

    subsection{*Levy's Cube Lemma*}

    lemma cube: "[|u~v; regular(v); regular(u); w~u|]==>
               (w|>u) |> (v|>u) = (w|>v) |> (u|>v)"
    apply (subst preservation [of u], assumption, assumption)
    apply (subst preservation [of v], erule comp_sym, assumption)
    apply (subst prism [symmetric, of v])
    apply (simp add: union_r comp_sym_iff)
    apply (simp add: union_preserve_regular comp_sym_iff)
    apply (erule comp_trans, assumption)
    apply (simp add: prism [symmetric] union_l union_preserve_regular
                     comp_sym_iff union_sym)
    done

    subsection{*paving theorem*}

    lemma paving: "[|w~u; w~v; regular(u); regular(v)|]==>
               ∃uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &
                 regular(vu) & (w|>v)~uv & regular(uv) "
    apply (subgoal_tac "u~v")
    apply (safe intro!: exI)
    apply (rule cube)
    apply (simp_all add: comp_sym_iff)
    apply (blast intro: residuals_preserve_comp comp_trans comp_sym)+
    done

    end

### Setting up rule lists

lemmas

      [| residuals(Var(n), Var(n), v); [| n ∈ nat; v = Var(n) |] ==> Q |] ==> Q

      [| residuals(Fun(t), Fun(u), v);
         !!w. [| residuals(t, u, w); v = Fun(w) |] ==> Q |]
      ==> Q

      [| residuals(App(b, u1.0, u2.0), App(0, v1.0, v2.0), v);
         !!w1 w2.
            [| residuals(u1.0, v1.0, w1); residuals(u2.0, v2.0, w2); b ∈ bool;
               v = App(b, w1, w2) |]
            ==> Q |]
      ==> Q

      [| residuals(App(b, u1.0, u2.0), App(1, Fun(v1.0), v2.0), v);
         !!u1 w1 w2.
            [| residuals(u1, v1.0, w1); residuals(u2.0, v2.0, w2); b ∈ bool;
               v = w2 / w1; u1.0 = Fun(u1) |]
            ==> Q |]
      ==> Q

      [| residuals(Var(n), u, v); [| n ∈ nat; u = Var(n); v = Var(n) |] ==> Q |] ==> Q

      [| residuals(Fun(t), u, v);
         !!v w. [| residuals(t, v, w); u = Fun(v); v = Fun(w) |] ==> Q |]
      ==> Q

      [| residuals(App(b, u1.0, u2.0), w, v);
         !!v1 v2 w1 w2.
            [| residuals(u1.0, v1, w1); residuals(u2.0, v2, w2); b ∈ bool;
               w = App(0, v1, v2); v = App(b, w1, w2) |]
            ==> Q;
         !!u1 v1 v2 w1 w2.
            [| residuals(u1, v1, w1); residuals(u2.0, v2, w2); b ∈ bool;
               w = App(1, Fun(v1), v2); v = w2 / w1; u1.0 = Fun(u1) |]
            ==> Q |]
      ==> Q

      [| residuals(u, Var(n), v); [| n ∈ nat; u = Var(n); v = Var(n) |] ==> Q |] ==> Q

      [| residuals(u, Fun(t), v);
         !!u w. [| residuals(u, t, w); u = Fun(u); v = Fun(w) |] ==> Q |]
      ==> Q

      [| residuals(w, App(b, u1.0, u2.0), v);
         !!b u1 u2 w1 w2.
            [| residuals(u1, u1.0, w1); residuals(u2, u2.0, w2); b ∈ bool;
               w = App(b, u1, u2); v = App(b, w1, w2); b = 0 |]
            ==> Q;
         !!b u1 u2 v1 w1 w2.
            [| residuals(u1, v1, w1); residuals(u2, u2.0, w2); b ∈ bool;
               w = App(b, Fun(u1), u2); v = w2 / w1; b = 1; u1.0 = Fun(v1) |]
            ==> Q |]
      ==> Q

lemmas

      [| Var(n) <== u; [| n ∈ nat; u = Var(n) |] ==> Q |] ==> Q

      [| Fun(n) <== u; !!v. [| n <== v; u = Fun(v) |] ==> Q |] ==> Q

      [| u <== Fun(n); !!u. [| u <== n; u = Fun(u) |] ==> Q |] ==> Q

      [| App(1, Fun(t), a) <== u;
         !!v1 v2. [| Fun(t) <== v1; a <== v2; u = App(1, v1, v2) |] ==> Q |]
      ==> Q

      [| App(0, t, a) <== u;
         !!b v1 v2. [| t <== v1; a <== v2; b ∈ bool; u = App(b, v1, v2) |] ==> Q |]
      ==> Q

lemmas

      [| Fun(t) ∈ redexes; t ∈ redexes ==> Q |] ==> Q

### residuals is a partial function

lemma residuals_function:

      [| residuals(u, v, w); residuals(u, v, w1.0) |] ==> w1.0 = w

lemma residuals_intro:

      [| u ~ v; regular(v) |] ==> ∃w. residuals(u, v, w)

lemma comp_resfuncD:

      [| u ~ v; regular(v) |] ==> residuals(u, v, THE w. residuals(u, v, w))

### Residual function

lemma res_Var:

      n ∈ nat ==> Var(n) |> Var(n) = Var(n)

lemma res_Fun:

      [| s ~ t; regular(t) |] ==> Fun(s) |> Fun(t) = Fun(s |> t)

lemma res_App:

      [| s ~ u; regular(u); t ~ v; regular(v); b ∈ bool |]
      ==> App(b, s, t) |> App(0, u, v) = App(b, s |> u, t |> v)

lemma res_redex:

      [| s ~ u; regular(u); t ~ v; regular(v); b ∈ bool |]
      ==> App(b, Fun(s), t) |> App(1, Fun(u), v) = t |> v / (s |> u)

lemma resfunc_type:

      [| s ~ t; regular(t) |] ==> regular(t) --> s |> t ∈ redexes

### Commutation theorem

lemma sub_comp:

      u <== v ==> u ~ v

lemma sub_preserve_reg:

      [| u <== v; regular(v) |] ==> regular(u)

lemma residuals_lift_rec:

      [| u ~ v; k ∈ nat |]
      ==> regular(v) -->
          (∀n∈nat. lift_rec(u, n) |> lift_rec(v, n) = lift_rec(u |> v, n))

lemma residuals_subst_rec:

      u1.0 ~ u2.0
      ==> ∀v1 v2.
             v1 ~ v2 -->
             regular(v2) -->
             regular(u2.0) -->
             (∀n∈nat.
                 subst_rec(v1, u1.0, n) |> subst_rec(v2, u2.0, n) =
                 subst_rec(v1 |> v2, u1.0 |> u2.0, n))

lemma commutation:

      [| u1.0 ~ u2.0; v1.0 ~ v2.0; regular(u2.0); regular(v2.0) |]
      ==> v1.0 / u1.0 |> (v2.0 / u2.0) = v1.0 |> v2.0 / (u1.0 |> u2.0)

### Residuals are comp and regular

lemma residuals_preserve_comp:

      [| u ~ v; u ~ w; v ~ w; regular(w) |] ==> u |> w ~ (v |> w)

lemma residuals_preserve_reg:

      [| u ~ v; regular(u); regular(v) |] ==> regular(u |> v)

### Preservation lemma

lemma union_preserve_comp:

      u ~ v ==> v ~ (u un v)

lemma preservation:

      [| u ~ v; regular(v) |] ==> u |> v = u un v |> v

### Prism theorem

lemma prism_l:

      [| v <== u; regular(u); w ~ v; w ~ u |] ==> w |> u = w |> v |> (u |> v)

lemma prism:

      [| v <== u; regular(u); w ~ v |] ==> w |> u = w |> v |> (u |> v)

### Levy's Cube Lemma

lemma cube:

      [| u ~ v; regular(v); regular(u); w ~ u |]
      ==> w |> u |> (v |> u) = w |> v |> (u |> v)

### paving theorem

lemma paving:

      [| w ~ u; w ~ v; regular(u); regular(v) |]
      ==> ∃uv vu.
             w |> u |> vu = w |> v |> uv ∧
             w |> u ~ vu ∧ regular(vu) ∧ w |> v ~ uv ∧ regular(uv)