src/HOL/Induct/Com.thy
author wenzelm
Thu, 26 Jun 1997 11:14:46 +0200
changeset 3462 3472fa00b1d4
parent 3146 922a60451382
child 4264 5e21f41ccd21
permissions -rw-r--r--
rearrange pages of ps file to be printed as booklet (duplex);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Induct/Com
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     2
    ID:         $Id$
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     4
    Copyright   1997  University of Cambridge
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     5
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     6
Example of Mutual Induction via Iteratived Inductive Definitions: Commands
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     7
*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     8
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     9
Com = Arith +
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    10
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    11
types loc
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    12
      state = "loc => nat"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    13
      n2n2n = "nat => nat => nat"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    14
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    15
arities loc :: term
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    16
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    17
(*To avoid a mutually recursive datatype declaration, expressions and commands
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    18
  are combined to form a single datatype.*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    19
datatype
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    20
  exp = N nat
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    21
      | X loc
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    22
      | Op n2n2n exp exp
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    23
      | valOf exp exp          ("VALOF _ RESULTIS _"  60)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    24
      | SKIP
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    25
      | ":="  loc exp          (infixl  60)
3146
922a60451382 Fixed precedence of semicolon
paulson
parents: 3120
diff changeset
    26
      | Semi  exp exp          ("_;;_"  [60, 60] 60)
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    27
      | Cond  exp exp exp      ("IF _ THEN _ ELSE _"  60)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    28
      | While exp exp          ("WHILE _ DO _"  60)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    29
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    30
(** Execution of commands **)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    31
consts  exec    :: "((exp*state) * (nat*state)) set => ((exp*state)*state)set"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    32
       "@exec"  :: "((exp*state) * (nat*state)) set => 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    33
                    [exp*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    34
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    35
translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    36
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    37
constdefs assign :: [state,nat,loc] => state    ("_[_'/_]" [95,0,0] 95)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    38
  "s[m/x] ==  (%y. if y=x then m else s y)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    39
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    40
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    41
(*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    42
inductive "exec eval"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    43
  intrs
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    44
    Skip    "(SKIP,s) -[eval]-> s"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    45
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    46
    Assign  "((e,s), (v,s')) : eval ==> (x := e, s) -[eval]-> s'[v/x]"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    47
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    48
    Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    49
            ==> (c0 ;; c1, s) -[eval]-> s1"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    50
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    51
    IfTrue "[| ((e,s), (0,s')) : eval;  (c0,s') -[eval]-> s1 |] 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    52
            ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    53
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    54
    IfFalse "[| ((e,s), (1,s')) : eval;  (c1,s') -[eval]-> s1 |] 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    55
             ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    56
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    57
    WhileFalse "((e,s), (1,s1)) : eval ==> (WHILE e DO c, s) -[eval]-> s1"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    58
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    59
    WhileTrue  "[| ((e,s), (0,s1)) : eval;
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    60
                (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    61
                ==> (WHILE e DO c, s) -[eval]-> s3"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    62
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    63
constdefs
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    64
    Unique   :: "['a, 'b, ('a*'b) set] => bool"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    65
    "Unique x y r == ALL y'. (x,y'): r --> y = y'"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    66
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    67
    Function :: "('a*'b) set => bool"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    68
    "Function r == ALL x y. (x,y): r --> Unique x y r"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    69
end