avoid rebinding of existing facts;
authorwenzelm
Mon Mar 17 18:37:07 2008 +0100 (2008-03-17)
changeset 26305651371f29e00
parent 26304 02fbd0e7954a
child 26306 ed3375ac152d
avoid rebinding of existing facts;
proper ML antiquotations;
src/HOL/TLA/TLA.thy
src/HOLCF/IOA/NTP/Impl.thy
     1.1 --- a/src/HOL/TLA/TLA.thy	Mon Mar 17 18:37:05 2008 +0100
     1.2 +++ b/src/HOL/TLA/TLA.thy	Mon Mar 17 18:37:07 2008 +0100
     1.3 @@ -115,26 +115,19 @@
     1.4     functions defined in theory Intensional in that they introduce a
     1.5     "world" parameter of type "behavior".
     1.6  *)
     1.7 -local
     1.8 -  val action_rews = thms "action_rews";
     1.9 -  val tempD = thm "tempD";
    1.10 -in
    1.11 -
    1.12  fun temp_unlift th =
    1.13 -  (rewrite_rule action_rews (th RS tempD)) handle THM _ => action_unlift th;
    1.14 +  (rewrite_rule @{thms action_rews} (th RS @{thm tempD})) handle THM _ => action_unlift th;
    1.15  
    1.16  (* Turn  |- F = G  into meta-level rewrite rule  F == G *)
    1.17  val temp_rewrite = int_rewrite
    1.18  
    1.19  fun temp_use th =
    1.20    case (concl_of th) of
    1.21 -    Const _ $ (Const ("Intensional.Valid", _) $ _) =>
    1.22 +    Const _ $ (Const (@{const_name Intensional.Valid}, _) $ _) =>
    1.23              ((flatten (temp_unlift th)) handle THM _ => th)
    1.24    | _ => th;
    1.25  
    1.26  fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th;
    1.27 -
    1.28 -end
    1.29  *}
    1.30  
    1.31  setup {*
    1.32 @@ -150,7 +143,7 @@
    1.33  declare tempI [intro!]
    1.34  declare tempD [dest]
    1.35  ML {*
    1.36 -val temp_css = (claset(), simpset())
    1.37 +val temp_css = (@{claset}, @{simpset})
    1.38  val temp_cs = op addss temp_css
    1.39  *}
    1.40  
    1.41 @@ -309,30 +302,20 @@
    1.42  lemma box_thin: "[| sigma |= []F; PROP W |] ==> PROP W" .
    1.43  
    1.44  ML {*
    1.45 -local
    1.46 -  val box_conjE = thm "box_conjE";
    1.47 -  val box_thin = thm "box_thin";
    1.48 -  val box_conjE_temp = thm "box_conjE_temp";
    1.49 -  val box_conjE_stp = thm "box_conjE_stp";
    1.50 -  val box_conjE_act = thm "box_conjE_act";
    1.51 -in
    1.52 -
    1.53  fun merge_box_tac i =
    1.54 -   REPEAT_DETERM (EVERY [etac box_conjE i, atac i, etac box_thin i])
    1.55 +   REPEAT_DETERM (EVERY [etac @{thm box_conjE} i, atac i, etac @{thm box_thin} i])
    1.56  
    1.57  fun merge_temp_box_tac i =
    1.58 -   REPEAT_DETERM (EVERY [etac box_conjE_temp i, atac i,
    1.59 -                         eres_inst_tac [("'a","behavior")] box_thin i])
    1.60 +   REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i,
    1.61 +                         eres_inst_tac [("'a","behavior")] @{thm box_thin} i])
    1.62  
    1.63  fun merge_stp_box_tac i =
    1.64 -   REPEAT_DETERM (EVERY [etac box_conjE_stp i, atac i,
    1.65 -                         eres_inst_tac [("'a","state")] box_thin i])
    1.66 +   REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i,
    1.67 +                         eres_inst_tac [("'a","state")] @{thm box_thin} i])
    1.68  
    1.69  fun merge_act_box_tac i =
    1.70 -   REPEAT_DETERM (EVERY [etac box_conjE_act i, atac i,
    1.71 -                         eres_inst_tac [("'a","state * state")] box_thin i])
    1.72 -
    1.73 -end
    1.74 +   REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
    1.75 +                         eres_inst_tac [("'a","state * state")] @{thm box_thin} i])
    1.76  *}
    1.77  
    1.78  (* rewrite rule to push universal quantification through box:
    1.79 @@ -450,7 +433,7 @@
    1.80  
    1.81  (* Make these rewrites active by default *)
    1.82  ML {*
    1.83 -val temp_css = temp_css addsimps2 (thms "temp_simps")
    1.84 +val temp_css = temp_css addsimps2 @{thms temp_simps}
    1.85  val temp_cs = op addss temp_css
    1.86  *}
    1.87  
    1.88 @@ -466,7 +449,7 @@
    1.89  
    1.90  (* These are not declared by default, because they could be harmful,
    1.91     e.g. []F & ~[]F becomes []F & <>~F !! *)
    1.92 -lemmas more_temp_simps =
    1.93 +lemmas more_temp_simps1 =
    1.94    STL3 [temp_rewrite] DmdDmd [temp_rewrite] NotBox [temp_rewrite] NotDmd [temp_rewrite]
    1.95    NotBox [temp_unlift, THEN eq_reflection]
    1.96    NotDmd [temp_unlift, THEN eq_reflection]
    1.97 @@ -480,7 +463,7 @@
    1.98      apply (drule STL6 [temp_use])
    1.99       apply assumption
   1.100      apply simp
   1.101 -   apply (simp_all add: more_temp_simps)
   1.102 +   apply (simp_all add: more_temp_simps1)
   1.103    done
   1.104  
   1.105  lemma DmdBoxDmd: "|- (<>[]<>F) = ([]<>F)"
   1.106 @@ -488,7 +471,7 @@
   1.107    apply (auto simp: BoxDmdBox [unfolded dmd_def, try_rewrite])
   1.108    done
   1.109  
   1.110 -lemmas more_temp_simps = more_temp_simps BoxDmdBox [temp_rewrite] DmdBoxDmd [temp_rewrite]
   1.111 +lemmas more_temp_simps2 = more_temp_simps1 BoxDmdBox [temp_rewrite] DmdBoxDmd [temp_rewrite]
   1.112  
   1.113  
   1.114  (* ------------------------ Miscellaneous ----------------------------------- *)
   1.115 @@ -500,7 +483,7 @@
   1.116  lemma DBImplBD: "|- <>[]F --> []<>F"
   1.117    apply clarsimp
   1.118    apply (rule ccontr)
   1.119 -  apply (simp add: more_temp_simps)
   1.120 +  apply (simp add: more_temp_simps2)
   1.121    apply (drule STL6 [temp_use])
   1.122     apply assumption
   1.123    apply simp
   1.124 @@ -509,7 +492,7 @@
   1.125  lemma BoxDmdDmdBox: "|- []<>F & <>[]G --> []<>(F & G)"
   1.126    apply clarsimp
   1.127    apply (rule ccontr)
   1.128 -  apply (unfold more_temp_simps)
   1.129 +  apply (unfold more_temp_simps2)
   1.130    apply (drule STL6 [temp_use])
   1.131     apply assumption
   1.132    apply (subgoal_tac "sigma |= <>[]~F")
   1.133 @@ -571,7 +554,7 @@
   1.134  lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2, standard]
   1.135  lemmas box_stp_actD = box_stp_act [temp_use, THEN iffD1, standard]
   1.136  
   1.137 -lemmas more_temp_simps = box_stp_act [temp_rewrite] more_temp_simps
   1.138 +lemmas more_temp_simps3 = box_stp_act [temp_rewrite] more_temp_simps2
   1.139  
   1.140  lemma INV1: 
   1.141    "|- (Init P) --> (stable P) --> []P"
   1.142 @@ -609,20 +592,12 @@
   1.143  (* ---------------- (Semi-)automatic invariant tactics ---------------------- *)
   1.144  
   1.145  ML {*
   1.146 -local
   1.147 -  val INV1 = thm "INV1";
   1.148 -  val Stable = thm "Stable";
   1.149 -  val Init_stp = thm "Init_stp";
   1.150 -  val Init_act = thm "Init_act";
   1.151 -  val squareE = thm "squareE";
   1.152 -in
   1.153 -
   1.154  (* inv_tac reduces goals of the form ... ==> sigma |= []P *)
   1.155  fun inv_tac css = SELECT_GOAL
   1.156       (EVERY [auto_tac css,
   1.157               TRY (merge_box_tac 1),
   1.158 -             rtac (temp_use INV1) 1, (* fail if the goal is not a box *)
   1.159 -             TRYALL (etac Stable)]);
   1.160 +             rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
   1.161 +             TRYALL (etac @{thm Stable})]);
   1.162  
   1.163  (* auto_inv_tac applies inv_tac and then tries to attack the subgoals
   1.164     in simple cases it may be able to handle goals like |- MyProg --> []Inv.
   1.165 @@ -631,9 +606,9 @@
   1.166     too late.
   1.167  *)
   1.168  fun auto_inv_tac ss = SELECT_GOAL
   1.169 -    ((inv_tac (claset(),ss) 1) THEN
   1.170 -     (TRYALL (action_simp_tac (ss addsimps [Init_stp, Init_act]) [] [squareE])));
   1.171 -end
   1.172 +    ((inv_tac (@{claset}, ss) 1) THEN
   1.173 +     (TRYALL (action_simp_tac
   1.174 +       (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
   1.175  *}
   1.176  
   1.177  lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q"
   1.178 @@ -673,7 +648,7 @@
   1.179     apply (subgoal_tac "sigma |= <>[] (<>P & []~P`)")
   1.180      apply (force simp: boxInit_stp [temp_use]
   1.181        elim!: DmdImplE [temp_use] STL4E [temp_use] DmdRec2 [temp_use])
   1.182 -   apply (force intro!: STL6 [temp_use] simp: more_temp_simps)
   1.183 +   apply (force intro!: STL6 [temp_use] simp: more_temp_simps3)
   1.184    apply (fastsimp intro: DmdPrime [temp_use] elim!: STL4E [temp_use])
   1.185    done
   1.186  
   1.187 @@ -700,18 +675,18 @@
   1.188  
   1.189  (* theorems to "box" fairness conditions *)
   1.190  lemma BoxWFI: "|- WF(A)_v --> []WF(A)_v"
   1.191 -  by (auto simp: WF_alt [try_rewrite] more_temp_simps intro!: BoxOr [temp_use])
   1.192 +  by (auto simp: WF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
   1.193  
   1.194  lemma WF_Box: "|- ([]WF(A)_v) = WF(A)_v"
   1.195    by (fastsimp intro!: BoxWFI [temp_use] dest!: STL2 [temp_use])
   1.196  
   1.197  lemma BoxSFI: "|- SF(A)_v --> []SF(A)_v"
   1.198 -  by (auto simp: SF_alt [try_rewrite] more_temp_simps intro!: BoxOr [temp_use])
   1.199 +  by (auto simp: SF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
   1.200  
   1.201  lemma SF_Box: "|- ([]SF(A)_v) = SF(A)_v"
   1.202    by (fastsimp intro!: BoxSFI [temp_use] dest!: STL2 [temp_use])
   1.203  
   1.204 -lemmas more_temp_simps = more_temp_simps WF_Box [temp_rewrite] SF_Box [temp_rewrite]
   1.205 +lemmas more_temp_simps = more_temp_simps3 WF_Box [temp_rewrite] SF_Box [temp_rewrite]
   1.206  
   1.207  lemma SFImplWF: "|- SF(A)_v --> WF(A)_v"
   1.208    apply (unfold SF_def WF_def)
   1.209 @@ -720,12 +695,7 @@
   1.210  
   1.211  (* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *)
   1.212  ML {*
   1.213 -local
   1.214 -  val BoxWFI = thm "BoxWFI";
   1.215 -  val BoxSFI = thm "BoxSFI";
   1.216 -in 
   1.217 -val box_fair_tac = SELECT_GOAL (REPEAT (dresolve_tac [BoxWFI,BoxSFI] 1))
   1.218 -end
   1.219 +val box_fair_tac = SELECT_GOAL (REPEAT (dresolve_tac [@{thm BoxWFI}, @{thm BoxSFI}] 1))
   1.220  *}
   1.221  
   1.222  
     2.1 --- a/src/HOLCF/IOA/NTP/Impl.thy	Mon Mar 17 18:37:05 2008 +0100
     2.2 +++ b/src/HOLCF/IOA/NTP/Impl.thy	Mon Mar 17 18:37:07 2008 +0100
     2.3 @@ -112,17 +112,17 @@
     2.4  3) renname_ss unfolds transitions and the abstract channel *)
     2.5  
     2.6  ML {*
     2.7 -val ss = simpset() addsimps thms "transitions";
     2.8 -val rename_ss = ss addsimps thms "unfold_renaming";
     2.9 +val ss = @{simpset} addsimps @{thms transitions};
    2.10 +val rename_ss = ss addsimps @{thms unfold_renaming};
    2.11  
    2.12 -val tac     = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if])
    2.13 -val tac_ren = asm_simp_tac (rename_ss addcongs [conj_cong] addsplits [split_if])
    2.14 +val tac     = asm_simp_tac (ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}])
    2.15 +val tac_ren = asm_simp_tac (rename_ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}])
    2.16  *}
    2.17  
    2.18  
    2.19  subsubsection {* Invariant 1 *}
    2.20  
    2.21 -lemma inv1: "invariant impl_ioa inv1"
    2.22 +lemma raw_inv1: "invariant impl_ioa inv1"
    2.23  
    2.24  apply (unfold impl_ioas)
    2.25  apply (rule invariantI)
    2.26 @@ -197,7 +197,7 @@
    2.27  
    2.28  subsubsection {* INVARIANT 2 *}
    2.29  
    2.30 -lemma inv2: "invariant impl_ioa inv2"
    2.31 +lemma raw_inv2: "invariant impl_ioa inv2"
    2.32  
    2.33    apply (rule invariantI1)
    2.34    txt {* Base case *}
    2.35 @@ -208,45 +208,45 @@
    2.36  
    2.37    txt {* 10 cases. First 4 are simple, since state doesn't change *}
    2.38  
    2.39 -ML {* val tac2 = asm_full_simp_tac (ss addsimps [thm "inv2_def"]) *}
    2.40 +ML {* val tac2 = asm_full_simp_tac (ss addsimps [@{thm inv2_def}]) *}
    2.41  
    2.42    txt {* 10 - 7 *}
    2.43    apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
    2.44    txt {* 6 *}
    2.45 -  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
    2.46 -                               (thm "inv1" RS thm "invariantE") RS conjunct1] 1 *})
    2.47 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
    2.48 +                               (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
    2.49  
    2.50    txt {* 6 - 5 *}
    2.51    apply (tactic "EVERY1 [tac2,tac2]")
    2.52  
    2.53    txt {* 4 *}
    2.54 -  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
    2.55 -                                (thm "inv1" RS thm "invariantE") RS conjunct1] 1 *})
    2.56 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
    2.57 +                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
    2.58    apply (tactic "tac2 1")
    2.59  
    2.60    txt {* 3 *}
    2.61 -  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
    2.62 -    (thm "inv1" RS thm "invariantE")] 1 *})
    2.63 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
    2.64 +    (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
    2.65  
    2.66    apply (tactic "tac2 1")
    2.67 -  apply (tactic {* fold_tac [rewrite_rule [thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")] *})
    2.68 +  apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
    2.69    apply arith
    2.70  
    2.71    txt {* 2 *}
    2.72    apply (tactic "tac2 1")
    2.73 -  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
    2.74 -                               (thm "inv1" RS thm "invariantE") RS conjunct1] 1 *})
    2.75 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
    2.76 +                               (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
    2.77    apply (intro strip)
    2.78    apply (erule conjE)+
    2.79    apply simp
    2.80  
    2.81    txt {* 1 *}
    2.82    apply (tactic "tac2 1")
    2.83 -  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
    2.84 -                               (thm "inv1" RS thm "invariantE") RS conjunct2] 1 *})
    2.85 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
    2.86 +                               (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
    2.87    apply (intro strip)
    2.88    apply (erule conjE)+
    2.89 -  apply (tactic {* fold_tac  [rewrite_rule[thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")] *})
    2.90 +  apply (tactic {* fold_tac  [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
    2.91    apply simp
    2.92  
    2.93    done
    2.94 @@ -254,7 +254,7 @@
    2.95  
    2.96  subsubsection {* INVARIANT 3 *}
    2.97  
    2.98 -lemma inv3: "invariant impl_ioa inv3"
    2.99 +lemma raw_inv3: "invariant impl_ioa inv3"
   2.100  
   2.101    apply (rule invariantI)
   2.102    txt {* Base case *}
   2.103 @@ -263,7 +263,7 @@
   2.104    apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
   2.105    apply (induct_tac "a")
   2.106  
   2.107 -ML {* val tac3 = asm_full_simp_tac (ss addsimps [thm "inv3_def"]) *}
   2.108 +ML {* val tac3 = asm_full_simp_tac (ss addsimps [@{thm inv3_def}]) *}
   2.109  
   2.110    txt {* 10 - 8 *}
   2.111  
   2.112 @@ -290,14 +290,14 @@
   2.113    apply (intro strip, (erule conjE)+)
   2.114    apply (rule imp_disjL [THEN iffD1])
   2.115    apply (rule impI)
   2.116 -  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
   2.117 -    (thm "inv2" RS thm "invariantE")] 1 *})
   2.118 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   2.119 +    (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   2.120    apply simp
   2.121    apply (erule conjE)+
   2.122    apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and
   2.123      k = "count (rsent (rec s)) (sbit (sen s))" in le_trans)
   2.124 -  apply (tactic {* forward_tac [rewrite_rule [thm "inv1_def"]
   2.125 -                                (thm "inv1" RS thm "invariantE") RS conjunct2] 1 *})
   2.126 +  apply (tactic {* forward_tac [rewrite_rule [@{thm inv1_def}]
   2.127 +                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
   2.128    apply (simp add: hdr_sum_def Multiset.count_def)
   2.129    apply (rule add_le_mono)
   2.130    apply (rule countm_props)
   2.131 @@ -311,15 +311,15 @@
   2.132    apply (intro strip, (erule conjE)+)
   2.133    apply (rule imp_disjL [THEN iffD1])
   2.134    apply (rule impI)
   2.135 -  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
   2.136 -    (thm "inv2" RS thm "invariantE")] 1 *})
   2.137 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   2.138 +    (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   2.139    apply simp
   2.140    done
   2.141  
   2.142  
   2.143  subsubsection {* INVARIANT 4 *}
   2.144  
   2.145 -lemma inv4: "invariant impl_ioa inv4"
   2.146 +lemma raw_inv4: "invariant impl_ioa inv4"
   2.147  
   2.148    apply (rule invariantI)
   2.149    txt {* Base case *}
   2.150 @@ -328,7 +328,7 @@
   2.151    apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
   2.152    apply (induct_tac "a")
   2.153  
   2.154 -ML {* val tac4 =  asm_full_simp_tac (ss addsimps [thm "inv4_def"]) *}
   2.155 +ML {* val tac4 =  asm_full_simp_tac (ss addsimps [@{thm inv4_def}]) *}
   2.156  
   2.157    txt {* 10 - 2 *}
   2.158  
   2.159 @@ -337,18 +337,18 @@
   2.160    txt {* 2 b *}
   2.161  
   2.162    apply (intro strip, (erule conjE)+)
   2.163 -  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
   2.164 -                               (thm "inv2" RS thm "invariantE")] 1 *})
   2.165 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   2.166 +                               (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   2.167    apply simp
   2.168  
   2.169    txt {* 1 *}
   2.170    apply (tactic "tac4 1")
   2.171    apply (intro strip, (erule conjE)+)
   2.172    apply (rule ccontr)
   2.173 -  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
   2.174 -                               (thm "inv2" RS thm "invariantE")] 1 *})
   2.175 -  apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv3_def"]
   2.176 -                               (thm "inv3" RS thm "invariantE")] 1 *})
   2.177 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
   2.178 +                               (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   2.179 +  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv3_def}]
   2.180 +                               (@{thm raw_inv3} RS @{thm invariantE})] 1 *})
   2.181    apply simp
   2.182    apply (erule_tac x = "m" in allE)
   2.183    apply simp
   2.184 @@ -357,9 +357,9 @@
   2.185  
   2.186  text {* rebind them *}
   2.187  
   2.188 -lemmas inv1 = inv1 [THEN invariantE, unfolded inv1_def]
   2.189 -  and inv2 = inv2 [THEN invariantE, unfolded inv2_def]
   2.190 -  and inv3 = inv3 [THEN invariantE, unfolded inv3_def]
   2.191 -  and inv4 = inv4 [THEN invariantE, unfolded inv4_def]
   2.192 +lemmas inv1 = raw_inv1 [THEN invariantE, unfolded inv1_def]
   2.193 +  and inv2 = raw_inv2 [THEN invariantE, unfolded inv2_def]
   2.194 +  and inv3 = raw_inv3 [THEN invariantE, unfolded inv3_def]
   2.195 +  and inv4 = raw_inv4 [THEN invariantE, unfolded inv4_def]
   2.196  
   2.197  end