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