src/HOL/IMP/Transition.ML
author paulson
Thu Sep 26 12:47:47 1996 +0200 (1996-09-26)
changeset 2031 03a843f0f447
parent 1973 8c94c9a5be10
child 2055 cc274e47f607
permissions -rw-r--r--
Ran expandshort
nipkow@1700
     1
(*  Title:      HOL/IMP/Transition.ML
nipkow@1700
     2
    ID:         $Id$
nipkow@1700
     3
    Author:     Tobias Nipkow & Robert Sandner, TUM
nipkow@1700
     4
    Copyright   1996 TUM
nipkow@1700
     5
nipkow@1700
     6
Equivalence of Natural and Transition semantics
nipkow@1700
     7
*)
nipkow@1700
     8
nipkow@1700
     9
open Transition;
nipkow@1700
    10
nipkow@1707
    11
section "Winskel's Proof";
nipkow@1707
    12
nipkow@1973
    13
AddSEs [rel_pow_0_E];
nipkow@1700
    14
nipkow@1973
    15
val evalc1_SEs = map (evalc1.mk_cases com.simps)
nipkow@1973
    16
   ["(SKIP,s) -1-> t", "(x:=a,s) -1-> t","(c1;c2, s) -1-> t", 
nipkow@1973
    17
    "(IF b THEN c1 ELSE c2, s) -1-> t"];
nipkow@1973
    18
val evalc1_Es = map (evalc1.mk_cases com.simps)
nipkow@1973
    19
   ["(WHILE b DO c,s) -1-> t"];
nipkow@1700
    20
nipkow@1973
    21
AddSEs evalc1_SEs;
nipkow@1973
    22
nipkow@1973
    23
AddIs evalc1.intrs;
nipkow@1700
    24
nipkow@1701
    25
goal Transition.thy "!!s. (SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0";
paulson@2031
    26
by (etac rel_pow_E2 1);
nipkow@1700
    27
by (Asm_full_simp_tac 1);
paulson@2031
    28
by (Fast_tac 1);
nipkow@1973
    29
val hlemma = result();
nipkow@1700
    30
nipkow@1700
    31
nipkow@1700
    32
goal Transition.thy
nipkow@1701
    33
  "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
nipkow@1700
    34
\              (c;d, s) -*-> (SKIP, u)";
paulson@2031
    35
by (nat_ind_tac "n" 1);
nipkow@1700
    36
 (* case n = 0 *)
nipkow@1973
    37
 by(fast_tac (!claset addIs [rtrancl_into_rtrancl2])1);
nipkow@1700
    38
(* induction step *)
nipkow@1973
    39
by (safe_tac (!claset addSDs [rel_pow_Suc_D2]));
paulson@2031
    40
by (split_all_tac 1);
paulson@2031
    41
by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
nipkow@1700
    42
qed_spec_mp "lemma1";
nipkow@1700
    43
nipkow@1700
    44
paulson@1730
    45
goal Transition.thy "!!c s s1. <c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";
paulson@2031
    46
by (etac evalc.induct 1);
nipkow@1700
    47
nipkow@1700
    48
(* SKIP *)
paulson@2031
    49
by (rtac rtrancl_refl 1);
nipkow@1700
    50
nipkow@1700
    51
(* ASSIGN *)
nipkow@1973
    52
by (fast_tac (!claset addSIs [r_into_rtrancl]) 1);
nipkow@1700
    53
nipkow@1700
    54
(* SEMI *)
nipkow@1973
    55
by (fast_tac (!claset addDs [rtrancl_imp_UN_rel_pow] addIs [lemma1]) 1);
nipkow@1700
    56
nipkow@1700
    57
(* IF *)
nipkow@1973
    58
by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
nipkow@1973
    59
by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
nipkow@1700
    60
nipkow@1700
    61
(* WHILE *)
nipkow@1973
    62
by (fast_tac (!claset addSIs [r_into_rtrancl]) 1);
nipkow@1973
    63
by (fast_tac (!claset addDs [rtrancl_imp_UN_rel_pow]
nipkow@1700
    64
                        addIs [rtrancl_into_rtrancl2,lemma1]) 1);
nipkow@1700
    65
paulson@1730
    66
qed "evalc_impl_evalc1";
nipkow@1700
    67
nipkow@1700
    68
