src/HOL/Induct/Exp.ML
author paulson
Wed, 15 Jul 1998 14:19:02 +0200
changeset 5148 74919e8f221c
parent 5143 b94cd208f073
child 5223 4cb05273f764
permissions -rw-r--r--
More tidying and removal of "\!\!... from Goal commands
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Induct/Exp
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     2
    ID:         $Id$
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     4
    Copyright   1997  University of Cambridge
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     5
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     6
Example of Mutual Induction via Iteratived Inductive Definitions: Expressions
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     7
*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     8
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     9
open Exp;
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    10
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
    11
AddSIs [eval.N, eval.X];
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
    12
AddIs  [eval.Op, eval.valOf];
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
    13
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    14
val eval_elim_cases = map (eval.mk_cases exp.simps)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    15
   ["(N(n),sigma) -|-> (n',s')", "(X(x),sigma) -|-> (n,s')",
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    16
    "(Op f a1 a2,sigma)  -|-> (n,s')",
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    17
    "(VALOF c RESULTIS e, s) -|-> (n, s1)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    18
   ];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    19
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    20
AddSEs eval_elim_cases;
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    21
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    22
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4477
diff changeset
    23
Goal "(X x, s[n/x]) -|-> (n, s[n/x])";
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
    24
by (rtac (assign_same RS subst) 1 THEN resolve_tac eval.intrs 1);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
    25
qed "var_assign_eval";
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
    26
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
    27
AddSIs [var_assign_eval];
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
    28
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
    29
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    30
(** Make the induction rule look nicer -- though eta_contract makes the new
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    31
    version look worse than it is...**)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    32
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4477
diff changeset
    33
