src/ZF/Resid/Reduction.thy
author wenzelm
Thu Apr 26 14:24:08 2007 +0200 (2007-04-26)
changeset 22808 a7daa74e2980
parent 16417 9bc16273c2d4
child 24892 c663e675e177
permissions -rw-r--r--
eliminated unnamed infixes, tuned syntax;
     1 (*  Title:      Reduction.thy
     2     ID:         $Id$
     3     Author:     Ole Rasmussen
     4     Copyright   1995  University of Cambridge
     5     Logic Image: ZF
     6 *)
     7 
     8 theory Reduction imports Residuals begin
     9 
    10 (**** Lambda-terms ****)
    11 
    12 consts
    13   lambda        :: "i"
    14   unmark        :: "i=>i"
    15   Apl           :: "[i,i]=>i"
    16 
    17 translations
    18   "Apl(n,m)" == "App(0,n,m)"
    19   
    20 inductive
    21   domains       "lambda" <= redexes
    22   intros
    23     Lambda_Var:  "               n \<in> nat ==>     Var(n) \<in> lambda"
    24     Lambda_Fun:  "            u \<in> lambda ==>     Fun(u) \<in> lambda"
    25     Lambda_App:  "[|u \<in> lambda; v \<in> lambda|] ==> Apl(u,v) \<in> lambda"
    26   type_intros    redexes.intros bool_typechecks
    27 
    28 declare lambda.intros [intro]
    29 
    30 primrec
    31   "unmark(Var(n)) = Var(n)"
    32   "unmark(Fun(u)) = Fun(unmark(u))"
    33   "unmark(App(b,f,a)) = Apl(unmark(f), unmark(a))"
    34 
    35 
    36 declare lambda.intros [simp] 
    37 declare lambda.dom_subset [THEN subsetD, simp, intro]
    38 
    39 
    40 (* ------------------------------------------------------------------------- *)
    41 (*        unmark lemmas                                                      *)
    42 (* ------------------------------------------------------------------------- *)
    43 
    44 lemma unmark_type [intro, simp]:
    45      "u \<in> redexes ==> unmark(u) \<in> lambda"
    46 by (erule redexes.induct, simp_all)
    47 
    48 lemma lambda_unmark: "u \<in> lambda ==> unmark(u) = u"
    49 by (erule lambda.induct, simp_all)
    50 
    51 
    52 (* ------------------------------------------------------------------------- *)
    53 (*         lift and subst preserve lambda                                    *)
    54 (* ------------------------------------------------------------------------- *)
    55 
    56 lemma liftL_type [rule_format]:
    57      "v \<in> lambda ==> \<forall>k \<in> nat. lift_rec(v,k) \<in> lambda"
    58 by (erule lambda.induct, simp_all add: lift_rec_Var)
    59 
    60 lemma substL_type [rule_format, simp]:
    61      "v \<in> lambda ==>  \<forall>n \<in> nat. \<forall>u \<in> lambda. subst_rec(u,v,n) \<in> lambda"
    62 by (erule lambda.induct, simp_all add: liftL_type subst_Var)
    63 
    64 
    65 (* ------------------------------------------------------------------------- *)
    66 (*        type-rule for reduction definitions                               *)
    67 (* ------------------------------------------------------------------------- *)
    68 
    69 lemmas red_typechecks = substL_type nat_typechecks lambda.intros 
    70                         bool_typechecks
    71 
    72 consts
    73   Sred1     :: "i"
    74   Sred      :: "i"
    75   Spar_red1 :: "i"
    76   Spar_red  :: "i"
    77 
    78 abbreviation
    79   Sred1_rel (infixl "-1->" 50) where
    80   "a -1-> b == <a,b> \<in> Sred1"
    81 
    82 abbreviation
    83   Sred_rel (infixl "--->" 50) where
    84   "a ---> b == <a,b> \<in> Sred"
    85 
    86 abbreviation
    87   Spar_red1_rel (infixl "=1=>" 50) where
    88   "a =1=> b == <a,b> \<in> Spar_red1"
    89 
    90 abbreviation
    91   Spar_red_rel (infixl "===>" 50) where
    92   "a ===> b == <a,b> \<in> Spar_red"
    93   
    94   
    95 inductive
    96   domains       "Sred1" <= "lambda*lambda"
    97   intros
    98     beta:       "[|m \<in> lambda; n \<in> lambda|] ==> Apl(Fun(m),n) -1-> n/m"
    99     rfun:       "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
   100     apl_l:      "[|m2 \<in> lambda; m1 -1-> n1|] ==> Apl(m1,m2) -1-> Apl(n1,m2)"
   101     apl_r:      "[|m1 \<in> lambda; m2 -1-> n2|] ==> Apl(m1,m2) -1-> Apl(m1,n2)"
   102   type_intros    red_typechecks
   103 
   104 declare Sred1.intros [intro, simp]
   105 
   106 inductive
   107   domains       "Sred" <= "lambda*lambda"
   108   intros
   109     one_step:   "m-1->n ==> m--->n"
   110     refl:       "m \<in> lambda==>m --->m"
   111     trans:      "[|m--->n; n--->p|] ==>m--->p"
   112   type_intros    Sred1.dom_subset [THEN subsetD] red_typechecks
   113 
   114 declare Sred.one_step [intro, simp]
   115 declare Sred.refl     [intro, simp]
   116 
   117 inductive
   118   domains       "Spar_red1" <= "lambda*lambda"
   119   intros
   120     beta:       "[|m =1=> m'; n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
   121     rvar:       "n \<in> nat ==> Var(n) =1=> Var(n)"
   122     rfun:       "m =1=> m' ==> Fun(m) =1=> Fun(m')"
   123     rapl:       "[|m =1=> m'; n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
   124   type_intros    red_typechecks
   125 
   126 declare Spar_red1.intros [intro, simp]
   127 
   128 inductive
   129   domains "Spar_red" <= "lambda*lambda"
   130   intros
   131     one_step:   "m =1=> n ==> m ===> n"
   132     trans:      "[|m===>n; n===>p|] ==> m===>p"
   133   type_intros    Spar_red1.dom_subset [THEN subsetD] red_typechecks
   134 
   135 declare Spar_red.one_step [intro, simp]
   136 
   137 
   138 
   139 (* ------------------------------------------------------------------------- *)
   140 (*     Setting up rule lists for reduction                                   *)
   141 (* ------------------------------------------------------------------------- *)
   142 
   143 lemmas red1D1 [simp] = Sred1.dom_subset [THEN subsetD, THEN SigmaD1]
   144 lemmas red1D2 [simp] = Sred1.dom_subset [THEN subsetD, THEN SigmaD2]
   145 lemmas redD1 [simp] = Sred.dom_subset [THEN subsetD, THEN SigmaD1]
   146 lemmas redD2 [simp] = Sred.dom_subset [THEN subsetD, THEN SigmaD2]
   147 
   148 lemmas par_red1D1 [simp] = Spar_red1.dom_subset [THEN subsetD, THEN SigmaD1]
   149 lemmas par_red1D2 [simp] = Spar_red1.dom_subset [THEN subsetD, THEN SigmaD2]
   150 lemmas par_redD1 [simp] = Spar_red.dom_subset [THEN subsetD, THEN SigmaD1]
   151 lemmas par_redD2 [simp] = Spar_red.dom_subset [THEN subsetD, THEN SigmaD2]
   152 
   153 declare bool_typechecks [intro]
   154 
   155 inductive_cases  [elim!]: "Fun(t) =1=> Fun(u)"
   156 
   157 
   158 
   159 (* ------------------------------------------------------------------------- *)
   160 (*     Lemmas for reduction                                                  *)
   161 (* ------------------------------------------------------------------------- *)
   162 
   163 lemma red_Fun: "m--->n ==> Fun(m) ---> Fun(n)"
   164 apply (erule Sred.induct)
   165 apply (rule_tac [3] Sred.trans, simp_all)
   166 done
   167 
   168 lemma red_Apll: "[|n \<in> lambda; m ---> m'|] ==> Apl(m,n)--->Apl(m',n)"
   169 apply (erule Sred.induct)
   170 apply (rule_tac [3] Sred.trans, simp_all)
   171 done
   172 
   173 lemma red_Aplr: "[|n \<in> lambda; m ---> m'|] ==> Apl(n,m)--->Apl(n,m')"
   174 apply (erule Sred.induct)
   175 apply (rule_tac [3] Sred.trans, simp_all)
   176 done
   177 
   178 lemma red_Apl: "[|m ---> m'; n--->n'|] ==> Apl(m,n)--->Apl(m',n')"
   179 apply (rule_tac n = "Apl (m',n) " in Sred.trans)
   180 apply (simp_all add: red_Apll red_Aplr)
   181 done
   182 
   183 lemma red_beta: "[|m \<in> lambda; m':lambda; n \<in> lambda; n':lambda; m ---> m'; n--->n'|] ==>  
   184                Apl(Fun(m),n)---> n'/m'"
   185 apply (rule_tac n = "Apl (Fun (m'),n') " in Sred.trans)
   186 apply (simp_all add: red_Apl red_Fun)
   187 done
   188 
   189 
   190 (* ------------------------------------------------------------------------- *)
   191 (*      Lemmas for parallel reduction                                        *)
   192 (* ------------------------------------------------------------------------- *)
   193 
   194 
   195 lemma refl_par_red1: "m \<in> lambda==> m =1=> m"
   196 by (erule lambda.induct, simp_all)
   197 
   198 lemma red1_par_red1: "m-1->n ==> m=1=>n"
   199 by (erule Sred1.induct, simp_all add: refl_par_red1)
   200 
   201 lemma red_par_red: "m--->n ==> m===>n"
   202 apply (erule Sred.induct)
   203 apply (rule_tac [3] Spar_red.trans)
   204 apply (simp_all add: refl_par_red1 red1_par_red1)
   205 done
   206 
   207 lemma par_red_red: "m===>n ==> m--->n"
   208 apply (erule Spar_red.induct)
   209 apply (erule Spar_red1.induct)
   210 apply (rule_tac [5] Sred.trans)
   211 apply (simp_all add: red_Fun red_beta red_Apl)
   212 done
   213 
   214 
   215 (* ------------------------------------------------------------------------- *)
   216 (*      Simulation                                                           *)
   217 (* ------------------------------------------------------------------------- *)
   218 
   219 lemma simulation: "m=1=>n ==> \<exists>v. m|>v = n & m~v & regular(v)"
   220 by (erule Spar_red1.induct, force+)
   221 
   222 
   223 (* ------------------------------------------------------------------------- *)
   224 (*           commuting of unmark and subst                                   *)
   225 (* ------------------------------------------------------------------------- *)
   226 
   227 lemma unmmark_lift_rec:
   228      "u \<in> redexes ==> \<forall>k \<in> nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)"
   229 by (erule redexes.induct, simp_all add: lift_rec_Var)
   230 
   231 lemma unmmark_subst_rec:
   232  "v \<in> redexes ==> \<forall>k \<in> nat. \<forall>u \<in> redexes.   
   233                   unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)"
   234 by (erule redexes.induct, simp_all add: unmmark_lift_rec subst_Var)
   235 
   236 
   237 (* ------------------------------------------------------------------------- *)
   238 (*        Completeness                                                       *)
   239 (* ------------------------------------------------------------------------- *)
   240 
   241 lemma completeness_l [rule_format]:
   242      "u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)"
   243 apply (erule Scomp.induct)
   244 apply (auto simp add: unmmark_subst_rec)
   245 done
   246 
   247 lemma completeness: "[|u \<in> lambda; u~v; regular(v)|] ==> u =1=> unmark(u|>v)"
   248 by (drule completeness_l, simp_all add: lambda_unmark)
   249 
   250 end
   251