author  paulson 
Wed, 07 May 1997 12:50:26 +0200  
changeset 3120  c58423c20740 
child 3144  04b0d8941365 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/Induct/Exp 
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: Expressions 
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 
open Exp; 
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 
val eval_elim_cases = map (eval.mk_cases exp.simps) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

12 
["(N(n),sigma) > (n',s')", "(X(x),sigma) > (n,s')", 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

13 
"(Op f a1 a2,sigma) > (n,s')", 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

14 
"(VALOF c RESULTIS e, s) > (n, s1)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

15 
]; 
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 
AddSEs eval_elim_cases; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

18 

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

19 

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

20 
(** Make the induction rule look nicer  though eta_contract makes the new 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

21 
version look worse than it is...**) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

22 

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

23 
goal thy "{((e,s),(n,s')). P e s n s'} = \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

24 
\ Collect (split (%v. split (split P v)))"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

25 
by (rtac Collect_cong 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

26 
by (split_all_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

27 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

28 
val split_lemma = result(); 
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 
(*New induction rule. Note the form of the VALOF induction hypothesis*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

31 
val major::prems = goal thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

32 
"[ (e,s) > (n,s'); \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

33 
\ !!n s. P (N n) s n s; \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

34 
\ !!s x. P (X x) s (s x) s; \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

35 
\ !!e0 e1 f n0 n1 s s0 s1. \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

36 
\ [ (e0,s) > (n0,s0); P e0 s n0 s0; \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

37 
\ (e1,s0) > (n1,s1); P e1 s0 n1 s1 \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

38 
\ ] ==> P (Op f e0 e1) s (f n0 n1) s1; \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

39 
\ !!c e n s s0 s1. \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

40 
\ [ (c,s) [eval Int {((e,s),(n,s')). P e s n s'}]> s0; \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

41 
\ (e,s0) > (n,s1); P e s0 n s1 ] \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

42 
\ ==> P (VALOF c RESULTIS e) s n s1 \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

43 
\ ] ==> P e s n s'"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

44 
by (rtac (major RS eval.induct) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

45 
by (blast_tac (!claset addIs prems) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

46 
by (blast_tac (!claset addIs prems) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

47 
by (blast_tac (!claset addIs prems) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

48 
by (fast_tac (!claset addIs prems addss (!simpset addsimps [split_lemma])) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

49 
qed "eval_induct"; 
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 

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

52 
(*Lemma for Function_eval. The major premise is that (c,s) executes to s1 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

53 
using eval restricted to its functional part. Note that the execution 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

54 
(c,s) [eval]> s2 can use unrestricted eval! The reason is that 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

55 
the execution (c,s) [eval Int {...}]> s1 assures us that execution is 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

56 
functional on the argument (c,s). 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

59 
"!!x. (c,s) [eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]> s1 \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

60 
\ ==> (ALL s2. (c,s) [eval]> s2 > s2=s1)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

61 
by (etac exec.induct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

62 
by (ALLGOALS Full_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

63 
by (Blast_tac 3); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

64 
by (Blast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

65 
by (rewtac Unique_def); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

66 
by (Blast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

67 
by (Blast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

68 
by (Blast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

69 
by (blast_tac (!claset addEs [exec_WHILE_case]) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

70 
by (thin_tac "(?c,s2) [?ev]> s3" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

71 
by (Step_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

72 
by (etac exec_WHILE_case 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

73 
by (ALLGOALS Fast_tac); (*Blast_tac: proof fails*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

74 
qed "com_Unique"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

75 

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

76 

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

77 
(*Expression evaluation is functional, or deterministic*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

78 
goal thy "Function eval"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

79 
by (simp_tac (!simpset addsimps [Function_def]) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

80 
by (REPEAT (rtac allI 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

81 
by (rtac impI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

82 
by (etac eval_induct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

83 
by (dtac com_Unique 4); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

84 
by (ALLGOALS (full_simp_tac (!simpset addsimps [Unique_def]))); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

85 
by (ALLGOALS Blast_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

86 
qed "Function_eval"; 