nipkow@1700
    69
goal Transition.thy
nipkow@1701
    70
  "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
nipkow@1701
    71
\            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)";
paulson@2031
    72
by (nat_ind_tac "n" 1);
nipkow@1700
    73
 (* case n = 0 *)
nipkow@1973
    74
 by (fast_tac (!claset addss !simpset) 1);
nipkow@1700
    75
(* induction step *)
nipkow@1973
    76
by (fast_tac (!claset addSIs [le_SucI,le_refl]
nipkow@1700
    77
                     addSDs [rel_pow_Suc_D2]
nipkow@1973
    78
                     addSEs [rel_pow_imp_rtrancl,rtrancl_into_rtrancl2]) 1);
nipkow@1700
    79
qed_spec_mp "lemma2";
nipkow@1700
    80
nipkow@1700
    81
goal Transition.thy "!s t. (c,s) -*-> (SKIP,t) --> <c,s> -c-> t";
nipkow@1700
    82
by (com.induct_tac "c" 1);
nipkow@1973
    83
by (safe_tac (!claset addSDs [rtrancl_imp_UN_rel_pow]));
nipkow@1700
    84
nipkow@1700
    85
(* SKIP *)
nipkow@1973
    86
by (fast_tac (!claset addSEs [rel_pow_E2]) 1);
nipkow@1700
    87
nipkow@1700
    88
(* ASSIGN *)
nipkow@1973
    89
by (fast_tac (!claset addSDs [hlemma]  addSEs [rel_pow_E2]
nipkow@1973
    90
                      addss !simpset) 1);
nipkow@1700
    91
nipkow@1700
    92
(* SEMI *)
nipkow@1973
    93
by (fast_tac (!claset addSDs [lemma2,rel_pow_imp_rtrancl]) 1);
nipkow@1700
    94
nipkow@1700
    95
(* IF *)
paulson@2031
    96
by (etac rel_pow_E2 1);
nipkow@1700
    97
by (Asm_full_simp_tac 1);
nipkow@1973
    98
by (fast_tac (!claset addSDs [rel_pow_imp_rtrancl]) 1);
nipkow@1700
    99
nipkow@1700
   100
(* WHILE, induction on the length of the computation *)
paulson@2031
   101
by (rotate_tac 1 1);
nipkow@1700
   102
by (etac rev_mp 1);
nipkow@1700
   103
by (res_inst_tac [("x","s")] spec 1);
paulson@2031
   104
by (res_inst_tac [("n","n")] less_induct 1);
nipkow@1700
   105
by (strip_tac 1);
paulson@2031
   106
by (etac rel_pow_E2 1);
nipkow@1700
   107
 by (Asm_full_simp_tac 1);
nipkow@1973
   108
by (eresolve_tac evalc1_Es 1);
nipkow@1700
   109
nipkow@1700
   110
(* WhileFalse *)
nipkow@1973
   111
 by (fast_tac (!claset addSDs [hlemma]) 1);
nipkow@1700
   112
nipkow@1700
   113
(* WhileTrue *)
paulson@2031
   114
