src/HOL/Induct/Com.ML
 author paulson Wed, 15 Jul 1998 10:15:13 +0200 changeset 5143 b94cd208f073 parent 5069 3ea049f7979d child 5223 4cb05273f764 permissions -rw-r--r--
Removal of leading "\!\!..." from most Goal commands
```
(*  Title:      HOL/Induct/Com
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Example of Mutual Induction via Iteratived Inductive Definitions: Commands
*)

open Com;

val exec_elim_cases = map (exec.mk_cases exp.simps)
["(SKIP,s) -[eval]-> t", "(x:=a,s) -[eval]-> t", "(c1;;c2, s) -[eval]-> t",
"(IF e THEN c1 ELSE c2, s) -[eval]-> t"];

val exec_WHILE_case = exec.mk_cases exp.simps "(WHILE b DO c,s) -[eval]-> t";

(*This theorem justifies using "exec" in the inductive definition of "eval"*)
Goalw exec.defs "A<=B ==> exec(A) <= exec(B)";
by (rtac lfp_mono 1);
by (REPEAT (ares_tac basic_monos 1));
qed "exec_mono";

Unify.trace_bound := 30;
Unify.search_bound := 60;

(*Command execution is functional (deterministic) provided evaluation is*)
Goal "Function ev ==> Function(exec ev)";
by (simp_tac (simpset() addsimps [Function_def, Unique_def]) 1);
by (REPEAT (rtac allI 1));
by (rtac impI 1);
by (etac exec.induct 1);
by (Blast_tac 3);
by (Blast_tac 1);
by (rewrite_goals_tac [Function_def, Unique_def]);
by (thin_tac "(?c,s1) -[ev]-> s2" 5);
by (rotate_tac 1 5);   (*PATCH to avoid very slow proof*)
(*SLOW (23s) due to proof reconstruction; needs 60s if thin_tac is omitted*)
by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1));
qed "Function_exec";

Goalw [assign_def] "(s[v/x])x = v";
by (Simp_tac 1);
qed "assign_same";

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

Goalw [assign_def] "s[s x/x] = s";
by (rtac ext 1);
by (Simp_tac 1);
qed "assign_triv";