--- a/src/HOL/UNITY/Comp.thy Sun Feb 16 12:16:07 2003 +0100
+++ b/src/HOL/UNITY/Comp.thy Sun Feb 16 12:17:40 2003 +0100
@@ -7,9 +7,9 @@
From Chandy and Sanders, "Reasoning About Program Composition",
Technical Report 2000-003, University of Florida, 2000.
-Revised by Sidi Ehmety on January 2001
+Revised by Sidi Ehmety on January 2001
-Added: a strong form of the \<subseteq> relation (component_of) and localize
+Added: a strong form of the \<subseteq> relation (component_of) and localize
*)
@@ -20,19 +20,19 @@
instance program :: (type) ord ..
defs
- component_def: "F \<le> H == \<exists>G. F Join G = H"
+ component_def: "F \<le> H == \<exists>G. F\<squnion>G = H"
strict_component_def: "(F < (H::'a program)) == (F \<le> H & F \<noteq> H)"
constdefs
component_of :: "'a program =>'a program=> bool"
(infixl "component'_of" 50)
- "F component_of H == \<exists>G. F ok G & F Join G = H"
+ "F component_of H == \<exists>G. F ok G & F\<squnion>G = H"
strict_component_of :: "'a program\<Rightarrow>'a program=> bool"
(infixl "strict'_component'_of" 50)
"F strict_component_of H == F component_of H & F\<noteq>H"
-
+
preserves :: "('a=>'b) => 'a program set"
"preserves v == \<Inter>z. stable {s. v s = z}"
@@ -45,15 +45,15 @@
subsection{*The component relation*}
-lemma componentI: "H \<le> F | H \<le> G ==> H \<le> (F Join G)"
+lemma componentI: "H \<le> F | H \<le> G ==> H \<le> (F\<squnion>G)"
apply (unfold component_def, auto)
-apply (rule_tac x = "G Join Ga" in exI)
-apply (rule_tac [2] x = "G Join F" in exI)
+apply (rule_tac x = "G\<squnion>Ga" in exI)
+apply (rule_tac [2] x = "G\<squnion>F" in exI)
apply (auto simp add: Join_ac)
done
-lemma component_eq_subset:
- "(F \<le> G) =
+lemma component_eq_subset:
+ "(F \<le> G) =
(Init G \<subseteq> Init F & Acts F \<subseteq> Acts G & AllowedActs G \<subseteq> AllowedActs F)"
apply (unfold component_def)
apply (force intro!: exI program_equalityI)
@@ -72,18 +72,18 @@
lemma SKIP_minimal: "F \<le> SKIP ==> F = SKIP"
by (auto intro!: program_equalityI simp add: component_eq_subset)
-lemma component_Join1: "F \<le> (F Join G)"
+lemma component_Join1: "F \<le> (F\<squnion>G)"
by (unfold component_def, blast)
-lemma component_Join2: "G \<le> (F Join G)"
+lemma component_Join2: "G \<le> (F\<squnion>G)"
apply (unfold component_def)
apply (simp add: Join_commute, blast)
done
-lemma Join_absorb1: "F \<le> G ==> F Join G = G"
+lemma Join_absorb1: "F \<le> G ==> F\<squnion>G = G"
by (auto simp add: component_def Join_left_absorb)
-lemma Join_absorb2: "G \<le> F ==> F Join G = F"
+lemma Join_absorb2: "G \<le> F ==> F\<squnion>G = F"
by (auto simp add: Join_ac component_def)
lemma JN_component_iff: "((JOIN I F) \<le> H) = (\<forall>i \<in> I. F i \<le> H)"
@@ -104,7 +104,7 @@
apply (blast intro!: program_equalityI)
done
-lemma Join_component_iff: "((F Join G) \<le> H) = (F \<le> H & G \<le> H)"
+lemma Join_component_iff: "((F\<squnion>G) \<le> H) = (F \<le> H & G \<le> H)"
by (simp add: component_eq_subset, blast)
lemma component_constrains: "[| F \<le> G; G \<in> A co B |] ==> F \<in> A co B"
@@ -119,20 +119,17 @@
lemma preservesI: "(!!z. F \<in> stable {s. v s = z}) ==> F \<in> preserves v"
by (unfold preserves_def, blast)
-lemma preserves_imp_eq:
+lemma preserves_imp_eq:
"[| F \<in> preserves v; act \<in> Acts F; (s,s') \<in> act |] ==> v s = v s'"
-apply (unfold preserves_def stable_def constrains_def, force)
-done
+by (unfold preserves_def stable_def constrains_def, force)
-lemma Join_preserves [iff]:
- "(F Join G \<in> preserves v) = (F \<in> preserves v & G \<in> preserves v)"
-apply (unfold preserves_def, auto)
-done
+lemma Join_preserves [iff]:
+ "(F\<squnion>G \<in> preserves v) = (F \<in> preserves v & G \<in> preserves v)"
+by (unfold preserves_def, auto)
lemma JN_preserves [iff]:
"(JOIN I F \<in> preserves v) = (\<forall>i \<in> I. F i \<in> preserves v)"
-apply (simp add: JN_stable preserves_def, blast)
-done
+by (simp add: JN_stable preserves_def, blast)
lemma SKIP_preserves [iff]: "SKIP \<in> preserves v"
by (auto simp add: preserves_def)
@@ -182,19 +179,19 @@
(** Some lemmas used only in Client.ML **)
lemma stable_localTo_stable2:
- "[| F \<in> stable {s. P (v s) (w s)};
- G \<in> preserves v; G \<in> preserves w |]
- ==> F Join G \<in> stable {s. P (v s) (w s)}"
+ "[| F \<in> stable {s. P (v s) (w s)};
+ G \<in> preserves v; G \<in> preserves w |]
+ ==> F\<squnion>G \<in> stable {s. P (v s) (w s)}"
apply simp
apply (subgoal_tac "G \<in> preserves (funPair v w) ")
- prefer 2 apply simp
-apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto)
+ prefer 2 apply simp
+apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD],
+ auto)
done
lemma Increasing_preserves_Stable:
- "[| F \<in> stable {s. v s \<le> w s}; G \<in> preserves v;
- F Join G \<in> Increasing w |]
- ==> F Join G \<in> Stable {s. v s \<le> w s}"
+ "[| F \<in> stable {s. v s \<le> w s}; G \<in> preserves v; F\<squnion>G \<in> Increasing w |]
+ ==> F\<squnion>G \<in> Stable {s. v s \<le> w s}"
apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib)
apply (blast intro: constrains_weaken)
(*The G case remains*)
@@ -204,8 +201,7 @@
apply (erule_tac V = "\<forall>act \<in> Acts F. ?P act" in thin_rl)
apply (erule_tac V = "\<forall>z. \<forall>act \<in> Acts F. ?P z act" in thin_rl)
apply (subgoal_tac "v x = v xa")
-prefer 2 apply blast
-apply auto
+ apply auto
apply (erule order_trans, blast)
done
@@ -225,7 +221,7 @@
lemma component_of_SKIP [simp]: "SKIP component_of F"
by (unfold component_of_def, auto)
-lemma component_of_trans:
+lemma component_of_trans:
"[| F component_of G; G component_of H |] ==> F component_of H"
apply (unfold component_of_def)
apply (blast intro: Join_assoc [symmetric])
@@ -241,8 +237,8 @@
lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F"
by (simp add: localize_def)
-lemma localize_AllowedActs_eq [simp]:
- "AllowedActs (localize v F) = AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G)"
+lemma localize_AllowedActs_eq [simp]:
+ "AllowedActs (localize v F) = AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G)"
by (unfold localize_def, auto)
end
--- a/src/HOL/UNITY/ELT.thy Sun Feb 16 12:16:07 2003 +0100
+++ b/src/HOL/UNITY/ELT.thy Sun Feb 16 12:17:40 2003 +0100
@@ -127,8 +127,7 @@
(*Useful with cancellation, disjunction*)
lemma leadsETo_Un_duplicate:
"F : A leadsTo[CC] (A' Un A') ==> F : A leadsTo[CC] A'"
-apply (simp add: Un_ac)
-done
+by (simp add: Un_ac)
lemma leadsETo_Un_duplicate2:
"F : A leadsTo[CC] (A' Un C Un C) ==> F : A leadsTo[CC] (A' Un C)"
@@ -195,12 +194,12 @@
lemma single_leadsETo_I:
"(!!x. x : A ==> F : {x} leadsTo[CC] B) ==> F : A leadsTo[CC] B"
-apply (subst UN_singleton [symmetric], rule leadsETo_UN, blast)
-done
+by (subst UN_singleton [symmetric], rule leadsETo_UN, blast)
lemma subset_imp_leadsETo: "A<=B ==> F : A leadsTo[CC] B"
-by (simp add: subset_imp_ensures [THEN leadsETo_Basis] Diff_eq_empty_iff [THEN iffD2])
+by (simp add: subset_imp_ensures [THEN leadsETo_Basis]
+ Diff_eq_empty_iff [THEN iffD2])
lemmas empty_leadsETo = empty_subsetI [THEN subset_imp_leadsETo, simp]
@@ -210,37 +209,33 @@
lemma leadsETo_weaken_R:
"[| F : A leadsTo[CC] A'; A'<=B' |] ==> F : A leadsTo[CC] B'"
-apply (blast intro: subset_imp_leadsETo leadsETo_Trans)
-done
+by (blast intro: subset_imp_leadsETo leadsETo_Trans)
lemma leadsETo_weaken_L [rule_format]:
"[| F : A leadsTo[CC] A'; B<=A |] ==> F : B leadsTo[CC] A'"
-apply (blast intro: leadsETo_Trans subset_imp_leadsETo)
-done
+by (blast intro: leadsETo_Trans subset_imp_leadsETo)
(*Distributes over binary unions*)
lemma leadsETo_Un_distrib:
"F : (A Un B) leadsTo[CC] C =
(F : A leadsTo[CC] C & F : B leadsTo[CC] C)"
-apply (blast intro: leadsETo_Un leadsETo_weaken_L)
-done
+by (blast intro: leadsETo_Un leadsETo_weaken_L)
lemma leadsETo_UN_distrib:
"F : (UN i:I. A i) leadsTo[CC] B =
(ALL i : I. F : (A i) leadsTo[CC] B)"
-apply (blast intro: leadsETo_UN leadsETo_weaken_L)
-done
+by (blast intro: leadsETo_UN leadsETo_weaken_L)
lemma leadsETo_Union_distrib:
"F : (Union S) leadsTo[CC] B = (ALL A : S. F : A leadsTo[CC] B)"
-apply (blast intro: leadsETo_Union leadsETo_weaken_L)
-done
+by (blast intro: leadsETo_Union leadsETo_weaken_L)
lemma leadsETo_weaken:
"[| F : A leadsTo[CC'] A'; B<=A; A'<=B'; CC' <= CC |]
==> F : B leadsTo[CC] B'"
apply (drule leadsETo_mono [THEN subsetD], assumption)
-apply (blast del: subsetCE intro: leadsETo_weaken_R leadsETo_weaken_L leadsETo_Trans)
+apply (blast del: subsetCE
+ intro: leadsETo_weaken_R leadsETo_weaken_L leadsETo_Trans)
done
lemma leadsETo_givenBy:
@@ -286,7 +281,6 @@
done
-
(** PSP: Progress-Safety-Progress **)
(*Special case of PSP: Misra's "stable conjunction"*)
@@ -299,7 +293,8 @@
prefer 2 apply (blast intro: leadsETo_Trans)
apply (rule leadsETo_Basis)
prefer 2 apply (force simp add: Diff_Int_distrib2 [symmetric])
-apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric])
+apply (simp add: ensures_def Diff_Int_distrib2 [symmetric]
+ Int_Un_distrib2 [symmetric])
apply (blast intro: transient_strengthen constrains_Int)
done
@@ -339,8 +334,8 @@
(*??IS THIS NEEDED?? or is it just an example of what's provable??*)
lemma gen_leadsETo_imp_Join_leadsETo:
"[| F: (A leadsTo[givenBy v] B); G : preserves v;
- F Join G : stable C |]
- ==> F Join G : ((C Int A) leadsTo[(%D. C Int D) ` givenBy v] B)"
+ F\<squnion>G : stable C |]
+ ==> F\<squnion>G : ((C Int A) leadsTo[(%D. C Int D) ` givenBy v] B)"
apply (erule leadsETo_induct)
prefer 3
apply (subst Int_Union)
@@ -348,7 +343,8 @@
prefer 2
apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
apply (rule leadsETo_Basis)
-apply (auto simp add: Diff_eq_empty_iff [THEN iffD2] Int_Diff ensures_def givenBy_eq_Collect Join_transient)
+apply (auto simp add: Diff_eq_empty_iff [THEN iffD2]
+ Int_Diff ensures_def givenBy_eq_Collect Join_transient)
prefer 3 apply (blast intro: transient_strengthen)
apply (drule_tac [2] P1 = P in preserves_subset_stable [THEN subsetD])
apply (drule_tac P1 = P in preserves_subset_stable [THEN subsetD])
@@ -363,8 +359,8 @@
lemma leadsETo_subset_leadsTo: "(A leadsTo[CC] B) <= (A leadsTo B)"
apply safe
apply (erule leadsETo_induct)
-prefer 3 apply (blast intro: leadsTo_Union)
-prefer 2 apply (blast intro: leadsTo_Trans, blast)
+ prefer 3 apply (blast intro: leadsTo_Union)
+ prefer 2 apply (blast intro: leadsTo_Trans, blast)
done
lemma leadsETo_UNIV_eq_leadsTo: "(A leadsTo[UNIV] B) = (A leadsTo B)"
@@ -372,8 +368,8 @@
apply (erule leadsETo_subset_leadsTo [THEN subsetD])
(*right-to-left case*)
apply (erule leadsTo_induct)
-prefer 3 apply (blast intro: leadsETo_Union)
-prefer 2 apply (blast intro: leadsETo_Trans, blast)
+ prefer 3 apply (blast intro: leadsETo_Union)
+ prefer 2 apply (blast intro: leadsETo_Trans, blast)
done
(**** weak ****)
@@ -420,8 +416,7 @@
(*Lets us look at the starting state*)
lemma single_LeadsETo_I:
"(!!s. s : A ==> F : {s} LeadsTo[CC] B) ==> F : A LeadsTo[CC] B"
-apply (subst UN_singleton [symmetric], rule LeadsETo_UN, blast)
-done
+by (subst UN_singleton [symmetric], rule LeadsETo_UN, blast)
lemma subset_imp_LeadsETo:
"A <= B ==> F : A LeadsTo[CC] B"
@@ -482,10 +477,9 @@
(**** EXTEND/PROJECT PROPERTIES ****)
-lemma (in Extend) givenBy_o_eq_extend_set: "givenBy (v o f) = extend_set h ` (givenBy v)"
-apply (simp (no_asm) add: givenBy_eq_Collect)
-apply best
-done
+lemma (in Extend) givenBy_o_eq_extend_set:
+ "givenBy (v o f) = extend_set h ` (givenBy v)"
+by (simp add: givenBy_eq_Collect, best)
lemma (in Extend) givenBy_eq_extend_set: "givenBy f = range (extend_set h)"
apply (simp (no_asm) add: givenBy_eq_Collect)
@@ -515,9 +509,9 @@
lemma (in Extend) Join_project_ensures_strong:
"[| project h C G ~: transient (project_set h C Int (A-B)) |
project_set h C Int (A - B) = {};
- extend h F Join G : stable C;
- F Join project h C G : (project_set h C Int A) ensures B |]
- ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"
+ extend h F\<squnion>G : stable C;
+ F\<squnion>project h C G : (project_set h C Int A) ensures B |]
+ ==> extend h F\<squnion>G : (C Int extend_set h A) ensures (extend_set h B)"
apply (subst Int_extend_set_lemma [symmetric])
apply (rule Join_project_ensures)
apply (auto simp add: Int_Diff)
@@ -525,10 +519,10 @@
(*NOT WORKING. MODIFY AS IN Project.thy
lemma (in Extend) pld_lemma:
- "[| extend h F Join G : stable C;
- F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B;
+ "[| extend h F\<squnion>G : stable C;
+ F\<squnion>project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B;
G : preserves (v o f) |]
- ==> extend h F Join G :
+ ==> extend h F\<squnion>G :
(C Int extend_set h (project_set h C Int A))
leadsTo[(%D. C Int extend_set h D)`givenBy v] (extend_set h B)"
apply (erule leadsETo_induct)
@@ -548,21 +542,21 @@
done
lemma (in Extend) project_leadsETo_D_lemma:
- "[| extend h F Join G : stable C;
- F Join project h C G :
+ "[| extend h F\<squnion>G : stable C;
+ F\<squnion>project h C G :
(project_set h C Int A)
leadsTo[(%D. project_set h C Int D)`givenBy v] B;
G : preserves (v o f) |]
- ==> extend h F Join G : (C Int extend_set h A)
+ ==> extend h F\<squnion>G : (C Int extend_set h A)
leadsTo[(%D. C Int extend_set h D)`givenBy v] (extend_set h B)"
apply (rule pld_lemma [THEN leadsETo_weaken])
apply (auto simp add: split_extended_all)
done
lemma (in Extend) project_leadsETo_D:
- "[| F Join project h UNIV G : A leadsTo[givenBy v] B;
+ "[| F\<squnion>project h UNIV G : A leadsTo[givenBy v] B;
G : preserves (v o f) |]
- ==> extend h F Join G : (extend_set h A)
+ ==> extend h F\<squnion>G : (extend_set h A)
leadsTo[givenBy (v o f)] (extend_set h B)"
apply (cut_tac project_leadsETo_D_lemma [of _ _ UNIV], auto)
apply (erule leadsETo_givenBy)
@@ -570,10 +564,10 @@
done
lemma (in Extend) project_LeadsETo_D:
- "[| F Join project h (reachable (extend h F Join G)) G
+ "[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G
: A LeadsTo[givenBy v] B;
G : preserves (v o f) |]
- ==> extend h F Join G :
+ ==> extend h F\<squnion>G :
(extend_set h A) LeadsTo[givenBy (v o f)] (extend_set h B)"
apply (cut_tac subset_refl [THEN stable_reachable, THEN project_leadsETo_D_lemma])
apply (auto simp add: LeadsETo_def)
@@ -593,7 +587,7 @@
lemma (in Extend) extending_LeadsETo:
"(ALL G. extend h F ok G --> G : preserves (v o f))
- ==> extending (%G. reachable (extend h F Join G)) h F
+ ==> extending (%G. reachable (extend h F\<squnion>G)) h F
(extend_set h A LeadsTo[givenBy (v o f)] extend_set h B)
(A LeadsTo[givenBy v] B)"
apply (unfold extending_def)
@@ -606,10 +600,10 @@
(*Lemma for the Trans case*)
lemma (in Extend) pli_lemma:
- "[| extend h F Join G : stable C;
- F Join project h C G
+ "[| extend h F\<squnion>G : stable C;
+ F\<squnion>project h C G
: project_set h C Int project_set h A leadsTo project_set h B |]
- ==> F Join project h C G
+ ==> F\<squnion>project h C G
: project_set h C Int project_set h A leadsTo
project_set h C Int project_set h B"
apply (rule psp_stable2 [THEN leadsTo_weaken_L])
@@ -617,10 +611,10 @@
done
lemma (in Extend) project_leadsETo_I_lemma:
- "[| extend h F Join G : stable C;
- extend h F Join G :
+ "[| extend h F\<squnion>G : stable C;
+ extend h F\<squnion>G :
(C Int A) leadsTo[(%D. C Int D)`givenBy f] B |]
- ==> F Join project h C G
+ ==> F\<squnion>project h C G
: (project_set h C Int project_set h (C Int A)) leadsTo (project_set h B)"
apply (erule leadsETo_induct)
prefer 3
@@ -633,14 +627,14 @@
done
lemma (in Extend) project_leadsETo_I:
- "extend h F Join G : (extend_set h A) leadsTo[givenBy f] (extend_set h B)
- ==> F Join project h UNIV G : A leadsTo B"
+ "extend h F\<squnion>G : (extend_set h A) leadsTo[givenBy f] (extend_set h B)
+ ==> F\<squnion>project h UNIV G : A leadsTo B"
apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken], auto)
done
lemma (in Extend) project_LeadsETo_I:
- "extend h F Join G : (extend_set h A) LeadsTo[givenBy f] (extend_set h B)
- ==> F Join project h (reachable (extend h F Join G)) G
+ "extend h F\<squnion>G : (extend_set h A) LeadsTo[givenBy f] (extend_set h B)
+ ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G
: A LeadsTo B"
apply (simp (no_asm_use) add: LeadsTo_def LeadsETo_def)
apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken])
@@ -656,7 +650,7 @@
done
lemma (in Extend) projecting_LeadsTo:
- "projecting (%G. reachable (extend h F Join G)) h F
+ "projecting (%G. reachable (extend h F\<squnion>G)) h F
(extend_set h A LeadsTo[givenBy f] extend_set h B)
(A LeadsTo B)"
apply (unfold projecting_def)
--- a/src/HOL/UNITY/Extend.thy Sun Feb 16 12:16:07 2003 +0100
+++ b/src/HOL/UNITY/Extend.thy Sun Feb 16 12:17:40 2003 +0100
@@ -429,7 +429,7 @@
done
lemma (in Extend) extend_Join [simp]:
- "extend h (F Join G) = extend h F Join extend h G"
+ "extend h (F\<squnion>G) = extend h F\<squnion>extend h G"
apply (rule program_equalityI)
apply (simp (no_asm) add: extend_set_Int_distrib)
apply (simp add: image_Un, auto)
@@ -679,14 +679,14 @@
subsection{*Guarantees*}
lemma (in Extend) project_extend_Join:
- "project h UNIV ((extend h F) Join G) = F Join (project h UNIV G)"
+ "project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
apply (rule program_equalityI)
apply (simp add: project_set_extend_set_Int)
apply (simp add: image_eq_UN UN_Un, auto)
done
lemma (in Extend) extend_Join_eq_extend_D:
- "(extend h F) Join G = extend h H ==> H = F Join (project h UNIV G)"
+ "(extend h F)\<squnion>G = extend h H ==> H = F\<squnion>(project h UNIV G)"
apply (drule_tac f = "project h UNIV" in arg_cong)
apply (simp add: project_extend_Join)
done
--- a/src/HOL/UNITY/Guar.thy Sun Feb 16 12:16:07 2003 +0100
+++ b/src/HOL/UNITY/Guar.thy Sun Feb 16 12:17:40 2003 +0100
@@ -32,21 +32,21 @@
case, proving equivalence with Chandy and Sanders's n-ary definitions*)
ex_prop :: "'a program set => bool"
- "ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F Join G) \<in> X"
+ "ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F\<squnion>G) \<in> X"
strict_ex_prop :: "'a program set => bool"
- "strict_ex_prop X == \<forall>F G. F ok G --> (F \<in> X | G \<in> X) = (F Join G \<in> X)"
+ "strict_ex_prop X == \<forall>F G. F ok G --> (F \<in> X | G \<in> X) = (F\<squnion>G \<in> X)"
uv_prop :: "'a program set => bool"
- "uv_prop X == SKIP \<in> X & (\<forall>F G. F ok G --> F \<in> X & G \<in> X --> (F Join G) \<in> X)"
+ "uv_prop X == SKIP \<in> X & (\<forall>F G. F ok G --> F \<in> X & G \<in> X --> (F\<squnion>G) \<in> X)"
strict_uv_prop :: "'a program set => bool"
"strict_uv_prop X ==
- SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F Join G \<in> X))"
+ SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F\<squnion>G \<in> X))"
guar :: "['a program set, 'a program set] => 'a program set"
(infixl "guarantees" 55) (*higher than membership, lower than Co*)
- "X guarantees Y == {F. \<forall>G. F ok G --> F Join G \<in> X --> F Join G \<in> Y}"
+ "X guarantees Y == {F. \<forall>G. F ok G --> F\<squnion>G \<in> X --> F\<squnion>G \<in> Y}"
(* Weakest guarantees *)
@@ -64,8 +64,8 @@
refines :: "['a program, 'a program, 'a program set] => bool"
("(3_ refines _ wrt _)" [10,10,10] 10)
"G refines F wrt X ==
- \<forall>H. (F ok H & G ok H & F Join H \<in> welldef \<inter> X) -->
- (G Join H \<in> welldef \<inter> X)"
+ \<forall>H. (F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X) -->
+ (G\<squnion>H \<in> welldef \<inter> X)"
iso_refines :: "['a program, 'a program, 'a program set] => bool"
("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
@@ -146,19 +146,19 @@
(*** guarantees ***)
lemma guaranteesI:
- "(!!G. [| F ok G; F Join G \<in> X |] ==> F Join G \<in> Y)
+ "(!!G. [| F ok G; F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y)
==> F \<in> X guarantees Y"
by (simp add: guar_def component_def)
lemma guaranteesD:
- "[| F \<in> X guarantees Y; F ok G; F Join G \<in> X |]
- ==> F Join G \<in> Y"
+ "[| F \<in> X guarantees Y; F ok G; F\<squnion>G \<in> X |]
+ ==> F\<squnion>G \<in> Y"
by (unfold guar_def component_def, blast)
(*This version of guaranteesD matches more easily in the conclusion
The major premise can no longer be F \<subseteq> H since we need to reason about G*)
lemma component_guaranteesD:
- "[| F \<in> X guarantees Y; F Join G = H; H \<in> X; F ok G |]
+ "[| F \<in> X guarantees Y; F\<squnion>G = H; H \<in> X; F ok G |]
==> H \<in> Y"
by (unfold guar_def, blast)
@@ -263,24 +263,24 @@
lemma guarantees_Join_Int:
"[| F \<in> U guarantees V; G \<in> X guarantees Y; F ok G |]
- ==> F Join G \<in> (U \<inter> X) guarantees (V \<inter> Y)"
+ ==> F\<squnion>G \<in> (U \<inter> X) guarantees (V \<inter> Y)"
apply (unfold guar_def)
apply (simp (no_asm))
apply safe
apply (simp add: Join_assoc)
-apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
+apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ")
apply (simp add: ok_commute)
apply (simp (no_asm_simp) add: Join_ac)
done
lemma guarantees_Join_Un:
"[| F \<in> U guarantees V; G \<in> X guarantees Y; F ok G |]
- ==> F Join G \<in> (U \<union> X) guarantees (V \<union> Y)"
+ ==> F\<squnion>G \<in> (U \<union> X) guarantees (V \<union> Y)"
apply (unfold guar_def)
apply (simp (no_asm))
apply safe
apply (simp add: Join_assoc)
-apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
+apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ")
apply (simp add: ok_commute)
apply (simp (no_asm_simp) add: Join_ac)
done
@@ -291,7 +291,7 @@
apply (unfold guar_def, auto)
apply (drule bspec, assumption)
apply (rename_tac "i")
-apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
+apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
apply (auto intro: OK_imp_ok
simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
done
@@ -302,7 +302,7 @@
apply (unfold guar_def, auto)
apply (drule bspec, assumption)
apply (rename_tac "i")
-apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
+apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
apply (auto intro: OK_imp_ok
simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
done
@@ -311,7 +311,7 @@
(*** guarantees laws for breaking down the program, by lcp ***)
lemma guarantees_Join_I1:
- "[| F \<in> X guarantees Y; F ok G |] ==> F Join G \<in> X guarantees Y"
+ "[| F \<in> X guarantees Y; F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
apply (unfold guar_def)
apply (simp (no_asm))
apply safe
@@ -319,7 +319,7 @@
done
lemma guarantees_Join_I2:
- "[| G \<in> X guarantees Y; F ok G |] ==> F Join G \<in> X guarantees Y"
+ "[| G \<in> X guarantees Y; F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
apply (blast intro: guarantees_Join_I1)
done
@@ -328,17 +328,17 @@
"[| i \<in> I; F i \<in> X guarantees Y; OK I F |]
==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y"
apply (unfold guar_def, clarify)
-apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
+apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
apply (auto intro: OK_imp_ok simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
done
(*** well-definedness ***)
-lemma Join_welldef_D1: "F Join G \<in> welldef ==> F \<in> welldef"
+lemma Join_welldef_D1: "F\<squnion>G \<in> welldef ==> F \<in> welldef"
by (unfold welldef_def, auto)
-lemma Join_welldef_D2: "F Join G \<in> welldef ==> G \<in> welldef"
+lemma Join_welldef_D2: "F\<squnion>G \<in> welldef ==> G \<in> welldef"
by (unfold welldef_def, auto)
(*** refinement ***)
@@ -356,13 +356,13 @@
lemma strict_ex_refine_lemma:
"strict_ex_prop X
- ==> (\<forall>H. F ok H & G ok H & F Join H \<in> X --> G Join H \<in> X)
+ ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X)
= (F \<in> X --> G \<in> X)"
by (unfold strict_ex_prop_def, auto)
lemma strict_ex_refine_lemma_v:
"strict_ex_prop X
- ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join H \<in> X) =
+ ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =
(F \<in> welldef \<inter> X --> G \<in> X)"
apply (unfold strict_ex_prop_def, safe)
apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
@@ -371,7 +371,7 @@
lemma ex_refinement_thm:
"[| strict_ex_prop X;
- \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X --> G Join H \<in> welldef |]
+ \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X --> G\<squnion>H \<in> welldef |]
==> (G refines F wrt X) = (G iso_refines F wrt X)"
apply (rule_tac x = SKIP in allE, assumption)
apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v)
@@ -380,12 +380,12 @@
lemma strict_uv_refine_lemma:
"strict_uv_prop X ==>
- (\<forall>H. F ok H & G ok H & F Join H \<in> X --> G Join H \<in> X) = (F \<in> X --> G \<in> X)"
+ (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) = (F \<in> X --> G \<in> X)"
by (unfold strict_uv_prop_def, blast)
lemma strict_uv_refine_lemma_v:
"strict_uv_prop X
- ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join H \<in> X) =
+ ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =
(F \<in> welldef \<inter> X --> G \<in> X)"
apply (unfold strict_uv_prop_def, safe)
apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
@@ -394,8 +394,8 @@
lemma uv_refinement_thm:
"[| strict_uv_prop X;
- \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X -->
- G Join H \<in> welldef |]
+ \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X -->
+ G\<squnion>H \<in> welldef |]
==> (G refines F wrt X) = (G iso_refines F wrt X)"
apply (rule_tac x = SKIP in allE, assumption)
apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v)
@@ -458,15 +458,15 @@
by (unfold wx_def, auto)
(* Proposition 6 *)
-lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F Join G \<in> X})"
+lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F\<squnion>G \<in> X})"
apply (unfold ex_prop_def, safe)
-apply (drule_tac x = "G Join Ga" in spec)
+apply (drule_tac x = "G\<squnion>Ga" in spec)
apply (force simp add: ok_Join_iff1 Join_assoc)
-apply (drule_tac x = "F Join Ga" in spec)
+apply (drule_tac x = "F\<squnion>Ga" in spec)
apply (simp (no_asm_use) add: ok_Join_iff1)
apply safe
apply (simp (no_asm_simp) add: ok_commute)
-apply (subgoal_tac "F Join G = G Join F")
+apply (subgoal_tac "F\<squnion>G = G\<squnion>F")
apply (simp (no_asm_simp) add: Join_assoc)
apply (simp (no_asm) add: Join_commute)
done
@@ -474,15 +474,15 @@
(* Equivalence with the other definition of wx *)
lemma wx_equiv:
- "wx X = {F. \<forall>G. F ok G --> (F Join G):X}"
+ "wx X = {F. \<forall>G. F ok G --> (F\<squnion>G):X}"
apply (unfold wx_def, safe)
apply (simp (no_asm_use) add: ex_prop_def)
apply (drule_tac x = x in spec)
apply (drule_tac x = G in spec)
-apply (frule_tac c = "x Join G" in subsetD, safe)
+apply (frule_tac c = "x\<squnion>G" in subsetD, safe)
apply (simp (no_asm))
-apply (rule_tac x = "{F. \<forall>G. F ok G --> F Join G \<in> X}" in exI, safe)
+apply (rule_tac x = "{F. \<forall>G. F ok G --> F\<squnion>G \<in> X}" in exI, safe)
apply (rule_tac [2] wx'_ex_prop)
apply (rotate_tac 1)
apply (drule_tac x = SKIP in spec, auto)
--- a/src/HOL/UNITY/Project.thy Sun Feb 16 12:16:07 2003 +0100
+++ b/src/HOL/UNITY/Project.thy Sun Feb 16 12:17:40 2003 +0100
@@ -16,13 +16,13 @@
projecting :: "['c program => 'c set, 'a*'b => 'c,
'a program, 'c program set, 'a program set] => bool"
"projecting C h F X' X ==
- \<forall>G. extend h F Join G \<in> X' --> F Join project h (C G) G \<in> X"
+ \<forall>G. extend h F\<squnion>G \<in> X' --> F\<squnion>project h (C G) G \<in> X"
extending :: "['c program => 'c set, 'a*'b => 'c, 'a program,
'c program set, 'a program set] => bool"
"extending C h F Y' Y ==
- \<forall>G. extend h F ok G --> F Join project h (C G) G \<in> Y
- --> extend h F Join G \<in> Y'"
+ \<forall>G. extend h F ok G --> F\<squnion>project h (C G) G \<in> Y
+ --> extend h F\<squnion>G \<in> Y'"
subset_closed :: "'a set set => bool"
"subset_closed U == \<forall>A \<in> U. Pow A \<subseteq> U"
@@ -44,11 +44,11 @@
apply (blast dest: stable_constrains_Int intro: constrains_weaken)
done
-(*Generalizes project_constrains to the program F Join project h C G
+(*Generalizes project_constrains to the program F\<squnion>project h C G
useful with guarantees reasoning*)
lemma (in Extend) Join_project_constrains:
- "(F Join project h C G \<in> A co B) =
- (extend h F Join G \<in> (C \<inter> extend_set h A) co (extend_set h B) &
+ "(F\<squnion>project h C G \<in> A co B) =
+ (extend h F\<squnion>G \<in> (C \<inter> extend_set h A) co (extend_set h B) &
F \<in> A co B)"
apply (simp (no_asm) add: project_constrains)
apply (blast intro: extend_constrains [THEN iffD2, THEN constrains_weaken]
@@ -58,9 +58,9 @@
(*The condition is required to prove the left-to-right direction
could weaken it to G \<in> (C \<inter> extend_set h A) co C*)
lemma (in Extend) Join_project_stable:
- "extend h F Join G \<in> stable C
- ==> (F Join project h C G \<in> stable A) =
- (extend h F Join G \<in> stable (C \<inter> extend_set h A) &
+ "extend h F\<squnion>G \<in> stable C
+ ==> (F\<squnion>project h C G \<in> stable A) =
+ (extend h F\<squnion>G \<in> stable (C \<inter> extend_set h A) &
F \<in> stable A)"
apply (unfold stable_def)
apply (simp only: Join_project_constrains)
@@ -69,23 +69,23 @@
(*For using project_guarantees in particular cases*)
lemma (in Extend) project_constrains_I:
- "extend h F Join G \<in> extend_set h A co extend_set h B
- ==> F Join project h C G \<in> A co B"
+ "extend h F\<squnion>G \<in> extend_set h A co extend_set h B
+ ==> F\<squnion>project h C G \<in> A co B"
apply (simp add: project_constrains extend_constrains)
apply (blast intro: constrains_weaken dest: constrains_imp_subset)
done
lemma (in Extend) project_increasing_I:
- "extend h F Join G \<in> increasing (func o f)
- ==> F Join project h C G \<in> increasing func"
+ "extend h F\<squnion>G \<in> increasing (func o f)
+ ==> F\<squnion>project h C G \<in> increasing func"
apply (unfold increasing_def stable_def)
apply (simp del: Join_constrains
add: project_constrains_I extend_set_eq_Collect)
done
lemma (in Extend) Join_project_increasing:
- "(F Join project h UNIV G \<in> increasing func) =
- (extend h F Join G \<in> increasing (func o f))"
+ "(F\<squnion>project h UNIV G \<in> increasing func) =
+ (extend h F\<squnion>G \<in> increasing (func o f))"
apply (rule iffI)
apply (erule_tac [2] project_increasing_I)
apply (simp del: Join_stable
@@ -95,8 +95,8 @@
(*The UNIV argument is essential*)
lemma (in Extend) project_constrains_D:
- "F Join project h UNIV G \<in> A co B
- ==> extend h F Join G \<in> extend_set h A co extend_set h B"
+ "F\<squnion>project h UNIV G \<in> A co B
+ ==> extend h F\<squnion>G \<in> extend_set h A co extend_set h B"
by (simp add: project_constrains extend_constrains)
@@ -204,9 +204,9 @@
(*In practice, C = reachable(...): the inclusion is equality*)
lemma (in Extend) reachable_imp_reachable_project:
- "[| reachable (extend h F Join G) \<subseteq> C;
- z \<in> reachable (extend h F Join G) |]
- ==> f z \<in> reachable (F Join project h C G)"
+ "[| reachable (extend h F\<squnion>G) \<subseteq> C;
+ z \<in> reachable (extend h F\<squnion>G) |]
+ ==> f z \<in> reachable (F\<squnion>project h C G)"
apply (erule reachable.induct)
apply (force intro!: reachable.Init simp add: split_extended_all, auto)
apply (rule_tac act = x in reachable.Acts)
@@ -217,8 +217,8 @@
done
lemma (in Extend) project_Constrains_D:
- "F Join project h (reachable (extend h F Join G)) G \<in> A Co B
- ==> extend h F Join G \<in> (extend_set h A) Co (extend_set h B)"
+ "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B
+ ==> extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)"
apply (unfold Constrains_def)
apply (simp del: Join_constrains
add: Join_project_constrains, clarify)
@@ -227,22 +227,22 @@
done
lemma (in Extend) project_Stable_D:
- "F Join project h (reachable (extend h F Join G)) G \<in> Stable A
- ==> extend h F Join G \<in> Stable (extend_set h A)"
+ "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A
+ ==> extend h F\<squnion>G \<in> Stable (extend_set h A)"
apply (unfold Stable_def)
apply (simp (no_asm_simp) add: project_Constrains_D)
done
lemma (in Extend) project_Always_D:
- "F Join project h (reachable (extend h F Join G)) G \<in> Always A
- ==> extend h F Join G \<in> Always (extend_set h A)"
+ "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A
+ ==> extend h F\<squnion>G \<in> Always (extend_set h A)"
apply (unfold Always_def)
apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all)
done
lemma (in Extend) project_Increasing_D:
- "F Join project h (reachable (extend h F Join G)) G \<in> Increasing func
- ==> extend h F Join G \<in> Increasing (func o f)"
+ "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func
+ ==> extend h F\<squnion>G \<in> Increasing (func o f)"
apply (unfold Increasing_def, auto)
apply (subst extend_set_eq_Collect [symmetric])
apply (simp (no_asm_simp) add: project_Stable_D)
@@ -253,9 +253,9 @@
(*In practice, C = reachable(...): the inclusion is equality*)
lemma (in Extend) reachable_project_imp_reachable:
- "[| C \<subseteq> reachable(extend h F Join G);
- x \<in> reachable (F Join project h C G) |]
- ==> \<exists>y. h(x,y) \<in> reachable (extend h F Join G)"
+ "[| C \<subseteq> reachable(extend h F\<squnion>G);
+ x \<in> reachable (F\<squnion>project h C G) |]
+ ==> \<exists>y. h(x,y) \<in> reachable (extend h F\<squnion>G)"
apply (erule reachable.induct)
apply (force intro: reachable.Init)
apply (auto simp add: project_act_def)
@@ -263,22 +263,22 @@
done
lemma (in Extend) project_set_reachable_extend_eq:
- "project_set h (reachable (extend h F Join G)) =
- reachable (F Join project h (reachable (extend h F Join G)) G)"
+ "project_set h (reachable (extend h F\<squnion>G)) =
+ reachable (F\<squnion>project h (reachable (extend h F\<squnion>G)) G)"
by (auto dest: subset_refl [THEN reachable_imp_reachable_project]
subset_refl [THEN reachable_project_imp_reachable])
(*UNUSED*)
lemma (in Extend) reachable_extend_Join_subset:
- "reachable (extend h F Join G) \<subseteq> C
- ==> reachable (extend h F Join G) \<subseteq>
- extend_set h (reachable (F Join project h C G))"
+ "reachable (extend h F\<squnion>G) \<subseteq> C
+ ==> reachable (extend h F\<squnion>G) \<subseteq>
+ extend_set h (reachable (F\<squnion>project h C G))"
apply (auto dest: reachable_imp_reachable_project)
done
lemma (in Extend) project_Constrains_I:
- "extend h F Join G \<in> (extend_set h A) Co (extend_set h B)
- ==> F Join project h (reachable (extend h F Join G)) G \<in> A Co B"
+ "extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)
+ ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B"
apply (unfold Constrains_def)
apply (simp del: Join_constrains
add: Join_project_constrains extend_set_Int_distrib)
@@ -291,43 +291,43 @@
done
lemma (in Extend) project_Stable_I:
- "extend h F Join G \<in> Stable (extend_set h A)
- ==> F Join project h (reachable (extend h F Join G)) G \<in> Stable A"
+ "extend h F\<squnion>G \<in> Stable (extend_set h A)
+ ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A"
apply (unfold Stable_def)
apply (simp (no_asm_simp) add: project_Constrains_I)
done
lemma (in Extend) project_Always_I:
- "extend h F Join G \<in> Always (extend_set h A)
- ==> F Join project h (reachable (extend h F Join G)) G \<in> Always A"
+ "extend h F\<squnion>G \<in> Always (extend_set h A)
+ ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A"
apply (unfold Always_def)
apply (auto simp add: project_Stable_I)
apply (unfold extend_set_def, blast)
done
lemma (in Extend) project_Increasing_I:
- "extend h F Join G \<in> Increasing (func o f)
- ==> F Join project h (reachable (extend h F Join G)) G \<in> Increasing func"
+ "extend h F\<squnion>G \<in> Increasing (func o f)
+ ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func"
apply (unfold Increasing_def, auto)
apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I)
done
lemma (in Extend) project_Constrains:
- "(F Join project h (reachable (extend h F Join G)) G \<in> A Co B) =
- (extend h F Join G \<in> (extend_set h A) Co (extend_set h B))"
+ "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B) =
+ (extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B))"
apply (blast intro: project_Constrains_I project_Constrains_D)
done
lemma (in Extend) project_Stable:
- "(F Join project h (reachable (extend h F Join G)) G \<in> Stable A) =
- (extend h F Join G \<in> Stable (extend_set h A))"
+ "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A) =
+ (extend h F\<squnion>G \<in> Stable (extend_set h A))"
apply (unfold Stable_def)
apply (rule project_Constrains)
done
lemma (in Extend) project_Increasing:
- "(F Join project h (reachable (extend h F Join G)) G \<in> Increasing func) =
- (extend h F Join G \<in> Increasing (func o f))"
+ "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func) =
+ (extend h F\<squnion>G \<in> Increasing (func o f))"
apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
done
@@ -335,7 +335,7 @@
about guarantees.*}
lemma (in Extend) projecting_Constrains:
- "projecting (%G. reachable (extend h F Join G)) h F
+ "projecting (%G. reachable (extend h F\<squnion>G)) h F
(extend_set h A Co extend_set h B) (A Co B)"
apply (unfold projecting_def)
@@ -343,49 +343,49 @@
done
lemma (in Extend) projecting_Stable:
- "projecting (%G. reachable (extend h F Join G)) h F
+ "projecting (%G. reachable (extend h F\<squnion>G)) h F
(Stable (extend_set h A)) (Stable A)"
apply (unfold Stable_def)
apply (rule projecting_Constrains)
done
lemma (in Extend) projecting_Always:
- "projecting (%G. reachable (extend h F Join G)) h F
+ "projecting (%G. reachable (extend h F\<squnion>G)) h F
(Always (extend_set h A)) (Always A)"
apply (unfold projecting_def)
apply (blast intro: project_Always_I)
done
lemma (in Extend) projecting_Increasing:
- "projecting (%G. reachable (extend h F Join G)) h F
+ "projecting (%G. reachable (extend h F\<squnion>G)) h F
(Increasing (func o f)) (Increasing func)"
apply (unfold projecting_def)
apply (blast intro: project_Increasing_I)
done
lemma (in Extend) extending_Constrains:
- "extending (%G. reachable (extend h F Join G)) h F
+ "extending (%G. reachable (extend h F\<squnion>G)) h F
(extend_set h A Co extend_set h B) (A Co B)"
apply (unfold extending_def)
apply (blast intro: project_Constrains_D)
done
lemma (in Extend) extending_Stable:
- "extending (%G. reachable (extend h F Join G)) h F
+ "extending (%G. reachable (extend h F\<squnion>G)) h F
(Stable (extend_set h A)) (Stable A)"
apply (unfold extending_def)
apply (blast intro: project_Stable_D)
done
lemma (in Extend) extending_Always:
- "extending (%G. reachable (extend h F Join G)) h F
+ "extending (%G. reachable (extend h F\<squnion>G)) h F
(Always (extend_set h A)) (Always A)"
apply (unfold extending_def)
apply (blast intro: project_Always_D)
done
lemma (in Extend) extending_Increasing:
- "extending (%G. reachable (extend h F Join G)) h F
+ "extending (%G. reachable (extend h F\<squnion>G)) h F
(Increasing (func o f)) (Increasing func)"
apply (unfold extending_def)
apply (blast intro: project_Increasing_D)
@@ -423,8 +423,8 @@
(*Used to prove project_leadsETo_I*)
lemma (in Extend) ensures_extend_set_imp_project_ensures:
"[| extend h F \<in> stable C; G \<in> stable C;
- extend h F Join G \<in> A ensures B; A-B = C \<inter> extend_set h D |]
- ==> F Join project h C G
+ extend h F\<squnion>G \<in> A ensures B; A-B = C \<inter> extend_set h D |]
+ ==> F\<squnion>project h C G
\<in> (project_set h C \<inter> project_set h A) ensures (project_set h B)"
apply (simp add: ensures_def project_constrains Join_transient extend_transient,
clarify)
@@ -482,9 +482,9 @@
(*Used to prove project_leadsETo_D*)
lemma (in Extend) Join_project_ensures [rule_format]:
- "[| extend h F Join G \<in> stable C;
- F Join project h C G \<in> A ensures B |]
- ==> extend h F Join G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
+ "[| extend h F\<squnion>G \<in> stable C;
+ F\<squnion>project h C G \<in> A ensures B |]
+ ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
apply (auto simp add: ensures_eq extend_unless project_unless)
apply (blast intro: extend_transient [THEN iffD2] transient_strengthen)
apply (blast intro: project_transient_extend_set transient_strengthen)
@@ -496,9 +496,9 @@
(*The strange induction formula allows induction over the leadsTo
assumption's non-atomic precondition*)
lemma (in Extend) PLD_lemma:
- "[| extend h F Join G \<in> stable C;
- F Join project h C G \<in> (project_set h C \<inter> A) leadsTo B |]
- ==> extend h F Join G \<in>
+ "[| extend h F\<squnion>G \<in> stable C;
+ F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]
+ ==> extend h F\<squnion>G \<in>
C \<inter> extend_set h (project_set h C \<inter> A) leadsTo (extend_set h B)"
apply (erule leadsTo_induct)
apply (blast intro: leadsTo_Basis Join_project_ensures)
@@ -507,17 +507,17 @@
done
lemma (in Extend) project_leadsTo_D_lemma:
- "[| extend h F Join G \<in> stable C;
- F Join project h C G \<in> (project_set h C \<inter> A) leadsTo B |]
- ==> extend h F Join G \<in> (C \<inter> extend_set h A) leadsTo (extend_set h B)"
+ "[| extend h F\<squnion>G \<in> stable C;
+ F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]
+ ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) leadsTo (extend_set h B)"
apply (rule PLD_lemma [THEN leadsTo_weaken])
apply (auto simp add: split_extended_all)
done
lemma (in Extend) Join_project_LeadsTo:
- "[| C = (reachable (extend h F Join G));
- F Join project h C G \<in> A LeadsTo B |]
- ==> extend h F Join G \<in> (extend_set h A) LeadsTo (extend_set h B)"
+ "[| C = (reachable (extend h F\<squnion>G));
+ F\<squnion>project h C G \<in> A LeadsTo B |]
+ ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)"
by (simp del: Join_stable add: LeadsTo_def project_leadsTo_D_lemma
project_set_reachable_extend_eq)
@@ -526,9 +526,9 @@
lemma (in Extend) project_ensures_D_lemma:
"[| G \<in> stable ((C \<inter> extend_set h A) - (extend_set h B));
- F Join project h C G \<in> (project_set h C \<inter> A) ensures B;
- extend h F Join G \<in> stable C |]
- ==> extend h F Join G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
+ F\<squnion>project h C G \<in> (project_set h C \<inter> A) ensures B;
+ extend h F\<squnion>G \<in> stable C |]
+ ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
(*unless*)
apply (auto intro!: project_unless2 [unfolded unless_def]
intro: project_extend_constrains_I
@@ -543,17 +543,17 @@
done
lemma (in Extend) project_ensures_D:
- "[| F Join project h UNIV G \<in> A ensures B;
+ "[| F\<squnion>project h UNIV G \<in> A ensures B;
G \<in> stable (extend_set h A - extend_set h B) |]
- ==> extend h F Join G \<in> (extend_set h A) ensures (extend_set h B)"
+ ==> extend h F\<squnion>G \<in> (extend_set h A) ensures (extend_set h B)"
apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto)
done
lemma (in Extend) project_Ensures_D:
- "[| F Join project h (reachable (extend h F Join G)) G \<in> A Ensures B;
- G \<in> stable (reachable (extend h F Join G) \<inter> extend_set h A -
+ "[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Ensures B;
+ G \<in> stable (reachable (extend h F\<squnion>G) \<inter> extend_set h A -
extend_set h B) |]
- ==> extend h F Join G \<in> (extend_set h A) Ensures (extend_set h B)"
+ ==> extend h F\<squnion>G \<in> (extend_set h A) Ensures (extend_set h B)"
apply (unfold Ensures_def)
apply (rule project_ensures_D_lemma [THEN revcut_rl])
apply (auto simp add: project_set_reachable_extend_eq [symmetric])
@@ -585,14 +585,14 @@
Not clear that it has a converse [or that we want one!]*)
(*The raw version; 3rd premise could be weakened by adding the
- precondition extend h F Join G \<in> X' *)
+ precondition extend h F\<squnion>G \<in> X' *)
lemma (in Extend) project_guarantees_raw:
assumes xguary: "F \<in> X guarantees Y"
and closed: "subset_closed (AllowedActs F)"
- and project: "!!G. extend h F Join G \<in> X'
- ==> F Join project h (C G) G \<in> X"
- and extend: "!!G. [| F Join project h (C G) G \<in> Y |]
- ==> extend h F Join G \<in> Y'"
+ and project: "!!G. extend h F\<squnion>G \<in> X'
+ ==> F\<squnion>project h (C G) G \<in> X"
+ and extend: "!!G. [| F\<squnion>project h (C G) G \<in> Y |]
+ ==> extend h F\<squnion>G \<in> Y'"
shows "extend h F \<in> X' guarantees Y'"
apply (rule xguary [THEN guaranteesD, THEN extend, THEN guaranteesI])
apply (blast intro: closed subset_closed_ok_extend_imp_ok_project)
@@ -648,14 +648,14 @@
subsubsection{*Guarantees with a leadsTo postcondition*}
lemma (in Extend) project_leadsTo_D:
- "F Join project h UNIV G \<in> A leadsTo B
- ==> extend h F Join G \<in> (extend_set h A) leadsTo (extend_set h B)"
+ "F\<squnion>project h UNIV G \<in> A leadsTo B
+ ==> extend h F\<squnion>G \<in> (extend_set h A) leadsTo (extend_set h B)"
apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken], auto)
done
lemma (in Extend) project_LeadsTo_D:
- "F Join project h (reachable (extend h F Join G)) G \<in> A LeadsTo B
- ==> extend h F Join G \<in> (extend_set h A) LeadsTo (extend_set h B)"
+ "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A LeadsTo B
+ ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)"
apply (rule refl [THEN Join_project_LeadsTo], auto)
done
@@ -667,7 +667,7 @@
done
lemma (in Extend) extending_LeadsTo:
- "extending (%G. reachable (extend h F Join G)) h F
+ "extending (%G. reachable (extend h F\<squnion>G)) h F
(extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"
apply (unfold extending_def)
apply (blast intro: project_LeadsTo_D)
--- a/src/HOL/UNITY/Union.thy Sun Feb 16 12:16:07 2003 +0100
+++ b/src/HOL/UNITY/Union.thy Sun Feb 16 12:17:40 2003 +0100
@@ -46,10 +46,10 @@
"JN x. B" == "JOIN UNIV (%x. B)"
syntax (xsymbols)
- SKIP :: "'a program" ("\<bottom>")
- "op Join" :: "['a program, 'a program] => 'a program" (infixl "\<squnion>" 65)
- "@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10)
- "@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _\<in>_./ _)" 10)
+ SKIP :: "'a program" ("\<bottom>")
+ Join :: "['a program, 'a program] => 'a program" (infixl "\<squnion>" 65)
+ "@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10)
+ "@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _\<in>_./ _)" 10)
subsection{*SKIP*}
@@ -82,14 +82,14 @@
subsection{*Join*}
-lemma Init_Join [simp]: "Init (F Join G) = Init F \<inter> Init G"
+lemma Init_Join [simp]: "Init (F\<squnion>G) = Init F \<inter> Init G"
by (simp add: Join_def)
-lemma Acts_Join [simp]: "Acts (F Join G) = Acts F \<union> Acts G"
+lemma Acts_Join [simp]: "Acts (F\<squnion>G) = Acts F \<union> Acts G"
by (auto simp add: Join_def)
lemma AllowedActs_Join [simp]:
- "AllowedActs (F Join G) = AllowedActs F \<inter> AllowedActs G"
+ "AllowedActs (F\<squnion>G) = AllowedActs F \<inter> AllowedActs G"
by (auto simp add: Join_def)
@@ -98,7 +98,7 @@
lemma JN_empty [simp]: "(\<Squnion>i\<in>{}. F i) = SKIP"
by (unfold JOIN_def SKIP_def, auto)
-lemma JN_insert [simp]: "(\<Squnion>i \<in> insert a I. F i) = (F a) Join (\<Squnion>i \<in> I. F i)"
+lemma JN_insert [simp]: "(\<Squnion>i \<in> insert a I. F i) = (F a)\<squnion>(\<Squnion>i \<in> I. F i)"
apply (rule program_equalityI)
apply (auto simp add: JOIN_def Join_def)
done
@@ -121,33 +121,33 @@
subsection{*Algebraic laws*}
-lemma Join_commute: "F Join G = G Join F"
+lemma Join_commute: "F\<squnion>G = G\<squnion>F"
by (simp add: Join_def Un_commute Int_commute)
-lemma Join_assoc: "(F Join G) Join H = F Join (G Join H)"
+lemma Join_assoc: "(F\<squnion>G)\<squnion>H = F\<squnion>(G\<squnion>H)"
by (simp add: Un_ac Join_def Int_assoc insert_absorb)
-lemma Join_left_commute: "A Join (B Join C) = B Join (A Join C)"
+lemma Join_left_commute: "A\<squnion>(B\<squnion>C) = B\<squnion>(A\<squnion>C)"
by (simp add: Un_ac Int_ac Join_def insert_absorb)
-lemma Join_SKIP_left [simp]: "SKIP Join F = F"
+lemma Join_SKIP_left [simp]: "SKIP\<squnion>F = F"
apply (unfold Join_def SKIP_def)
apply (rule program_equalityI)
apply (simp_all (no_asm) add: insert_absorb)
done
-lemma Join_SKIP_right [simp]: "F Join SKIP = F"
+lemma Join_SKIP_right [simp]: "F\<squnion>SKIP = F"
apply (unfold Join_def SKIP_def)
apply (rule program_equalityI)
apply (simp_all (no_asm) add: insert_absorb)
done
-lemma Join_absorb [simp]: "F Join F = F"
+lemma Join_absorb [simp]: "F\<squnion>F = F"
apply (unfold Join_def)
apply (rule program_equalityI, auto)
done
-lemma Join_left_absorb: "F Join (F Join G) = F Join G"
+lemma Join_left_absorb: "F\<squnion>(F\<squnion>G) = F\<squnion>G"
apply (unfold Join_def)
apply (rule program_equalityI, auto)
done
@@ -159,25 +159,25 @@
subsection{*\<Squnion>laws*}
(*Also follows by JN_insert and insert_absorb, but the proof is longer*)
-lemma JN_absorb: "k \<in> I ==> F k Join (\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> I. F i)"
+lemma JN_absorb: "k \<in> I ==> F k\<squnion>(\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> I. F i)"
by (auto intro!: program_equalityI)
-lemma JN_Un: "(\<Squnion>i \<in> I \<union> J. F i) = ((\<Squnion>i \<in> I. F i) Join (\<Squnion>i \<in> J. F i))"
+lemma JN_Un: "(\<Squnion>i \<in> I \<union> J. F i) = ((\<Squnion>i \<in> I. F i)\<squnion>(\<Squnion>i \<in> J. F i))"
by (auto intro!: program_equalityI)
lemma JN_constant: "(\<Squnion>i \<in> I. c) = (if I={} then SKIP else c)"
by (rule program_equalityI, auto)
lemma JN_Join_distrib:
- "(\<Squnion>i \<in> I. F i Join G i) = (\<Squnion>i \<in> I. F i) Join (\<Squnion>i \<in> I. G i)"
+ "(\<Squnion>i \<in> I. F i\<squnion>G i) = (\<Squnion>i \<in> I. F i) \<squnion> (\<Squnion>i \<in> I. G i)"
by (auto intro!: program_equalityI)
lemma JN_Join_miniscope:
- "i \<in> I ==> (\<Squnion>i \<in> I. F i Join G) = ((\<Squnion>i \<in> I. F i) Join G)"
+ "i \<in> I ==> (\<Squnion>i \<in> I. F i\<squnion>G) = ((\<Squnion>i \<in> I. F i)\<squnion>G)"
by (auto simp add: JN_Join_distrib JN_constant)
(*Used to prove guarantees_JN_I*)
-lemma JN_Join_diff: "i \<in> I ==> F i Join JOIN (I - {i}) F = JOIN I F"
+lemma JN_Join_diff: "i \<in> I ==> F i\<squnion>JOIN (I - {i}) F = JOIN I F"
apply (unfold JOIN_def Join_def)
apply (rule program_equalityI, auto)
done
@@ -193,21 +193,21 @@
by (simp add: constrains_def JOIN_def, blast)
lemma Join_constrains [simp]:
- "(F Join G \<in> A co B) = (F \<in> A co B & G \<in> A co B)"
+ "(F\<squnion>G \<in> A co B) = (F \<in> A co B & G \<in> A co B)"
by (auto simp add: constrains_def Join_def)
lemma Join_unless [simp]:
- "(F Join G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)"
+ "(F\<squnion>G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)"
by (simp add: Join_constrains unless_def)
(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
- reachable (F Join G) could be much bigger than reachable F, reachable G
+ reachable (F\<squnion>G) could be much bigger than reachable F, reachable G
*)
lemma Join_constrains_weaken:
"[| F \<in> A co A'; G \<in> B co B' |]
- ==> F Join G \<in> (A \<inter> B) co (A' \<union> B')"
+ ==> F\<squnion>G \<in> (A \<inter> B) co (A' \<union> B')"
by (simp, blast intro: constrains_weaken)
(*If I={}, it degenerates to SKIP \<in> UNIV co {}, which is false.*)
@@ -227,18 +227,18 @@
by (simp add: invariant_def JN_stable, blast)
lemma Join_stable [simp]:
- "(F Join G \<in> stable A) =
+ "(F\<squnion>G \<in> stable A) =
(F \<in> stable A & G \<in> stable A)"
by (simp add: stable_def)
lemma Join_increasing [simp]:
- "(F Join G \<in> increasing f) =
+ "(F\<squnion>G \<in> increasing f) =
(F \<in> increasing f & G \<in> increasing f)"
by (simp add: increasing_def Join_stable, blast)
lemma invariant_JoinI:
"[| F \<in> invariant A; G \<in> invariant A |]
- ==> F Join G \<in> invariant A"
+ ==> F\<squnion>G \<in> invariant A"
by (simp add: invariant_def, blast)
lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))"
@@ -253,14 +253,14 @@
by (auto simp add: transient_def JOIN_def)
lemma Join_transient [simp]:
- "F Join G \<in> transient A =
+ "F\<squnion>G \<in> transient A =
(F \<in> transient A | G \<in> transient A)"
by (auto simp add: bex_Un transient_def Join_def)
-lemma Join_transient_I1: "F \<in> transient A ==> F Join G \<in> transient A"
+lemma Join_transient_I1: "F \<in> transient A ==> F\<squnion>G \<in> transient A"
by (simp add: Join_transient)
-lemma Join_transient_I2: "G \<in> transient A ==> F Join G \<in> transient A"
+lemma Join_transient_I2: "G \<in> transient A ==> F\<squnion>G \<in> transient A"
by (simp add: Join_transient)
(*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *)
@@ -271,14 +271,14 @@
by (auto simp add: ensures_def JN_constrains JN_transient)
lemma Join_ensures:
- "F Join G \<in> A ensures B =
+ "F\<squnion>G \<in> A ensures B =
(F \<in> (A-B) co (A \<union> B) & G \<in> (A-B) co (A \<union> B) &
(F \<in> transient (A-B) | G \<in> transient (A-B)))"
by (auto simp add: ensures_def Join_transient)
lemma stable_Join_constrains:
"[| F \<in> stable A; G \<in> A co A' |]
- ==> F Join G \<in> A co A'"
+ ==> F\<squnion>G \<in> A co A'"
apply (unfold stable_def constrains_def Join_def)
apply (simp add: ball_Un, blast)
done
@@ -286,20 +286,20 @@
(*Premise for G cannot use Always because F \<in> Stable A is weaker than
G \<in> stable A *)
lemma stable_Join_Always1:
- "[| F \<in> stable A; G \<in> invariant A |] ==> F Join G \<in> Always A"
+ "[| F \<in> stable A; G \<in> invariant A |] ==> F\<squnion>G \<in> Always A"
apply (simp (no_asm_use) add: Always_def invariant_def Stable_eq_stable)
apply (force intro: stable_Int)
done
(*As above, but exchanging the roles of F and G*)
lemma stable_Join_Always2:
- "[| F \<in> invariant A; G \<in> stable A |] ==> F Join G \<in> Always A"
+ "[| F \<in> invariant A; G \<in> stable A |] ==> F\<squnion>G \<in> Always A"
apply (subst Join_commute)
apply (blast intro: stable_Join_Always1)
done
lemma stable_Join_ensures1:
- "[| F \<in> stable A; G \<in> A ensures B |] ==> F Join G \<in> A ensures B"
+ "[| F \<in> stable A; G \<in> A ensures B |] ==> F\<squnion>G \<in> A ensures B"
apply (simp (no_asm_simp) add: Join_ensures)
apply (simp add: stable_def ensures_def)
apply (erule constrains_weaken, auto)
@@ -307,7 +307,7 @@
(*As above, but exchanging the roles of F and G*)
lemma stable_Join_ensures2:
- "[| F \<in> A ensures B; G \<in> stable A |] ==> F Join G \<in> A ensures B"
+ "[| F \<in> A ensures B; G \<in> stable A |] ==> F\<squnion>G \<in> A ensures B"
apply (subst Join_commute)
apply (blast intro: stable_Join_ensures1)
done
@@ -322,7 +322,7 @@
by (simp add: ok_def)
lemma ok_Join_commute:
- "(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))"
+ "(F ok G & (F\<squnion>G) ok H) = (G ok H & F ok (G\<squnion>H))"
by (auto simp add: ok_def)
lemma ok_commute: "(F ok G) = (G ok F)"
@@ -331,18 +331,18 @@
lemmas ok_sym = ok_commute [THEN iffD1, standard]
lemma ok_iff_OK:
- "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)"
+ "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F\<squnion>G) ok H)"
by (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb
all_conj_distrib eq_commute, blast)
-lemma ok_Join_iff1 [iff]: "F ok (G Join H) = (F ok G & F ok H)"
+lemma ok_Join_iff1 [iff]: "F ok (G\<squnion>H) = (F ok G & F ok H)"
by (auto simp add: ok_def)
-lemma ok_Join_iff2 [iff]: "(G Join H) ok F = (G ok F & H ok F)"
+lemma ok_Join_iff2 [iff]: "(G\<squnion>H) ok F = (G ok F & H ok F)"
by (auto simp add: ok_def)
(*useful? Not with the previous two around*)
-lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)"
+lemma ok_Join_commute_I: "[| F ok G; (F\<squnion>G) ok H |] ==> F ok (G\<squnion>H)"
by (auto simp add: ok_def)
lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (\<forall>i \<in> I. F ok G i)"
@@ -363,7 +363,7 @@
lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"
by (auto simp add: Allowed_def)
-lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F \<inter> Allowed G"
+lemma Allowed_Join [simp]: "Allowed (F\<squnion>G) = Allowed F \<inter> Allowed G"
by (auto simp add: Allowed_def)
lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (\<Inter>i \<in> I. Allowed (F i))"
@@ -428,10 +428,10 @@
by (auto simp add: ok_def safety_prop_Acts_iff)
text{*The union of two total programs is total.*}
-lemma totalize_Join: "totalize F Join totalize G = totalize (F Join G)"
+lemma totalize_Join: "totalize F\<squnion>totalize G = totalize (F\<squnion>G)"
by (simp add: program_equalityI totalize_def Join_def image_Un)
-lemma all_total_Join: "[|all_total F; all_total G|] ==> all_total (F Join G)"
+lemma all_total_Join: "[|all_total F; all_total G|] ==> all_total (F\<squnion>G)"
by (simp add: all_total_def, blast)
lemma totalize_JN: "(\<Squnion>i \<in> I. totalize (F i)) = totalize(\<Squnion>i \<in> I. F i)"