src/HOL/Induct/Com.thy
author wenzelm
Fri Nov 25 21:14:34 2005 +0100 (2005-11-25)
changeset 18260 5597cfcecd49
parent 16417 9bc16273c2d4
child 19736 d8d0f8f51d69
permissions -rw-r--r--
tuned induct proofs;
     1 (*  Title:      HOL/Induct/Com
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 Example of Mutual Induction via Iteratived Inductive Definitions: Commands
     7 *)
     8 
     9 header{*Mutual Induction via Iteratived Inductive Definitions*}
    10 
    11 theory Com imports Main begin
    12 
    13 typedecl loc
    14 
    15 types  state = "loc => nat"
    16        n2n2n = "nat => nat => nat"
    17 
    18 arities loc :: type
    19 
    20 datatype
    21   exp = N nat
    22       | X loc
    23       | Op n2n2n exp exp
    24       | valOf com exp          ("VALOF _ RESULTIS _"  60)
    25 and
    26   com = SKIP
    27       | ":="  loc exp          (infixl  60)
    28       | Semi  com com          ("_;;_"  [60, 60] 60)
    29       | Cond  exp com com      ("IF _ THEN _ ELSE _"  60)
    30       | While exp com          ("WHILE _ DO _"  60)
    31 
    32 
    33 subsection {* Commands *}
    34 
    35 text{* Execution of commands *}
    36 consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
    37 syntax "@exec"  :: "((exp*state) * (nat*state)) set =>
    38                     [com*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
    39 
    40 translations  "csig -[eval]-> s" == "(csig,s) \<in> exec eval"
    41 
    42 syntax  eval'   :: "[exp*state,nat*state] =>
    43                     ((exp*state) * (nat*state)) set => bool"
    44                                            ("_/ -|[_]-> _" [50,0,50] 50)
    45 
    46 translations
    47     "esig -|[eval]-> ns" => "(esig,ns) \<in> eval"
    48 
    49 text{*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*}
    50 inductive "exec eval"
    51   intros
    52     Skip:    "(SKIP,s) -[eval]-> s"
    53 
    54     Assign:  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
    55 
    56     Semi:    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
    57              ==> (c0 ;; c1, s) -[eval]-> s1"
    58 
    59     IfTrue: "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |]
    60              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    61 
    62     IfFalse: "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |]
    63               ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    64 
    65     WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1)
    66                  ==> (WHILE e DO c, s) -[eval]-> s1"
    67 
    68     WhileTrue:  "[| (e,s) -|[eval]-> (0,s1);
    69                     (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |]
    70                  ==> (WHILE e DO c, s) -[eval]-> s3"
    71 
    72 declare exec.intros [intro]
    73 
    74 
    75 inductive_cases
    76         [elim!]: "(SKIP,s) -[eval]-> t"
    77     and [elim!]: "(x:=a,s) -[eval]-> t"
    78     and [elim!]: "(c1;;c2, s) -[eval]-> t"
    79     and [elim!]: "(IF e THEN c1 ELSE c2, s) -[eval]-> t"
    80     and exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t"
    81 
    82 
    83 text{*Justifies using "exec" in the inductive definition of "eval"*}
    84 lemma exec_mono: "A<=B ==> exec(A) <= exec(B)"
    85 apply (unfold exec.defs )
    86 apply (rule lfp_mono)
    87 apply (assumption | rule basic_monos)+
    88 done
    89 
    90 ML {*
    91 Unify.trace_bound := 30;
    92 Unify.search_bound := 60;
    93 *}
    94 
    95 text{*Command execution is functional (deterministic) provided evaluation is*}
    96 theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
    97 apply (simp add: single_valued_def)
    98 apply (intro allI)
    99 apply (rule impI)
   100 apply (erule exec.induct)
   101 apply (blast elim: exec_WHILE_case)+
   102 done
   103 
   104 
   105 subsection {* Expressions *}
   106 
   107 text{* Evaluation of arithmetic expressions *}
   108 consts  eval    :: "((exp*state) * (nat*state)) set"
   109        "-|->"   :: "[exp*state,nat*state] => bool"         (infixl 50)
   110 
   111 translations
   112     "esig -|-> (n,s)" <= "(esig,n,s) \<in> eval"
   113     "esig -|-> ns"    == "(esig,ns ) \<in> eval"
   114 
   115 inductive eval
   116   intros
   117     N [intro!]: "(N(n),s) -|-> (n,s)"
   118 
   119     X [intro!]: "(X(x),s) -|-> (s(x),s)"
   120 
   121     Op [intro]: "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |]
   122                  ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"
   123 
   124     valOf [intro]: "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |]
   125                     ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
   126 
   127   monos exec_mono
   128 
   129 
   130 inductive_cases
   131         [elim!]: "(N(n),sigma) -|-> (n',s')"
   132     and [elim!]: "(X(x),sigma) -|-> (n,s')"
   133     and [elim!]: "(Op f a1 a2,sigma)  -|-> (n,s')"
   134     and [elim!]: "(VALOF c RESULTIS e, s) -|-> (n, s1)"
   135 
   136 
   137 lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))"
   138 by (rule fun_upd_same [THEN subst], fast)
   139 
   140 
   141 text{* Make the induction rule look nicer -- though eta_contract makes the new
   142     version look worse than it is...*}
   143 
   144 lemma split_lemma:
   145      "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
   146 by auto
   147 
   148 text{*New induction rule.  Note the form of the VALOF induction hypothesis*}
   149 lemma eval_induct
   150   [case_names N X Op valOf, consumes 1, induct set: eval]:
   151   "[| (e,s) -|-> (n,s');
   152       !!n s. P (N n) s n s;
   153       !!s x. P (X x) s (s x) s;
   154       !!e0 e1 f n0 n1 s s0 s1.
   155          [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;
   156             (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1
   157          |] ==> P (Op f e0 e1) s (f n0 n1) s1;
   158       !!c e n s s0 s1.
   159          [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0;
   160             (c,s) -[eval]-> s0;
   161             (e,s0) -|-> (n,s1); P e s0 n s1 |]
   162          ==> P (VALOF c RESULTIS e) s n s1
   163    |] ==> P e s n s'"
   164 apply (induct set: eval)
   165 apply blast
   166 apply blast
   167 apply blast
   168 apply (frule Int_lower1 [THEN exec_mono, THEN subsetD])
   169 apply (auto simp add: split_lemma)
   170 done
   171 
   172 
   173 text{*Lemma for Function_eval.  The major premise is that (c,s) executes to s1
   174   using eval restricted to its functional part.  Note that the execution
   175   (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that
   176   the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
   177   functional on the argument (c,s).
   178 *}
   179 lemma com_Unique:
   180  "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1
   181   ==> \<forall>s2. (c,s) -[eval]-> s2 --> s2=s1"
   182 apply (induct set: exec)
   183       apply simp_all
   184       apply blast
   185      apply force
   186     apply blast
   187    apply blast
   188   apply blast
   189  apply (blast elim: exec_WHILE_case)
   190 apply (erule_tac V = "(?c,s2) -[?ev]-> s3" in thin_rl)
   191 apply clarify
   192 apply (erule exec_WHILE_case, blast+)
   193 done
   194 
   195 
   196 text{*Expression evaluation is functional, or deterministic*}
   197 theorem single_valued_eval: "single_valued eval"
   198 apply (unfold single_valued_def)
   199 apply (intro allI, rule impI)
   200 apply (simp (no_asm_simp) only: split_tupled_all)
   201 apply (erule eval_induct)
   202 apply (drule_tac [4] com_Unique)
   203 apply (simp_all (no_asm_use))
   204 apply blast+
   205 done
   206 
   207 lemma eval_N_E [dest!]: "(N n, s) -|-> (v, s') ==> (v = n & s' = s)"
   208   by (induct e == "N n" s v s' set: eval) simp_all
   209 
   210 text{*This theorem says that "WHILE TRUE DO c" cannot terminate*}
   211 lemma while_true_E:
   212     "(c', s) -[eval]-> t ==> c' = WHILE (N 0) DO c ==> False"
   213   by (induct set: exec) auto
   214 
   215 
   216 subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and
   217        WHILE e DO c *}
   218 
   219 lemma while_if1:
   220      "(c',s) -[eval]-> t
   221       ==> c' = WHILE e DO c ==>
   222           (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t"
   223   by (induct set: exec) auto
   224 
   225 lemma while_if2:
   226      "(c',s) -[eval]-> t
   227       ==> c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP ==>
   228           (WHILE e DO c, s) -[eval]-> t"
   229   by (induct set: exec) auto
   230 
   231 
   232 theorem while_if:
   233      "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t)  =
   234       ((WHILE e DO c, s) -[eval]-> t)"
   235 by (blast intro: while_if1 while_if2)
   236 
   237 
   238 
   239 subsection{* Equivalence of  (IF e THEN c1 ELSE c2);;c
   240                          and  IF e THEN (c1;;c) ELSE (c2;;c)   *}
   241 
   242 lemma if_semi1:
   243      "(c',s) -[eval]-> t
   244       ==> c' = (IF e THEN c1 ELSE c2);;c ==>
   245           (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t"
   246   by (induct set: exec) auto
   247 
   248 lemma if_semi2:
   249      "(c',s) -[eval]-> t
   250       ==> c' = IF e THEN (c1;;c) ELSE (c2;;c) ==>
   251           ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t"
   252   by (induct set: exec) auto
   253 
   254 theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t)  =
   255                   ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)"
   256   by (blast intro: if_semi1 if_semi2)
   257 
   258 
   259 
   260 subsection{* Equivalence of  VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
   261                   and  VALOF c1;;c2 RESULTIS e
   262  *}
   263 
   264 lemma valof_valof1:
   265      "(e',s) -|-> (v,s')
   266       ==> e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e) ==>
   267           (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')"
   268   by (induct set: eval) auto
   269 
   270 lemma valof_valof2:
   271      "(e',s) -|-> (v,s')
   272       ==> e' = VALOF c1;;c2 RESULTIS e ==>
   273           (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')"
   274   by (induct set: eval) auto
   275 
   276 theorem valof_valof:
   277      "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s'))  =
   278       ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))"
   279   by (blast intro: valof_valof1 valof_valof2)
   280 
   281 
   282 subsection{* Equivalence of  VALOF SKIP RESULTIS e  and  e *}
   283 
   284 lemma valof_skip1:
   285      "(e',s) -|-> (v,s')
   286       ==> e' = VALOF SKIP RESULTIS e ==>
   287           (e, s) -|-> (v,s')"
   288   by (induct set: eval) auto
   289 
   290 lemma valof_skip2:
   291     "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')"
   292   by blast
   293 
   294 theorem valof_skip:
   295     "((VALOF SKIP RESULTIS e, s) -|-> (v,s'))  =  ((e, s) -|-> (v,s'))"
   296   by (blast intro: valof_skip1 valof_skip2)
   297 
   298 
   299 subsection{* Equivalence of  VALOF x:=e RESULTIS x  and  e *}
   300 
   301 lemma valof_assign1:
   302      "(e',s) -|-> (v,s'')
   303       ==> e' = VALOF x:=e RESULTIS X x ==>
   304           (\<exists>s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))"
   305   by (induct set: eval) (simp_all del: fun_upd_apply, clarify, auto)
   306 
   307 lemma valof_assign2:
   308     "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))"
   309   by blast
   310 
   311 end