src/HOLCF/IOA/NTP/Impl.thy
author wenzelm
Sun, 28 May 2006 19:54:20 +0200
changeset 19741 f65265d71426
parent 19739 c58ef2aa5430
child 24327 a207114007c6
permissions -rw-r--r--
removed legacy ML scripts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     1
(*  Title:      HOL/IOA/NTP/Impl.thy
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     2
    ID:         $Id$
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     3
    Author:     Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     4
*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     5
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     6
header {* The implementation *}
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     7
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     8
theory Impl
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     9
imports Sender Receiver Abschannel
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    10
begin
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    11
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    12
types 'm impl_state
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    13
  = "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    14
  (*  sender_state   *  receiver_state   *    srch_state      * rsch_state *)
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    15
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    16
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    17
consts
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    18
 impl_ioa    :: "('m action, 'm impl_state)ioa"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    19
 sen         :: "'m impl_state => 'm sender_state"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    20
 rec         :: "'m impl_state => 'm receiver_state"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    21
 srch        :: "'m impl_state => 'm packet multiset"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    22
 rsch        :: "'m impl_state => bool multiset"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    23
 inv1  :: "'m impl_state => bool"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    24
 inv2  :: "'m impl_state => bool"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    25
 inv3  :: "'m impl_state => bool"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    26
 inv4  :: "'m impl_state => bool"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    27
 hdr_sum     :: "'m packet multiset => bool => nat"
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    28
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    29
defs
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    30
 impl_def:
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    31
  "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    32
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    33
 sen_def:   "sen == fst"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    34
 rec_def:   "rec == fst o snd"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    35
 srch_def: "srch == fst o snd o snd"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    36
 rsch_def: "rsch == snd o snd o snd"
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    37
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    38
hdr_sum_def:
3852
e694c660055b fixed dots;
wenzelm
parents: 3073
diff changeset
    39
   "hdr_sum M b == countm M (%pkt. hdr(pkt) = b)"
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    40
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    41
(* Lemma 5.1 *)
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    42
inv1_def:
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    43
  "inv1(s) ==
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    44
     (!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b)
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    45
   & (!b. count (ssent(sen s)) b
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    46
          = hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    47
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    48
(* Lemma 5.2 *)
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    49
 inv2_def: "inv2(s) ==
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    50
  (rbit(rec(s)) = sbit(sen(s)) &
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    51
   ssending(sen(s)) &
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    52
   count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) &
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    53
   count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)))
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    54
   |
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    55
  (rbit(rec(s)) = (~sbit(sen(s))) &
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    56
   rsending(rec(s)) &
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    57
   count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)) &
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    58
   count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    59
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    60
(* Lemma 5.3 *)
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    61
 inv3_def: "inv3(s) ==
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    62
   rbit(rec(s)) = sbit(sen(s))
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    63
   --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s)))
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    64
        -->  count (rrcvd(rec s)) (sbit(sen(s)),m)
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    65
             + count (srch s) (sbit(sen(s)),m)
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    66
            <= count (rsent(rec s)) (~sbit(sen s)))"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    67
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    68
(* Lemma 5.4 *)
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    69
 inv4_def: "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    70
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    71
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    72
subsection {* Invariants *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    73
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    74
declare Let_def [simp] le_SucI [simp]
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    75
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    76
lemmas impl_ioas =
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    77
  impl_def sender_ioa_def receiver_ioa_def srch_ioa_thm [THEN eq_reflection]
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    78
  rsch_ioa_thm [THEN eq_reflection]
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    79
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    80
lemmas "transitions" =
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    81
  sender_trans_def receiver_trans_def srch_trans_def rsch_trans_def
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    82
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    83
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    84
lemmas [simp] =
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    85
  ioa_triple_proj starts_of_par trans_of_par4 in_sender_asig
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    86
  in_receiver_asig in_srch_asig in_rsch_asig
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    87
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    88
declare let_weak_cong [cong]
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    89
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    90
lemma [simp]:
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    91
  "fst(x) = sen(x)"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    92
  "fst(snd(x)) = rec(x)"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    93
  "fst(snd(snd(x))) = srch(x)"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    94
  "snd(snd(snd(x))) = rsch(x)"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    95
  by (simp_all add: sen_def rec_def srch_def rsch_def)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    96
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    97
lemma [simp]:
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    98
  "a:actions(sender_asig)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    99
  | a:actions(receiver_asig)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   100
  | a:actions(srch_asig)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   101
  | a:actions(rsch_asig)"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   102
  by (induct a) simp_all
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   103
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   104
declare split_paired_All [simp del]
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   105
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   106
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   107
(* Three Simp_sets in different sizes
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   108
----------------------------------------------
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   109
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   110
1) simpset() does not unfold the transition relations
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   111
2) ss unfolds transition relations
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   112
3) renname_ss unfolds transitions and the abstract channel *)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   113
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   114
ML {*
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   115
val ss = simpset() addsimps thms "transitions";
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   116
val rename_ss = ss addsimps thms "unfold_renaming";
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   117
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   118
val tac     = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if])
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   119
val tac_ren = asm_simp_tac (rename_ss addcongs [conj_cong] addsplits [split_if])
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   120
*}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   121
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   122
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   123
subsubsection {* Invariant 1 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   124
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   125
lemma inv1: "invariant impl_ioa inv1"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   126
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   127
apply (unfold impl_ioas)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   128
apply (rule invariantI)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   129
apply (simp add: inv1_def hdr_sum_def srcvd_def ssent_def rsent_def rrcvd_def)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   130
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   131
apply (simp (no_asm) del: trans_of_par4 add: imp_conjR inv1_def)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   132
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   133
txt {* Split proof in two *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   134
apply (rule conjI)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   135
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   136
(* First half *)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   137
apply (simp add: Impl.inv1_def split del: split_if)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   138
apply (induct_tac a)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   139
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   140
apply (tactic "EVERY1[tac, tac, tac, tac]")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   141
apply (tactic "tac 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   142
apply (tactic "tac_ren 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   143
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   144
txt {* 5 + 1 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   145
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   146
apply (tactic "tac 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   147
apply (tactic "tac_ren 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   148
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   149
txt {* 4 + 1 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   150
apply (tactic {* EVERY1[tac, tac, tac, tac] *})
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   151
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   152
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   153
txt {* Now the other half *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   154
apply (simp add: Impl.inv1_def split del: split_if)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   155
apply (induct_tac a)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   156
apply (tactic "EVERY1 [tac, tac]")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   157
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   158
txt {* detour 1 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   159
apply (tactic "tac 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   160
apply (tactic "tac_ren 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   161
apply (rule impI)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   162
apply (erule conjE)+
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   163
apply (simp (no_asm_simp) add: hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   164
  split add: split_if)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   165
txt {* detour 2 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   166
apply (tactic "tac 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   167
apply (tactic "tac_ren 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   168
apply (rule impI)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   169
apply (erule conjE)+
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   170
apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   171
  Multiset.delm_nonempty_def split add: split_if)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   172
apply (rule allI)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   173
apply (rule conjI)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   174
apply (rule impI)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   175
apply hypsubst
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   176
apply (rule pred_suc [THEN iffD1])
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   177
apply (drule less_le_trans)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   178
apply (cut_tac eq_packet_imp_eq_hdr [unfolded Packet.hdr_def, THEN countm_props])
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   179
apply assumption
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   180
apply assumption
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   181
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   182
apply (rule countm_done_delm [THEN mp, symmetric])
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   183
apply (rule refl)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   184
apply (simp (no_asm_simp) add: Multiset.count_def)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   185
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   186
apply (rule impI)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   187
apply (simp add: neg_flip)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   188
apply hypsubst
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   189
apply (rule countm_spurious_delm)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   190
apply (simp (no_asm))
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   191
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   192
apply (tactic "EVERY1 [tac, tac, tac, tac, tac, tac]")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   193
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   194
done
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   195
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   196
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   197
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   198
subsubsection {* INVARIANT 2 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   199
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   200
lemma inv2: "invariant impl_ioa inv2"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   201
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   202
  apply (rule invariantI1)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   203
  txt {* Base case *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   204
  apply (simp add: inv2_def receiver_projections sender_projections impl_ioas)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   205
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   206
  apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   207
  apply (induct_tac "a")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   208
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   209
  txt {* 10 cases. First 4 are simple, since state doesn't change *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   210
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   211
ML {* val tac2 = asm_full_simp_tac (ss addsimps [thm "inv2_def"]) *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   212
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   213
  txt {* 10 - 7 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   214
  apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   215
  txt {* 6 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   216
  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19739
diff changeset
   217
                               (thm "inv1" RS thm "invariantE") RS conjunct1] 1 *})
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   218
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   219
  txt {* 6 - 5 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   220
  apply (tactic "EVERY1 [tac2,tac2]")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   221
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   222
  txt {* 4 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   223
  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19739
diff changeset
   224
                                (thm "inv1" RS thm "invariantE") RS conjunct1] 1 *})
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   225
  apply (tactic "tac2 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   226
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   227
  txt {* 3 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   228
  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19739
diff changeset
   229
    (thm "inv1" RS thm "invariantE")] 1 *})
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   230
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   231
  apply (tactic "tac2 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   232
  apply (tactic {* fold_tac [rewrite_rule [thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")] *})
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   233
  apply arith
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   234
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   235
  txt {* 2 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   236
  apply (tactic "tac2 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   237
  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19739
diff changeset
   238
                               (thm "inv1" RS thm "invariantE") RS conjunct1] 1 *})
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   239
  apply (intro strip)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   240
  apply (erule conjE)+
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   241
  apply simp
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   242
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   243
  txt {* 1 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   244
  apply (tactic "tac2 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   245
  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19739
diff changeset
   246
                               (thm "inv1" RS thm "invariantE") RS conjunct2] 1 *})
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   247
  apply (intro strip)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   248
  apply (erule conjE)+
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   249
  apply (tactic {* fold_tac  [rewrite_rule[thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")] *})
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   250
  apply simp
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   251
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   252
  done
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   253
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   254
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   255
subsubsection {* INVARIANT 3 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   256
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   257
lemma inv3: "invariant impl_ioa inv3"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   258
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   259
  apply (rule invariantI)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   260
  txt {* Base case *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   261
  apply (simp add: Impl.inv3_def receiver_projections sender_projections impl_ioas)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   262
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   263
  apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   264
  apply (induct_tac "a")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   265
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   266
ML {* val tac3 = asm_full_simp_tac (ss addsimps [thm "inv3_def"]) *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   267
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   268
  txt {* 10 - 8 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   269
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   270
  apply (tactic "EVERY1[tac3,tac3,tac3]")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   271
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   272
  apply (tactic "tac_ren 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   273
  apply (intro strip, (erule conjE)+)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   274
  apply hypsubst
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   275
  apply (erule exE)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   276
  apply simp
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   277
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   278
  txt {* 7 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   279
  apply (tactic "tac3 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   280
  apply (tactic "tac_ren 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   281
  apply force
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   282
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   283
  txt {* 6 - 3 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   284
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   285
  apply (tactic "EVERY1[tac3,tac3,tac3,tac3]")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   286
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   287
  txt {* 2 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   288
  apply (tactic "asm_full_simp_tac ss 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   289
  apply (simp (no_asm) add: inv3_def)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   290
  apply (intro strip, (erule conjE)+)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   291
  apply (rule imp_disjL [THEN iffD1])
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   292
  apply (rule impI)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   293
  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19739
diff changeset
   294
    (thm "inv2" RS thm "invariantE")] 1 *})
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   295
  apply simp
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   296
  apply (erule conjE)+
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   297
  apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   298
    k = "count (rsent (rec s)) (sbit (sen s))" in le_trans)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   299
  apply (tactic {* forward_tac [rewrite_rule [thm "inv1_def"]
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19739
diff changeset
   300
                                (thm "inv1" RS thm "invariantE") RS conjunct2] 1 *})
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   301
  apply (simp add: hdr_sum_def Multiset.count_def)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   302
  apply (rule add_le_mono)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   303
  apply (rule countm_props)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   304
  apply (simp (no_asm))
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   305
  apply (rule countm_props)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   306
  apply (simp (no_asm))
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   307
  apply assumption
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   308
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   309
  txt {* 1 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   310
  apply (tactic "tac3 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   311
  apply (intro strip, (erule conjE)+)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   312
  apply (rule imp_disjL [THEN iffD1])
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   313
  apply (rule impI)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   314
  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19739
diff changeset
   315
    (thm "inv2" RS thm "invariantE")] 1 *})
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   316
  apply simp
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   317
  done
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   318
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   319
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   320
subsubsection {* INVARIANT 4 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   321
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   322
lemma inv4: "invariant impl_ioa inv4"
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   323
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   324
  apply (rule invariantI)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   325
  txt {* Base case *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   326
  apply (simp add: Impl.inv4_def receiver_projections sender_projections impl_ioas)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   327
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   328
  apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   329
  apply (induct_tac "a")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   330
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   331
ML {* val tac4 =  asm_full_simp_tac (ss addsimps [thm "inv4_def"]) *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   332
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   333
  txt {* 10 - 2 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   334
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   335
  apply (tactic "EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   336
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   337
  txt {* 2 b *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   338
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   339
  apply (intro strip, (erule conjE)+)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   340
  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19739
diff changeset
   341
                               (thm "inv2" RS thm "invariantE")] 1 *})
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   342
  apply simp
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   343
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   344
  txt {* 1 *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   345
  apply (tactic "tac4 1")
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   346
  apply (intro strip, (erule conjE)+)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   347
  apply (rule ccontr)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   348
  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19739
diff changeset
   349
                               (thm "inv2" RS thm "invariantE")] 1 *})
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   350
  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv3_def"]
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19739
diff changeset
   351
                               (thm "inv3" RS thm "invariantE")] 1 *})
19739
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   352
  apply simp
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   353
  apply (erule_tac x = "m" in allE)
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   354
  apply simp
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   355
  done
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   356
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   357
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   358
text {* rebind them *}
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   359
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   360
ML_setup {*
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   361
bind_thm ("inv1", rewrite_rule [thm "Impl.inv1_def"] (thm "inv1" RS thm "invariantE"));
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   362
bind_thm ("inv2", rewrite_rule [thm "Impl.inv2_def"] (thm "inv2" RS thm "invariantE"));
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   363
bind_thm ("inv3", rewrite_rule [thm "Impl.inv3_def"] (thm "inv3" RS thm "invariantE"));
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   364
bind_thm ("inv4", rewrite_rule [thm "Impl.inv4_def"] (thm "inv4" RS thm "invariantE"));
c58ef2aa5430 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   365
*}
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   366
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   367
end