--- a/src/HOL/Fun.ML Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/Fun.ML Fri Oct 02 14:28:39 1998 +0200
@@ -31,10 +31,10 @@
qed "bchoice";
-section "Id";
+section "id";
-qed_goalw "Id_apply" thy [Id_def] "Id x = x" (K [rtac refl 1]);
-Addsimps [Id_apply];
+qed_goalw "id_apply" thy [id_def] "id x = x" (K [rtac refl 1]);
+Addsimps [id_apply];
section "o";
@@ -46,13 +46,13 @@
qed_goalw "o_assoc" thy [o_def] "f o (g o h) = f o g o h"
(K [rtac ext 1, rtac refl 1]);
-qed_goalw "Id_o" thy [Id_def] "Id o g = g"
+qed_goalw "id_o" thy [id_def] "id o g = g"
(K [rtac ext 1, Simp_tac 1]);
-Addsimps [Id_o];
+Addsimps [id_o];
-qed_goalw "o_Id" thy [Id_def] "f o Id = f"
+qed_goalw "o_id" thy [id_def] "f o id = f"
(K [rtac ext 1, Simp_tac 1]);
-Addsimps [o_Id];
+Addsimps [o_id];
Goalw [o_def] "(f o g)``r = f``(g``r)";
by (Blast_tac 1);
--- a/src/HOL/Fun.thy Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/Fun.thy Fri Oct 02 14:28:39 1998 +0200
@@ -12,7 +12,7 @@
(subset_refl,subset_trans,subset_antisym,psubset_eq)
consts
- Id :: 'a => 'a
+ id :: 'a => 'a
o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55)
inj, surj :: ('a => 'b) => bool (*inj/surjective*)
inj_on :: ['a => 'b, 'a set] => bool
@@ -37,7 +37,7 @@
defs
- Id_def "Id == %x. x"
+ id_def "id == %x. x"
o_def "f o g == %x. f(g(x))"
inj_def "inj f == ! x y. f(x)=f(y) --> x=y"
inj_on_def "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
--- a/src/HOL/IMP/Denotation.thy Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/IMP/Denotation.thy Fri Oct 02 14:28:39 1998 +0200
@@ -19,7 +19,7 @@
C :: com => com_den
primrec
- C_skip "C(SKIP) = id"
+ C_skip "C(SKIP) = Id"
C_assign "C(x := a) = {(s,t). t = s[x:=a(s)]}"
C_comp "C(c0 ; c1) = C(c1) O C(c0)"
C_if "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un
@@ -27,5 +27,3 @@
C_while "C(WHILE b DO c) = lfp (Gamma b (C c))"
end
-
-
--- a/src/HOL/Lex/NA.thy Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/Lex/NA.thy Fri Oct 02 14:28:39 1998 +0200
@@ -25,7 +25,7 @@
consts steps :: "('a,'s)na => 'a list => ('s * 's)set"
primrec
-"steps A [] = id"
+"steps A [] = Id"
"steps A (a#w) = steps A w O step A a"
end
--- a/src/HOL/Lex/RegExp2NAe.ML Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/Lex/RegExp2NAe.ML Fri Oct 02 14:28:39 1998 +0200
@@ -152,7 +152,7 @@
(***** Epsilonhuelle des Startzustands *****)
Goal
- "R^* = id Un (R^* O R)";
+ "R^* = Id Un (R^* O R)";
by (rtac set_ext 1);
by (split_all_tac 1);
by (rtac iffI 1);
--- a/src/HOL/RelPow.thy Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/RelPow.thy Fri Oct 02 14:28:39 1998 +0200
@@ -9,7 +9,7 @@
RelPow = Nat +
primrec
- "R^0 = id"
+ "R^0 = Id"
"R^(Suc n) = R O (R^n)"
end
--- a/src/HOL/Relation.ML Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/Relation.ML Fri Oct 02 14:28:39 1998 +0200
@@ -8,22 +8,22 @@
(** Identity relation **)
-Goalw [id_def] "(a,a) : id";
+Goalw [Id_def] "(a,a) : Id";
by (Blast_tac 1);
-qed "idI";
+qed "IdI";
-val major::prems = Goalw [id_def]
- "[| p: id; !!x.[| p = (x,x) |] ==> P \
+val major::prems = Goalw [Id_def]
+ "[| p: Id; !!x.[| p = (x,x) |] ==> P \
\ |] ==> P";
by (rtac (major RS CollectE) 1);
by (etac exE 1);
by (eresolve_tac prems 1);
-qed "idE";
+qed "IdE";
-Goalw [id_def] "(a,b):id = (a=b)";
+Goalw [Id_def] "(a,b):Id = (a=b)";
by (Blast_tac 1);
-qed "pair_in_id_conv";
-Addsimps [pair_in_id_conv];
+qed "pair_in_Id_conv";
+Addsimps [pair_in_Id_conv];
(** Composition of two relations **)
@@ -51,18 +51,18 @@
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1));
qed "compEpair";
-AddIs [compI, idI];
-AddSEs [compE, idE];
+AddIs [compI, IdI];
+AddSEs [compE, IdE];
-Goal "R O id = R";
+Goal "R O Id = R";
by (Fast_tac 1);
-qed "R_O_id";
+qed "R_O_Id";
-Goal "id O R = R";
+Goal "Id O R = R";
by (Fast_tac 1);
-qed "id_O_R";
+qed "Id_O_R";
-Addsimps [R_O_id,id_O_R];
+Addsimps [R_O_Id,Id_O_R];
Goal "(R O S) O T = R O (S O T)";
by (Blast_tac 1);
@@ -124,10 +124,10 @@
by (Blast_tac 1);
qed "converse_comp";
-Goal "id^-1 = id";
+Goal "Id^-1 = Id";
by (Blast_tac 1);
-qed "converse_id";
-Addsimps [converse_id];
+qed "converse_Id";
+Addsimps [converse_Id];
(** Domain **)
@@ -147,10 +147,10 @@
AddIs [DomainI];
AddSEs [DomainE];
-Goal "Domain id = UNIV";
+Goal "Domain Id = UNIV";
by (Blast_tac 1);
-qed "Domain_id";
-Addsimps [Domain_id];
+qed "Domain_Id";
+Addsimps [Domain_Id];
(** Range **)
@@ -167,10 +167,10 @@
AddIs [RangeI];
AddSEs [RangeE];
-Goal "Range id = UNIV";
+Goal "Range Id = UNIV";
by (Blast_tac 1);
-qed "Range_id";
-Addsimps [Range_id];
+qed "Range_Id";
+Addsimps [Range_Id];
(*** Image of a set under a relation ***)
@@ -213,11 +213,11 @@
Addsimps [Image_empty];
-Goal "id ^^ A = A";
+Goal "Id ^^ A = A";
by (Blast_tac 1);
-qed "Image_id";
+qed "Image_Id";
-Addsimps [Image_id];
+Addsimps [Image_Id];
qed_goal "Image_Int_subset" thy
"R ^^ (A Int B) <= R ^^ A Int R ^^ B"
--- a/src/HOL/Relation.thy Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/Relation.thy Fri Oct 02 14:28:39 1998 +0200
@@ -6,7 +6,7 @@
Relation = Prod +
consts
- id :: "('a * 'a)set" (*the identity relation*)
+ Id :: "('a * 'a)set" (*the identity relation*)
O :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
converse :: "('a*'b) set => ('b*'a) set" ("(_^-1)" [1000] 999)
"^^" :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
@@ -15,7 +15,7 @@
trans :: "('a * 'a)set => bool" (*transitivity predicate*)
Univalent :: "('a * 'b)set => bool"
defs
- id_def "id == {p. ? x. p = (x,x)}"
+ Id_def "Id == {p. ? x. p = (x,x)}"
comp_def "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
converse_def "r^-1 == {(y,x). (x,y):r}"
Domain_def "Domain(r) == {x. ? y. (x,y):r}"
--- a/src/HOL/Trancl.ML Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/Trancl.ML Fri Oct 02 14:28:39 1998 +0200
@@ -10,7 +10,7 @@
(** The relation rtrancl **)
-Goal "mono(%s. id Un (r O s))";
+Goal "mono(%s. Id Un (r O s))";
by (rtac monoI 1);
by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
qed "rtrancl_fun_mono";
@@ -343,6 +343,6 @@
(K [auto_tac (claset() addEs [trancl_induct], simpset())]);
Addsimps[trancl_empty];
-qed_goal "rtrancl_empty" Trancl.thy "{}^* = id"
+qed_goal "rtrancl_empty" Trancl.thy "{}^* = Id"
(K [rtac (reflcl_trancl RS subst) 1, Simp_tac 1]);
Addsimps[rtrancl_empty];
--- a/src/HOL/Trancl.thy Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/Trancl.thy Fri Oct 02 14:28:39 1998 +0200
@@ -17,7 +17,7 @@
constdefs
rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [1000] 999)
- "r^* == lfp(%s. id Un (r O s))"
+ "r^* == lfp(%s. Id Un (r O s))"
trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [1000] 999)
"r^+ == r O rtrancl(r)"
@@ -26,6 +26,6 @@
reflcl :: "('a*'a)set => ('a*'a)set" ("(_^=)" [1000] 999)
translations
- "r^=" == "r Un id"
+ "r^=" == "r Un Id"
end
--- a/src/HOL/UNITY/Channel.thy Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/UNITY/Channel.thy Fri Oct 02 14:28:39 1998 +0200
@@ -18,7 +18,7 @@
rules
- skip "id: acts"
+ skip "Id: acts"
UC1 "constrains acts (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))"
--- a/src/HOL/UNITY/Common.ML Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/UNITY/Common.ML Fri Oct 02 14:28:39 1998 +0200
@@ -31,7 +31,7 @@
(*** Some programs that implement the safety property above ***)
(*This one is just Skip*)
-Goal "constrains {id} {m} (maxfg m)";
+Goal "constrains {Id} {m} (maxfg m)";
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
fasc, gasc]) 1);
result();
--- a/src/HOL/UNITY/Token.thy Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/UNITY/Token.thy Fri Oct 02 14:28:39 1998 +0200
@@ -43,7 +43,7 @@
assumes
N_positive "0<N"
- skip "id: acts"
+ skip "Id: acts"
TR2 "!!i. constrains acts (T i) (T i Un H i)"
--- a/src/HOL/UNITY/Traces.ML Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML Fri Oct 02 14:28:39 1998 +0200
@@ -17,18 +17,18 @@
Rep_Program_inverse, Abs_Program_inverse];
-Goal "id: Acts prg";
+Goal "Id: Acts prg";
by (cut_inst_tac [("x", "prg")] Rep_Program 1);
by (auto_tac (claset(), rep_ss));
-qed "id_in_Acts";
-AddIffs [id_in_Acts];
+qed "Id_in_Acts";
+AddIffs [Id_in_Acts];
Goal "Init (mk_program (init,acts)) = init";
by (auto_tac (claset(), rep_ss));
qed "Init_eq";
-Goal "Acts (mk_program (init,acts)) = insert id acts";
+Goal "Acts (mk_program (init,acts)) = insert Id acts";
by (auto_tac (claset(), rep_ss));
qed "Acts_eq";
@@ -47,7 +47,7 @@
val [rew] = goal thy
"[| prg == mk_program (init,acts) |] \
-\ ==> Init prg = init & Acts prg = insert id acts";
+\ ==> Init prg = init & Acts prg = insert Id acts";
by (rewtac rew);
by Auto_tac;
qed "def_prg_simps";
--- a/src/HOL/UNITY/Traces.thy Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/UNITY/Traces.thy Fri Oct 02 14:28:39 1998 +0200
@@ -25,11 +25,11 @@
typedef (Program)
- 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). id:acts}"
+ 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
constdefs
mk_program :: "('a set * ('a * 'a)set set) => 'a program"
- "mk_program == %(init, acts). Abs_Program (init, insert id acts)"
+ "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
Init :: "'a program => 'a set"
"Init prg == fst (Rep_Program prg)"
--- a/src/HOL/UNITY/UNITY.ML Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/UNITY/UNITY.ML Fri Oct 02 14:28:39 1998 +0200
@@ -97,12 +97,12 @@
by (Blast_tac 1);
qed "all_constrains_INT";
-Goalw [constrains_def] "[| constrains acts A A'; id: acts |] ==> A<=A'";
+Goalw [constrains_def] "[| constrains acts A A'; Id: acts |] ==> A<=A'";
by (Blast_tac 1);
qed "constrains_imp_subset";
Goalw [constrains_def]
- "[| id: acts; constrains acts A B; constrains acts B C |] \
+ "[| Id: acts; constrains acts A B; constrains acts B C |] \
\ ==> constrains acts A C";
by (Blast_tac 1);
qed "constrains_trans";
@@ -160,7 +160,7 @@
Goalw [constrains_def]
- "[| constrains acts A (A' Un B); constrains acts B B'; id: acts |] \
+ "[| constrains acts A (A' Un B); constrains acts B B'; Id: acts |] \
\ ==> constrains acts A (A' Un B')";
by (Blast_tac 1);
qed "constrains_cancel";
--- a/src/HOL/UNITY/Union.ML Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/UNITY/Union.ML Fri Oct 02 14:28:39 1998 +0200
@@ -21,7 +21,7 @@
by (simp_tac (simpset() addsimps [JOIN_def]) 1);
qed "Init_JN";
-Goal "Acts (JN i:I. prg i) = insert id (UN i:I. Acts (prg i))";
+Goal "Acts (JN i:I. prg i) = insert Id (UN i:I. Acts (prg i))";
by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
qed "Acts_JN";
@@ -142,7 +142,7 @@
qed "ensures_Join";
Goalw [stable_def, constrains_def, Join_def]
- "[| stable (Acts prgF) A; constrains (Acts prgG) A A'; id: Acts prgG |] \
+ "[| stable (Acts prgF) A; constrains (Acts prgG) A A'; Id: Acts prgG |] \
\ ==> constrains (Acts (Join prgF prgG)) A A'";
by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
by (Blast_tac 1);
--- a/src/HOL/UNITY/WFair.ML Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML Fri Oct 02 14:28:39 1998 +0200
@@ -125,7 +125,7 @@
qed "leadsTo_induct";
-Goal "[| A<=B; id: acts |] ==> leadsTo acts A B";
+Goal "[| A<=B; Id: acts |] ==> leadsTo acts A B";
by (rtac leadsTo_Basis 1);
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
by (Blast_tac 1);
@@ -136,7 +136,7 @@
(*There's a direct proof by leadsTo_Trans and subset_imp_leadsTo, but it
- needs the extra premise id:acts*)
+ needs the extra premise Id:acts*)
Goal "leadsTo acts A A' ==> A'<=B' --> leadsTo acts A B'";
by (etac leadsTo_induct 1);
by (Clarify_tac 3);
@@ -146,30 +146,30 @@
qed_spec_mp "leadsTo_weaken_R";
-Goal "[| leadsTo acts A A'; B<=A; id: acts |] ==> \
+Goal "[| leadsTo acts A A'; B<=A; Id: acts |] ==> \
\ leadsTo acts B A'";
by (blast_tac (claset() addIs [leadsTo_Basis, leadsTo_Trans,
subset_imp_leadsTo]) 1);
qed_spec_mp "leadsTo_weaken_L";
(*Distributes over binary unions*)
-Goal "id: acts ==> \
+Goal "Id: acts ==> \
\ leadsTo acts (A Un B) C = (leadsTo acts A C & leadsTo acts B C)";
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
qed "leadsTo_Un_distrib";
-Goal "id: acts ==> \
+Goal "Id: acts ==> \
\ leadsTo acts (UN i:I. A i) B = (ALL i : I. leadsTo acts (A i) B)";
by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
qed "leadsTo_UN_distrib";
-Goal "id: acts ==> \
+Goal "Id: acts ==> \
\ leadsTo acts (Union S) B = (ALL A : S. leadsTo acts A B)";
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
qed "leadsTo_Union_distrib";
-Goal "[| leadsTo acts A A'; id: acts; B<=A; A'<=B' |] \
+Goal "[| leadsTo acts A A'; Id: acts; B<=A; A'<=B' |] \
\ ==> leadsTo acts B B'";
by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
leadsTo_Trans]) 1);
@@ -177,7 +177,7 @@
(*Set difference: maybe combine with leadsTo_weaken_L??*)
-Goal "[| leadsTo acts (A-B) C; leadsTo acts B C; id: acts |] \
+Goal "[| leadsTo acts (A-B) C; leadsTo acts B C; Id: acts |] \
\ ==> leadsTo acts A C";
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
qed "leadsTo_Diff";
@@ -220,26 +220,26 @@
(** The cancellation law **)
-Goal "[| leadsTo acts A (A' Un B); leadsTo acts B B'; id: acts |] \
+Goal "[| leadsTo acts A (A' Un B); leadsTo acts B B'; Id: acts |] \
\ ==> leadsTo acts A (A' Un B')";
by (blast_tac (claset() addIs [leadsTo_Un_Un,
subset_imp_leadsTo, leadsTo_Trans]) 1);
qed "leadsTo_cancel2";
-Goal "[| leadsTo acts A (A' Un B); leadsTo acts (B-A') B'; id: acts |] \
+Goal "[| leadsTo acts A (A' Un B); leadsTo acts (B-A') B'; Id: acts |] \
\ ==> leadsTo acts A (A' Un B')";
by (rtac leadsTo_cancel2 1);
by (assume_tac 2);
by (ALLGOALS Asm_simp_tac);
qed "leadsTo_cancel_Diff2";
-Goal "[| leadsTo acts A (B Un A'); leadsTo acts B B'; id: acts |] \
+Goal "[| leadsTo acts A (B Un A'); leadsTo acts B B'; Id: acts |] \
\ ==> leadsTo acts A (B' Un A')";
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1);
qed "leadsTo_cancel1";
-Goal "[| leadsTo acts A (B Un A'); leadsTo acts (B-A') B'; id: acts |] \
+Goal "[| leadsTo acts A (B Un A'); leadsTo acts (B-A') B'; Id: acts |] \
\ ==> leadsTo acts A (B' Un A')";
by (rtac leadsTo_cancel1 1);
by (assume_tac 2);
@@ -264,7 +264,7 @@
(** PSP: Progress-Safety-Progress **)
-(*Special case of PSP: Misra's "stable conjunction". Doesn't need id:acts. *)
+(*Special case of PSP: Misra's "stable conjunction". Doesn't need Id:acts. *)
Goalw [stable_def]
"[| leadsTo acts A A'; stable acts B |] \
\ ==> leadsTo acts (A Int B) (A' Int B)";
@@ -290,7 +290,7 @@
by (blast_tac (claset() addIs [transient_strengthen]) 1);
qed "psp_ensures";
-Goal "[| leadsTo acts A A'; constrains acts B B'; id: acts |] \
+Goal "[| leadsTo acts A A'; constrains acts B B'; Id: acts |] \
\ ==> leadsTo acts (A Int B) ((A' Int B) Un (B' - B))";
by (etac leadsTo_induct 1);
by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
@@ -304,14 +304,14 @@
by (blast_tac (claset() addIs [leadsTo_Basis, psp_ensures]) 1);
qed "psp";
-Goal "[| leadsTo acts A A'; constrains acts B B'; id: acts |] \
+Goal "[| leadsTo acts A A'; constrains acts B B'; Id: acts |] \
\ ==> leadsTo acts (B Int A) ((B Int A') Un (B' - B))";
by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1);
qed "psp2";
Goalw [unless_def]
- "[| leadsTo acts A A'; unless acts B B'; id: acts |] \
+ "[| leadsTo acts A A'; unless acts B B'; Id: acts |] \
\ ==> leadsTo acts (A Int B) ((A' Int B) Un B')";
by (dtac psp 1);
by (assume_tac 1);
@@ -330,7 +330,7 @@
Goal "[| wf r; \
\ ALL m. leadsTo acts (A Int f-``{m}) \
\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
-\ id: acts |] \
+\ Id: acts |] \
\ ==> leadsTo acts (A Int f-``{m}) B";
by (eres_inst_tac [("a","m")] wf_induct 1);
by (subgoal_tac "leadsTo acts (A Int (f -`` (r^-1 ^^ {x}))) B" 1);
@@ -345,7 +345,7 @@
Goal "[| wf r; \
\ ALL m. leadsTo acts (A Int f-``{m}) \
\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
-\ id: acts |] \
+\ Id: acts |] \
\ ==> leadsTo acts A B";
by (res_inst_tac [("t", "A")] subst 1);
by (rtac leadsTo_UN 2);
@@ -358,7 +358,7 @@
Goal "[| wf r; \
\ ALL m:I. leadsTo acts (A Int f-``{m}) \
\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
-\ id: acts |] \
+\ Id: acts |] \
\ ==> leadsTo acts A ((A - (f-``I)) Un B)";
by (etac leadsTo_wf_induct 1);
by Safe_tac;
@@ -371,7 +371,7 @@
(*Alternative proof is via the lemma leadsTo acts (A Int f-``(lessThan m)) B*)
Goal "[| ALL m. leadsTo acts (A Int f-``{m}) \
\ ((A Int f-``(lessThan m)) Un B); \
-\ id: acts |] \
+\ Id: acts |] \
\ ==> leadsTo acts A B";
by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
by (assume_tac 2);
@@ -380,7 +380,7 @@
Goal "[| ALL m:(greaterThan l). leadsTo acts (A Int f-``{m}) \
\ ((A Int f-``(lessThan m)) Un B); \
-\ id: acts |] \
+\ Id: acts |] \
\ ==> leadsTo acts A ((A Int (f-``(atMost l))) Un B)";
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
by (rtac (wf_less_than RS bounded_induct) 1);
@@ -390,7 +390,7 @@
Goal "[| ALL m:(lessThan l). leadsTo acts (A Int f-``{m}) \
\ ((A Int f-``(greaterThan m)) Un B); \
-\ id: acts |] \
+\ Id: acts |] \
\ ==> leadsTo acts A ((A Int (f-``(atLeast l))) Un B)";
by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
(wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
@@ -416,13 +416,13 @@
qed "leadsTo_subset";
(*Misra's property W2*)
-Goal "id: acts ==> leadsTo acts A B = (A <= wlt acts B)";
+Goal "Id: acts ==> leadsTo acts A B = (A <= wlt acts B)";
by (blast_tac (claset() addSIs [leadsTo_subset,
wlt_leadsTo RS leadsTo_weaken_L]) 1);
qed "leadsTo_eq_subset_wlt";
(*Misra's property W4*)
-Goal "id: acts ==> B <= wlt acts B";
+Goal "Id: acts ==> B <= wlt acts B";
by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym,
subset_imp_leadsTo]) 1);
qed "wlt_increasing";
@@ -439,7 +439,7 @@
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
-Goal "[| leadsTo acts A A'; id: acts |] ==> \
+Goal "[| leadsTo acts A A'; Id: acts |] ==> \
\ EX B. A<=B & leadsTo acts B A' & constrains acts (B-A') (B Un A')";
by (etac leadsTo_induct 1);
(*Basis*)
@@ -459,7 +459,7 @@
(*Misra's property W5*)
-Goal "id: acts ==> constrains acts (wlt acts B - B) (wlt acts B)";
+Goal "Id: acts ==> constrains acts (wlt acts B - B) (wlt acts B)";
by (forward_tac [wlt_leadsTo RS leadsTo_123] 1);
by (Clarify_tac 1);
by (subgoal_tac "Ba = wlt acts B" 1);
@@ -472,7 +472,7 @@
(*** Completion: Binary and General Finite versions ***)
Goal "[| leadsTo acts A A'; stable acts A'; \
-\ leadsTo acts B B'; stable acts B'; id: acts |] \
+\ leadsTo acts B B'; stable acts B'; Id: acts |] \
\ ==> leadsTo acts (A Int B) (A' Int B')";
by (subgoal_tac "stable acts (wlt acts B')" 1);
by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
@@ -491,7 +491,7 @@
qed "stable_completion";
-Goal "[| finite I; id: acts |] \
+Goal "[| finite I; Id: acts |] \
\ ==> (ALL i:I. leadsTo acts (A i) (A' i)) --> \
\ (ALL i:I. stable acts (A' i)) --> \
\ leadsTo acts (INT i:I. A i) (INT i:I. A' i)";
@@ -506,7 +506,7 @@
Goal "[| W = wlt acts (B' Un C); \
\ leadsTo acts A (A' Un C); constrains acts A' (A' Un C); \
\ leadsTo acts B (B' Un C); constrains acts B' (B' Un C); \
-\ id: acts |] \
+\ Id: acts |] \
\ ==> leadsTo acts (A Int B) ((A' Int B') Un C)";
by (subgoal_tac "constrains acts (W-C) (W Un B' Un C)" 1);
by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt]
@@ -533,7 +533,7 @@
bind_thm("completion", refl RS result());
-Goal "[| finite I; id: acts |] \
+Goal "[| finite I; Id: acts |] \
\ ==> (ALL i:I. leadsTo acts (A i) (A' i Un C)) --> \
\ (ALL i:I. constrains acts (A' i) (A' i Un C)) --> \
\ leadsTo acts (INT i:I. A i) ((INT i:I. A' i) Un C)";