author | wenzelm |
Thu, 26 Jun 1997 11:14:46 +0200 | |
changeset 3462 | 3472fa00b1d4 |
parent 3457 | a8ab7c64817c |
child 3919 | c036caebfc75 |
permissions | -rw-r--r-- |
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"*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
22 |
goalw thy exec.defs "!!A B. A<=B ==> exec(A) <= exec(B)"; |
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*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
32 |
goal thy "!!x. Function ev ==> Function(exec ev)"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
33 |
by (simp_tac (!simpset addsimps [Function_def, Unique_def]) 1); |
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); |
41 |
(*SLOW (23s) due to proof reconstruction; needs 60s if thin_tac is omitted*) |
|
42 |
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
|
43 |
qed "Function_exec"; |
3147 | 44 |
|
45 |
||
46 |
goalw thy [assign_def] "(s[v/x])x = v"; |
|
47 |
by (Simp_tac 1); |
|
48 |
qed "assign_same"; |
|
49 |
||
50 |
goalw thy [assign_def] "!!y. y~=x ==> (s[v/x])y = s y"; |
|
51 |
by (Asm_simp_tac 1); |
|
52 |
qed "assign_different"; |
|
53 |
||
54 |
goalw thy [assign_def] "s[s x/x] = s"; |
|
3457 | 55 |
by (rtac ext 1); |
3147 | 56 |
by (simp_tac (!simpset setloop split_tac[expand_if]) 1); |
57 |
qed "assign_triv"; |
|
58 |
||
59 |
Addsimps [assign_same, assign_different, assign_triv]; |