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