src/HOL/Induct/Com.ML
changeset 3120 c58423c20740
child 3142 a6f73a02c619
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Induct/Com.ML	Wed May 07 12:50:26 1997 +0200
     1.3 @@ -0,0 +1,43 @@
     1.4 +(*  Title:      HOL/Induct/Com
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1997  University of Cambridge
     1.8 +
     1.9 +Example of Mutual Induction via Iteratived Inductive Definitions: Commands
    1.10 +*)
    1.11 +
    1.12 +open Com;
    1.13 +
    1.14 +AddIs exec.intrs;
    1.15 +
    1.16 +val exec_elim_cases = map (exec.mk_cases exp.simps)
    1.17 +   ["(SKIP,s) -[eval]-> t", "(x:=a,s) -[eval]-> t", "(c1;;c2, s) -[eval]-> t",
    1.18 +    "(IF e THEN c1 ELSE c2, s) -[eval]-> t"];
    1.19 +
    1.20 +val exec_WHILE_case = exec.mk_cases exp.simps "(WHILE b DO c,s) -[eval]-> t";
    1.21 +
    1.22 +AddSEs exec_elim_cases;
    1.23 +
    1.24 +(*This theorem justifies using "exec" in the inductive definition of "eval"*)
    1.25 +goalw thy exec.defs "!!A B. A<=B ==> exec(A) <= exec(B)";
    1.26 +by (rtac lfp_mono 1);
    1.27 +by (REPEAT (ares_tac basic_monos 1));
    1.28 +qed "exec_mono";
    1.29 +
    1.30 +
    1.31 +Unify.trace_bound := 30;
    1.32 +Unify.search_bound := 60;
    1.33 +
    1.34 +(*Command execution is functional (deterministic) provided evaluation is*)
    1.35 +goal thy "!!x. Function ev ==> Function(exec ev)";
    1.36 +by (simp_tac (!simpset addsimps [Function_def, Unique_def]) 1);
    1.37 +by (REPEAT (rtac allI 1));
    1.38 +by (rtac impI 1);
    1.39 +by (etac exec.induct 1);
    1.40 +by (Blast_tac 3);
    1.41 +by (Blast_tac 1);
    1.42 +by (rewrite_goals_tac [Function_def, Unique_def]);
    1.43 +(*Takes ONE MINUTE due to slow proof reconstruction*)
    1.44 +by (ALLGOALS (blast_tac (!claset addEs [exec_WHILE_case])));
    1.45 +qed "Function_exec";
    1.46 +