wneuper/isa: src/HOL/IMP/Transition.ML@b7713108ffd8

     1 (*  Title:      HOL/IMP/Transition.ML

     2     ID:         $Id$

     3     Author:     Tobias Nipkow & Robert Sandner, TUM

     4     Copyright   1996 TUM

     6 Equivalence of Natural and Transition semantics

     7 *)

     9 section "Winskel's Proof";

    11 AddSEs [rel_pow_0_E];

    13 val evalc1_SEs =

    14     map evalc1.mk_cases

    15        ["(SKIP,s) -1-> t",

    16 	"(x:=a,s) -1-> t",

    17 	"(c1;c2, s) -1-> t",

    18 	"(IF b THEN c1 ELSE c2, s) -1-> t",

    19         "(WHILE b DO c, s) -1-> t"];

    21 val evalc1_E = evalc1.mk_cases "(WHILE b DO c,s) -1-> t";

    23 AddSEs evalc1_SEs;

    25 AddIs evalc1.intrs;

    27 Goal "(SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0";

    28 by (etac rel_pow_E2 1);

    29 by (Asm_full_simp_tac 1);

    30 by (Fast_tac 1);

    31 val hlemma = result();

    34 Goal "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \

    35 \              (c;d, s) -*-> (SKIP, u)";

    36 by (induct_tac "n" 1);

    37  by (fast_tac (claset() addIs [rtrancl_into_rtrancl2])1);

    38 by (fast_tac  (claset() addIs [rtrancl_into_rtrancl2]addSDs [rel_pow_Suc_D2])1);

    39 qed_spec_mp "lemma1";

    42 Goal "<c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";

    43 by (etac evalc.induct 1);

    45 (* SKIP *)

    46 by (rtac rtrancl_refl 1);

    48 (* ASSIGN *)

    49 by (fast_tac (claset() addSIs [r_into_rtrancl]) 1);

    51 (* SEMI *)

    52 by (fast_tac (claset() addDs [rtrancl_imp_UN_rel_pow] addIs [lemma1]) 1);

    54 (* IF *)

    55 by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);

    56 by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);

    58 (* WHILE *)

    59 by (fast_tac (claset() addSIs [r_into_rtrancl]) 1);

    60 by (fast_tac (claset() addDs [rtrancl_imp_UN_rel_pow]

    61                         addIs [rtrancl_into_rtrancl2,lemma1]) 1);

    63 qed "evalc_impl_evalc1";

    66 Goal "!c d s u. (c;d,s) -n-> (SKIP,u) --> \

    67 \            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)";

    68 by (induct_tac "n" 1);

    69  (* case n = 0 *)

    70  by (fast_tac (claset() addss simpset()) 1);

    71 (* induction step *)

    72 by (fast_tac (claset() addSIs [le_SucI,le_refl]

    73                      addSDs [rel_pow_Suc_D2]

    74                      addSEs [rel_pow_imp_rtrancl,rtrancl_into_rtrancl2]) 1);

    75 qed_spec_mp "lemma2";

    77 Goal "!s t. (c,s) -*-> (SKIP,t) --> <c,s> -c-> t";

    78 by (induct_tac "c" 1);

    79 by (safe_tac (claset() addSDs [rtrancl_imp_UN_rel_pow]));

    81 (* SKIP *)

    82 by (fast_tac (claset() addSEs [rel_pow_E2]) 1);

    84 (* ASSIGN *)

    85 by (fast_tac (claset() addSDs [hlemma]  addSEs [rel_pow_E2]) 1);

    87 (* SEMI *)

    88 by (fast_tac (claset() addSDs [lemma2,rel_pow_imp_rtrancl]) 1);

    90 (* IF *)

    91 by (etac rel_pow_E2 1);

    92 by (Asm_full_simp_tac 1);

    93 by (fast_tac (claset() addSDs [rel_pow_imp_rtrancl]) 1);

    95 (* WHILE, induction on the length of the computation *)

    96 by (eres_inst_tac [("P","?X -n-> ?Y")] rev_mp 1);

    97 by (res_inst_tac [("x","s")] spec 1);

    98 by (res_inst_tac [("n","n")] less_induct 1);

    99 by (strip_tac 1);

   100 by (etac rel_pow_E2 1);

   101  by (Asm_full_simp_tac 1);

   102 by (etac evalc1_E 1);

   104 (* WhileFalse *)

   105  by (fast_tac (claset() addSDs [hlemma]) 1);

   107 (* WhileTrue *)

   108 by (fast_tac(claset() addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1);

   110 qed_spec_mp "evalc1_impl_evalc";

   113 (**** proof of the equivalence of evalc and evalc1 ****)

   115 Goal "((c, s) -*-> (SKIP, t)) = (<c,s> -c-> t)";

   116 by (fast_tac (HOL_cs addSEs [evalc1_impl_evalc,evalc_impl_evalc1]) 1);

   117 qed "evalc1_eq_evalc";

   120 section "A Proof Without -n->";

   122 Goal "(c1,s1) -*-> (SKIP,s2) ==> \

   123 \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";

   124 by (etac converse_rtrancl_induct2 1);

   125 by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);

   126 by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);

   127 qed_spec_mp "my_lemma1";

   130 Goal "<c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";

   131 by (etac evalc.induct 1);

   133 (* SKIP *)

   134 by (rtac rtrancl_refl 1);

   136 (* ASSIGN *)

   137 by (fast_tac (claset() addSIs [r_into_rtrancl]) 1);

   139 (* SEMI *)

   140 by (fast_tac (claset() addIs [my_lemma1]) 1);

   142 (* IF *)

   143 by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);

   144 by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);

   146 (* WHILE *)

   147 by (fast_tac (claset() addSIs [r_into_rtrancl]) 1);

   148 by (fast_tac (claset() addIs [rtrancl_into_rtrancl2,my_lemma1]) 1);

   150 qed "evalc_impl_evalc1";

   152 (* The opposite direction is based on a Coq proof done by Ranan Fraer and

   153    Yves Bertot. The following sketch is from an email by Ranan Fraer.

   154 *)

   155 (*

   156 First we've broke it into 2 lemmas:

   158 Lemma 1

   159 ((c,s) --> (SKIP,t)) => (<c,s> -c-> t)

   161 This is a quick one, dealing with the cases skip, assignment

   162 and while_false.

   164 Lemma 2

   165 ((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t

   166   =>

   167 <c,s> -c-> t

   169 This is proved by rule induction on the  -*-> relation

   170 and the induction step makes use of a third lemma:

   172 Lemma 3

   173 ((c,s) --> (c',s')) /\ <c',s'> -c'-> t

   174   =>

   175 <c,s> -c-> t

   177 This captures the essence of the proof, as it shows that <c',s'>

   178 behaves as the continuation of <c,s> with respect to the natural

   179 semantics.

   180 The proof of Lemma 3 goes by rule induction on the --> relation,

   181 dealing with the cases sequence1, sequence2, if_true, if_false and

   182 while_true. In particular in the case (sequence1) we make use again

   183 of Lemma 1.

   184 *)

   186 (*Delsimps [update_apply];*)

   187 Goal "((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";

   188 by (etac evalc1.induct 1);

   189 by Auto_tac;

   190 qed_spec_mp "FB_lemma3";

   191 (*Addsimps [update_apply];*)

   193 val [major] = goal Transition.thy

   194   "(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t";

   195 by (rtac (major RS rtrancl_induct2) 1);

   196  by (Fast_tac 1);

   197 by (fast_tac (claset() addIs [FB_lemma3]) 1);

   198 qed_spec_mp "FB_lemma2";

   200 Goal "(c,s) -*-> (SKIP,t) ==> <c,s> -c-> t";

   201 by (fast_tac (claset() addEs [FB_lemma2]) 1);

   202 qed "evalc1_impl_evalc";

   205 section "The proof in Nielson and Nielson";

   207 (* The more precise n=i1+i2+1 is proved by the same script but complicates

   208    life further down, where i1,i2 < n is needed.

   209 *)

   210 Goal "!c1 s. (c1;c2,s) -n-> (SKIP,t) --> \

   211 \     (? i1 i2 u. (c1,s) -i1-> (SKIP,u) & (c2,u) -i2-> (SKIP,t) & i1<n & i2<n)";

   212 by(induct_tac "n" 1);

   213  by (fast_tac (claset() addSDs [hlemma]) 1);

   214 by(fast_tac (claset() addSIs [rel_pow_0_I,rel_pow_Suc_I2]

   215                       addSDs [rel_pow_Suc_D2] addss simpset()) 1);

   216 qed_spec_mp "comp_decomp_lemma";

   218 Goal "!c s t. (c,s) -n-> (SKIP,t) --> <c,s> -c-> t";

   219 by(res_inst_tac [("n","n")] less_induct 1);

   220 by(Clarify_tac 1);

   221 be rel_pow_E2 1;

   222  by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1);

   223 by(exhaust_tac "c" 1);

   224     by (fast_tac (claset() addSDs [hlemma]) 1);

   225    by(Blast_tac 1);

   226   by(blast_tac (claset() addSDs [rel_pow_Suc_I2 RS comp_decomp_lemma]) 1);

   227  by(Blast_tac 1);

   228 by(Blast_tac 1);

   229 qed_spec_mp "evalc1_impl_evalc";

author	nipkow
	Fri, 12 Nov 1999 17:45:36 +0100
changeset 8016	b7713108ffd8
parent 6141	a6922171b396
child 8064	357652a08ee0
permissions	-rw-r--r--