src/HOL/IMP/Transition.ML
author nipkow
Mon Apr 29 20:15:33 1996 +0200 (1996-04-29)
changeset 1701 a26fbeaaaabd
parent 1700 afd3b60660db
child 1707 e1a64a6c454d
permissions -rw-r--r--
Streamlined syntax: -(n)-> is now -n->.
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@1700
    11
val relpow_cs = rel_cs addSEs [rel_pow_0_E];
nipkow@1700
    12
nipkow@1700
    13
val evalc1_elim_cases = map (evalc1.mk_cases com.simps)
nipkow@1700
    14
   ["(SKIP,s) -1-> t", "(x:=a,s) -1-> t", "(c1;c2, s) -1-> t",
nipkow@1700
    15
    "(IF b THEN c1 ELSE c2, s) -1-> t", "(WHILE b DO c,s) -1-> t"];
nipkow@1700
    16
nipkow@1700
    17
val evalc1_cs = relpow_cs addIs (evalc.intrs@evalc1.intrs);
nipkow@1700
    18
nipkow@1701
    19
goal Transition.thy "!!c. (c,s) -0-> (SKIP,u) ==> c = SKIP & s = u";
nipkow@1700
    20
by(fast_tac evalc1_cs 1);
nipkow@1700
    21
val hlemma1 = result();
nipkow@1700
    22
nipkow@1701
    23
goal Transition.thy "!!s. (SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0";
nipkow@1700
    24
be rel_pow_E2 1;
nipkow@1700
    25
by (Asm_full_simp_tac 1);
nipkow@1700
    26
by (eresolve_tac evalc1_elim_cases 1);
nipkow@1700
    27
val hlemma2 = result();
nipkow@1700
    28
nipkow@1700
    29
nipkow@1700
    30
goal Transition.thy
nipkow@1701
    31
  "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
nipkow@1700
    32
\              (c;d, s) -*-> (SKIP, u)";
nipkow@1700
    33
by(nat_ind_tac "n" 1);
nipkow@1700
    34
 (* case n = 0 *)
nipkow@1700
    35
 by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2])1);
nipkow@1700
    36
(* induction step *)
nipkow@1700
    37
by (safe_tac (HOL_cs addSDs [rel_pow_Suc_D2]));
nipkow@1700
    38
by(split_all_tac 1);
nipkow@1700
    39
by(fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
nipkow@1700
    40
qed_spec_mp "lemma1";
nipkow@1700
    41
nipkow@1700
    42
nipkow@1700
    43
goal Transition.thy "!c s s1. <c,s> -c-> s1 --> (c,s) -*-> (SKIP,s1)";
nipkow@1700
    44
br evalc.mutual_induct 1;
nipkow@1700
    45
nipkow@1700
    46
(* SKIP *)
nipkow@1700
    47
br rtrancl_refl 1;
nipkow@1700
    48
nipkow@1700
    49
(* ASSIGN *)
nipkow@1700
    50
by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1);
nipkow@1700
    51
nipkow@1700
    52
(* SEMI *)
nipkow@1700
    53
by (fast_tac (set_cs addDs [rtrancl_imp_UN_rel_pow] addIs [lemma1]) 1);
nipkow@1700
    54
nipkow@1700
    55
(* IF *)
nipkow@1700
    56
by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
nipkow@1700
    57
by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2]) 1);
nipkow@1700
    58
nipkow@1700
    59
(* WHILE *)
nipkow@1700
    60
by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1);
nipkow@1700
    61
by (fast_tac (evalc1_cs addDs [rtrancl_imp_UN_rel_pow]
nipkow@1700
    62
                        addIs [rtrancl_into_rtrancl2,lemma1]) 1);
nipkow@1700
    63
nipkow@1700
    64
qed_spec_mp "evalc_impl_evalc1";
nipkow@1700
    65
nipkow@1700
    66
nipkow@1700
    67
goal Transition.thy
nipkow@1701
    68
  "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
nipkow@1701
    69
\            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)";
nipkow@1700
    70
by(nat_ind_tac "n" 1);
nipkow@1700
    71
 (* case n = 0 *)
nipkow@1700
    72
 by (fast_tac (HOL_cs addSDs [hlemma1] addss !simpset) 1);
nipkow@1700
    73
(* induction step *)
nipkow@1700
    74
by (fast_tac (HOL_cs addSIs [rtrancl_refl,le_SucI,le_refl]
nipkow@1700
    75
                     addSDs [rel_pow_Suc_D2]
nipkow@1700
    76
                     addSEs (evalc1_elim_cases@
nipkow@1700
    77
                             [rel_pow_imp_rtrancl,rtrancl_into_rtrancl2])) 1);
nipkow@1700
    78
qed_spec_mp "lemma2";
nipkow@1700
    79
nipkow@1700
    80
goal Transition.thy "!s t. (c,s) -*-> (SKIP,t) --> <c,s> -c-> t";
nipkow@1700
    81
by (com.induct_tac "c" 1);
nipkow@1700
    82
by (safe_tac (evalc1_cs addSDs [rtrancl_imp_UN_rel_pow]));
nipkow@1700
    83
nipkow@1700
    84
(* SKIP *)
nipkow@1700
    85
by (fast_tac (evalc1_cs addSEs rel_pow_E2::evalc1_elim_cases) 1);
nipkow@1700
    86
nipkow@1700
    87
(* ASSIGN *)
nipkow@1700
    88
by (fast_tac (evalc1_cs addSDs [hlemma2]
nipkow@1700
    89
                        addSEs rel_pow_E2::evalc1_elim_cases
nipkow@1700
    90
                        addss !simpset) 1);
nipkow@1700
    91
nipkow@1700
    92
(* SEMI *)
nipkow@1700
    93
by (fast_tac (evalc1_cs addSDs [lemma2,rel_pow_imp_rtrancl]) 1);
nipkow@1700
    94
nipkow@1700
    95
(* IF *)
nipkow@1700
    96
be rel_pow_E2 1;
nipkow@1700
    97
by (Asm_full_simp_tac 1);
nipkow@1700
    98
by (fast_tac (evalc1_cs addSDs[rel_pow_imp_rtrancl]addEs evalc1_elim_cases) 1);
nipkow@1700
    99
nipkow@1700
   100
(* WHILE, induction on the length of the computation *)
nipkow@1700
   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);
nipkow@1700
   104
by(res_inst_tac [("n","n")] less_induct 1);
nipkow@1700
   105
by (strip_tac 1);
nipkow@1700
   106
be rel_pow_E2 1;
nipkow@1700
   107
 by (Asm_full_simp_tac 1);
nipkow@1700
   108
by (eresolve_tac evalc1_elim_cases 1);
nipkow@1700
   109
nipkow@1700
   110
(* WhileFalse *)
nipkow@1700
   111
 by (fast_tac (evalc1_cs addSDs [hlemma2]) 1);
nipkow@1700
   112
nipkow@1700
   113
(* WhileTrue *)
nipkow@1700
   114
by(fast_tac(evalc1_cs 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";