src/HOLCF/IOA/NTP/Impl.ML
author nipkow
Thu, 07 Jul 2005 12:42:21 +0200
changeset 16734 2c76db916c51
parent 15408 6001135caa91
child 17244 0b2ff9541727
permissions -rw-r--r--
linear arithmetic is more powerful now
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.ML
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
12218
wenzelm
parents: 9636
diff changeset
     5
The implementation --- Invariants.
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     6
*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     7
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     8
8741
61bc5ed22b62 removal of less_SucI, le_SucI from default simpset
paulson
parents: 7322
diff changeset
     9
Addsimps [Let_def, le_SucI];
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    10
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    11
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    12
open Abschannel Impl;
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    13
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    14
val impl_ioas =
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    15
  [Impl.impl_def,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    16
   Sender.sender_ioa_def, 
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    17
   Receiver.receiver_ioa_def, 
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    18
   srch_ioa_thm RS eq_reflection,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    19
   rsch_ioa_thm RS eq_reflection];
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    20
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    21
val transitions = [Sender.sender_trans_def, Receiver.receiver_trans_def,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    22
                   srch_trans_def, rsch_trans_def];
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    23
 
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    24
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    25
Addsimps [ioa_triple_proj, starts_of_par, trans_of_par4,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    26
          in_sender_asig, in_receiver_asig, in_srch_asig,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    27
          in_rsch_asig];
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    28
Addcongs [let_weak_cong];
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    29
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    30
Goal
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    31
  "fst(x) = sen(x)            & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    32
\  fst(snd(x)) = rec(x)       & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    33
\  fst(snd(snd(x))) = srch(x) & \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    34
\  snd(snd(snd(x))) = rsch(x)";
4423
a129b817b58a expandshort;
wenzelm
parents: 4377
diff changeset
    35
by (simp_tac (simpset() addsimps
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    36
             [sen_def,rec_def,srch_def,rsch_def]) 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    37
Addsimps [result()];
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    38
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    39
Goal "a:actions(sender_asig)   \
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    40
\            | a:actions(receiver_asig) \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    41
\            | a:actions(srch_asig)     \
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    42
\            | a:actions(rsch_asig)";
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5068
diff changeset
    43
  by (induct_tac "a" 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4377
diff changeset
    44
  by (ALLGOALS (Simp_tac));
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    45
Addsimps [result()];
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    46
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    47
Delsimps [split_paired_All];
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    48
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
(* Three Simp_sets in different sizes 
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    51
----------------------------------------------
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    52
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    53
1) simpset() does not unfold the transition relations 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    54
2) ss unfolds transition relations 
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    55
3) renname_ss unfolds transitions and the abstract channel *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    56
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    57
6918
63c9df6b5c4b Now if_weak_cong is a standard congruence rule
paulson
parents: 6129
diff changeset
    58
val ss = (simpset() addsimps transitions);     
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    59
val rename_ss = (ss addsimps unfold_renaming);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    60
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4731
diff changeset
    61
val tac     = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if]);
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4731
diff changeset
    62
