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