src/HOL/Induct/Com.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Com.ML	Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,43 @@
+(*  Title:      HOL/Induct/Com
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+Example of Mutual Induction via Iteratived Inductive Definitions: Commands
+*)
+
+open Com;
+
+AddIs exec.intrs;
+
+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";
+
+AddSEs exec_elim_cases;
+
+(*This theorem justifies using "exec" in the inductive definition of "eval"*)
+goalw thy exec.defs "!!A B. 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 thy "!!x. 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]);
+(*Takes ONE MINUTE due to slow proof reconstruction*)
+by (ALLGOALS (blast_tac (!claset addEs [exec_WHILE_case])));
+qed "Function_exec";
+