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