src/HOLCF/IOA/NTP/Impl.thy
changeset 27361 24ec32bee347
parent 27355 a9d738d20174
child 28265 7e14443f2dd6
--- a/src/HOLCF/IOA/NTP/Impl.thy	Wed Jun 25 18:23:50 2008 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.thy	Wed Jun 25 21:25:51 2008 +0200
@@ -14,39 +14,29 @@
   (*  sender_state   *  receiver_state   *    srch_state      * rsch_state *)
 
 
-consts
- impl_ioa    :: "('m action, 'm impl_state)ioa"
- sen         :: "'m impl_state => 'm sender_state"
- rec         :: "'m impl_state => 'm receiver_state"
- srch        :: "'m impl_state => 'm packet multiset"
- rsch        :: "'m impl_state => bool multiset"
- inv1  :: "'m impl_state => bool"
- inv2  :: "'m impl_state => bool"
- inv3  :: "'m impl_state => bool"
- inv4  :: "'m impl_state => bool"
- hdr_sum     :: "'m packet multiset => bool => nat"
+definition
+  impl_ioa :: "('m action, 'm impl_state)ioa" where
+  impl_def: "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
 
-defs
- impl_def:
-  "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
+definition sen :: "'m impl_state => 'm sender_state" where "sen = fst"
+definition rec :: "'m impl_state => 'm receiver_state" where "rec = fst o snd"
+definition srch :: "'m impl_state => 'm packet multiset" where "srch = fst o snd o snd"
+definition rsch :: "'m impl_state => bool multiset" where "rsch = snd o snd o snd"
 
- sen_def:   "sen == fst"
- rec_def:   "rec == fst o snd"
- srch_def: "srch == fst o snd o snd"
- rsch_def: "rsch == snd o snd o snd"
-
-hdr_sum_def:
-   "hdr_sum M b == countm M (%pkt. hdr(pkt) = b)"
+definition
+  hdr_sum :: "'m packet multiset => bool => nat" where
+  "hdr_sum M b == countm M (%pkt. hdr(pkt) = b)"
 
 (* Lemma 5.1 *)
-inv1_def:
+definition
   "inv1(s) ==
      (!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b)
    & (!b. count (ssent(sen s)) b
           = hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)"
 
 (* Lemma 5.2 *)
- inv2_def: "inv2(s) ==
+definition
+  "inv2(s) ==
   (rbit(rec(s)) = sbit(sen(s)) &
    ssending(sen(s)) &
    count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) &
@@ -58,7 +48,8 @@
    count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))"
 
 (* Lemma 5.3 *)
- inv3_def: "inv3(s) ==
+definition
+  "inv3(s) ==
    rbit(rec(s)) = sbit(sen(s))
    --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s)))
         -->  count (rrcvd(rec s)) (sbit(sen(s)),m)
@@ -66,7 +57,7 @@
             <= count (rsent(rec s)) (~sbit(sen s)))"
 
 (* Lemma 5.4 *)
- inv4_def: "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
+definition "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
 
 
 subsection {* Invariants *}
@@ -229,7 +220,8 @@
     (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
 
   apply (tactic "tac2 1")
-  apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
+  apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}]
+    (@{thm Impl.hdr_sum_def})] *})
   apply arith
 
   txt {* 2 *}