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