author  paulson 
Fri, 09 May 1997 10:18:07 +0200  
changeset 3146  922a60451382 
parent 3120  c58423c20740 
child 4264  5e21f41ccd21 
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 

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