val tac_ren = asm_simp_tac (rename_ss addcongs [conj_cong] addsplits [split_if]);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    63
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    64
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    65
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    66
(* INVARIANT 1 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    67
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    68
Goalw impl_ioas "invariant impl_ioa inv1";
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    69
by (rtac invariantI 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4377
diff changeset
    70
by (asm_full_simp_tac (simpset()
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    71
   addsimps [inv1_def, hdr_sum_def, Sender.srcvd_def,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    72
             Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    73
4423
a129b817b58a expandshort;
wenzelm
parents: 4377
diff changeset
    74
by (simp_tac (simpset() delsimps [trans_of_par4]
15408
6001135caa91 tidied; removed references to HOL theories
paulson
parents: 14981
diff changeset
    75
                addsimps [imp_conjR,inv1_def]) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    76
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    77
(* Split proof in two *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    78
by (rtac conjI 1); 
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    79
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    80
(* First half *)
4681
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4423
diff changeset
    81
by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4731
diff changeset
    82
                                 delsplits [split_if]) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    83
by (rtac Action.action.induct 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    84
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    85
by (EVERY1[tac, tac, tac, tac]);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    86
by (tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    87
by (tac_ren 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    88
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    89
(* 5 + 1 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    90
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    91
by (tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    92
by (tac_ren 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    93
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    94
(* 4 + 1 *)
4423
a129b817b58a expandshort;
wenzelm
parents: 4377
diff changeset
    95
by (EVERY1[tac, tac, tac, tac]);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    96
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    97
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    98
(* Now the other half *)
4681
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4423
diff changeset
    99
by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4731
diff changeset
   100
                                 delsplits [split_if]) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   101
by (rtac Action.action.induct 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4377
diff changeset
   102
by (EVERY1[tac, tac]);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   103
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   104
(* detour 1 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   105
by (tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   106
by (tac_ren 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   107
by (rtac impI 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   108
by (REPEAT (etac conjE 1));
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
   109
by (asm_simp_tac (simpset() addsimps [hdr_sum_def, Multiset.count_def,
4377
2cba48b0f1c4 Cleaned up arithmetic mess.
nipkow
parents: 4098
diff changeset
   110
                                      Multiset.countm_nonempty_def]
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4731
diff changeset
   111
                            addsplits [split_if]) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   112
(* detour 2 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   113
by (tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   114
by (tac_ren 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   115
by (rtac impI 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   116
by (REPEAT (etac conjE 1));
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
   117
by (asm_full_simp_tac (simpset() addsimps [Impl.hdr_sum_def, 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   118
                                         Multiset.count_def,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   119
                                         Multiset.countm_nonempty_def,
4377
2cba48b0f1c4 Cleaned up arithmetic mess.
nipkow
parents: 4098
diff changeset
   120
                                         Multiset.delm_nonempty_def]
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4731
diff changeset
   121
                                 addsplits [split_if]) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   122
by (rtac allI 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   123
by (rtac conjI 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   124
by (rtac impI 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   125
by (hyp_subst_tac 1);
4377
2cba48b0f1c4 Cleaned up arithmetic mess.
nipkow
parents: 4098
diff changeset
   126
by (rtac (pred_suc RS iffD1) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   127
by (dtac less_le_trans 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   128
by (cut_facts_tac [rewrite_rule[Packet.hdr_def]
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   129
                   eq_packet_imp_eq_hdr RS countm_props] 1);;
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   130
by (assume_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   131
by (assume_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   132
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   133
by (rtac (countm_done_delm RS mp RS sym) 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   134
by (rtac refl 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
   135
by (asm_simp_tac (simpset() addsimps [Multiset.count_def]) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   136
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   137
by (rtac impI 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
   138
by (asm_full_simp_tac (simpset() addsimps [neg_flip]) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   139
by (hyp_subst_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   140
by (rtac countm_spurious_delm 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   141
by (Simp_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   142
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   143
by (EVERY1[tac, tac, tac, tac, tac, tac]);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   144
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   145
qed "inv1";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   146
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   147
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   148
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   149
(* INVARIANT 2 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   150
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
   151
Goal "invariant impl_ioa inv2";
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   152
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   153
  by (rtac invariantI1 1); 
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   154
  (* Base case *)
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
   155
  by (asm_full_simp_tac (simpset() addsimps (inv2_def ::
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   156
                          (receiver_projections 
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   157
                           @ sender_projections @ impl_ioas)))
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   158
      1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   159
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4731
diff changeset
   160
  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5068
diff changeset
   161
  by (induct_tac "a" 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   162
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   163
  (* 10 cases. First 4 are simple, since state doesn't change *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   164
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   165
val tac2 = asm_full_simp_tac (ss addsimps [inv2_def]);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   166
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   167
  (* 10 - 7 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   168
  by (EVERY1[tac2,tac2,tac2,tac2]);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   169
  (* 6 *)
4423
a129b817b58a expandshort;
wenzelm
parents: 4377
diff changeset
   170
  by (forward_tac [rewrite_rule [Impl.inv1_def]
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   171
                               (inv1 RS invariantE) RS conjunct1] 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   172
  (* 6 - 5 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   173
  by (EVERY1[tac2,tac2]);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   174
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   175
  (* 4 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   176
  by (forward_tac [rewrite_rule [Impl.inv1_def]
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   177
                                (inv1 RS invariantE) RS conjunct1] 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   178
  by (tac2 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   179
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   180
  (* 3 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   181
  by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   182
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   183
  by (tac2 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   184
  by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]);
7322
d16d7ddcc842 isatool expandshort;
wenzelm
parents: 6918
diff changeset
   185
  by (arith_tac 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   186
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   187
  (* 2 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   188
  by (tac2 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4377
diff changeset
   189
  by (forward_tac [rewrite_rule [Impl.inv1_def]
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   190
                               (inv1 RS invariantE) RS conjunct1] 1);
6081
aa97eb904692 Some simplifications.
nipkow
parents: 5274
diff changeset
   191
  by (strip_tac 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   192
  by (REPEAT (etac conjE 1));
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   193
  by (Asm_full_simp_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   194
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   195
  (* 1 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   196
  by (tac2 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4377
diff changeset
   197
  by (forward_tac [rewrite_rule [Impl.inv1_def]
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   198
                               (inv1 RS invariantE) RS conjunct2] 1);
6081
aa97eb904692 Some simplifications.
nipkow
parents: 5274
diff changeset
   199
  by (strip_tac 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   200
  by (REPEAT (etac conjE 1));
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   201
  by (fold_tac  [rewrite_rule[Packet.hdr_def]Impl.hdr_sum_def]);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   202
  by (Asm_full_simp_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   203
qed "inv2";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   204
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   205
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   206
(* INVARIANT 3 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   207
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
   208
Goal "invariant impl_ioa inv3";
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   209
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   210
  by (rtac invariantI 1); 
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   211
  (* Base case *)
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
   212
  by (asm_full_simp_tac (simpset() addsimps 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   213
                    (Impl.inv3_def :: (receiver_projections 
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   214
                                       @ sender_projections @ impl_ioas))) 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   215
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4731
diff changeset
   216
  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5068
diff changeset
   217
  by (induct_tac "a" 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   218
6081
aa97eb904692 Some simplifications.
nipkow
parents: 5274
diff changeset
   219
val tac3 = asm_full_simp_tac (ss addsimps [inv3_def]);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   220
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   221
  (* 10 - 8 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   222
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   223
  by (EVERY1[tac3,tac3,tac3]);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   224
 
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   225
  by (tac_ren 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   226
  by (strip_tac  1 THEN REPEAT (etac conjE 1));
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   227
  by (hyp_subst_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   228
  by (etac exE 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   229
  by (Asm_full_simp_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   230
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   231
  (* 7 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   232
  by (tac3 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   233
  by (tac_ren 1);
9636
a0d4d9de9893 fixed a proof that had stopped working ???
paulson
parents: 8741
diff changeset
   234
  by (Force_tac 1);	
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   235
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   236
  (* 6 - 3 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   237
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   238
  by (EVERY1[tac3,tac3,tac3,tac3]);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   239
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   240
  (* 2 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   241
  by (asm_full_simp_tac ss 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
   242
  by (simp_tac (simpset() addsimps [inv3_def]) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   243
  by (strip_tac  1 THEN REPEAT (etac conjE 1));
15408
6001135caa91 tidied; removed references to HOL theories
paulson
parents: 14981
diff changeset
   244
  by (rtac (imp_disjL RS iffD1) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   245
  by (rtac impI 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   246
  by (forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   247
  by (Asm_full_simp_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   248
  by (REPEAT (etac conjE 1));
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   249
  by (res_inst_tac [("j","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
   250
                    ("k","count (rsent(rec s)) (sbit(sen s))")] le_trans 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   251
  by (forward_tac [rewrite_rule [inv1_def]
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   252
                                (inv1 RS invariantE) RS conjunct2] 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
   253
  by (asm_full_simp_tac (simpset() addsimps
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   254
                         [hdr_sum_def, Multiset.count_def]) 1);
4377
2cba48b0f1c4 Cleaned up arithmetic mess.
nipkow
parents: 4098
diff changeset
   255
  by (rtac add_le_mono 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   256
  by (rtac countm_props 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   257
  by (Simp_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   258
  by (rtac countm_props 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   259
  by (Simp_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   260
  by (assume_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   261
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   262
  (* 1 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   263
  by (tac3 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   264
  by (strip_tac  1 THEN REPEAT (etac conjE 1));
15408
6001135caa91 tidied; removed references to HOL theories
paulson
parents: 14981
diff changeset
   265
  by (rtac (imp_disjL RS iffD1) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   266
  by (rtac impI 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   267
  by (forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   268
  by (Asm_full_simp_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   269
qed "inv3";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   270
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   271
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   272
(* INVARIANT 4 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   273
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
   274
Goal "invariant impl_ioa inv4";
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   275
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   276
  by (rtac invariantI 1); 
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   277
  (* Base case *)
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
   278
  by (asm_full_simp_tac (simpset() addsimps 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   279
                    (Impl.inv4_def :: (receiver_projections 
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   280
                                       @ sender_projections @ impl_ioas))) 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   281
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4731
diff changeset
   282
  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5068
diff changeset
   283
  by (induct_tac "a" 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   284
6081
aa97eb904692 Some simplifications.
nipkow
parents: 5274
diff changeset
   285
val tac4 =  asm_full_simp_tac (ss addsimps [inv4_def]);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   286
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   287
  (* 10 - 2 *)
6081
aa97eb904692 Some simplifications.
nipkow
parents: 5274
diff changeset
   288
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   289
  by (EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]);
4731
0196377b5703 New Asm_full_simp_tac shortens proof.
nipkow
parents: 4681
diff changeset
   290
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   291
 (* 2 b *)
6081
aa97eb904692 Some simplifications.
nipkow
parents: 5274
diff changeset
   292
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   293
  by (strip_tac  1 THEN REPEAT (etac conjE 1));
4423
a129b817b58a expandshort;
wenzelm
parents: 4377
diff changeset
   294
  by (forward_tac [rewrite_rule [Impl.inv2_def]
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   295
                               (inv2 RS invariantE)] 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   296
  by (Asm_full_simp_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   297
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   298
  (* 1 *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   299
  by (tac4 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   300
  by (strip_tac  1 THEN REPEAT (etac conjE 1));
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   301
  by (rtac ccontr 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4377
diff changeset
   302
  by (forward_tac [rewrite_rule [Impl.inv2_def]
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   303
                               (inv2 RS invariantE)] 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4377
diff changeset
   304
  by (forward_tac [rewrite_rule [Impl.inv3_def]
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   305
                               (inv3 RS invariantE)] 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   306
  by (Asm_full_simp_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   307
  by (eres_inst_tac [("x","m")] allE 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   308
  by (Asm_full_simp_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   309
qed "inv4";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   310
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   311
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   312
(* rebind them *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   313
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   314
val inv1 = rewrite_rule [Impl.inv1_def] (inv1 RS invariantE);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   315
val inv2 = rewrite_rule [Impl.inv2_def] (inv2 RS invariantE);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   316
val inv3 = rewrite_rule [Impl.inv3_def] (inv3 RS invariantE);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
   317
val inv4 = rewrite_rule [Impl.inv4_def] (inv4 RS invariantE);