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