Goal "{((e,s),(n,s')). P e s n s'} = \
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    34
\         Collect (split (%v. split (split P v)))";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    35
by (rtac Collect_cong 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    36
by (split_all_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    37
by (Simp_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    38
val split_lemma = result();
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    39
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    40
(*New induction rule.  Note the form of the VALOF induction hypothesis*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    41
val major::prems = goal thy
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    42
  "[| (e,s) -|-> (n,s');                                         \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    43
\     !!n s. P (N n) s n s;                                      \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    44
\     !!s x. P (X x) s (s x) s;                                  \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    45
\     !!e0 e1 f n0 n1 s s0 s1.                                   \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    46
\        [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;                   \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    47
\           (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1                  \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    48
\        |] ==> P (Op f e0 e1) s (f n0 n1) s1;                   \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    49
\     !!c e n s s0 s1.                                           \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    50
\        [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0; \
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
    51
\           (c,s) -[eval]-> s0;                                  \
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    52
\           (e,s0) -|-> (n,s1); P e s0 n s1 |]                   \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    53
\        ==> P (VALOF c RESULTIS e) s n s1                       \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    54
\  |] ==> P e s n s'";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    55
by (rtac (major RS eval.induct) 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3718
diff changeset
    56
by (blast_tac (claset() addIs prems) 1);
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3718
diff changeset
    57
by (blast_tac (claset() addIs prems) 1);
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3718
diff changeset
    58
by (blast_tac (claset() addIs prems) 1);
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
    59
by (forward_tac [impOfSubs (Int_lower1 RS exec_mono)] 1);
4264
5e21f41ccd21 minor improvements of formulation and proofs
oheimb
parents: 4089
diff changeset
    60
by (auto_tac (claset() addIs prems,simpset() addsimps [split_lemma]));
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    61
qed "eval_induct";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    62
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    63
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    64
(*Lemma for Function_eval.  The major premise is that (c,s) executes to s1
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    65
  using eval restricted to its functional part.  Note that the execution
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    66
  (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    67
  the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    68
  functional on the argument (c,s).
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    69
*)
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
    70
Goal "(c,s) -[eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]-> s1 \
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
    71
\     ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    72
by (etac exec.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    73
by (ALLGOALS Full_simp_tac);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    74
by (Blast_tac 3);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    75
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    76
by (rewtac Unique_def);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    77
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    78
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    79
by (Blast_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3718
diff changeset
    80
by (blast_tac (claset() addEs [exec_WHILE_case]) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    81
by (thin_tac "(?c,s2) -[?ev]-> s3" 1);
3718
d78cf498a88c Minor tidying to use Clarify_tac, etc.
paulson
parents: 3145
diff changeset
    82
by (Clarify_tac 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    83
by (etac exec_WHILE_case 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    84
by (ALLGOALS Fast_tac);         (*Blast_tac: proof fails*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    85
qed "com_Unique";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    86
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    87
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    88
(*Expression evaluation is functional, or deterministic*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4477
diff changeset
    89
Goalw [Function_def] "Function eval";
4264
5e21f41ccd21 minor improvements of formulation and proofs
oheimb
parents: 4089
diff changeset
    90
by (strip_tac 1);
5e21f41ccd21 minor improvements of formulation and proofs
oheimb
parents: 4089
diff changeset
    91
by (split_all_tac 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    92
by (etac eval_induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    93
by (dtac com_Unique 4);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3718
diff changeset
    94
by (ALLGOALS (full_simp_tac (simpset() addsimps [Unique_def])));
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    95
by (ALLGOALS Blast_tac);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    96
qed "Function_eval";
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
    97
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
    98
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    99
Goal "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   100
by (etac eval_induct 1);
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   101
by (ALLGOALS Asm_simp_tac);
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   102
val lemma = result();
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   103
bind_thm ("eval_N_E", refl RSN (2, lemma RS mp));
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   104
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   105
AddSEs [eval_N_E];
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   106
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   107
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   108
(*This theorem says that "WHILE TRUE DO c" cannot terminate*)
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   109
Goal "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False";
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   110
by (etac exec.induct 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4264
diff changeset
   111
by Auto_tac;
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   112
bind_thm ("while_true_E", refl RSN (2, result() RS mp));
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   113
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   114
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   115
(** Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and  WHILE e DO c **)
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   116
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   117
Goal "(c',s) -[eval]-> t ==> \
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   118
\              (c' = WHILE e DO c) --> \
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   119
\              (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t";
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   120
by (etac exec.induct 1);
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   121
by (ALLGOALS Asm_simp_tac);
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   122
by (ALLGOALS Blast_tac); 
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   123
bind_thm ("while_if1", refl RSN (2, result() RS mp));
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   124
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   125
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   126
Goal "(c',s) -[eval]-> t ==> \
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   127
\              (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) --> \
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   128
\              (WHILE e DO c, s) -[eval]-> t";
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   129
by (etac exec.induct 1);
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   130
by (ALLGOALS Asm_simp_tac);
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   131
by (ALLGOALS Blast_tac); 
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   132
bind_thm ("while_if2", refl RSN (2, result() RS mp));
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   133
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   134
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   135
Goal "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t)  =  \
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   136
\         ((WHILE e DO c, s) -[eval]-> t)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3718
diff changeset
   137
by (blast_tac (claset() addIs [while_if1, while_if2]) 1);
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   138
qed "while_if";
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   139
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   140
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   141
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   142
(** Equivalence of  (IF e THEN c1 ELSE c2);;c
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   143
               and  IF e THEN (c1;;c) ELSE (c2;;c)   **)
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   144
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   145
Goal "(c',s) -[eval]-> t ==> \
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   146
\              (c' = (IF e THEN c1 ELSE c2);;c) --> \
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   147
\              (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t";
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   148
by (etac exec.induct 1);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   149
by (ALLGOALS Asm_simp_tac);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   150
by (Blast_tac 1); 
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   151
bind_thm ("if_semi1", refl RSN (2, result() RS mp));
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   152
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   153
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   154
Goal "(c',s) -[eval]-> t ==> \
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   155
\              (c' = IF e THEN (c1;;c) ELSE (c2;;c)) --> \
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   156
\              ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t";
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   157
by (etac exec.induct 1);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   158
by (ALLGOALS Asm_simp_tac);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   159
by (ALLGOALS Blast_tac); 
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   160
bind_thm ("if_semi2", refl RSN (2, result() RS mp));
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   161
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   162
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   163
Goal "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t)  =  \
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   164
\         ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3718
diff changeset
   165
by (blast_tac (claset() addIs [if_semi1, if_semi2]) 1);
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   166
qed "if_semi";
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   167
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   168
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   169
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   170
(** Equivalence of  VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   171
               and  VALOF c1;;c2 RESULTIS e
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   172
 **)
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   173
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   174
Goal "(e',s) -|-> (v,s') ==> \
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   175
\              (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) --> \
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   176
\              (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')";
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   177
by (etac eval_induct 1);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   178
by (ALLGOALS Asm_simp_tac);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   179
by (Blast_tac 1); 
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   180
bind_thm ("valof_valof1", refl RSN (2, result() RS mp));
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   181
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   182
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   183
Goal "(e',s) -|-> (v,s') ==> \
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   184
\              (e' = VALOF c1;;c2 RESULTIS e) --> \
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   185
\              (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')";
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   186
by (etac eval_induct 1);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   187
by (ALLGOALS Asm_simp_tac);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   188
by (Blast_tac 1); 
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   189
bind_thm ("valof_valof2", refl RSN (2, result() RS mp));
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   190
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   191
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   192
Goal "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s'))  =  \
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   193
\         ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3718
diff changeset
   194
by (blast_tac (claset() addIs [valof_valof1, valof_valof2]) 1);
3144
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   195
qed "valof_valof";
04b0d8941365 New proofs about WHILE and VALOF
paulson
parents: 3120
diff changeset
   196
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   197
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   198
(** Equivalence of  VALOF SKIP RESULTIS e  and  e **)
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   199
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   200
Goal "(e',s) -|-> (v,s') ==> \
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   201
\              (e' = VALOF SKIP RESULTIS e) --> \
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   202
\              (e, s) -|-> (v,s')";
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   203
by (etac eval_induct 1);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   204
by (ALLGOALS Asm_simp_tac);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   205
by (Blast_tac 1); 
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   206
bind_thm ("valof_skip1", refl RSN (2, result() RS mp));
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   207
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   208
Goal "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')";
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   209
by (Blast_tac 1);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   210
qed "valof_skip2";
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   211
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   212
Goal "((VALOF SKIP RESULTIS e, s) -|-> (v,s'))  =  ((e, s) -|-> (v,s'))";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3718
diff changeset
   213
by (blast_tac (claset() addIs [valof_skip1, valof_skip2]) 1);
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   214
qed "valof_skip";
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   215
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   216
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   217
(** Equivalence of  VALOF x:=e RESULTIS x  and  e **)
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   218
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   219
Goal "(e',s) -|-> (v,s'') ==> \
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   220
\              (e' = VALOF x:=e RESULTIS X x) --> \
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   221
\              (EX s'. (e, s) -|-> (v,s') & (s'' = s'[v/x]))";
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   222
by (etac eval_induct 1);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   223
by (ALLGOALS Asm_simp_tac);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   224
by (thin_tac "?PP-->?QQ" 1);
3718
d78cf498a88c Minor tidying to use Clarify_tac, etc.
paulson
parents: 3145
diff changeset
   225
by (Clarify_tac 1);
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   226
by (Simp_tac 1);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   227
by (Blast_tac 1); 
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   228
bind_thm ("valof_assign1", refl RSN (2, result() RS mp));
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   229
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   230
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   231
Goal "(e,s) -|-> (v,s') ==> \
3145
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   232
\              (VALOF x:=e RESULTIS X x, s) -|-> (v,s'[v/x])";
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   233
by (Blast_tac 1);
809a2c9902f7 New equivalence proofs
paulson
parents: 3144
diff changeset
   234
qed "valof_assign2";