src/HOL/Induct/Com.thy
author berghofe
Fri Jul 24 13:19:38 1998 +0200 (1998-07-24)
changeset 5184 9b8547a9496a
parent 5102 8c782c25a11e
child 10759 994877ee68cb
permissions -rw-r--r--
Adapted to new datatype package.
paulson@3120
     1
(*  Title:      HOL/Induct/Com
paulson@3120
     2
    ID:         $Id$
paulson@3120
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3120
     4
    Copyright   1997  University of Cambridge
paulson@3120
     5
paulson@3120
     6
Example of Mutual Induction via Iteratived Inductive Definitions: Commands
paulson@3120
     7
*)
paulson@3120
     8
berghofe@5184
     9
Com = Datatype +
paulson@3120
    10
paulson@3120
    11
types loc
paulson@3120
    12
      state = "loc => nat"
paulson@3120
    13
      n2n2n = "nat => nat => nat"
paulson@3120
    14
paulson@3120
    15
arities loc :: term
paulson@3120
    16
paulson@3120
    17
(*To avoid a mutually recursive datatype declaration, expressions and commands
paulson@3120
    18
  are combined to form a single datatype.*)
paulson@3120
    19
datatype
paulson@3120
    20
  exp = N nat
paulson@3120
    21
      | X loc
paulson@3120
    22
      | Op n2n2n exp exp
paulson@3120
    23
      | valOf exp exp          ("VALOF _ RESULTIS _"  60)
paulson@3120
    24
      | SKIP
paulson@3120
    25
      | ":="  loc exp          (infixl  60)
paulson@3146
    26
      | Semi  exp exp          ("_;;_"  [60, 60] 60)
paulson@3120
    27
      | Cond  exp exp exp      ("IF _ THEN _ ELSE _"  60)
paulson@3120
    28
      | While exp exp          ("WHILE _ DO _"  60)
paulson@3120
    29
paulson@3120
    30
(** Execution of commands **)
paulson@3120
    31
consts  exec    :: "((exp*state) * (nat*state)) set => ((exp*state)*state)set"
paulson@3120
    32
       "@exec"  :: "((exp*state) * (nat*state)) set => 
paulson@3120
    33
                    [exp*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
paulson@3120
    34
paulson@3120
    35
translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
paulson@3120
    36
oheimb@4264
    37
syntax  eval'   :: "[exp*state,nat*state] => 
oheimb@4264
    38
		    ((exp*state) * (nat*state)) set => bool"
oheimb@4264
    39
						   ("_/ -|[_]-> _" [50,0,50] 50)
oheimb@4264
    40
translations
oheimb@4264
    41
    "esig -|[eval]-> ns" => "(esig,ns) : eval"
oheimb@4264
    42
paulson@3120
    43
constdefs assign :: [state,nat,loc] => state    ("_[_'/_]" [95,0,0] 95)
paulson@3120
    44
  "s[m/x] ==  (%y. if y=x then m else s y)"
paulson@3120
    45
paulson@3120
    46
paulson@3120
    47
(*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*)
paulson@3120
    48
inductive "exec eval"
paulson@3120
    49
  intrs
paulson@3120
    50
    Skip    "(SKIP,s) -[eval]-> s"
paulson@3120
    51
oheimb@4264
    52
    Assign  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'[v/x]"
paulson@3120
    53
paulson@3120
    54
    Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
paulson@3120
    55
            ==> (c0 ;; c1, s) -[eval]-> s1"
paulson@3120
    56
oheimb@4264
    57
    IfTrue "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |] 
paulson@3120
    58
            ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
paulson@3120
    59
oheimb@4264
    60
    IfFalse "[| (e,s) -|[eval]->  (1,s');  (c1,s') -[eval]-> s1 |] 
paulson@3120
    61
             ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
paulson@3120
    62
oheimb@4264
    63
    WhileFalse "(e,s) -|[eval]-> (1,s1) ==> (WHILE e DO c, s) -[eval]-> s1"
paulson@3120
    64
oheimb@4264
    65
    WhileTrue  "[| (e,s) -|[eval]-> (0,s1);
paulson@3120
    66
                (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
paulson@3120
    67
                ==> (WHILE e DO c, s) -[eval]-> s3"
paulson@3120
    68
paulson@3120
    69
constdefs
paulson@3120
    70
    Unique   :: "['a, 'b, ('a*'b) set] => bool"
paulson@3120
    71
    "Unique x y r == ALL y'. (x,y'): r --> y = y'"
paulson@3120
    72
paulson@3120
    73
    Function :: "('a*'b) set => bool"
paulson@3120
    74
    "Function r == ALL x y. (x,y): r --> Unique x y r"
paulson@3120
    75
end