# HG changeset patch # User nipkow # Date 907331319 -7200 # Node ID a82a038a3e7a6b859a65d17fc2eadc68e65bba0f # Parent 5db9e2343ade30fa93233e32a9c7ee5e4db2ce21 id <-> Id diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/Fun.ML --- 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); diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/Fun.thy --- 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" diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/IMP/Denotation.thy --- 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 - - diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/Lex/NA.thy --- 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 diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/Lex/RegExp2NAe.ML --- 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); diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/RelPow.thy --- 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 diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/Relation.ML --- 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" diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/Relation.thy --- 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}" diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/Trancl.ML --- 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]; diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/Trancl.thy --- 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 diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/UNITY/Channel.thy --- 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))" diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/UNITY/Common.ML --- 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(); diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/UNITY/Token.thy --- 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 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"; diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/UNITY/Traces.thy --- 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)" diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/UNITY/UNITY.ML --- 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"; diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/UNITY/Union.ML --- 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); diff -r 5db9e2343ade -r a82a038a3e7a src/HOL/UNITY/WFair.ML --- 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)";