src/HOLCF/IOA/NTP/Impl.thy
changeset 19739 c58ef2aa5430
parent 17244 0b2ff9541727
child 19741 f65265d71426
--- a/src/HOLCF/IOA/NTP/Impl.thy	Sat May 27 19:49:36 2006 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.thy	Sat May 27 21:00:31 2006 +0200
@@ -9,11 +9,9 @@
 imports Sender Receiver Abschannel
 begin
 
-types
-
-'m impl_state
-= "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset"
-(*  sender_state   *  receiver_state   *    srch_state      * rsch_state *)
+types 'm impl_state
+  = "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset"
+  (*  sender_state   *  receiver_state   *    srch_state      * rsch_state *)
 
 
 consts
@@ -29,7 +27,6 @@
  hdr_sum     :: "'m packet multiset => bool => nat"
 
 defs
-
  impl_def:
   "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
 
@@ -71,6 +68,300 @@
 (* Lemma 5.4 *)
  inv4_def: "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
 
-ML {* use_legacy_bindings (the_context ()) *}
+
+subsection {* Invariants *}
+
+declare Let_def [simp] le_SucI [simp]
+
+lemmas impl_ioas =
+  impl_def sender_ioa_def receiver_ioa_def srch_ioa_thm [THEN eq_reflection]
+  rsch_ioa_thm [THEN eq_reflection]
+
+lemmas "transitions" =
+  sender_trans_def receiver_trans_def srch_trans_def rsch_trans_def
+
+
+lemmas [simp] =
+  ioa_triple_proj starts_of_par trans_of_par4 in_sender_asig
+  in_receiver_asig in_srch_asig in_rsch_asig
+
+declare let_weak_cong [cong]
+
+lemma [simp]:
+  "fst(x) = sen(x)"
+  "fst(snd(x)) = rec(x)"
+  "fst(snd(snd(x))) = srch(x)"
+  "snd(snd(snd(x))) = rsch(x)"
+  by (simp_all add: sen_def rec_def srch_def rsch_def)
+
+lemma [simp]:
+  "a:actions(sender_asig)
+  | a:actions(receiver_asig)
+  | a:actions(srch_asig)
+  | a:actions(rsch_asig)"
+  by (induct a) simp_all
+
+declare split_paired_All [simp del]
+
+
+(* Three Simp_sets in different sizes
+----------------------------------------------
+
+1) simpset() does not unfold the transition relations
+2) ss unfolds transition relations
+3) renname_ss unfolds transitions and the abstract channel *)
+
+ML {*
+val ss = simpset() addsimps thms "transitions";
+val rename_ss = ss addsimps thms "unfold_renaming";
+
+val tac     = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if])
+val tac_ren = asm_simp_tac (rename_ss addcongs [conj_cong] addsplits [split_if])
+*}
+
+
+subsubsection {* Invariant 1 *}
+
+lemma inv1: "invariant impl_ioa inv1"
+
+apply (unfold impl_ioas)
+apply (rule invariantI)
+apply (simp add: inv1_def hdr_sum_def srcvd_def ssent_def rsent_def rrcvd_def)
+
+apply (simp (no_asm) del: trans_of_par4 add: imp_conjR inv1_def)
+
+txt {* Split proof in two *}
+apply (rule conjI)
+
+(* First half *)
+apply (simp add: Impl.inv1_def split del: split_if)
+apply (induct_tac a)
+
+apply (tactic "EVERY1[tac, tac, tac, tac]")
+apply (tactic "tac 1")
+apply (tactic "tac_ren 1")
+
+txt {* 5 + 1 *}
+
+apply (tactic "tac 1")
+apply (tactic "tac_ren 1")
+
+txt {* 4 + 1 *}
+apply (tactic {* EVERY1[tac, tac, tac, tac] *})
+
+
+txt {* Now the other half *}
+apply (simp add: Impl.inv1_def split del: split_if)
+apply (induct_tac a)
+apply (tactic "EVERY1 [tac, tac]")
+
+txt {* detour 1 *}
+apply (tactic "tac 1")
+apply (tactic "tac_ren 1")
+apply (rule impI)
+apply (erule conjE)+
+apply (simp (no_asm_simp) add: hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
+  split add: split_if)
+txt {* detour 2 *}
+apply (tactic "tac 1")
+apply (tactic "tac_ren 1")
+apply (rule impI)
+apply (erule conjE)+
+apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
+  Multiset.delm_nonempty_def split add: split_if)
+apply (rule allI)
+apply (rule conjI)
+apply (rule impI)
+apply hypsubst
+apply (rule pred_suc [THEN iffD1])
+apply (drule less_le_trans)
+apply (cut_tac eq_packet_imp_eq_hdr [unfolded Packet.hdr_def, THEN countm_props])
+apply assumption
+apply assumption
+
+apply (rule countm_done_delm [THEN mp, symmetric])
+apply (rule refl)
+apply (simp (no_asm_simp) add: Multiset.count_def)
+
+apply (rule impI)
+apply (simp add: neg_flip)
+apply hypsubst
+apply (rule countm_spurious_delm)
+apply (simp (no_asm))
+
+apply (tactic "EVERY1 [tac, tac, tac, tac, tac, tac]")
+
+done
+
+
+
+subsubsection {* INVARIANT 2 *}
+
+lemma inv2: "invariant impl_ioa inv2"
+
+  apply (rule invariantI1)
+  txt {* Base case *}
+  apply (simp add: inv2_def receiver_projections sender_projections impl_ioas)
+
+  apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
+  apply (induct_tac "a")
+
+  txt {* 10 cases. First 4 are simple, since state doesn't change *}
+
+ML {* val tac2 = asm_full_simp_tac (ss addsimps [thm "inv2_def"]) *}
+
+  txt {* 10 - 7 *}
+  apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
+  txt {* 6 *}
+  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
+                               (thm "inv1" RS invariantE) RS conjunct1] 1 *})
+
+  txt {* 6 - 5 *}
+  apply (tactic "EVERY1 [tac2,tac2]")
+
+  txt {* 4 *}
+  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
+                                (thm "inv1" RS invariantE) RS conjunct1] 1 *})
+  apply (tactic "tac2 1")
+
+  txt {* 3 *}
+  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
+    (thm "inv1" RS invariantE)] 1 *})
+
+  apply (tactic "tac2 1")
+  apply (tactic {* fold_tac [rewrite_rule [thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")] *})
+  apply arith
+
+  txt {* 2 *}
+  apply (tactic "tac2 1")
+  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
+                               (thm "inv1" RS invariantE) RS conjunct1] 1 *})
+  apply (intro strip)
+  apply (erule conjE)+
+  apply simp
+
+  txt {* 1 *}
+  apply (tactic "tac2 1")
+  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
+                               (thm "inv1" RS invariantE) RS conjunct2] 1 *})
+  apply (intro strip)
+  apply (erule conjE)+
+  apply (tactic {* fold_tac  [rewrite_rule[thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")] *})
+  apply simp
+
+  done
+
+
+subsubsection {* INVARIANT 3 *}
+
+lemma inv3: "invariant impl_ioa inv3"
+
+  apply (rule invariantI)
+  txt {* Base case *}
+  apply (simp add: Impl.inv3_def receiver_projections sender_projections impl_ioas)
+
+  apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
+  apply (induct_tac "a")
+
+ML {* val tac3 = asm_full_simp_tac (ss addsimps [thm "inv3_def"]) *}
+
+  txt {* 10 - 8 *}
+
+  apply (tactic "EVERY1[tac3,tac3,tac3]")
+
+  apply (tactic "tac_ren 1")
+  apply (intro strip, (erule conjE)+)
+  apply hypsubst
+  apply (erule exE)
+  apply simp
+
+  txt {* 7 *}
+  apply (tactic "tac3 1")
+  apply (tactic "tac_ren 1")
+  apply force
+
+  txt {* 6 - 3 *}
+
+  apply (tactic "EVERY1[tac3,tac3,tac3,tac3]")
+
+  txt {* 2 *}
+  apply (tactic "asm_full_simp_tac ss 1")
+  apply (simp (no_asm) add: inv3_def)
+  apply (intro strip, (erule conjE)+)
+  apply (rule imp_disjL [THEN iffD1])
+  apply (rule impI)
+  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
+    (thm "inv2" RS invariantE)] 1 *})
+  apply simp
+  apply (erule conjE)+
+  apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and
+    k = "count (rsent (rec s)) (sbit (sen s))" in le_trans)
+  apply (tactic {* forward_tac [rewrite_rule [thm "inv1_def"]
+                                (thm "inv1" RS invariantE) RS conjunct2] 1 *})
+  apply (simp add: hdr_sum_def Multiset.count_def)
+  apply (rule add_le_mono)
+  apply (rule countm_props)
+  apply (simp (no_asm))
+  apply (rule countm_props)
+  apply (simp (no_asm))
+  apply assumption
+
+  txt {* 1 *}
+  apply (tactic "tac3 1")
+  apply (intro strip, (erule conjE)+)
+  apply (rule imp_disjL [THEN iffD1])
+  apply (rule impI)
+  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
+    (thm "inv2" RS invariantE)] 1 *})
+  apply simp
+  done
+
+
+subsubsection {* INVARIANT 4 *}
+
+lemma inv4: "invariant impl_ioa inv4"
+
+  apply (rule invariantI)
+  txt {* Base case *}
+  apply (simp add: Impl.inv4_def receiver_projections sender_projections impl_ioas)
+
+  apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
+  apply (induct_tac "a")
+
+ML {* val tac4 =  asm_full_simp_tac (ss addsimps [thm "inv4_def"]) *}
+
+  txt {* 10 - 2 *}
+
+  apply (tactic "EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]")
+
+  txt {* 2 b *}
+
+  apply (intro strip, (erule conjE)+)
+  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
+                               (thm "inv2" RS invariantE)] 1 *})
+  apply simp
+
+  txt {* 1 *}
+  apply (tactic "tac4 1")
+  apply (intro strip, (erule conjE)+)
+  apply (rule ccontr)
+  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
+                               (thm "inv2" RS invariantE)] 1 *})
+  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv3_def"]
+                               (thm "inv3" RS invariantE)] 1 *})
+  apply simp
+  apply (erule_tac x = "m" in allE)
+  apply simp
+  done
+
+
+text {* rebind them *}
+
+ML_setup {*
+bind_thm ("inv1", rewrite_rule [thm "Impl.inv1_def"] (thm "inv1" RS thm "invariantE"));
+bind_thm ("inv2", rewrite_rule [thm "Impl.inv2_def"] (thm "inv2" RS thm "invariantE"));
+bind_thm ("inv3", rewrite_rule [thm "Impl.inv3_def"] (thm "inv3" RS thm "invariantE"));
+bind_thm ("inv4", rewrite_rule [thm "Impl.inv4_def"] (thm "inv4" RS thm "invariantE"));
+*}
 
 end