src/ZF/IMP/Com.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 1534 e8de1db81559
     1.1 --- a/src/ZF/IMP/Com.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/IMP/Com.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	ZF/IMP/Com.thy
     1.5 +(*  Title:      ZF/IMP/Com.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     1.8 +    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     1.9      Copyright   1994 TUM
    1.10  
    1.11  Arithmetic expressions, Boolean expressions, Commands
    1.12 @@ -23,14 +23,14 @@
    1.13  
    1.14  (** Evaluation of arithmetic expressions **)
    1.15  consts  evala    :: i
    1.16 -       "@evala"  :: [i,i,i] => o		("<_,_>/ -a-> _"  [0,0,50] 50)
    1.17 +       "@evala"  :: [i,i,i] => o                ("<_,_>/ -a-> _"  [0,0,50] 50)
    1.18  translations
    1.19      "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
    1.20  inductive
    1.21    domains "evala" <= "aexp * (loc -> nat) * nat"
    1.22    intrs 
    1.23      N   "[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
    1.24 -    X  	"[| x:loc;  sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
    1.25 +    X   "[| x:loc;  sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
    1.26      Op1 "[| <e,sigma> -a-> n;  f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
    1.27      Op2 "[| <e0,sigma> -a-> n0;  <e1,sigma>  -a-> n1; f: (nat*nat) -> nat |] 
    1.28             ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
    1.29 @@ -46,13 +46,13 @@
    1.30           | false
    1.31           | ROp  ("f: (nat*nat)->bool", "a0 : aexp", "a1 : aexp")
    1.32           | noti ("b : bexp")
    1.33 -         | andi ("b0 : bexp", "b1 : bexp")	(infixl 60)
    1.34 -         | ori  ("b0 : bexp", "b1 : bexp")	(infixl 60)
    1.35 +         | andi ("b0 : bexp", "b1 : bexp")      (infixl 60)
    1.36 +         | ori  ("b0 : bexp", "b1 : bexp")      (infixl 60)
    1.37  
    1.38  
    1.39  (** Evaluation of boolean expressions **)
    1.40 -consts evalb	:: i	
    1.41 -       "@evalb" :: [i,i,i] => o		("<_,_>/ -b-> _" [0,0,50] 50)
    1.42 +consts evalb    :: i    
    1.43 +       "@evalb" :: [i,i,i] => o         ("<_,_>/ -b-> _" [0,0,50] 50)
    1.44  
    1.45  translations
    1.46      "<be,sig> -b-> b" == "<be,sig,b> : evalb"
    1.47 @@ -63,15 +63,15 @@
    1.48      tru   "[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1"
    1.49      fls   "[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0"
    1.50      ROp   "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] 
    1.51 -	   ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
    1.52 +           ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
    1.53      noti  "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
    1.54      andi  "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 
    1.55            ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
    1.56      ori   "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 
    1.57 -	    ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
    1.58 +            ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
    1.59  
    1.60    type_intrs "bexp.intrs @   
    1.61 -	      [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
    1.62 +              [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
    1.63    type_elims "[make_elim(evala.dom_subset RS subsetD)]"
    1.64  
    1.65  
    1.66 @@ -80,24 +80,24 @@
    1.67  
    1.68  datatype <= "univ(loc Un aexp Un bexp)"
    1.69    "com" = skip
    1.70 -        | ":="  ("x:loc", "a:aexp")		(infixl 60)
    1.71 -        | semic ("c0:com", "c1:com")		("_; _"  [60, 60] 10)
    1.72 -	| while ("b:bexp", "c:com")		("while _ do _"  60)
    1.73 -	| ifc   ("b:bexp", "c0:com", "c1:com")	("ifc _ then _ else _"  60)
    1.74 +        | ":="  ("x:loc", "a:aexp")             (infixl 60)
    1.75 +        | semic ("c0:com", "c1:com")            ("_; _"  [60, 60] 10)
    1.76 +        | while ("b:bexp", "c:com")             ("while _ do _"  60)
    1.77 +        | ifc   ("b:bexp", "c0:com", "c1:com")  ("ifc _ then _ else _"  60)
    1.78  
    1.79  (*Constructor ";" has low precedence to avoid syntactic ambiguities
    1.80    with [| m: nat; x: loc; ... |] ==> ...  It usually will need parentheses.*)
    1.81  
    1.82  (** Execution of commands **)
    1.83  consts  evalc    :: i
    1.84 -        "@evalc" :: [i,i,i] => o   		("<_,_>/ -c-> _" [0,0,50] 50)
    1.85 -	"assign" :: [i,i,i] => i   		("_[_'/_]"       [95,0,0] 95)
    1.86 +        "@evalc" :: [i,i,i] => o                ("<_,_>/ -c-> _" [0,0,50] 50)
    1.87 +        "assign" :: [i,i,i] => i                ("_[_'/_]"       [95,0,0] 95)
    1.88  
    1.89  translations
    1.90         "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
    1.91  
    1.92  defs 
    1.93 -	assign_def	"sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
    1.94 +        assign_def      "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
    1.95  
    1.96  inductive
    1.97    domains "evalc" <= "com * (loc -> nat) * (loc -> nat)"
    1.98 @@ -111,11 +111,11 @@
    1.99              <c0 ; c1, sigma> -c-> sigma1"
   1.100  
   1.101      ifc1     "[| b:bexp; c1:com; sigma:loc->nat;   
   1.102 -		 <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> 
   1.103 +                 <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> 
   1.104               <ifc b then c0 else c1, sigma> -c-> sigma1"
   1.105  
   1.106      ifc0     "[| b:bexp; c0:com; sigma:loc->nat;   
   1.107 -		 <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> 
   1.108 +                 <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> 
   1.109               <ifc b then c0 else c1, sigma> -c-> sigma1"
   1.110  
   1.111      while0   "[| c: com; <b, sigma> -b-> 0 |] ==> 
   1.112 @@ -128,6 +128,6 @@
   1.113    con_defs   "[assign_def]"
   1.114    type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]"
   1.115    type_elims "[make_elim(evala.dom_subset RS subsetD),   
   1.116 -	      make_elim(evalb.dom_subset RS subsetD) ]"
   1.117 +              make_elim(evalb.dom_subset RS subsetD) ]"
   1.118  
   1.119  end