src/ZF/Resid/Residuals.thy
author wenzelm
Thu Apr 26 14:24:08 2007 +0200 (2007-04-26)
changeset 22808 a7daa74e2980
parent 16417 9bc16273c2d4
child 24893 b8ef7afe3a6b
permissions -rw-r--r--
eliminated unnamed infixes, tuned syntax;
     1 (*  Title:      Residuals.thy
     2     ID:         $Id$
     3     Author:     Ole Rasmussen
     4     Copyright   1995  University of Cambridge
     5     Logic Image: ZF
     6 
     7 *)
     8 
     9 theory Residuals imports Substitution begin
    10 
    11 consts
    12   Sres          :: "i"
    13   res_func      :: "[i,i]=>i"     (infixl "|>" 70)
    14 
    15 abbreviation
    16   "residuals(u,v,w) == <u,v,w> \<in> Sres"
    17 
    18 inductive
    19   domains       "Sres" <= "redexes*redexes*redexes"
    20   intros
    21     Res_Var:    "n \<in> nat ==> residuals(Var(n),Var(n),Var(n))"
    22     Res_Fun:    "[|residuals(u,v,w)|]==>   
    23                      residuals(Fun(u),Fun(v),Fun(w))"
    24     Res_App:    "[|residuals(u1,v1,w1);   
    25                    residuals(u2,v2,w2); b \<in> bool|]==>   
    26                  residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
    27     Res_redex:  "[|residuals(u1,v1,w1);   
    28                    residuals(u2,v2,w2); b \<in> bool|]==>   
    29                  residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
    30   type_intros    subst_type nat_typechecks redexes.intros bool_typechecks
    31 
    32 defs
    33   res_func_def:  "u |> v == THE w. residuals(u,v,w)"
    34 
    35 
    36 subsection{*Setting up rule lists*}
    37 
    38 declare Sres.intros [intro]
    39 declare Sreg.intros [intro]
    40 declare subst_type [intro]
    41 
    42 inductive_cases [elim!]:
    43   "residuals(Var(n),Var(n),v)"
    44   "residuals(Fun(t),Fun(u),v)"
    45   "residuals(App(b, u1, u2), App(0, v1, v2),v)"
    46   "residuals(App(b, u1, u2), App(1, Fun(v1), v2),v)"
    47   "residuals(Var(n),u,v)"
    48   "residuals(Fun(t),u,v)"
    49   "residuals(App(b, u1, u2), w,v)"
    50   "residuals(u,Var(n),v)"
    51   "residuals(u,Fun(t),v)"
    52   "residuals(w,App(b, u1, u2),v)"
    53 
    54 
    55 inductive_cases [elim!]:
    56   "Var(n) <== u"
    57   "Fun(n) <== u"
    58   "u <== Fun(n)"
    59   "App(1,Fun(t),a) <== u"
    60   "App(0,t,a) <== u"
    61 
    62 inductive_cases [elim!]:
    63   "Fun(t) \<in> redexes"
    64 
    65 declare Sres.intros [simp]
    66 
    67 subsection{*residuals is a  partial function*}
    68 
    69 lemma residuals_function [rule_format]:
    70      "residuals(u,v,w) ==> \<forall>w1. residuals(u,v,w1) --> w1 = w"
    71 by (erule Sres.induct, force+)
    72 
    73 lemma residuals_intro [rule_format]:
    74      "u~v ==> regular(v) --> (\<exists>w. residuals(u,v,w))"
    75 by (erule Scomp.induct, force+)
    76 
    77 lemma comp_resfuncD:
    78      "[| u~v;  regular(v) |] ==> residuals(u, v, THE w. residuals(u, v, w))"
    79 apply (frule residuals_intro, assumption, clarify)
    80 apply (subst the_equality)
    81 apply (blast intro: residuals_function)+
    82 done
    83 
    84 subsection{*Residual function*}
    85 
    86 lemma res_Var [simp]: "n \<in> nat ==> Var(n) |> Var(n) = Var(n)"
    87 by (unfold res_func_def, blast)
    88 
    89 lemma res_Fun [simp]: 
    90     "[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)"
    91 apply (unfold res_func_def)
    92 apply (blast intro: comp_resfuncD residuals_function) 
    93 done
    94 
    95 lemma res_App [simp]: 
    96     "[|s~u; regular(u); t~v; regular(v); b \<in> bool|]
    97      ==> App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)"
    98 apply (unfold res_func_def) 
    99 apply (blast dest!: comp_resfuncD intro: residuals_function)
   100 done
   101 
   102 lemma res_redex [simp]: 
   103     "[|s~u; regular(u); t~v; regular(v); b \<in> bool|]
   104      ==> App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)"
   105 apply (unfold res_func_def)
   106 apply (blast elim!: redexes.free_elims dest!: comp_resfuncD 
   107              intro: residuals_function)
   108 done
   109 
   110 lemma resfunc_type [simp]:
   111      "[|s~t; regular(t)|]==> regular(t) --> s |> t \<in> redexes"
   112   by (erule Scomp.induct, auto)
   113 
   114 subsection{*Commutation theorem*}
   115 
   116 lemma sub_comp [simp]: "u<==v ==> u~v"
   117 by (erule Ssub.induct, simp_all)
   118 
   119 lemma sub_preserve_reg [rule_format, simp]:
   120      "u<==v  ==> regular(v) --> regular(u)"
   121 by (erule Ssub.induct, auto)
   122 
   123 lemma residuals_lift_rec: "[|u~v; k \<in> nat|]==> regular(v)--> (\<forall>n \<in> nat.   
   124          lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))"
   125 apply (erule Scomp.induct, safe)
   126 apply (simp_all add: lift_rec_Var subst_Var lift_subst)
   127 done
   128 
   129 lemma residuals_subst_rec:
   130      "u1~u2 ==>  \<forall>v1 v2. v1~v2 --> regular(v2) --> regular(u2) --> 
   131                   (\<forall>n \<in> nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) =  
   132                     subst_rec(v1 |> v2, u1 |> u2,n))"
   133 apply (erule Scomp.induct, safe)
   134 apply (simp_all add: lift_rec_Var subst_Var residuals_lift_rec)
   135 apply (drule_tac psi = "\<forall>x.?P (x) " in asm_rl)
   136 apply (simp add: substitution)
   137 done
   138 
   139 
   140 lemma commutation [simp]:
   141      "[|u1~u2; v1~v2; regular(u2); regular(v2)|]
   142       ==> (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)"
   143 by (simp add: residuals_subst_rec)
   144 
   145 
   146 subsection{*Residuals are comp and regular*}
   147 
   148 lemma residuals_preserve_comp [rule_format, simp]:
   149      "u~v ==> \<forall>w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)"
   150 by (erule Scomp.induct, force+)
   151 
   152 lemma residuals_preserve_reg [rule_format, simp]:
   153      "u~v ==> regular(u) --> regular(v) --> regular(u|>v)"
   154 apply (erule Scomp.induct, auto)
   155 done
   156 
   157 subsection{*Preservation lemma*}
   158 
   159 lemma union_preserve_comp: "u~v ==> v ~ (u un v)"
   160 by (erule Scomp.induct, simp_all)
   161 
   162 lemma preservation [rule_format]:
   163      "u ~ v ==> regular(v) --> u|>v = (u un v)|>v"
   164 apply (erule Scomp.induct, safe)
   165 apply (drule_tac [3] psi = "Fun (?u) |> ?v = ?w" in asm_rl)
   166 apply (auto simp add: union_preserve_comp comp_sym_iff)
   167 done
   168 
   169 
   170 declare sub_comp [THEN comp_sym, simp]
   171 
   172 subsection{*Prism theorem*}
   173 
   174 (* Having more assumptions than needed -- removed below  *)
   175 lemma prism_l [rule_format]:
   176      "v<==u ==>  
   177        regular(u) --> (\<forall>w. w~v --> w~u -->   
   178                             w |> u = (w|>v) |> (u|>v))"
   179 by (erule Ssub.induct, force+)
   180 
   181 lemma prism: "[|v <== u; regular(u); w~v|] ==> w |> u = (w|>v) |> (u|>v)"
   182 apply (rule prism_l)
   183 apply (rule_tac [4] comp_trans, auto)
   184 done
   185 
   186 
   187 subsection{*Levy's Cube Lemma*}
   188 
   189 lemma cube: "[|u~v; regular(v); regular(u); w~u|]==>   
   190            (w|>u) |> (v|>u) = (w|>v) |> (u|>v)"
   191 apply (subst preservation [of u], assumption, assumption)
   192 apply (subst preservation [of v], erule comp_sym, assumption)
   193 apply (subst prism [symmetric, of v])
   194 apply (simp add: union_r comp_sym_iff)
   195 apply (simp add: union_preserve_regular comp_sym_iff)
   196 apply (erule comp_trans, assumption)
   197 apply (simp add: prism [symmetric] union_l union_preserve_regular 
   198                  comp_sym_iff union_sym)
   199 done
   200 
   201 
   202 subsection{*paving theorem*}
   203 
   204 lemma paving: "[|w~u; w~v; regular(u); regular(v)|]==>  
   205            \<exists>uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu & 
   206              regular(vu) & (w|>v)~uv & regular(uv) "
   207 apply (subgoal_tac "u~v")
   208 apply (safe intro!: exI)
   209 apply (rule cube)
   210 apply (simp_all add: comp_sym_iff)
   211 apply (blast intro: residuals_preserve_comp comp_trans comp_sym)+
   212 done
   213 
   214 
   215 end
   216