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