by (fast_tac(!claset addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1);
nipkow@1700
   115
nipkow@1700
   116
qed_spec_mp "evalc1_impl_evalc";
nipkow@1700
   117
nipkow@1700
   118
nipkow@1700
   119
(**** proof of the equivalence of evalc and evalc1 ****)
nipkow@1700
   120
nipkow@1700
   121
goal Transition.thy "((c, s) -*-> (SKIP, t)) = (<c,s> -c-> t)";
nipkow@1700
   122
by (fast_tac (HOL_cs addSEs [evalc1_impl_evalc,evalc_impl_evalc1]) 1);
nipkow@1700
   123
qed "evalc1_eq_evalc";
nipkow@1707
   124
nipkow@1707
   125
nipkow@1707
   126
section "A Proof Without -n->";
nipkow@1707
   127
nipkow@1707
   128
goal Transition.thy
nipkow@1707
   129
 "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \
nipkow@1939
   130
\ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
paulson@2031
   131
by (etac converse_rtrancl_induct2 1);
paulson@2031
   132
by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
paulson@2031
   133
by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
nipkow@1707
   134
qed_spec_mp "my_lemma1";
nipkow@1707
   135
nipkow@1707
   136
paulson@1730
   137
goal Transition.thy "!!c s s1. <c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";
paulson@2031
   138
by (etac evalc.induct 1);
nipkow@1707
   139
nipkow@1707
   140
(* SKIP *)
paulson@2031
   141
by (rtac rtrancl_refl 1);
nipkow@1707
   142
nipkow@1707
   143
(* ASSIGN *)
nipkow@1973
   144
by (fast_tac (!claset addSIs [r_into_rtrancl]) 1);
nipkow@1707
   145
nipkow@1707
   146
(* SEMI *)
nipkow@1973
   147
by (fast_tac (!claset addIs [my_lemma1]) 1);
nipkow@1707
   148
nipkow@1707
   149
(* IF *)
nipkow@1973
   150
by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
nipkow@1973
   151
by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
nipkow@1707
   152
nipkow@1707
   153
(* WHILE *)
nipkow@1973
   154
by (fast_tac (!claset addSIs [r_into_rtrancl]) 1);
nipkow@1973
   155
by (fast_tac (!claset addIs [rtrancl_into_rtrancl2,my_lemma1]) 1);
nipkow@1707
   156
paulson@1730
   157
qed "evalc_impl_evalc1";
nipkow@1707
   158
nipkow@1707
   159
(* The opposite direction is based on a Coq proof done by Ranan Fraer and
nipkow@1707
   160
   Yves Bertot. The following sketch is from an email by Ranan Fraer.
nipkow@1707
   161
*)
nipkow@1707
   162
(*
nipkow@1707
   163
First we've broke it into 2 lemmas:
nipkow@1707
   164
nipkow@1707
   165
Lemma 1
nipkow@1707
   166
((c,s) --> (SKIP,t)) => (<c,s> -c-> t)
nipkow@1707
   167
nipkow@1707
   168
This is a quick one, dealing with the cases skip, assignment
nipkow@1707
   169
and while_false.
nipkow@1707
   170
nipkow@1707
   171
Lemma 2
nipkow@1707
   172
((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t
nipkow@1707
   173
  => 
nipkow@1707
   174
<c,s> -c-> t
nipkow@1707
   175
nipkow@1707
   176
This is proved by rule induction on the  -*-> relation
nipkow@1707
   177
and the induction step makes use of a third lemma: 
nipkow@1707
   178
nipkow@1707
   179
Lemma 3
nipkow@1707
   180
((c,s) --> (c',s')) /\ <c',s'> -c'-> t
nipkow@1707
   181
  => 
nipkow@1707
   182
<c,s> -c-> t
nipkow@1707
   183
nipkow@1707
   184
This captures the essence of the proof, as it shows that <c',s'> 
nipkow@1707
   185
behaves as the continuation of <c,s> with respect to the natural
nipkow@1707
   186
semantics.
nipkow@1707
   187
The proof of Lemma 3 goes by rule induction on the --> relation,
nipkow@1707
   188
dealing with the cases sequence1, sequence2, if_true, if_false and
nipkow@1707
   189
while_true. In particular in the case (sequence1) we make use again
nipkow@1707
   190
of Lemma 1.
nipkow@1707
   191
*)
nipkow@1707
   192
nipkow@1707
   193
paulson@1730
   194
goal Transition.thy 
paulson@1730
   195
  "!!c s. ((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
paulson@2031
   196
by (etac evalc1.induct 1);
nipkow@1973
   197
auto();
paulson@1730
   198
qed_spec_mp "FB_lemma3";
nipkow@1707
   199
nipkow@1707
   200
val [major] = goal Transition.thy
nipkow@1707
   201
  "(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t";
paulson@2031
   202
by (rtac (major RS rtrancl_induct2) 1);
paulson@2031
   203
by (Fast_tac 1);
paulson@2031
   204
by (fast_tac (!claset addIs [FB_lemma3] addbefore (split_all_tac 1)) 1);
nipkow@1707
   205
qed_spec_mp "FB_lemma2";
nipkow@1707
   206
nipkow@1707
   207
goal Transition.thy "!!c. (c,s) -*-> (SKIP,t) ==> <c,s> -c-> t";
nipkow@1973
   208
by (fast_tac (!claset addEs [FB_lemma2]) 1);
nipkow@1707
   209
qed "evalc1_impl_evalc";