src/HOL/Induct/Com.thy
author wenzelm
Fri, 05 Oct 2001 21:52:39 +0200
changeset 11701 3d51fbf81c17
parent 11464 ddea204de5bc
child 12338 de0f4a63baa5
permissions -rw-r--r--
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
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
10759
994877ee68cb *** empty log message ***
nipkow
parents: 5184
diff changeset
     9
Com = Main +
3120
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
datatype
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    18
  exp = N nat
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    19
      | X loc
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    20
      | Op n2n2n exp exp
10759
994877ee68cb *** empty log message ***
nipkow
parents: 5184
diff changeset
    21
      | valOf com exp          ("VALOF _ RESULTIS _"  60)
994877ee68cb *** empty log message ***
nipkow
parents: 5184
diff changeset
    22
and
994877ee68cb *** empty log message ***
nipkow
parents: 5184
diff changeset
    23
  com = SKIP
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    24
      | ":="  loc exp          (infixl  60)
10759
994877ee68cb *** empty log message ***
nipkow
parents: 5184
diff changeset
    25
      | Semi  com com          ("_;;_"  [60, 60] 60)
994877ee68cb *** empty log message ***
nipkow
parents: 5184
diff changeset
    26
      | Cond  exp com com      ("IF _ THEN _ ELSE _"  60)
994877ee68cb *** empty log message ***
nipkow
parents: 5184
diff changeset
    27
      | While exp com          ("WHILE _ DO _"  60)
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    28
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    29
(** Execution of commands **)
10759
994877ee68cb *** empty log message ***
nipkow
parents: 5184
diff changeset
    30
consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    31
       "@exec"  :: "((exp*state) * (nat*state)) set => 
10759
994877ee68cb *** empty log message ***
nipkow
parents: 5184
diff changeset
    32
                    [com*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    33
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    34
translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    35
4264
5e21f41ccd21 minor improvements of formulation and proofs
oheimb
parents: 3146
diff changeset
    36
syntax  eval'   :: "[exp*state,nat*state] => 
5e21f41ccd21 minor improvements of formulation and proofs
oheimb
parents: 3146
diff changeset
    37
		    ((exp*state) * (nat*state)) set => bool"
5e21f41ccd21 minor improvements of formulation and proofs
oheimb
parents: 3146
diff changeset
    38
						   ("_/ -|[_]-> _" [50,0,50] 50)
5e21f41ccd21 minor improvements of formulation and proofs
oheimb
parents: 3146
diff changeset
    39
translations
5e21f41ccd21 minor improvements of formulation and proofs
oheimb
parents: 3146
diff changeset
    40
    "esig -|[eval]-> ns" => "(esig,ns) : eval"
5e21f41ccd21 minor improvements of formulation and proofs
oheimb
parents: 3146
diff changeset
    41
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    42
(*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    43
inductive "exec eval"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    44
  intrs
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    45
    Skip    "(SKIP,s) -[eval]-> s"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    46
10759
994877ee68cb *** empty log message ***
nipkow
parents: 5184
diff changeset
    47
    Assign  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    48
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    49
    Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    50
            ==> (c0 ;; c1, s) -[eval]-> s1"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    51
4264
5e21f41ccd21 minor improvements of formulation and proofs
oheimb
parents: 3146
diff changeset
    52
    IfTrue "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |] 
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    53
            ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    54
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11464
diff changeset
    55
    IfFalse "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |] 
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    56
             ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    57
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11464
diff changeset
    58
    WhileFalse "(e,s) -|[eval]-> (Suc 0, s1) ==> (WHILE e DO c, s) -[eval]-> s1"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    59
4264
5e21f41ccd21 minor improvements of formulation and proofs
oheimb
parents: 3146
diff changeset
    60
    WhileTrue  "[| (e,s) -|[eval]-> (0,s1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    61
                (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
    62
                ==> (WHILE e DO c, s) -[eval]-> s3"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    63
end