src/HOL/Induct/Com.thy
changeset 10759 994877ee68cb
parent 5184 9b8547a9496a
child 11464 ddea204de5bc
     1.1 --- a/src/HOL/Induct/Com.thy	Mon Jan 01 11:52:04 2001 +0100
     1.2 +++ b/src/HOL/Induct/Com.thy	Tue Jan 02 10:27:10 2001 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  Example of Mutual Induction via Iteratived Inductive Definitions: Commands
     1.5  *)
     1.6  
     1.7 -Com = Datatype +
     1.8 +Com = Main +
     1.9  
    1.10  types loc
    1.11        state = "loc => nat"
    1.12 @@ -14,23 +14,22 @@
    1.13  
    1.14  arities loc :: term
    1.15  
    1.16 -(*To avoid a mutually recursive datatype declaration, expressions and commands
    1.17 -  are combined to form a single datatype.*)
    1.18  datatype
    1.19    exp = N nat
    1.20        | X loc
    1.21        | Op n2n2n exp exp
    1.22 -      | valOf exp exp          ("VALOF _ RESULTIS _"  60)
    1.23 -      | SKIP
    1.24 +      | valOf com exp          ("VALOF _ RESULTIS _"  60)
    1.25 +and
    1.26 +  com = SKIP
    1.27        | ":="  loc exp          (infixl  60)
    1.28 -      | Semi  exp exp          ("_;;_"  [60, 60] 60)
    1.29 -      | Cond  exp exp exp      ("IF _ THEN _ ELSE _"  60)
    1.30 -      | While exp exp          ("WHILE _ DO _"  60)
    1.31 +      | Semi  com com          ("_;;_"  [60, 60] 60)
    1.32 +      | Cond  exp com com      ("IF _ THEN _ ELSE _"  60)
    1.33 +      | While exp com          ("WHILE _ DO _"  60)
    1.34  
    1.35  (** Execution of commands **)
    1.36 -consts  exec    :: "((exp*state) * (nat*state)) set => ((exp*state)*state)set"
    1.37 +consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
    1.38         "@exec"  :: "((exp*state) * (nat*state)) set => 
    1.39 -                    [exp*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
    1.40 +                    [com*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
    1.41  
    1.42  translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
    1.43  
    1.44 @@ -40,16 +39,12 @@
    1.45  translations
    1.46      "esig -|[eval]-> ns" => "(esig,ns) : eval"
    1.47  
    1.48 -constdefs assign :: [state,nat,loc] => state    ("_[_'/_]" [95,0,0] 95)
    1.49 -  "s[m/x] ==  (%y. if y=x then m else s y)"
    1.50 -
    1.51 -
    1.52  (*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*)
    1.53  inductive "exec eval"
    1.54    intrs
    1.55      Skip    "(SKIP,s) -[eval]-> s"
    1.56  
    1.57 -    Assign  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'[v/x]"
    1.58 +    Assign  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
    1.59  
    1.60      Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
    1.61              ==> (c0 ;; c1, s) -[eval]-> s1"
    1.62 @@ -65,11 +60,4 @@
    1.63      WhileTrue  "[| (e,s) -|[eval]-> (0,s1);
    1.64                  (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
    1.65                  ==> (WHILE e DO c, s) -[eval]-> s3"
    1.66 -
    1.67 -constdefs
    1.68 -    Unique   :: "['a, 'b, ('a*'b) set] => bool"
    1.69 -    "Unique x y r == ALL y'. (x,y'): r --> y = y'"
    1.70 -
    1.71 -    Function :: "('a*'b) set => bool"
    1.72 -    "Function r == ALL x y. (x,y): r --> Unique x y r"
    1.73  end