author  berghofe 
Fri, 24 Jul 1998 13:39:47 +0200  
changeset 5191  8ceaa19f7717 
parent 5184  9b8547a9496a 
child 10759  994877ee68cb 
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 

5184  9 
Com = Datatype + 
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 
(*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  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 

4264  37 
syntax eval' :: "[exp*state,nat*state] => 
38 
((exp*state) * (nat*state)) set => bool" 

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

40 
translations 

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

42 

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

43 
constdefs assign :: [state,nat,loc] => state ("_[_'/_]" [95,0,0] 95) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

45 

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

46 

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

47 
(*Command execution. Natural numbers represent Booleans: 0=True, 1=False*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

48 
inductive "exec eval" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

50 
Skip "(SKIP,s) [eval]> s" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

51 

4264  52 
Assign "(e,s) [eval]> (v,s') ==> (x := e, s) [eval]> s'[v/x]" 
3120
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 
Semi "[ (c0,s) [eval]> s2; (c1,s2) [eval]> s1 ] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

55 
==> (c0 ;; c1, s) [eval]> s1" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

56 

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

58 
==> (IF e THEN c0 ELSE c1, s) [eval]> s1" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

59 

4264  60 
IfFalse "[ (e,s) [eval]> (1,s'); (c1,s') [eval]> s1 ] 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

61 
==> (IF e THEN c0 ELSE c1, s) [eval]> s1" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

62 

4264  63 
WhileFalse "(e,s) [eval]> (1,s1) ==> (WHILE e DO c, s) [eval]> s1" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

64 

4264  65 
WhileTrue "[ (e,s) [eval]> (0,s1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

67 
==> (WHILE e DO c, s) [eval]> s3" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

68 

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

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

70 
Unique :: "['a, 'b, ('a*'b) set] => bool" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

72 

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

73 
Function :: "('a*'b) set => bool" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

75 
end 