author  berghofe 
Fri, 24 Jul 1998 13:39:47 +0200  
changeset 5191  8ceaa19f7717 
parent 5143  b94cd208f073 
child 5223  4cb05273f764 
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 
open Com; 
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 
AddIs exec.intrs; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

12 

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

13 
val exec_elim_cases = map (exec.mk_cases exp.simps) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

14 
["(SKIP,s) [eval]> t", "(x:=a,s) [eval]> t", "(c1;;c2, s) [eval]> t", 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

15 
"(IF e THEN c1 ELSE c2, s) [eval]> t"]; 
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 
val exec_WHILE_case = exec.mk_cases exp.simps "(WHILE b DO c,s) [eval]> t"; 
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 
AddSEs exec_elim_cases; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

20 

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

21 
(*This theorem justifies using "exec" in the inductive definition of "eval"*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

22 
Goalw exec.defs "A<=B ==> exec(A) <= exec(B)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

24 
by (REPEAT (ares_tac basic_monos 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

26 

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

27 

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

28 
Unify.trace_bound := 30; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

29 
Unify.search_bound := 60; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

30 

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

31 
(*Command execution is functional (deterministic) provided evaluation is*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

32 
Goal "Function ev ==> Function(exec ev)"; 
4089  33 
by (simp_tac (simpset() addsimps [Function_def, Unique_def]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

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

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

39 
by (rewrite_goals_tac [Function_def, Unique_def]); 
3142  40 
by (thin_tac "(?c,s1) [ev]> s2" 5); 
4390  41 
by (rotate_tac 1 5); (*PATCH to avoid very slow proof*) 
3142  42 
(*SLOW (23s) due to proof reconstruction; needs 60s if thin_tac is omitted*) 
4089  43 
by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1)); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

44 
qed "Function_exec"; 
3147  45 

46 

5069  47 
Goalw [assign_def] "(s[v/x])x = v"; 
3147  48 
by (Simp_tac 1); 
49 
qed "assign_same"; 

50 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

51 
Goalw [assign_def] "y~=x ==> (s[v/x])y = s y"; 
3147  52 
by (Asm_simp_tac 1); 
53 
qed "assign_different"; 

54 

5069  55 
Goalw [assign_def] "s[s x/x] = s"; 
3457  56 
by (rtac ext 1); 
4686  57 
by (Simp_tac 1); 
3147  58 
qed "assign_triv"; 
59 

60 
Addsimps [assign_same, assign_different, assign_triv]; 