author  wenzelm 
Sat, 01 Dec 2001 18:52:32 +0100  
changeset 12338  de0f4a63baa5 
parent 11701  3d51fbf81c17 
child 13075  d3e1d554cd6d 
permissions  rwrr 
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  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 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11701
diff
changeset

15 
arities loc :: type 
3120
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  21 
 valOf com exp ("VALOF _ RESULTIS _" 60) 
22 
and 

23 
com = SKIP 

3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

24 
 ":=" loc exp (infixl 60) 
10759  25 
 Semi com com ("_;;_" [60, 60] 60) 
26 
 Cond exp com com ("IF _ THEN _ ELSE _" 60) 

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  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  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  36 
syntax eval' :: "[exp*state,nat*state] => 
37 
((exp*state) * (nat*state)) set => bool" 

38 
("_/ [_]> _" [50,0,50] 50) 

39 
translations 

40 
"esig [eval]> ns" => "(esig,ns) : eval" 

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  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  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  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 