id <-> Id
authornipkow
Fri Oct 02 14:28:39 1998 +0200 (1998-10-02)
changeset 5608a82a038a3e7a
parent 5607 5db9e2343ade
child 5609 03d74c85a818
id <-> Id
src/HOL/Fun.ML
src/HOL/Fun.thy
src/HOL/IMP/Denotation.thy
src/HOL/Lex/NA.thy
src/HOL/Lex/RegExp2NAe.ML
src/HOL/RelPow.thy
src/HOL/Relation.ML
src/HOL/Relation.thy
src/HOL/Trancl.ML
src/HOL/Trancl.thy
src/HOL/UNITY/Channel.thy
src/HOL/UNITY/Common.ML
src/HOL/UNITY/Token.thy
src/HOL/UNITY/Traces.ML
src/HOL/UNITY/Traces.thy
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/Union.ML
src/HOL/UNITY/WFair.ML
     1.1 --- a/src/HOL/Fun.ML	Fri Oct 02 10:44:20 1998 +0200
     1.2 +++ b/src/HOL/Fun.ML	Fri Oct 02 14:28:39 1998 +0200
     1.3 @@ -31,10 +31,10 @@
     1.4  qed "bchoice";
     1.5  
     1.6  
     1.7 -section "Id";
     1.8 +section "id";
     1.9  
    1.10 -qed_goalw "Id_apply" thy [Id_def] "Id x = x" (K [rtac refl 1]);
    1.11 -Addsimps [Id_apply];
    1.12 +qed_goalw "id_apply" thy [id_def] "id x = x" (K [rtac refl 1]);
    1.13 +Addsimps [id_apply];
    1.14  
    1.15  
    1.16  section "o";
    1.17 @@ -46,13 +46,13 @@
    1.18  qed_goalw "o_assoc" thy [o_def] "f o (g o h) = f o g o h"
    1.19    (K [rtac ext 1, rtac refl 1]);
    1.20  
    1.21 -qed_goalw "Id_o" thy [Id_def] "Id o g = g"
    1.22 +qed_goalw "id_o" thy [id_def] "id o g = g"
    1.23   (K [rtac ext 1, Simp_tac 1]);
    1.24 -Addsimps [Id_o];
    1.25 +Addsimps [id_o];
    1.26  
    1.27 -qed_goalw "o_Id" thy [Id_def] "f o Id = f"
    1.28 +qed_goalw "o_id" thy [id_def] "f o id = f"
    1.29   (K [rtac ext 1, Simp_tac 1]);
    1.30 -Addsimps [o_Id];
    1.31 +Addsimps [o_id];
    1.32  
    1.33  Goalw [o_def] "(f o g)``r = f``(g``r)";
    1.34  by (Blast_tac 1);
     2.1 --- a/src/HOL/Fun.thy	Fri Oct 02 10:44:20 1998 +0200
     2.2 +++ b/src/HOL/Fun.thy	Fri Oct 02 14:28:39 1998 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4                         (subset_refl,subset_trans,subset_antisym,psubset_eq)
     2.5  consts
     2.6  
     2.7 -  Id          ::  'a => 'a
     2.8 +  id          ::  'a => 'a
     2.9    o           :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
    2.10    inj, surj   :: ('a => 'b) => bool                   (*inj/surjective*)
    2.11    inj_on      :: ['a => 'b, 'a set] => bool
    2.12 @@ -37,7 +37,7 @@
    2.13  
    2.14  defs
    2.15  
    2.16 -  Id_def	"Id             == %x. x"
    2.17 +  id_def	"id             == %x. x"
    2.18    o_def   	"f o g          == %x. f(g(x))"
    2.19    inj_def	"inj f          == ! x y. f(x)=f(y) --> x=y"
    2.20    inj_on_def	"inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"
     3.1 --- a/src/HOL/IMP/Denotation.thy	Fri Oct 02 10:44:20 1998 +0200
     3.2 +++ b/src/HOL/IMP/Denotation.thy	Fri Oct 02 14:28:39 1998 +0200
     3.3 @@ -19,7 +19,7 @@
     3.4    C     :: com => com_den
     3.5  
     3.6  primrec
     3.7 -  C_skip    "C(SKIP) = id"
     3.8 +  C_skip    "C(SKIP) = Id"
     3.9    C_assign  "C(x := a) = {(s,t). t = s[x:=a(s)]}"
    3.10    C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
    3.11    C_if      "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un
    3.12 @@ -27,5 +27,3 @@
    3.13    C_while   "C(WHILE b DO c) = lfp (Gamma b (C c))"
    3.14  
    3.15  end
    3.16 -
    3.17 -
     4.1 --- a/src/HOL/Lex/NA.thy	Fri Oct 02 10:44:20 1998 +0200
     4.2 +++ b/src/HOL/Lex/NA.thy	Fri Oct 02 14:28:39 1998 +0200
     4.3 @@ -25,7 +25,7 @@
     4.4  
     4.5  consts steps :: "('a,'s)na => 'a list => ('s * 's)set"
     4.6  primrec
     4.7 -"steps A [] = id"
     4.8 +"steps A [] = Id"
     4.9  "steps A (a#w) = steps A w  O  step A a"
    4.10  
    4.11  end
     5.1 --- a/src/HOL/Lex/RegExp2NAe.ML	Fri Oct 02 10:44:20 1998 +0200
     5.2 +++ b/src/HOL/Lex/RegExp2NAe.ML	Fri Oct 02 14:28:39 1998 +0200
     5.3 @@ -152,7 +152,7 @@
     5.4  (***** Epsilonhuelle des Startzustands  *****)
     5.5  
     5.6  Goal
     5.7 - "R^* = id Un (R^* O R)";
     5.8 + "R^* = Id Un (R^* O R)";
     5.9  by (rtac set_ext 1);
    5.10  by (split_all_tac 1);
    5.11  by (rtac iffI 1);
     6.1 --- a/src/HOL/RelPow.thy	Fri Oct 02 10:44:20 1998 +0200
     6.2 +++ b/src/HOL/RelPow.thy	Fri Oct 02 14:28:39 1998 +0200
     6.3 @@ -9,7 +9,7 @@
     6.4  RelPow = Nat +
     6.5  
     6.6  primrec
     6.7 -  "R^0 = id"
     6.8 +  "R^0 = Id"
     6.9    "R^(Suc n) = R O (R^n)"
    6.10  
    6.11  end
     7.1 --- a/src/HOL/Relation.ML	Fri Oct 02 10:44:20 1998 +0200
     7.2 +++ b/src/HOL/Relation.ML	Fri Oct 02 14:28:39 1998 +0200
     7.3 @@ -8,22 +8,22 @@
     7.4  
     7.5  (** Identity relation **)
     7.6  
     7.7 -Goalw [id_def] "(a,a) : id";  
     7.8 +Goalw [Id_def] "(a,a) : Id";  
     7.9  by (Blast_tac 1);
    7.10 -qed "idI";
    7.11 +qed "IdI";
    7.12  
    7.13 -val major::prems = Goalw [id_def]
    7.14 -    "[| p: id;  !!x.[| p = (x,x) |] ==> P  \
    7.15 +val major::prems = Goalw [Id_def]
    7.16 +    "[| p: Id;  !!x.[| p = (x,x) |] ==> P  \
    7.17  \    |] ==>  P";  
    7.18  by (rtac (major RS CollectE) 1);
    7.19  by (etac exE 1);
    7.20  by (eresolve_tac prems 1);
    7.21 -qed "idE";
    7.22 +qed "IdE";
    7.23  
    7.24 -Goalw [id_def] "(a,b):id = (a=b)";
    7.25 +Goalw [Id_def] "(a,b):Id = (a=b)";
    7.26  by (Blast_tac 1);
    7.27 -qed "pair_in_id_conv";
    7.28 -Addsimps [pair_in_id_conv];
    7.29 +qed "pair_in_Id_conv";
    7.30 +Addsimps [pair_in_Id_conv];
    7.31  
    7.32  
    7.33  (** Composition of two relations **)
    7.34 @@ -51,18 +51,18 @@
    7.35  by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1));
    7.36  qed "compEpair";
    7.37  
    7.38 -AddIs [compI, idI];
    7.39 -AddSEs [compE, idE];
    7.40 +AddIs [compI, IdI];
    7.41 +AddSEs [compE, IdE];
    7.42  
    7.43 -Goal "R O id = R";
    7.44 +Goal "R O Id = R";
    7.45  by (Fast_tac 1);
    7.46 -qed "R_O_id";
    7.47 +qed "R_O_Id";
    7.48  
    7.49 -Goal "id O R = R";
    7.50 +Goal "Id O R = R";
    7.51  by (Fast_tac 1);
    7.52 -qed "id_O_R";
    7.53 +qed "Id_O_R";
    7.54  
    7.55 -Addsimps [R_O_id,id_O_R];
    7.56 +Addsimps [R_O_Id,Id_O_R];
    7.57  
    7.58  Goal "(R O S) O T = R O (S O T)";
    7.59  by (Blast_tac 1);
    7.60 @@ -124,10 +124,10 @@
    7.61  by (Blast_tac 1);
    7.62  qed "converse_comp";
    7.63  
    7.64 -Goal "id^-1 = id";
    7.65 +Goal "Id^-1 = Id";
    7.66  by (Blast_tac 1);
    7.67 -qed "converse_id";
    7.68 -Addsimps [converse_id];
    7.69 +qed "converse_Id";
    7.70 +Addsimps [converse_Id];
    7.71  
    7.72  (** Domain **)
    7.73  
    7.74 @@ -147,10 +147,10 @@
    7.75  AddIs  [DomainI];
    7.76  AddSEs [DomainE];
    7.77  
    7.78 -Goal "Domain id = UNIV";
    7.79 +Goal "Domain Id = UNIV";
    7.80  by (Blast_tac 1);
    7.81 -qed "Domain_id";
    7.82 -Addsimps [Domain_id];
    7.83 +qed "Domain_Id";
    7.84 +Addsimps [Domain_Id];
    7.85  
    7.86  (** Range **)
    7.87  
    7.88 @@ -167,10 +167,10 @@
    7.89  AddIs  [RangeI];
    7.90  AddSEs [RangeE];
    7.91  
    7.92 -Goal "Range id = UNIV";
    7.93 +Goal "Range Id = UNIV";
    7.94  by (Blast_tac 1);
    7.95 -qed "Range_id";
    7.96 -Addsimps [Range_id];
    7.97 +qed "Range_Id";
    7.98 +Addsimps [Range_Id];
    7.99  
   7.100  (*** Image of a set under a relation ***)
   7.101  
   7.102 @@ -213,11 +213,11 @@
   7.103  
   7.104  Addsimps [Image_empty];
   7.105  
   7.106 -Goal "id ^^ A = A";
   7.107 +Goal "Id ^^ A = A";
   7.108  by (Blast_tac 1);
   7.109 -qed "Image_id";
   7.110 +qed "Image_Id";
   7.111  
   7.112 -Addsimps [Image_id];
   7.113 +Addsimps [Image_Id];
   7.114  
   7.115  qed_goal "Image_Int_subset" thy
   7.116      "R ^^ (A Int B) <= R ^^ A Int R ^^ B"
     8.1 --- a/src/HOL/Relation.thy	Fri Oct 02 10:44:20 1998 +0200
     8.2 +++ b/src/HOL/Relation.thy	Fri Oct 02 14:28:39 1998 +0200
     8.3 @@ -6,7 +6,7 @@
     8.4  
     8.5  Relation = Prod +
     8.6  consts
     8.7 -    id          :: "('a * 'a)set"               (*the identity relation*)
     8.8 +    Id          :: "('a * 'a)set"               (*the identity relation*)
     8.9      O           :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
    8.10      converse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 999)
    8.11      "^^"        :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
    8.12 @@ -15,7 +15,7 @@
    8.13      trans       :: "('a * 'a)set => bool"       (*transitivity predicate*)
    8.14      Univalent   :: "('a * 'b)set => bool"
    8.15  defs
    8.16 -    id_def        "id == {p. ? x. p = (x,x)}"
    8.17 +    Id_def        "Id == {p. ? x. p = (x,x)}"
    8.18      comp_def      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
    8.19      converse_def   "r^-1 == {(y,x). (x,y):r}"
    8.20      Domain_def    "Domain(r) == {x. ? y. (x,y):r}"
     9.1 --- a/src/HOL/Trancl.ML	Fri Oct 02 10:44:20 1998 +0200
     9.2 +++ b/src/HOL/Trancl.ML	Fri Oct 02 14:28:39 1998 +0200
     9.3 @@ -10,7 +10,7 @@
     9.4  
     9.5  (** The relation rtrancl **)
     9.6  
     9.7 -Goal "mono(%s. id Un (r O s))";
     9.8 +Goal "mono(%s. Id Un (r O s))";
     9.9  by (rtac monoI 1);
    9.10  by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
    9.11  qed "rtrancl_fun_mono";
    9.12 @@ -343,6 +343,6 @@
    9.13    (K [auto_tac (claset() addEs [trancl_induct], simpset())]);
    9.14  Addsimps[trancl_empty];
    9.15  
    9.16 -qed_goal "rtrancl_empty" Trancl.thy "{}^* = id" 
    9.17 +qed_goal "rtrancl_empty" Trancl.thy "{}^* = Id" 
    9.18    (K [rtac (reflcl_trancl RS subst) 1, Simp_tac 1]);
    9.19  Addsimps[rtrancl_empty];
    10.1 --- a/src/HOL/Trancl.thy	Fri Oct 02 10:44:20 1998 +0200
    10.2 +++ b/src/HOL/Trancl.thy	Fri Oct 02 14:28:39 1998 +0200
    10.3 @@ -17,7 +17,7 @@
    10.4  
    10.5  constdefs
    10.6    rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [1000] 999)
    10.7 -  "r^*  ==  lfp(%s. id Un (r O s))"
    10.8 +  "r^*  ==  lfp(%s. Id Un (r O s))"
    10.9  
   10.10    trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [1000] 999)
   10.11    "r^+  ==  r O rtrancl(r)"
   10.12 @@ -26,6 +26,6 @@
   10.13    reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [1000] 999)
   10.14  
   10.15  translations
   10.16 -  "r^=" == "r Un id"
   10.17 +  "r^=" == "r Un Id"
   10.18  
   10.19  end
    11.1 --- a/src/HOL/UNITY/Channel.thy	Fri Oct 02 10:44:20 1998 +0200
    11.2 +++ b/src/HOL/UNITY/Channel.thy	Fri Oct 02 14:28:39 1998 +0200
    11.3 @@ -18,7 +18,7 @@
    11.4  
    11.5  rules
    11.6  
    11.7 -  skip "id: acts"
    11.8 +  skip "Id: acts"
    11.9  
   11.10    UC1  "constrains acts (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))"
   11.11  
    12.1 --- a/src/HOL/UNITY/Common.ML	Fri Oct 02 10:44:20 1998 +0200
    12.2 +++ b/src/HOL/UNITY/Common.ML	Fri Oct 02 14:28:39 1998 +0200
    12.3 @@ -31,7 +31,7 @@
    12.4  (*** Some programs that implement the safety property above ***)
    12.5  
    12.6  (*This one is just Skip*)
    12.7 -Goal "constrains {id} {m} (maxfg m)";
    12.8 +Goal "constrains {Id} {m} (maxfg m)";
    12.9  by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
   12.10  				  fasc, gasc]) 1);
   12.11  result();
    13.1 --- a/src/HOL/UNITY/Token.thy	Fri Oct 02 10:44:20 1998 +0200
    13.2 +++ b/src/HOL/UNITY/Token.thy	Fri Oct 02 14:28:39 1998 +0200
    13.3 @@ -43,7 +43,7 @@
    13.4    assumes
    13.5      N_positive "0<N"
    13.6  
    13.7 -    skip "id: acts"
    13.8 +    skip "Id: acts"
    13.9  
   13.10      TR2  "!!i. constrains acts (T i) (T i Un H i)"
   13.11  
    14.1 --- a/src/HOL/UNITY/Traces.ML	Fri Oct 02 10:44:20 1998 +0200
    14.2 +++ b/src/HOL/UNITY/Traces.ML	Fri Oct 02 14:28:39 1998 +0200
    14.3 @@ -17,18 +17,18 @@
    14.4  		 Rep_Program_inverse, Abs_Program_inverse];
    14.5  
    14.6  
    14.7 -Goal "id: Acts prg";
    14.8 +Goal "Id: Acts prg";
    14.9  by (cut_inst_tac [("x", "prg")] Rep_Program 1);
   14.10  by (auto_tac (claset(), rep_ss));
   14.11 -qed "id_in_Acts";
   14.12 -AddIffs [id_in_Acts];
   14.13 +qed "Id_in_Acts";
   14.14 +AddIffs [Id_in_Acts];
   14.15  
   14.16  
   14.17  Goal "Init (mk_program (init,acts)) = init";
   14.18  by (auto_tac (claset(), rep_ss));
   14.19  qed "Init_eq";
   14.20  
   14.21 -Goal "Acts (mk_program (init,acts)) = insert id acts";
   14.22 +Goal "Acts (mk_program (init,acts)) = insert Id acts";
   14.23  by (auto_tac (claset(), rep_ss));
   14.24  qed "Acts_eq";
   14.25  
   14.26 @@ -47,7 +47,7 @@
   14.27  
   14.28  val [rew] = goal thy
   14.29      "[| prg == mk_program (init,acts) |] \
   14.30 -\    ==> Init prg = init & Acts prg = insert id acts";
   14.31 +\    ==> Init prg = init & Acts prg = insert Id acts";
   14.32  by (rewtac rew);
   14.33  by Auto_tac;
   14.34  qed "def_prg_simps";
    15.1 --- a/src/HOL/UNITY/Traces.thy	Fri Oct 02 10:44:20 1998 +0200
    15.2 +++ b/src/HOL/UNITY/Traces.thy	Fri Oct 02 14:28:39 1998 +0200
    15.3 @@ -25,11 +25,11 @@
    15.4  
    15.5  
    15.6  typedef (Program)
    15.7 -  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). id:acts}"
    15.8 +  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
    15.9  
   15.10  constdefs
   15.11      mk_program :: "('a set * ('a * 'a)set set) => 'a program"
   15.12 -    "mk_program == %(init, acts). Abs_Program (init, insert id acts)"
   15.13 +    "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
   15.14  
   15.15      Init :: "'a program => 'a set"
   15.16      "Init prg == fst (Rep_Program prg)"
    16.1 --- a/src/HOL/UNITY/UNITY.ML	Fri Oct 02 10:44:20 1998 +0200
    16.2 +++ b/src/HOL/UNITY/UNITY.ML	Fri Oct 02 14:28:39 1998 +0200
    16.3 @@ -97,12 +97,12 @@
    16.4  by (Blast_tac 1);
    16.5  qed "all_constrains_INT";
    16.6  
    16.7 -Goalw [constrains_def] "[| constrains acts A A'; id: acts |] ==> A<=A'";
    16.8 +Goalw [constrains_def] "[| constrains acts A A'; Id: acts |] ==> A<=A'";
    16.9  by (Blast_tac 1);
   16.10  qed "constrains_imp_subset";
   16.11  
   16.12  Goalw [constrains_def]
   16.13 -    "[| id: acts; constrains acts A B; constrains acts B C |]   \
   16.14 +    "[| Id: acts; constrains acts A B; constrains acts B C |]   \
   16.15  \    ==> constrains acts A C";
   16.16  by (Blast_tac 1);
   16.17  qed "constrains_trans";
   16.18 @@ -160,7 +160,7 @@
   16.19  
   16.20  
   16.21  Goalw [constrains_def]
   16.22 -   "[| constrains acts A (A' Un B); constrains acts B B'; id: acts |] \
   16.23 +   "[| constrains acts A (A' Un B); constrains acts B B'; Id: acts |] \
   16.24  \   ==> constrains acts A (A' Un B')";
   16.25  by (Blast_tac 1);
   16.26  qed "constrains_cancel";
    17.1 --- a/src/HOL/UNITY/Union.ML	Fri Oct 02 10:44:20 1998 +0200
    17.2 +++ b/src/HOL/UNITY/Union.ML	Fri Oct 02 14:28:39 1998 +0200
    17.3 @@ -21,7 +21,7 @@
    17.4  by (simp_tac (simpset() addsimps [JOIN_def]) 1);
    17.5  qed "Init_JN";
    17.6  
    17.7 -Goal "Acts (JN i:I. prg i) = insert id (UN i:I. Acts (prg i))";
    17.8 +Goal "Acts (JN i:I. prg i) = insert Id (UN i:I. Acts (prg i))";
    17.9  by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
   17.10  qed "Acts_JN";
   17.11  
   17.12 @@ -142,7 +142,7 @@
   17.13  qed "ensures_Join";
   17.14  
   17.15  Goalw [stable_def, constrains_def, Join_def]
   17.16 -    "[| stable (Acts prgF) A;  constrains (Acts prgG) A A';  id: Acts prgG |] \
   17.17 +    "[| stable (Acts prgF) A;  constrains (Acts prgG) A A';  Id: Acts prgG |] \
   17.18  \    ==> constrains (Acts (Join prgF prgG)) A A'";
   17.19  by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
   17.20  by (Blast_tac 1);
    18.1 --- a/src/HOL/UNITY/WFair.ML	Fri Oct 02 10:44:20 1998 +0200
    18.2 +++ b/src/HOL/UNITY/WFair.ML	Fri Oct 02 14:28:39 1998 +0200
    18.3 @@ -125,7 +125,7 @@
    18.4  qed "leadsTo_induct";
    18.5  
    18.6  
    18.7 -Goal "[| A<=B;  id: acts |] ==> leadsTo acts A B";
    18.8 +Goal "[| A<=B;  Id: acts |] ==> leadsTo acts A B";
    18.9  by (rtac leadsTo_Basis 1);
   18.10  by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
   18.11  by (Blast_tac 1);
   18.12 @@ -136,7 +136,7 @@
   18.13  
   18.14  
   18.15  (*There's a direct proof by leadsTo_Trans and subset_imp_leadsTo, but it
   18.16 -  needs the extra premise id:acts*)
   18.17 +  needs the extra premise Id:acts*)
   18.18  Goal "leadsTo acts A A' ==> A'<=B' --> leadsTo acts A B'";
   18.19  by (etac leadsTo_induct 1);
   18.20  by (Clarify_tac 3);
   18.21 @@ -146,30 +146,30 @@
   18.22  qed_spec_mp "leadsTo_weaken_R";
   18.23  
   18.24  
   18.25 -Goal "[| leadsTo acts A A'; B<=A; id: acts |] ==>  \
   18.26 +Goal "[| leadsTo acts A A'; B<=A; Id: acts |] ==>  \
   18.27  \         leadsTo acts B A'";
   18.28  by (blast_tac (claset() addIs [leadsTo_Basis, leadsTo_Trans, 
   18.29  			       subset_imp_leadsTo]) 1);
   18.30  qed_spec_mp "leadsTo_weaken_L";
   18.31  
   18.32  (*Distributes over binary unions*)
   18.33 -Goal "id: acts ==> \
   18.34 +Goal "Id: acts ==> \
   18.35  \       leadsTo acts (A Un B) C  =  (leadsTo acts A C & leadsTo acts B C)";
   18.36  by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
   18.37  qed "leadsTo_Un_distrib";
   18.38  
   18.39 -Goal "id: acts ==> \
   18.40 +Goal "Id: acts ==> \
   18.41  \       leadsTo acts (UN i:I. A i) B  =  (ALL i : I. leadsTo acts (A i) B)";
   18.42  by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
   18.43  qed "leadsTo_UN_distrib";
   18.44  
   18.45 -Goal "id: acts ==> \
   18.46 +Goal "Id: acts ==> \
   18.47  \       leadsTo acts (Union S) B  =  (ALL A : S. leadsTo acts A B)";
   18.48  by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
   18.49  qed "leadsTo_Union_distrib";
   18.50  
   18.51  
   18.52 -Goal "[| leadsTo acts A A'; id: acts; B<=A; A'<=B' |] \
   18.53 +Goal "[| leadsTo acts A A'; Id: acts; B<=A; A'<=B' |] \
   18.54  \   ==> leadsTo acts B B'";
   18.55  by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
   18.56  			       leadsTo_Trans]) 1);
   18.57 @@ -177,7 +177,7 @@
   18.58  
   18.59  
   18.60  (*Set difference: maybe combine with leadsTo_weaken_L??*)
   18.61 -Goal "[| leadsTo acts (A-B) C; leadsTo acts B C; id: acts |] \
   18.62 +Goal "[| leadsTo acts (A-B) C; leadsTo acts B C; Id: acts |] \
   18.63  \       ==> leadsTo acts A C";
   18.64  by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
   18.65  qed "leadsTo_Diff";
   18.66 @@ -220,26 +220,26 @@
   18.67  
   18.68  (** The cancellation law **)
   18.69  
   18.70 -Goal "[| leadsTo acts A (A' Un B); leadsTo acts B B'; id: acts |] \
   18.71 +Goal "[| leadsTo acts A (A' Un B); leadsTo acts B B'; Id: acts |] \
   18.72  \   ==> leadsTo acts A (A' Un B')";
   18.73  by (blast_tac (claset() addIs [leadsTo_Un_Un, 
   18.74  			       subset_imp_leadsTo, leadsTo_Trans]) 1);
   18.75  qed "leadsTo_cancel2";
   18.76  
   18.77 -Goal "[| leadsTo acts A (A' Un B); leadsTo acts (B-A') B'; id: acts |] \
   18.78 +Goal "[| leadsTo acts A (A' Un B); leadsTo acts (B-A') B'; Id: acts |] \
   18.79  \   ==> leadsTo acts A (A' Un B')";
   18.80  by (rtac leadsTo_cancel2 1);
   18.81  by (assume_tac 2);
   18.82  by (ALLGOALS Asm_simp_tac);
   18.83  qed "leadsTo_cancel_Diff2";
   18.84  
   18.85 -Goal "[| leadsTo acts A (B Un A'); leadsTo acts B B'; id: acts |] \
   18.86 +Goal "[| leadsTo acts A (B Un A'); leadsTo acts B B'; Id: acts |] \
   18.87  \   ==> leadsTo acts A (B' Un A')";
   18.88  by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
   18.89  by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1);
   18.90  qed "leadsTo_cancel1";
   18.91  
   18.92 -Goal "[| leadsTo acts A (B Un A'); leadsTo acts (B-A') B'; id: acts |] \
   18.93 +Goal "[| leadsTo acts A (B Un A'); leadsTo acts (B-A') B'; Id: acts |] \
   18.94  \   ==> leadsTo acts A (B' Un A')";
   18.95  by (rtac leadsTo_cancel1 1);
   18.96  by (assume_tac 2);
   18.97 @@ -264,7 +264,7 @@
   18.98  
   18.99  (** PSP: Progress-Safety-Progress **)
  18.100  
  18.101 -(*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:acts. *)
  18.102 +(*Special case of PSP: Misra's "stable conjunction".  Doesn't need Id:acts. *)
  18.103  Goalw [stable_def]
  18.104     "[| leadsTo acts A A'; stable acts B |] \
  18.105  \   ==> leadsTo acts (A Int B) (A' Int B)";
  18.106 @@ -290,7 +290,7 @@
  18.107  by (blast_tac (claset() addIs [transient_strengthen]) 1);
  18.108  qed "psp_ensures";
  18.109  
  18.110 -Goal "[| leadsTo acts A A'; constrains acts B B'; id: acts |] \
  18.111 +Goal "[| leadsTo acts A A'; constrains acts B B'; Id: acts |] \
  18.112  \           ==> leadsTo acts (A Int B) ((A' Int B) Un (B' - B))";
  18.113  by (etac leadsTo_induct 1);
  18.114  by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
  18.115 @@ -304,14 +304,14 @@
  18.116  by (blast_tac (claset() addIs [leadsTo_Basis, psp_ensures]) 1);
  18.117  qed "psp";
  18.118  
  18.119 -Goal "[| leadsTo acts A A'; constrains acts B B'; id: acts |] \
  18.120 +Goal "[| leadsTo acts A A'; constrains acts B B'; Id: acts |] \
  18.121  \   ==> leadsTo acts (B Int A) ((B Int A') Un (B' - B))";
  18.122  by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1);
  18.123  qed "psp2";
  18.124  
  18.125  
  18.126  Goalw [unless_def]
  18.127 -   "[| leadsTo acts A A'; unless acts B B'; id: acts |] \
  18.128 +   "[| leadsTo acts A A'; unless acts B B'; Id: acts |] \
  18.129  \   ==> leadsTo acts (A Int B) ((A' Int B) Un B')";
  18.130  by (dtac psp 1);
  18.131  by (assume_tac 1);
  18.132 @@ -330,7 +330,7 @@
  18.133  Goal "[| wf r;     \
  18.134  \        ALL m. leadsTo acts (A Int f-``{m})                     \
  18.135  \                            ((A Int f-``(r^-1 ^^ {m})) Un B);   \
  18.136 -\        id: acts |] \
  18.137 +\        Id: acts |] \
  18.138  \     ==> leadsTo acts (A Int f-``{m}) B";
  18.139  by (eres_inst_tac [("a","m")] wf_induct 1);
  18.140  by (subgoal_tac "leadsTo acts (A Int (f -`` (r^-1 ^^ {x}))) B" 1);
  18.141 @@ -345,7 +345,7 @@
  18.142  Goal "[| wf r;     \
  18.143  \        ALL m. leadsTo acts (A Int f-``{m})                     \
  18.144  \                            ((A Int f-``(r^-1 ^^ {m})) Un B);   \
  18.145 -\        id: acts |] \
  18.146 +\        Id: acts |] \
  18.147  \     ==> leadsTo acts A B";
  18.148  by (res_inst_tac [("t", "A")] subst 1);
  18.149  by (rtac leadsTo_UN 2);
  18.150 @@ -358,7 +358,7 @@
  18.151  Goal "[| wf r;     \
  18.152  \        ALL m:I. leadsTo acts (A Int f-``{m})                   \
  18.153  \                              ((A Int f-``(r^-1 ^^ {m})) Un B);   \
  18.154 -\        id: acts |] \
  18.155 +\        Id: acts |] \
  18.156  \     ==> leadsTo acts A ((A - (f-``I)) Un B)";
  18.157  by (etac leadsTo_wf_induct 1);
  18.158  by Safe_tac;
  18.159 @@ -371,7 +371,7 @@
  18.160  (*Alternative proof is via the lemma leadsTo acts (A Int f-``(lessThan m)) B*)
  18.161  Goal "[| ALL m. leadsTo acts (A Int f-``{m})                     \
  18.162  \                            ((A Int f-``(lessThan m)) Un B);   \
  18.163 -\        id: acts |] \
  18.164 +\        Id: acts |] \
  18.165  \     ==> leadsTo acts A B";
  18.166  by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
  18.167  by (assume_tac 2);
  18.168 @@ -380,7 +380,7 @@
  18.169  
  18.170  Goal "[| ALL m:(greaterThan l). leadsTo acts (A Int f-``{m})   \
  18.171  \                                  ((A Int f-``(lessThan m)) Un B);   \
  18.172 -\        id: acts |] \
  18.173 +\        Id: acts |] \
  18.174  \     ==> leadsTo acts A ((A Int (f-``(atMost l))) Un B)";
  18.175  by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
  18.176  by (rtac (wf_less_than RS bounded_induct) 1);
  18.177 @@ -390,7 +390,7 @@
  18.178  
  18.179  Goal "[| ALL m:(lessThan l). leadsTo acts (A Int f-``{m})   \
  18.180  \                              ((A Int f-``(greaterThan m)) Un B);   \
  18.181 -\        id: acts |] \
  18.182 +\        Id: acts |] \
  18.183  \     ==> leadsTo acts A ((A Int (f-``(atLeast l))) Un B)";
  18.184  by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
  18.185      (wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
  18.186 @@ -416,13 +416,13 @@
  18.187  qed "leadsTo_subset";
  18.188  
  18.189  (*Misra's property W2*)
  18.190 -Goal "id: acts ==> leadsTo acts A B = (A <= wlt acts B)";
  18.191 +Goal "Id: acts ==> leadsTo acts A B = (A <= wlt acts B)";
  18.192  by (blast_tac (claset() addSIs [leadsTo_subset, 
  18.193  				wlt_leadsTo RS leadsTo_weaken_L]) 1);
  18.194  qed "leadsTo_eq_subset_wlt";
  18.195  
  18.196  (*Misra's property W4*)
  18.197 -Goal "id: acts ==> B <= wlt acts B";
  18.198 +Goal "Id: acts ==> B <= wlt acts B";
  18.199  by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym,
  18.200  				      subset_imp_leadsTo]) 1);
  18.201  qed "wlt_increasing";
  18.202 @@ -439,7 +439,7 @@
  18.203  
  18.204  
  18.205  (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
  18.206 -Goal "[| leadsTo acts A A';  id: acts |] ==> \
  18.207 +Goal "[| leadsTo acts A A';  Id: acts |] ==> \
  18.208  \      EX B. A<=B & leadsTo acts B A' & constrains acts (B-A') (B Un A')";
  18.209  by (etac leadsTo_induct 1);
  18.210  (*Basis*)
  18.211 @@ -459,7 +459,7 @@
  18.212  
  18.213  
  18.214  (*Misra's property W5*)
  18.215 -Goal "id: acts ==> constrains acts (wlt acts B - B) (wlt acts B)";
  18.216 +Goal "Id: acts ==> constrains acts (wlt acts B - B) (wlt acts B)";
  18.217  by (forward_tac [wlt_leadsTo RS leadsTo_123] 1);
  18.218  by (Clarify_tac 1);
  18.219  by (subgoal_tac "Ba = wlt acts B" 1);
  18.220 @@ -472,7 +472,7 @@
  18.221  (*** Completion: Binary and General Finite versions ***)
  18.222  
  18.223  Goal "[| leadsTo acts A A';  stable acts A';   \
  18.224 -\        leadsTo acts B B';  stable acts B';  id: acts |] \
  18.225 +\        leadsTo acts B B';  stable acts B';  Id: acts |] \
  18.226  \   ==> leadsTo acts (A Int B) (A' Int B')";
  18.227  by (subgoal_tac "stable acts (wlt acts B')" 1);
  18.228  by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
  18.229 @@ -491,7 +491,7 @@
  18.230  qed "stable_completion";
  18.231  
  18.232  
  18.233 -Goal "[| finite I;  id: acts |]                     \
  18.234 +Goal "[| finite I;  Id: acts |]                     \
  18.235  \   ==> (ALL i:I. leadsTo acts (A i) (A' i)) -->  \
  18.236  \       (ALL i:I. stable acts (A' i)) -->         \
  18.237  \       leadsTo acts (INT i:I. A i) (INT i:I. A' i)";
  18.238 @@ -506,7 +506,7 @@
  18.239  Goal "[| W = wlt acts (B' Un C);     \
  18.240  \      leadsTo acts A (A' Un C);  constrains acts A' (A' Un C);   \
  18.241  \      leadsTo acts B (B' Un C);  constrains acts B' (B' Un C);   \
  18.242 -\      id: acts |] \
  18.243 +\      Id: acts |] \
  18.244  \   ==> leadsTo acts (A Int B) ((A' Int B') Un C)";
  18.245  by (subgoal_tac "constrains acts (W-C) (W Un B' Un C)" 1);
  18.246  by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] 
  18.247 @@ -533,7 +533,7 @@
  18.248  bind_thm("completion", refl RS result());
  18.249  
  18.250  
  18.251 -Goal "[| finite I;  id: acts |] \
  18.252 +Goal "[| finite I;  Id: acts |] \
  18.253  \   ==> (ALL i:I. leadsTo acts (A i) (A' i Un C)) -->  \
  18.254  \       (ALL i:I. constrains acts (A' i) (A' i Un C)) --> \
  18.255  \       leadsTo acts (INT i:I. A i) ((INT i:I. A' i) Un C)";