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