wneuper/isa: src/ZF/Resid/Reduction.thy@9bc16273c2d4

     1 (*  Title:      Reduction.thy

     2     ID:         $Id$

     3     Author:     Ole Rasmussen

     4     Copyright   1995  University of Cambridge

     5     Logic Image: ZF

     6 *)

     8 theory Reduction imports Residuals begin

    10 (**** Lambda-terms ****)

    12 consts

    13   lambda        :: "i"

    14   unmark        :: "i=>i"

    15   Apl           :: "[i,i]=>i"

    17 translations

    18   "Apl(n,m)" == "App(0,n,m)"

    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

    28 declare lambda.intros [intro]

    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))"

    36 declare lambda.intros [simp]

    37 declare lambda.dom_subset [THEN subsetD, simp, intro]

    40 (* ------------------------------------------------------------------------- *)

    41 (*        unmark lemmas                                                      *)

    42 (* ------------------------------------------------------------------------- *)

    44 lemma unmark_type [intro, simp]:

    45      "u \<in> redexes ==> unmark(u) \<in> lambda"

    46 by (erule redexes.induct, simp_all)

    48 lemma lambda_unmark: "u \<in> lambda ==> unmark(u) = u"

    49 by (erule lambda.induct, simp_all)

    52 (* ------------------------------------------------------------------------- *)

    53 (*         lift and subst preserve lambda                                    *)

    54 (* ------------------------------------------------------------------------- *)

    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)

    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)

    65 (* ------------------------------------------------------------------------- *)

    66 (*        type-rule for reduction definitions                               *)

    67 (* ------------------------------------------------------------------------- *)

    69 lemmas red_typechecks = substL_type nat_typechecks lambda.intros

    70                         bool_typechecks

    72 consts

    73   Sred1     :: "i"

    74   Sred      :: "i"

    75   Spar_red1 :: "i"

    76   Spar_red  :: "i"

    77   "-1->"    :: "[i,i]=>o"  (infixl 50)

    78   "--->"    :: "[i,i]=>o"  (infixl 50)

    79   "=1=>"    :: "[i,i]=>o"  (infixl 50)

    80   "===>"    :: "[i,i]=>o"  (infixl 50)

    82 translations

    83   "a -1-> b" == "<a,b> \<in> Sred1"

    84   "a ---> b" == "<a,b> \<in> Sred"

    85   "a =1=> b" == "<a,b> \<in> Spar_red1"

    86   "a ===> b" == "<a,b> \<in> Spar_red"

    89 inductive

    90   domains       "Sred1" <= "lambda*lambda"

    91   intros

    92     beta:       "[|m \<in> lambda; n \<in> lambda|] ==> Apl(Fun(m),n) -1-> n/m"

    93     rfun:       "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"

    94     apl_l:      "[|m2 \<in> lambda; m1 -1-> n1|] ==> Apl(m1,m2) -1-> Apl(n1,m2)"

    95     apl_r:      "[|m1 \<in> lambda; m2 -1-> n2|] ==> Apl(m1,m2) -1-> Apl(m1,n2)"

    96   type_intros    red_typechecks

    98 declare Sred1.intros [intro, simp]

   100 inductive

   101   domains       "Sred" <= "lambda*lambda"

   102   intros

   103     one_step:   "m-1->n ==> m--->n"

   104     refl:       "m \<in> lambda==>m --->m"

   105     trans:      "[|m--->n; n--->p|] ==>m--->p"

   106   type_intros    Sred1.dom_subset [THEN subsetD] red_typechecks

   108 declare Sred.one_step [intro, simp]

   109 declare Sred.refl     [intro, simp]

   111 inductive

   112   domains       "Spar_red1" <= "lambda*lambda"

   113   intros

   114     beta:       "[|m =1=> m'; n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"

   115     rvar:       "n \<in> nat ==> Var(n) =1=> Var(n)"

   116     rfun:       "m =1=> m' ==> Fun(m) =1=> Fun(m')"

   117     rapl:       "[|m =1=> m'; n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"

   118   type_intros    red_typechecks

   120 declare Spar_red1.intros [intro, simp]

   122 inductive

   123   domains "Spar_red" <= "lambda*lambda"

   124   intros

   125     one_step:   "m =1=> n ==> m ===> n"

   126     trans:      "[|m===>n; n===>p|] ==> m===>p"

   127   type_intros    Spar_red1.dom_subset [THEN subsetD] red_typechecks

   129 declare Spar_red.one_step [intro, simp]

   133 (* ------------------------------------------------------------------------- *)

   134 (*     Setting up rule lists for reduction                                   *)

   135 (* ------------------------------------------------------------------------- *)

   137 lemmas red1D1 [simp] = Sred1.dom_subset [THEN subsetD, THEN SigmaD1]

   138 lemmas red1D2 [simp] = Sred1.dom_subset [THEN subsetD, THEN SigmaD2]

   139 lemmas redD1 [simp] = Sred.dom_subset [THEN subsetD, THEN SigmaD1]

   140 lemmas redD2 [simp] = Sred.dom_subset [THEN subsetD, THEN SigmaD2]

   142 lemmas par_red1D1 [simp] = Spar_red1.dom_subset [THEN subsetD, THEN SigmaD1]

   143 lemmas par_red1D2 [simp] = Spar_red1.dom_subset [THEN subsetD, THEN SigmaD2]

   144 lemmas par_redD1 [simp] = Spar_red.dom_subset [THEN subsetD, THEN SigmaD1]

   145 lemmas par_redD2 [simp] = Spar_red.dom_subset [THEN subsetD, THEN SigmaD2]

   147 declare bool_typechecks [intro]

   149 inductive_cases  [elim!]: "Fun(t) =1=> Fun(u)"

   153 (* ------------------------------------------------------------------------- *)

   154 (*     Lemmas for reduction                                                  *)

   155 (* ------------------------------------------------------------------------- *)

   157 lemma red_Fun: "m--->n ==> Fun(m) ---> Fun(n)"

   158 apply (erule Sred.induct)

   159 apply (rule_tac [3] Sred.trans, simp_all)

   160 done

   162 lemma red_Apll: "[|n \<in> lambda; m ---> m'|] ==> Apl(m,n)--->Apl(m',n)"

   163 apply (erule Sred.induct)

   164 apply (rule_tac [3] Sred.trans, simp_all)

   165 done

   167 lemma red_Aplr: "[|n \<in> lambda; m ---> m'|] ==> Apl(n,m)--->Apl(n,m')"

   168 apply (erule Sred.induct)

   169 apply (rule_tac [3] Sred.trans, simp_all)

   170 done

   172 lemma red_Apl: "[|m ---> m'; n--->n'|] ==> Apl(m,n)--->Apl(m',n')"

   173 apply (rule_tac n = "Apl (m',n) " in Sred.trans)

   174 apply (simp_all add: red_Apll red_Aplr)

   175 done

   177 lemma red_beta: "[|m \<in> lambda; m':lambda; n \<in> lambda; n':lambda; m ---> m'; n--->n'|] ==>

   178                Apl(Fun(m),n)---> n'/m'"

   179 apply (rule_tac n = "Apl (Fun (m'),n') " in Sred.trans)

   180 apply (simp_all add: red_Apl red_Fun)

   181 done

   184 (* ------------------------------------------------------------------------- *)

   185 (*      Lemmas for parallel reduction                                        *)

   186 (* ------------------------------------------------------------------------- *)

   189 lemma refl_par_red1: "m \<in> lambda==> m =1=> m"

   190 by (erule lambda.induct, simp_all)

   192 lemma red1_par_red1: "m-1->n ==> m=1=>n"

   193 by (erule Sred1.induct, simp_all add: refl_par_red1)

   195 lemma red_par_red: "m--->n ==> m===>n"

   196 apply (erule Sred.induct)

   197 apply (rule_tac [3] Spar_red.trans)

   198 apply (simp_all add: refl_par_red1 red1_par_red1)

   199 done

   201 lemma par_red_red: "m===>n ==> m--->n"

   202 apply (erule Spar_red.induct)

   203 apply (erule Spar_red1.induct)

   204 apply (rule_tac [5] Sred.trans)

   205 apply (simp_all add: red_Fun red_beta red_Apl)

   206 done

   209 (* ------------------------------------------------------------------------- *)

   210 (*      Simulation                                                           *)

   211 (* ------------------------------------------------------------------------- *)

   213 lemma simulation: "m=1=>n ==> \<exists>v. m|>v = n & m~v & regular(v)"

   214 by (erule Spar_red1.induct, force+)

   217 (* ------------------------------------------------------------------------- *)

   218 (*           commuting of unmark and subst                                   *)

   219 (* ------------------------------------------------------------------------- *)

   221 lemma unmmark_lift_rec:

   222      "u \<in> redexes ==> \<forall>k \<in> nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)"

   223 by (erule redexes.induct, simp_all add: lift_rec_Var)

   225 lemma unmmark_subst_rec:

   226  "v \<in> redexes ==> \<forall>k \<in> nat. \<forall>u \<in> redexes.

   227                   unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)"

   228 by (erule redexes.induct, simp_all add: unmmark_lift_rec subst_Var)

   231 (* ------------------------------------------------------------------------- *)

   232 (*        Completeness                                                       *)

   233 (* ------------------------------------------------------------------------- *)

   235 lemma completeness_l [rule_format]:

   236      "u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)"

   237 apply (erule Scomp.induct)

   238 apply (auto simp add: unmmark_subst_rec)

   239 done

   241 lemma completeness: "[|u \<in> lambda; u~v; regular(v)|] ==> u =1=> unmark(u|>v)"

   242 by (drule completeness_l, simp_all add: lambda_unmark)

   244 end

author	haftmann
	Fri, 17 Jun 2005 16:12:49 +0200
changeset 16417	9bc16273c2d4
parent 13612	55d32e76ef4e
child 22808	a7daa74e2980
permissions	-rw-r--r--