# HG changeset patch # User paulson # Date 1044378760 -3600 # Node ID 3786b2fd680800c64032056fff8b5aea71b55384 # Parent d643300e4fc073c940699e7bceb591a2c5ddf7d3 some x-symbols diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Comp.thy --- a/src/HOL/UNITY/Comp.thy Mon Feb 03 11:45:05 2003 +0100 +++ b/src/HOL/UNITY/Comp.thy Tue Feb 04 18:12:40 2003 +0100 @@ -9,7 +9,7 @@ Revised by Sidi Ehmety on January 2001 -Added: a strong form of the <= relation (component_of) and localize +Added: a strong form of the \ relation (component_of) and localize *) @@ -20,33 +20,32 @@ instance program :: (type) ord .. defs - component_def: "F <= H == EX G. F Join G = H" - strict_component_def: "(F < (H::'a program)) == (F <= H & F ~= H)" + component_def: "F \ H == \G. F Join G = H" + strict_component_def: "(F < (H::'a program)) == (F \ H & F \ H)" constdefs - component_of :: "'a program=>'a program=> bool" + component_of :: "'a program =>'a program=> bool" (infixl "component'_of" 50) - "F component_of H == EX G. F ok G & F Join G = H" + "F component_of H == \G. F ok G & F Join G = H" strict_component_of :: "'a program\'a program=> bool" (infixl "strict'_component'_of" 50) - "F strict_component_of H == F component_of H & F~=H" + "F strict_component_of H == F component_of H & F\H" preserves :: "('a=>'b) => 'a program set" - "preserves v == INT z. stable {s. v s = z}" + "preserves v == \z. stable {s. v s = z}" localize :: "('a=>'b) => 'a program => 'a program" "localize v F == mk_program(Init F, Acts F, - AllowedActs F Int (UN G:preserves v. Acts G))" + AllowedActs F \ (\G \ preserves v. Acts G))" funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c" "funPair f g == %x. (f x, g x)" subsection{*The component relation*} -lemma componentI: - "H <= F | H <= G ==> H <= (F Join G)" +lemma componentI: "H \ F | H \ G ==> H \ (F Join 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) @@ -54,61 +53,61 @@ done lemma component_eq_subset: - "(F <= G) = - (Init G <= Init F & Acts F <= Acts G & AllowedActs G <= AllowedActs F)" + "(F \ G) = + (Init G \ Init F & Acts F \ Acts G & AllowedActs G \ AllowedActs F)" apply (unfold component_def) apply (force intro!: exI program_equalityI) done -lemma component_SKIP [iff]: "SKIP <= F" +lemma component_SKIP [iff]: "SKIP \ F" apply (unfold component_def) apply (force intro: Join_SKIP_left) done -lemma component_refl [iff]: "F <= (F :: 'a program)" +lemma component_refl [iff]: "F \ (F :: 'a program)" apply (unfold component_def) apply (blast intro: Join_SKIP_right) done -lemma SKIP_minimal: "F <= SKIP ==> F = SKIP" +lemma SKIP_minimal: "F \ SKIP ==> F = SKIP" by (auto intro!: program_equalityI simp add: component_eq_subset) -lemma component_Join1: "F <= (F Join G)" +lemma component_Join1: "F \ (F Join G)" by (unfold component_def, blast) -lemma component_Join2: "G <= (F Join G)" +lemma component_Join2: "G \ (F Join G)" apply (unfold component_def) apply (simp add: Join_commute, blast) done -lemma Join_absorb1: "F<=G ==> F Join G = G" +lemma Join_absorb1: "F \ G ==> F Join G = G" by (auto simp add: component_def Join_left_absorb) -lemma Join_absorb2: "G<=F ==> F Join G = F" +lemma Join_absorb2: "G \ F ==> F Join G = F" by (auto simp add: Join_ac component_def) -lemma JN_component_iff: "((JOIN I F) <= H) = (ALL i: I. F i <= H)" +lemma JN_component_iff: "((JOIN I F) \ H) = (\i \ I. F i \ H)" by (simp add: component_eq_subset, blast) -lemma component_JN: "i : I ==> (F i) <= (JN i:I. (F i))" +lemma component_JN: "i \ I ==> (F i) \ (\i \ I. (F i))" apply (unfold component_def) apply (blast intro: JN_absorb) done -lemma component_trans: "[| F <= G; G <= H |] ==> F <= (H :: 'a program)" +lemma component_trans: "[| F \ G; G \ H |] ==> F \ (H :: 'a program)" apply (unfold component_def) apply (blast intro: Join_assoc [symmetric]) done -lemma component_antisym: "[| F <= G; G <= F |] ==> F = (G :: 'a program)" +lemma component_antisym: "[| F \ G; G \ F |] ==> F = (G :: 'a program)" apply (simp (no_asm_use) add: component_eq_subset) apply (blast intro!: program_equalityI) done -lemma Join_component_iff: "((F Join G) <= H) = (F <= H & G <= H)" +lemma Join_component_iff: "((F Join G) \ H) = (F \ H & G \ H)" by (simp add: component_eq_subset, blast) -lemma component_constrains: "[| F <= G; G : A co B |] ==> F : A co B" +lemma component_constrains: "[| F \ G; G \ A co B |] ==> F \ A co B" by (auto simp add: constrains_def component_eq_subset) (*Used in Guar.thy to show that programs are partially ordered*) @@ -117,34 +116,34 @@ subsection{*The preserves property*} -lemma preservesI: "(!!z. F : stable {s. v s = z}) ==> F : preserves v" +lemma preservesI: "(!!z. F \ stable {s. v s = z}) ==> F \ preserves v" by (unfold preserves_def, blast) lemma preserves_imp_eq: - "[| F : preserves v; act : Acts F; (s,s') : act |] ==> v s = v s'" + "[| F \ preserves v; act \ Acts F; (s,s') \ act |] ==> v s = v s'" apply (unfold preserves_def stable_def constrains_def, force) done lemma Join_preserves [iff]: - "(F Join G : preserves v) = (F : preserves v & G : preserves v)" + "(F Join G \ preserves v) = (F \ preserves v & G \ preserves v)" apply (unfold preserves_def, auto) done lemma JN_preserves [iff]: - "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)" + "(JOIN I F \ preserves v) = (\i \ I. F i \ preserves v)" apply (simp add: JN_stable preserves_def, blast) done -lemma SKIP_preserves [iff]: "SKIP : preserves v" +lemma SKIP_preserves [iff]: "SKIP \ preserves v" by (auto simp add: preserves_def) lemma funPair_apply [simp]: "(funPair f g) x = (f x, g x)" by (simp add: funPair_def) -lemma preserves_funPair: "preserves (funPair v w) = preserves v Int preserves w" +lemma preserves_funPair: "preserves (funPair v w) = preserves v \ preserves w" by (auto simp add: preserves_def stable_def constrains_def, blast) -(* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *) +(* (F \ preserves (funPair v w)) = (F \ preserves v \ preserves w) *) declare preserves_funPair [THEN eqset_imp_iff, iff] @@ -157,20 +156,20 @@ lemma snd_o_funPair [simp]: "snd o (funPair f g) = g" by (simp add: funPair_def o_def) -lemma subset_preserves_o: "preserves v <= preserves (w o v)" +lemma subset_preserves_o: "preserves v \ preserves (w o v)" by (force simp add: preserves_def stable_def constrains_def) -lemma preserves_subset_stable: "preserves v <= stable {s. P (v s)}" +lemma preserves_subset_stable: "preserves v \ stable {s. P (v s)}" apply (auto simp add: preserves_def stable_def constrains_def) apply (rename_tac s' s) apply (subgoal_tac "v s = v s'") apply (force+) done -lemma preserves_subset_increasing: "preserves v <= increasing v" +lemma preserves_subset_increasing: "preserves v \ increasing v" by (auto simp add: preserves_subset_stable [THEN subsetD] increasing_def) -lemma preserves_id_subset_stable: "preserves id <= stable A" +lemma preserves_id_subset_stable: "preserves id \ stable A" by (force simp add: preserves_def stable_def constrains_def) @@ -183,27 +182,27 @@ (** Some lemmas used only in Client.ML **) lemma stable_localTo_stable2: - "[| F : stable {s. P (v s) (w s)}; - G : preserves v; G : preserves w |] - ==> F Join G : stable {s. P (v s) (w s)}" -apply (simp (no_asm_simp)) -apply (subgoal_tac "G: preserves (funPair v w) ") + "[| F \ stable {s. P (v s) (w s)}; + G \ preserves v; G \ preserves w |] + ==> F Join G \ stable {s. P (v s) (w s)}" +apply (simp) +apply (subgoal_tac "G \ preserves (funPair v w) ") prefer 2 apply simp -apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto) +apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto) done lemma Increasing_preserves_Stable: - "[| F : stable {s. v s <= w s}; G : preserves v; - F Join G : Increasing w |] - ==> F Join G : Stable {s. v s <= w s}" + "[| F \ stable {s. v s \ w s}; G \ preserves v; + F Join G \ Increasing w |] + ==> F Join G \ Stable {s. v s \ 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*) apply (auto simp add: preserves_def stable_def constrains_def) apply (case_tac "act: Acts F", blast) (*We have a G-action, so delete assumptions about F-actions*) -apply (erule_tac V = "ALL act:Acts F. ?P act" in thin_rl) -apply (erule_tac V = "ALL z. ALL act:Acts F. ?P z act" in thin_rl) +apply (erule_tac V = "\act \ Acts F. ?P act" in thin_rl) +apply (erule_tac V = "\z. \act \ Acts F. ?P z act" in thin_rl) apply (subgoal_tac "v x = v xa") prefer 2 apply blast apply auto @@ -212,12 +211,12 @@ (** component_of **) -(* component_of is stronger than <= *) -lemma component_of_imp_component: "F component_of H ==> F <= H" +(* component_of is stronger than \ *) +lemma component_of_imp_component: "F component_of H ==> F \ H" by (unfold component_def component_of_def, blast) -(* component_of satisfies many of the <='s properties *) +(* component_of satisfies many of the same properties as \ *) lemma component_of_refl [simp]: "F component_of F" apply (unfold component_of_def) apply (rule_tac x = SKIP in exI, auto) @@ -243,7 +242,7 @@ by (simp add: localize_def) lemma localize_AllowedActs_eq [simp]: - "AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)" + "AllowedActs (localize v F) = AllowedActs F \ (\G \ preserves v. Acts G)" by (unfold localize_def, auto) end diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Constrains.thy --- a/src/HOL/UNITY/Constrains.thy Mon Feb 03 11:45:05 2003 +0100 +++ b/src/HOL/UNITY/Constrains.thy Tue Feb 04 18:12:40 2003 +0100 @@ -18,65 +18,65 @@ inductive "traces init acts" intros (*Initial trace is empty*) - Init: "s: init ==> (s,[]) : traces init acts" + Init: "s \ init ==> (s,[]) \ traces init acts" - Acts: "[| act: acts; (s,evs) : traces init acts; (s,s'): act |] - ==> (s', s#evs) : traces init acts" + Acts: "[| act: acts; (s,evs) \ traces init acts; (s,s'): act |] + ==> (s', s#evs) \ traces init acts" consts reachable :: "'a program => 'a set" inductive "reachable F" intros - Init: "s: Init F ==> s : reachable F" + Init: "s \ Init F ==> s \ reachable F" - Acts: "[| act: Acts F; s : reachable F; (s,s'): act |] - ==> s' : reachable F" + Acts: "[| act: Acts F; s \ reachable F; (s,s'): act |] + ==> s' \ reachable F" constdefs Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60) - "A Co B == {F. F : (reachable F Int A) co B}" + "A Co B == {F. F \ (reachable F \ A) co B}" Unless :: "['a set, 'a set] => 'a program set" (infixl "Unless" 60) - "A Unless B == (A-B) Co (A Un B)" + "A Unless B == (A-B) Co (A \ B)" Stable :: "'a set => 'a program set" "Stable A == A Co A" (*Always is the weak form of "invariant"*) Always :: "'a set => 'a program set" - "Always A == {F. Init F <= A} Int Stable A" + "Always A == {F. Init F \ A} \ Stable A" - (*Polymorphic in both states and the meaning of <= *) + (*Polymorphic in both states and the meaning of \ *) Increasing :: "['a => 'b::{order}] => 'a program set" - "Increasing f == INT z. Stable {s. z <= f s}" + "Increasing f == \z. Stable {s. z \ f s}" subsection{*traces and reachable*} lemma reachable_equiv_traces: - "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}" + "reachable F = {s. \evs. (s,evs): traces (Init F) (Acts F)}" apply safe apply (erule_tac [2] traces.induct) apply (erule reachable.induct) apply (blast intro: reachable.intros traces.intros)+ done -lemma Init_subset_reachable: "Init F <= reachable F" +lemma Init_subset_reachable: "Init F \ reachable F" by (blast intro: reachable.intros) lemma stable_reachable [intro!,simp]: - "Acts G <= Acts F ==> G : stable (reachable F)" + "Acts G \ Acts F ==> G \ stable (reachable F)" by (blast intro: stableI constrainsI reachable.intros) (*The set of all reachable states is an invariant...*) -lemma invariant_reachable: "F : invariant (reachable F)" +lemma invariant_reachable: "F \ invariant (reachable F)" apply (simp add: invariant_def) apply (blast intro: reachable.intros) done (*...in fact the strongest invariant!*) -lemma invariant_includes_reachable: "F : invariant A ==> reachable F <= A" +lemma invariant_includes_reachable: "F \ invariant A ==> reachable F \ A" apply (simp add: stable_def constrains_def invariant_def) apply (rule subsetI) apply (erule reachable.induct) @@ -86,55 +86,55 @@ subsection{*Co*} -(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*) +(*F \ B co B' ==> F \ (reachable F \ B) co (reachable F \ B')*) lemmas constrains_reachable_Int = subset_refl [THEN stable_reachable [unfolded stable_def], THEN constrains_Int, standard] (*Resembles the previous definition of Constrains*) lemma Constrains_eq_constrains: - "A Co B = {F. F : (reachable F Int A) co (reachable F Int B)}" + "A Co B = {F. F \ (reachable F \ A) co (reachable F \ B)}" apply (unfold Constrains_def) apply (blast dest: constrains_reachable_Int intro: constrains_weaken) done -lemma constrains_imp_Constrains: "F : A co A' ==> F : A Co A'" +lemma constrains_imp_Constrains: "F \ A co A' ==> F \ A Co A'" apply (unfold Constrains_def) apply (blast intro: constrains_weaken_L) done -lemma stable_imp_Stable: "F : stable A ==> F : Stable A" +lemma stable_imp_Stable: "F \ stable A ==> F \ Stable A" apply (unfold stable_def Stable_def) apply (erule constrains_imp_Constrains) done lemma ConstrainsI: - "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') - ==> F : A Co A'" + "(!!act s s'. [| act: Acts F; (s,s') \ act; s \ A |] ==> s': A') + ==> F \ A Co A'" apply (rule constrains_imp_Constrains) apply (blast intro: constrainsI) done -lemma Constrains_empty [iff]: "F : {} Co B" +lemma Constrains_empty [iff]: "F \ {} Co B" by (unfold Constrains_def constrains_def, blast) -lemma Constrains_UNIV [iff]: "F : A Co UNIV" +lemma Constrains_UNIV [iff]: "F \ A Co UNIV" by (blast intro: ConstrainsI) lemma Constrains_weaken_R: - "[| F : A Co A'; A'<=B' |] ==> F : A Co B'" + "[| F \ A Co A'; A'<=B' |] ==> F \ A Co B'" apply (unfold Constrains_def) apply (blast intro: constrains_weaken_R) done lemma Constrains_weaken_L: - "[| F : A Co A'; B<=A |] ==> F : B Co A'" + "[| F \ A Co A'; B \ A |] ==> F \ B Co A'" apply (unfold Constrains_def) apply (blast intro: constrains_weaken_L) done lemma Constrains_weaken: - "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'" + "[| F \ A Co A'; B \ A; A'<=B' |] ==> F \ B Co B'" apply (unfold Constrains_def) apply (blast intro: constrains_weaken) done @@ -142,14 +142,14 @@ (** Union **) lemma Constrains_Un: - "[| F : A Co A'; F : B Co B' |] ==> F : (A Un B) Co (A' Un B')" + "[| F \ A Co A'; F \ B Co B' |] ==> F \ (A \ B) Co (A' \ B')" apply (unfold Constrains_def) apply (blast intro: constrains_Un [THEN constrains_weaken]) done lemma Constrains_UN: - assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)" - shows "F : (UN i:I. A i) Co (UN i:I. A' i)" + assumes Co: "!!i. i \ I ==> F \ (A i) Co (A' i)" + shows "F \ (\i \ I. A i) Co (\i \ I. A' i)" apply (unfold Constrains_def) apply (rule CollectI) apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_UN, @@ -159,83 +159,83 @@ (** Intersection **) lemma Constrains_Int: - "[| F : A Co A'; F : B Co B' |] ==> F : (A Int B) Co (A' Int B')" + "[| F \ A Co A'; F \ B Co B' |] ==> F \ (A \ B) Co (A' \ B')" apply (unfold Constrains_def) apply (blast intro: constrains_Int [THEN constrains_weaken]) done lemma Constrains_INT: - assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)" - shows "F : (INT i:I. A i) Co (INT i:I. A' i)" + assumes Co: "!!i. i \ I ==> F \ (A i) Co (A' i)" + shows "F \ (\i \ I. A i) Co (\i \ I. A' i)" apply (unfold Constrains_def) apply (rule CollectI) apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_INT, THEN constrains_weaken], auto) done -lemma Constrains_imp_subset: "F : A Co A' ==> reachable F Int A <= A'" +lemma Constrains_imp_subset: "F \ A Co A' ==> reachable F \ A \ A'" by (simp add: constrains_imp_subset Constrains_def) -lemma Constrains_trans: "[| F : A Co B; F : B Co C |] ==> F : A Co C" +lemma Constrains_trans: "[| F \ A Co B; F \ B Co C |] ==> F \ A Co C" apply (simp add: Constrains_eq_constrains) apply (blast intro: constrains_trans constrains_weaken) done lemma Constrains_cancel: - "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')" + "[| F \ A Co (A' \ B); F \ B Co B' |] ==> F \ A Co (A' \ B')" by (simp add: Constrains_eq_constrains constrains_def, blast) subsection{*Stable*} (*Useful because there's no Stable_weaken. [Tanja Vos]*) -lemma Stable_eq: "[| F: Stable A; A = B |] ==> F : Stable B" +lemma Stable_eq: "[| F \ Stable A; A = B |] ==> F \ Stable B" by blast -lemma Stable_eq_stable: "(F : Stable A) = (F : stable (reachable F Int A))" +lemma Stable_eq_stable: "(F \ Stable A) = (F \ stable (reachable F \ A))" by (simp add: Stable_def Constrains_eq_constrains stable_def) -lemma StableI: "F : A Co A ==> F : Stable A" +lemma StableI: "F \ A Co A ==> F \ Stable A" by (unfold Stable_def, assumption) -lemma StableD: "F : Stable A ==> F : A Co A" +lemma StableD: "F \ Stable A ==> F \ A Co A" by (unfold Stable_def, assumption) lemma Stable_Un: - "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Un A')" + "[| F \ Stable A; F \ Stable A' |] ==> F \ Stable (A \ A')" apply (unfold Stable_def) apply (blast intro: Constrains_Un) done lemma Stable_Int: - "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Int A')" + "[| F \ Stable A; F \ Stable A' |] ==> F \ Stable (A \ A')" apply (unfold Stable_def) apply (blast intro: Constrains_Int) done lemma Stable_Constrains_Un: - "[| F : Stable C; F : A Co (C Un A') |] - ==> F : (C Un A) Co (C Un A')" + "[| F \ Stable C; F \ A Co (C \ A') |] + ==> F \ (C \ A) Co (C \ A')" apply (unfold Stable_def) apply (blast intro: Constrains_Un [THEN Constrains_weaken]) done lemma Stable_Constrains_Int: - "[| F : Stable C; F : (C Int A) Co A' |] - ==> F : (C Int A) Co (C Int A')" + "[| F \ Stable C; F \ (C \ A) Co A' |] + ==> F \ (C \ A) Co (C \ A')" apply (unfold Stable_def) apply (blast intro: Constrains_Int [THEN Constrains_weaken]) done lemma Stable_UN: - "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (UN i:I. A i)" + "(!!i. i \ I ==> F \ Stable (A i)) ==> F \ Stable (\i \ I. A i)" by (simp add: Stable_def Constrains_UN) lemma Stable_INT: - "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (INT i:I. A i)" + "(!!i. i \ I ==> F \ Stable (A i)) ==> F \ Stable (\i \ I. A i)" by (simp add: Stable_def Constrains_INT) -lemma Stable_reachable: "F : Stable (reachable F)" +lemma Stable_reachable: "F \ Stable (reachable F)" by (simp add: Stable_eq_stable) @@ -243,22 +243,22 @@ subsection{*Increasing*} lemma IncreasingD: - "F : Increasing f ==> F : Stable {s. x <= f s}" + "F \ Increasing f ==> F \ Stable {s. x \ f s}" by (unfold Increasing_def, blast) lemma mono_Increasing_o: - "mono g ==> Increasing f <= Increasing (g o f)" + "mono g ==> Increasing f \ Increasing (g o f)" apply (simp add: Increasing_def Stable_def Constrains_def stable_def constrains_def) apply (blast intro: monoD order_trans) done lemma strict_IncreasingD: - "!!z::nat. F : Increasing f ==> F: Stable {s. z < f s}" + "!!z::nat. F \ Increasing f ==> F \ Stable {s. z < f s}" by (simp add: Increasing_def Suc_le_eq [symmetric]) lemma increasing_imp_Increasing: - "F : increasing f ==> F : Increasing f" + "F \ increasing f ==> F \ Increasing f" apply (unfold increasing_def Increasing_def) apply (blast intro: stable_imp_Stable) done @@ -270,17 +270,17 @@ subsection{*The Elimination Theorem*} (*The "free" m has become universally quantified! Should the premise be !!m -instead of ALL m ? Would make it harder to use in forward proof.*) +instead of \m ? Would make it harder to use in forward proof.*) lemma Elimination: - "[| ALL m. F : {s. s x = m} Co (B m) |] - ==> F : {s. s x : M} Co (UN m:M. B m)" + "[| \m. F \ {s. s x = m} Co (B m) |] + ==> F \ {s. s x \ M} Co (\m \ M. B m)" by (unfold Constrains_def constrains_def, blast) (*As above, but for the trivial case of a one-variable state, in which the state is identified with its one variable.*) lemma Elimination_sing: - "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)" + "(\m. F \ {m} Co (B m)) ==> F \ M Co (\m \ M. B m)" by (unfold Constrains_def constrains_def, blast) @@ -288,10 +288,10 @@ (** Natural deduction rules for "Always A" **) -lemma AlwaysI: "[| Init F<=A; F : Stable A |] ==> F : Always A" +lemma AlwaysI: "[| Init F \ A; F \ Stable A |] ==> F \ Always A" by (simp add: Always_def) -lemma AlwaysD: "F : Always A ==> Init F<=A & F : Stable A" +lemma AlwaysD: "F \ Always A ==> Init F \ A & F \ Stable A" by (simp add: Always_def) lemmas AlwaysE = AlwaysD [THEN conjE, standard] @@ -299,7 +299,7 @@ (*The set of all reachable states is Always*) -lemma Always_includes_reachable: "F : Always A ==> reachable F <= A" +lemma Always_includes_reachable: "F \ Always A ==> reachable F \ A" apply (simp add: Stable_def Constrains_def constrains_def Always_def) apply (rule subsetI) apply (erule reachable.induct) @@ -307,7 +307,7 @@ done lemma invariant_imp_Always: - "F : invariant A ==> F : Always A" + "F \ invariant A ==> F \ Always A" apply (unfold Always_def invariant_def Stable_def stable_def) apply (blast intro: constrains_imp_Constrains) done @@ -316,55 +316,55 @@ invariant_reachable [THEN invariant_imp_Always, standard] lemma Always_eq_invariant_reachable: - "Always A = {F. F : invariant (reachable F Int A)}" + "Always A = {F. F \ invariant (reachable F \ A)}" apply (simp add: Always_def invariant_def Stable_def Constrains_eq_constrains stable_def) apply (blast intro: reachable.intros) done (*the RHS is the traditional definition of the "always" operator*) -lemma Always_eq_includes_reachable: "Always A = {F. reachable F <= A}" +lemma Always_eq_includes_reachable: "Always A = {F. reachable F \ A}" by (auto dest: invariant_includes_reachable simp add: Int_absorb2 invariant_reachable Always_eq_invariant_reachable) lemma Always_UNIV_eq [simp]: "Always UNIV = UNIV" by (auto simp add: Always_eq_includes_reachable) -lemma UNIV_AlwaysI: "UNIV <= A ==> F : Always A" +lemma UNIV_AlwaysI: "UNIV \ A ==> F \ Always A" by (auto simp add: Always_eq_includes_reachable) -lemma Always_eq_UN_invariant: "Always A = (UN I: Pow A. invariant I)" +lemma Always_eq_UN_invariant: "Always A = (\I \ Pow A. invariant I)" apply (simp add: Always_eq_includes_reachable) apply (blast intro: invariantI Init_subset_reachable [THEN subsetD] invariant_includes_reachable [THEN subsetD]) done -lemma Always_weaken: "[| F : Always A; A <= B |] ==> F : Always B" +lemma Always_weaken: "[| F \ Always A; A \ B |] ==> F \ Always B" by (auto simp add: Always_eq_includes_reachable) subsection{*"Co" rules involving Always*} lemma Always_Constrains_pre: - "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')" + "F \ Always INV ==> (F \ (INV \ A) Co A') = (F \ A Co A')" by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def Int_assoc [symmetric]) lemma Always_Constrains_post: - "F : Always INV ==> (F : A Co (INV Int A')) = (F : A Co A')" + "F \ Always INV ==> (F \ A Co (INV \ A')) = (F \ A Co A')" by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_eq_constrains Int_assoc [symmetric]) -(* [| F : Always INV; F : (INV Int A) Co A' |] ==> F : A Co A' *) +(* [| F \ Always INV; F \ (INV \ A) Co A' |] ==> F \ A Co A' *) lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1, standard] -(* [| F : Always INV; F : A Co A' |] ==> F : A Co (INV Int A') *) +(* [| F \ Always INV; F \ A Co A' |] ==> F \ A Co (INV \ A') *) lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard] (*The analogous proof of Always_LeadsTo_weaken doesn't terminate*) lemma Always_Constrains_weaken: - "[| F : Always C; F : A Co A'; - C Int B <= A; C Int A' <= B' |] - ==> F : B Co B'" + "[| F \ Always C; F \ A Co A'; + C \ B \ A; C \ A' \ B' |] + ==> F \ B Co B'" apply (rule Always_ConstrainsI, assumption) apply (drule Always_ConstrainsD, assumption) apply (blast intro: Constrains_weaken) @@ -373,23 +373,23 @@ (** Conjoining Always properties **) -lemma Always_Int_distrib: "Always (A Int B) = Always A Int Always B" +lemma Always_Int_distrib: "Always (A \ B) = Always A \ Always B" by (auto simp add: Always_eq_includes_reachable) -lemma Always_INT_distrib: "Always (INTER I A) = (INT i:I. Always (A i))" +lemma Always_INT_distrib: "Always (INTER I A) = (\i \ I. Always (A i))" by (auto simp add: Always_eq_includes_reachable) lemma Always_Int_I: - "[| F : Always A; F : Always B |] ==> F : Always (A Int B)" + "[| F \ Always A; F \ Always B |] ==> F \ Always (A \ B)" by (simp add: Always_Int_distrib) (*Allows a kind of "implication introduction"*) lemma Always_Compl_Un_eq: - "F : Always A ==> (F : Always (-A Un B)) = (F : Always B)" + "F \ Always A ==> (F \ Always (-A \ B)) = (F \ Always B)" by (auto simp add: Always_eq_includes_reachable) (*Delete the nearest invariance assumption (which will be the second one used by Always_Int_I) *) -lemmas Always_thin = thin_rl [of "F : Always A", standard] +lemmas Always_thin = thin_rl [of "F \ Always A", standard] end diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Detects.thy --- a/src/HOL/UNITY/Detects.thy Mon Feb 03 11:45:05 2003 +0100 +++ b/src/HOL/UNITY/Detects.thy Tue Feb 04 18:12:40 2003 +0100 @@ -15,47 +15,47 @@ op_Equality :: "['a set, 'a set] => 'a set" (infixl "<==>" 60) defs - Detects_def: "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)" - Equality_def: "A <==> B == (-A Un B) Int (A Un -B)" + Detects_def: "A Detects B == (Always (-A \ B)) \ (B LeadsTo A)" + Equality_def: "A <==> B == (-A \ B) \ (A \ -B)" (* Corollary from Sectiom 3.6.4 *) -lemma Always_at_FP: "F: A LeadsTo B ==> F : Always (-((FP F) Int A Int -B))" +lemma Always_at_FP: "F \ A LeadsTo B ==> F \ Always (-((FP F) \ A \ -B))" apply (rule LeadsTo_empty) -apply (subgoal_tac "F : (FP F Int A Int - B) LeadsTo (B Int (FP F Int -B))") -apply (subgoal_tac [2] " (FP F Int A Int - B) = (A Int (FP F Int -B))") -apply (subgoal_tac "(B Int (FP F Int -B)) = {}") +apply (subgoal_tac "F \ (FP F \ A \ - B) LeadsTo (B \ (FP F \ -B))") +apply (subgoal_tac [2] " (FP F \ A \ - B) = (A \ (FP F \ -B))") +apply (subgoal_tac "(B \ (FP F \ -B)) = {}") apply auto apply (blast intro: PSP_Stable stable_imp_Stable stable_FP_Int) done lemma Detects_Trans: - "[| F : A Detects B; F : B Detects C |] ==> F : A Detects C" + "[| F \ A Detects B; F \ B Detects C |] ==> F \ A Detects C" apply (unfold Detects_def Int_def) apply (simp (no_asm)) apply safe apply (rule_tac [2] LeadsTo_Trans) apply auto -apply (subgoal_tac "F : Always ((-A Un B) Int (-B Un C))") +apply (subgoal_tac "F \ Always ((-A \ B) \ (-B \ C))") apply (blast intro: Always_weaken) apply (simp add: Always_Int_distrib) done -lemma Detects_refl: "F : A Detects A" +lemma Detects_refl: "F \ A Detects A" apply (unfold Detects_def) apply (simp (no_asm) add: Un_commute Compl_partition subset_imp_LeadsTo) done -lemma Detects_eq_Un: "(A<==>B) = (A Int B) Un (-A Int -B)" +lemma Detects_eq_Un: "(A<==>B) = (A \ B) \ (-A \ -B)" apply (unfold Equality_def) apply blast done (*Not quite antisymmetry: sets A and B agree in all reachable states *) lemma Detects_antisym: - "[| F : A Detects B; F : B Detects A|] ==> F : Always (A <==> B)" + "[| F \ A Detects B; F \ B Detects A|] ==> F \ Always (A <==> B)" apply (unfold Detects_def Equality_def) apply (simp add: Always_Int_I Un_commute) done @@ -64,7 +64,7 @@ (* Theorem from Section 3.8 *) lemma Detects_Always: - "F : A Detects B ==> F : Always ((-(FP F)) Un (A <==> B))" + "F \ A Detects B ==> F \ Always ((-(FP F)) \ (A <==> B))" apply (unfold Detects_def Equality_def) apply (simp (no_asm) add: Un_Int_distrib Always_Int_distrib) apply (blast dest: Always_at_FP intro: Always_weaken) @@ -73,11 +73,11 @@ (* Theorem from exercise 11.1 Section 11.3.1 *) lemma Detects_Imp_LeadstoEQ: - "F : A Detects B ==> F : UNIV LeadsTo (A <==> B)" + "F \ A Detects B ==> F \ UNIV LeadsTo (A <==> B)" apply (unfold Detects_def Equality_def) apply (rule_tac B = "B" in LeadsTo_Diff) -prefer 2 apply (blast intro: Always_LeadsTo_weaken) -apply (blast intro: Always_LeadsToI subset_imp_LeadsTo) + apply (blast intro: Always_LeadsToI subset_imp_LeadsTo) +apply (blast intro: Always_LeadsTo_weaken) done diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Extend.thy --- a/src/HOL/UNITY/Extend.thy Mon Feb 03 11:45:05 2003 +0100 +++ b/src/HOL/UNITY/Extend.thy Tue Feb 04 18:12:40 2003 +0100 @@ -16,23 +16,23 @@ (*MOVE to Relation.thy?*) Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set" - "Restrict A r == r Int (A <*> UNIV)" + "Restrict A r == r \ (A <*> UNIV)" good_map :: "['a*'b => 'c] => bool" - "good_map h == surj h & (ALL x y. fst (inv h (h (x,y))) = x)" + "good_map h == surj h & (\x y. fst (inv h (h (x,y))) = x)" (*Using the locale constant "f", this is f (h (x,y))) = x*) extend_set :: "['a*'b => 'c, 'a set] => 'c set" "extend_set h A == h ` (A <*> UNIV)" project_set :: "['a*'b => 'c, 'c set] => 'a set" - "project_set h C == {x. EX y. h(x,y) : C}" + "project_set h C == {x. \y. h(x,y) \ C}" extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set" - "extend_act h == %act. UN (s,s'): act. UN y. {(h(s,y), h(s',y))}" + "extend_act h == %act. \(s,s') \ act. \y. {(h(s,y), h(s',y))}" project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set" - "project_act h act == {(x,x'). EX y y'. (h(x,y), h(x',y')) : act}" + "project_act h act == {(x,x'). \y y'. (h(x,y), h(x',y')) \ act}" extend :: "['a*'b => 'c, 'a program] => 'c program" "extend h F == mk_program (extend_set h (Init F), @@ -56,7 +56,7 @@ good_h: "good_map h" defines f_def: "f z == fst (inv h z)" and g_def: "g z == snd (inv h z)" - and slice_def: "slice Z y == {x. h(x,y) : Z}" + and slice_def: "slice Z y == {x. h(x,y) \ Z}" (** These we prove OUTSIDE the locale. **) @@ -65,7 +65,7 @@ subsection{*Restrict*} (*MOVE to Relation.thy?*) -lemma Restrict_iff [iff]: "((x,y): Restrict A r) = ((x,y): r & x: A)" +lemma Restrict_iff [iff]: "((x,y): Restrict A r) = ((x,y): r & x \ A)" by (unfold Restrict_def, blast) lemma Restrict_UNIV [simp]: "Restrict UNIV = id" @@ -76,29 +76,29 @@ lemma Restrict_empty [simp]: "Restrict {} r = {}" by (auto simp add: Restrict_def) -lemma Restrict_Int [simp]: "Restrict A (Restrict B r) = Restrict (A Int B) r" +lemma Restrict_Int [simp]: "Restrict A (Restrict B r) = Restrict (A \ B) r" by (unfold Restrict_def, blast) -lemma Restrict_triv: "Domain r <= A ==> Restrict A r = r" +lemma Restrict_triv: "Domain r \ A ==> Restrict A r = r" by (unfold Restrict_def, auto) -lemma Restrict_subset: "Restrict A r <= r" +lemma Restrict_subset: "Restrict A r \ r" by (unfold Restrict_def, auto) lemma Restrict_eq_mono: - "[| A <= B; Restrict B r = Restrict B s |] + "[| A \ B; Restrict B r = Restrict B s |] ==> Restrict A r = Restrict A s" by (unfold Restrict_def, blast) lemma Restrict_imageI: - "[| s : RR; Restrict A r = Restrict A s |] - ==> Restrict A r : Restrict A ` RR" + "[| s \ RR; Restrict A r = Restrict A s |] + ==> Restrict A r \ Restrict A ` RR" by (unfold Restrict_def image_def, auto) -lemma Domain_Restrict [simp]: "Domain (Restrict A r) = A Int Domain r" +lemma Domain_Restrict [simp]: "Domain (Restrict A r) = A \ Domain r" by blast -lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A Int B)" +lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A \ B)" by blast lemma insert_Id_image_Acts: "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F" @@ -169,19 +169,19 @@ subsection{*@{term extend_set}: basic properties*} lemma project_set_iff [iff]: - "(x : project_set h C) = (EX y. h(x,y) : C)" + "(x \ project_set h C) = (\y. h(x,y) \ C)" by (simp add: project_set_def) -lemma extend_set_mono: "A<=B ==> extend_set h A <= extend_set h B" +lemma extend_set_mono: "A \ B ==> extend_set h A \ extend_set h B" by (unfold extend_set_def, blast) -lemma (in Extend) mem_extend_set_iff [iff]: "z : extend_set h A = (f z : A)" +lemma (in Extend) mem_extend_set_iff [iff]: "z \ extend_set h A = (f z \ A)" apply (unfold extend_set_def) apply (force intro: h_f_g_eq [symmetric]) done lemma (in Extend) extend_set_strict_mono [iff]: - "(extend_set h A <= extend_set h B) = (A <= B)" + "(extend_set h A \ extend_set h B) = (A \ B)" by (unfold extend_set_def, force) lemma extend_set_empty [simp]: "extend_set h {} = {}" @@ -198,7 +198,7 @@ by (unfold extend_set_def, auto) lemma (in Extend) extend_set_project_set: - "C <= extend_set h (project_set h C)" + "C \ extend_set h (project_set h C)" apply (unfold extend_set_def) apply (auto simp add: split_extended_all, blast) done @@ -220,7 +220,7 @@ by (auto intro: f_h_eq [symmetric] simp add: split_extended_all) (*Converse appears to fail*) -lemma (in Extend) project_set_I: "!!z. z : C ==> f z : project_set h C" +lemma (in Extend) project_set_I: "!!z. z \ C ==> f z \ project_set h C" by (auto simp add: split_extended_all) @@ -228,31 +228,31 @@ (*Because A and B could differ on the "other" part of the state, cannot generalize to - project_set h (A Int B) = project_set h A Int project_set h B + project_set h (A \ B) = project_set h A \ project_set h B *) lemma (in Extend) project_set_extend_set_Int: - "project_set h ((extend_set h A) Int B) = A Int (project_set h B)" + "project_set h ((extend_set h A) \ B) = A \ (project_set h B)" by auto (*Unused, but interesting?*) lemma (in Extend) project_set_extend_set_Un: - "project_set h ((extend_set h A) Un B) = A Un (project_set h B)" + "project_set h ((extend_set h A) \ B) = A \ (project_set h B)" by auto lemma project_set_Int_subset: - "project_set h (A Int B) <= (project_set h A) Int (project_set h B)" + "project_set h (A \ B) \ (project_set h A) \ (project_set h B)" by auto lemma (in Extend) extend_set_Un_distrib: - "extend_set h (A Un B) = extend_set h A Un extend_set h B" + "extend_set h (A \ B) = extend_set h A \ extend_set h B" by auto lemma (in Extend) extend_set_Int_distrib: - "extend_set h (A Int B) = extend_set h A Int extend_set h B" + "extend_set h (A \ B) = extend_set h A \ extend_set h B" by auto lemma (in Extend) extend_set_INT_distrib: - "extend_set h (INTER A B) = (INT x:A. extend_set h (B x))" + "extend_set h (INTER A B) = (\x \ A. extend_set h (B x))" by auto lemma (in Extend) extend_set_Diff_distrib: @@ -260,26 +260,26 @@ by auto lemma (in Extend) extend_set_Union: - "extend_set h (Union A) = (UN X:A. extend_set h X)" + "extend_set h (Union A) = (\X \ A. extend_set h X)" by blast lemma (in Extend) extend_set_subset_Compl_eq: - "(extend_set h A <= - extend_set h B) = (A <= - B)" + "(extend_set h A \ - extend_set h B) = (A \ - B)" by (unfold extend_set_def, auto) subsection{*@{term extend_act}*} (*Can't strengthen it to - ((h(s,y), h(s',y')) : extend_act h act) = ((s, s') : act & y=y') + ((h(s,y), h(s',y')) \ extend_act h act) = ((s, s') \ act & y=y') because h doesn't have to be injective in the 2nd argument*) lemma (in Extend) mem_extend_act_iff [iff]: - "((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)" + "((h(s,y), h(s',y)) \ extend_act h act) = ((s, s') \ act)" by (unfold extend_act_def, auto) (*Converse fails: (z,z') would include actions that changed the g-part*) lemma (in Extend) extend_act_D: - "(z, z') : extend_act h act ==> (f z, f z') : act" + "(z, z') \ extend_act h act ==> (f z, f z') \ act" by (unfold extend_act_def, auto) lemma (in Extend) extend_act_inverse [simp]: @@ -292,7 +292,7 @@ by (unfold extend_act_def project_act_def, blast) lemma (in Extend) subset_extend_act_D: - "act' <= extend_act h act ==> project_act h act' <= act" + "act' \ extend_act h act ==> project_act h act' \ act" by (unfold extend_act_def project_act_def, force) lemma (in Extend) inj_extend_act: "inj (extend_act h)" @@ -305,7 +305,7 @@ by (unfold extend_set_def extend_act_def, force) lemma (in Extend) extend_act_strict_mono [iff]: - "(extend_act h act' <= extend_act h act) = (act'<=act)" + "(extend_act h act' \ extend_act h act) = (act'<=act)" by (unfold extend_act_def, auto) declare (in Extend) inj_extend_act [THEN inj_eq, iff] @@ -322,7 +322,7 @@ done lemma (in Extend) project_act_I: - "!!z z'. (z, z') : act ==> (f z, f z') : project_act h act" + "!!z z'. (z, z') \ act ==> (f z, f z') \ project_act h act" apply (unfold project_act_def) apply (force simp add: split_extended_all) done @@ -365,7 +365,7 @@ lemma (in Extend) AllowedActs_project [simp]: "AllowedActs(project h C F) = {act. Restrict (project_set h C) act - : project_act h ` Restrict C ` AllowedActs F}" + \ project_act h ` Restrict C ` AllowedActs F}" apply (simp (no_asm) add: project_def image_iff) apply (subst insert_absorb) apply (auto intro!: bexI [of _ Id] simp add: project_act_def) @@ -386,14 +386,14 @@ by auto lemma project_set_Union: - "project_set h (Union A) = (UN X:A. project_set h X)" + "project_set h (Union A) = (\X \ A. project_set h X)" by blast (*Converse FAILS: the extended state contributing to project_set h C may not coincide with the one contributing to project_act h act*) lemma (in Extend) project_act_Restrict_subset: - "project_act h (Restrict C act) <= + "project_act h (Restrict C act) \ Restrict (project_set h C) (project_act h act)" by (auto simp add: project_act_def) @@ -405,7 +405,7 @@ "project h C (extend h F) = mk_program (Init F, Restrict (project_set h C) ` Acts F, {act. Restrict (project_set h C) act - : project_act h ` Restrict C ` + \ project_act h ` Restrict C ` (project_act h -` AllowedActs F)})" apply (rule program_equalityI) apply simp @@ -439,7 +439,7 @@ done lemma (in Extend) extend_JN [simp]: - "extend h (JOIN I F) = (JN i:I. extend h (F i))" + "extend h (JOIN I F) = (\i \ I. extend h (F i))" apply (rule program_equalityI) apply (simp (no_asm) add: extend_set_INT_distrib) apply (simp add: image_UN, auto) @@ -447,49 +447,49 @@ (** These monotonicity results look natural but are UNUSED **) -lemma (in Extend) extend_mono: "F <= G ==> extend h F <= extend h G" +lemma (in Extend) extend_mono: "F \ G ==> extend h F \ extend h G" by (force simp add: component_eq_subset) -lemma (in Extend) project_mono: "F <= G ==> project h C F <= project h C G" +lemma (in Extend) project_mono: "F \ G ==> project h C F \ project h C G" by (simp add: component_eq_subset, blast) subsection{*Safety: co, stable*} lemma (in Extend) extend_constrains: - "(extend h F : (extend_set h A) co (extend_set h B)) = - (F : A co B)" + "(extend h F \ (extend_set h A) co (extend_set h B)) = + (F \ A co B)" by (simp add: constrains_def) lemma (in Extend) extend_stable: - "(extend h F : stable (extend_set h A)) = (F : stable A)" + "(extend h F \ stable (extend_set h A)) = (F \ stable A)" by (simp add: stable_def extend_constrains) lemma (in Extend) extend_invariant: - "(extend h F : invariant (extend_set h A)) = (F : invariant A)" + "(extend h F \ invariant (extend_set h A)) = (F \ invariant A)" by (simp add: invariant_def extend_stable) (*Projects the state predicates in the property satisfied by extend h F. Converse fails: A and B may differ in their extra variables*) lemma (in Extend) extend_constrains_project_set: - "extend h F : A co B ==> F : (project_set h A) co (project_set h B)" + "extend h F \ A co B ==> F \ (project_set h A) co (project_set h B)" by (auto simp add: constrains_def, force) lemma (in Extend) extend_stable_project_set: - "extend h F : stable A ==> F : stable (project_set h A)" + "extend h F \ stable A ==> F \ stable (project_set h A)" by (simp add: stable_def extend_constrains_project_set) subsection{*Weak safety primitives: Co, Stable*} lemma (in Extend) reachable_extend_f: - "p : reachable (extend h F) ==> f p : reachable F" + "p \ reachable (extend h F) ==> f p \ reachable F" apply (erule reachable.induct) apply (auto intro: reachable.intros simp add: extend_act_def image_iff) done lemma (in Extend) h_reachable_extend: - "h(s,y) : reachable (extend h F) ==> s : reachable F" + "h(s,y) \ reachable (extend h F) ==> s \ reachable F" by (force dest!: reachable_extend_f) lemma (in Extend) reachable_extend_eq: @@ -502,17 +502,17 @@ done lemma (in Extend) extend_Constrains: - "(extend h F : (extend_set h A) Co (extend_set h B)) = - (F : A Co B)" + "(extend h F \ (extend_set h A) Co (extend_set h B)) = + (F \ A Co B)" by (simp add: Constrains_def reachable_extend_eq extend_constrains extend_set_Int_distrib [symmetric]) lemma (in Extend) extend_Stable: - "(extend h F : Stable (extend_set h A)) = (F : Stable A)" + "(extend h F \ Stable (extend_set h A)) = (F \ Stable A)" by (simp add: Stable_def extend_Constrains) lemma (in Extend) extend_Always: - "(extend h F : Always (extend_set h A)) = (F : Always A)" + "(extend h F \ Always (extend_set h A)) = (F \ Always A)" by (simp (no_asm_simp) add: Always_def extend_Stable) @@ -521,24 +521,24 @@ (** projection: monotonicity for safety **) lemma project_act_mono: - "D <= C ==> - project_act h (Restrict D act) <= project_act h (Restrict C act)" + "D \ C ==> + project_act h (Restrict D act) \ project_act h (Restrict C act)" by (auto simp add: project_act_def) lemma (in Extend) project_constrains_mono: - "[| D <= C; project h C F : A co B |] ==> project h D F : A co B" + "[| D \ C; project h C F \ A co B |] ==> project h D F \ A co B" apply (auto simp add: constrains_def) apply (drule project_act_mono, blast) done lemma (in Extend) project_stable_mono: - "[| D <= C; project h C F : stable A |] ==> project h D F : stable A" + "[| D \ C; project h C F \ stable A |] ==> project h D F \ stable A" by (simp add: stable_def project_constrains_mono) (*Key lemma used in several proofs about project and co*) lemma (in Extend) project_constrains: - "(project h C F : A co B) = - (F : (C Int extend_set h A) co (extend_set h B) & A <= B)" + "(project h C F \ A co B) = + (F \ (C \ extend_set h A) co (extend_set h B) & A \ B)" apply (unfold constrains_def) apply (auto intro!: project_act_I simp add: ball_Un) apply (force intro!: project_act_I dest!: subsetD) @@ -548,46 +548,46 @@ done lemma (in Extend) project_stable: - "(project h UNIV F : stable A) = (F : stable (extend_set h A))" + "(project h UNIV F \ stable A) = (F \ stable (extend_set h A))" apply (unfold stable_def) apply (simp (no_asm) add: project_constrains) done lemma (in Extend) project_stable_I: - "F : stable (extend_set h A) ==> project h C F : stable A" + "F \ stable (extend_set h A) ==> project h C F \ stable A" apply (drule project_stable [THEN iffD2]) apply (blast intro: project_stable_mono) done lemma (in Extend) Int_extend_set_lemma: - "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B" + "A \ extend_set h ((project_set h A) \ B) = A \ extend_set h B" by (auto simp add: split_extended_all) (*Strange (look at occurrences of C) but used in leadsETo proofs*) lemma project_constrains_project_set: - "G : C co B ==> project h C G : project_set h C co project_set h B" + "G \ C co B ==> project h C G \ project_set h C co project_set h B" by (simp add: constrains_def project_def project_act_def, blast) lemma project_stable_project_set: - "G : stable C ==> project h C G : stable (project_set h C)" + "G \ stable C ==> project h C G \ stable (project_set h C)" by (simp add: stable_def project_constrains_project_set) subsection{*Progress: transient, ensures*} lemma (in Extend) extend_transient: - "(extend h F : transient (extend_set h A)) = (F : transient A)" + "(extend h F \ transient (extend_set h A)) = (F \ transient A)" by (auto simp add: transient_def extend_set_subset_Compl_eq Domain_extend_act) lemma (in Extend) extend_ensures: - "(extend h F : (extend_set h A) ensures (extend_set h B)) = - (F : A ensures B)" + "(extend h F \ (extend_set h A) ensures (extend_set h B)) = + (F \ A ensures B)" by (simp add: ensures_def extend_constrains extend_transient extend_set_Un_distrib [symmetric] extend_set_Diff_distrib [symmetric]) lemma (in Extend) leadsTo_imp_extend_leadsTo: - "F : A leadsTo B - ==> extend h F : (extend_set h A) leadsTo (extend_set h B)" + "F \ A leadsTo B + ==> extend h F \ (extend_set h A) leadsTo (extend_set h B)" apply (erule leadsTo_induct) apply (simp add: leadsTo_Basis extend_ensures) apply (blast intro: leadsTo_Trans) @@ -596,21 +596,21 @@ subsection{*Proving the converse takes some doing!*} -lemma (in Extend) slice_iff [iff]: "(x : slice C y) = (h(x,y) : C)" +lemma (in Extend) slice_iff [iff]: "(x \ slice C y) = (h(x,y) \ C)" by (simp (no_asm) add: slice_def) -lemma (in Extend) slice_Union: "slice (Union S) y = (UN x:S. slice x y)" +lemma (in Extend) slice_Union: "slice (Union S) y = (\x \ S. slice x y)" by auto lemma (in Extend) slice_extend_set: "slice (extend_set h A) y = A" by auto lemma (in Extend) project_set_is_UN_slice: - "project_set h A = (UN y. slice A y)" + "project_set h A = (\y. slice A y)" by auto lemma (in Extend) extend_transient_slice: - "extend h F : transient A ==> F : transient (slice A y)" + "extend h F \ transient A ==> F \ transient (slice A y)" apply (unfold transient_def, auto) apply (rule bexI, auto) apply (force simp add: extend_act_def) @@ -618,25 +618,25 @@ (*Converse?*) lemma (in Extend) extend_constrains_slice: - "extend h F : A co B ==> F : (slice A y) co (slice B y)" + "extend h F \ A co B ==> F \ (slice A y) co (slice B y)" by (auto simp add: constrains_def) lemma (in Extend) extend_ensures_slice: - "extend h F : A ensures B ==> F : (slice A y) ensures (project_set h B)" + "extend h F \ A ensures B ==> F \ (slice A y) ensures (project_set h B)" apply (auto simp add: ensures_def extend_constrains extend_transient) apply (erule_tac [2] extend_transient_slice [THEN transient_strengthen]) apply (erule extend_constrains_slice [THEN constrains_weaken], auto) done lemma (in Extend) leadsTo_slice_project_set: - "ALL y. F : (slice B y) leadsTo CU ==> F : (project_set h B) leadsTo CU" + "\y. F \ (slice B y) leadsTo CU ==> F \ (project_set h B) leadsTo CU" apply (simp (no_asm) add: project_set_is_UN_slice) apply (blast intro: leadsTo_UN) done lemma (in Extend) extend_leadsTo_slice [rule_format]: - "extend h F : AU leadsTo BU - ==> ALL y. F : (slice AU y) leadsTo (project_set h BU)" + "extend h F \ AU leadsTo BU + ==> \y. F \ (slice AU y) leadsTo (project_set h BU)" apply (erule leadsTo_induct) apply (blast intro: extend_ensures_slice leadsTo_Basis) apply (blast intro: leadsTo_slice_project_set leadsTo_Trans) @@ -644,8 +644,8 @@ done lemma (in Extend) extend_leadsTo: - "(extend h F : (extend_set h A) leadsTo (extend_set h B)) = - (F : A leadsTo B)" + "(extend h F \ (extend_set h A) leadsTo (extend_set h B)) = + (F \ A leadsTo B)" apply safe apply (erule_tac [2] leadsTo_imp_extend_leadsTo) apply (drule extend_leadsTo_slice) @@ -653,8 +653,8 @@ done lemma (in Extend) extend_LeadsTo: - "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) = - (F : A LeadsTo B)" + "(extend h F \ (extend_set h A) LeadsTo (extend_set h B)) = + (F \ A LeadsTo B)" by (simp add: LeadsTo_def reachable_extend_eq extend_leadsTo extend_set_Int_distrib [symmetric]) @@ -662,20 +662,20 @@ subsection{*preserves*} lemma (in Extend) project_preserves_I: - "G : preserves (v o f) ==> project h C G : preserves v" + "G \ preserves (v o f) ==> project h C G \ preserves v" by (auto simp add: preserves_def project_stable_I extend_set_eq_Collect) (*to preserve f is to preserve the whole original state*) lemma (in Extend) project_preserves_id_I: - "G : preserves f ==> project h C G : preserves id" + "G \ preserves f ==> project h C G \ preserves id" by (simp add: project_preserves_I) lemma (in Extend) extend_preserves: - "(extend h G : preserves (v o f)) = (G : preserves v)" + "(extend h G \ preserves (v o f)) = (G \ preserves v)" by (auto simp add: preserves_def extend_stable [symmetric] extend_set_eq_Collect) -lemma (in Extend) inj_extend_preserves: "inj h ==> (extend h G : preserves g)" +lemma (in Extend) inj_extend_preserves: "inj h ==> (extend h G \ preserves g)" by (auto simp add: preserves_def extend_def extend_act_def stable_def constrains_def g_def) @@ -719,16 +719,16 @@ done lemma (in Extend) guarantees_imp_extend_guarantees: - "F : X guarantees Y ==> - extend h F : (extend h ` X) guarantees (extend h ` Y)" + "F \ X guarantees Y ==> + extend h F \ (extend h ` X) guarantees (extend h ` Y)" apply (rule guaranteesI, clarify) apply (blast dest: ok_extend_imp_ok_project extend_Join_eq_extend_D guaranteesD) done lemma (in Extend) extend_guarantees_imp_guarantees: - "extend h F : (extend h ` X) guarantees (extend h ` Y) - ==> F : X guarantees Y" + "extend h F \ (extend h ` X) guarantees (extend h ` Y) + ==> F \ X guarantees Y" apply (auto simp add: guar_def) apply (drule_tac x = "extend h G" in spec) apply (simp del: extend_Join @@ -737,8 +737,8 @@ done lemma (in Extend) extend_guarantees_eq: - "(extend h F : (extend h ` X) guarantees (extend h ` Y)) = - (F : X guarantees Y)" + "(extend h F \ (extend h ` X) guarantees (extend h ` Y)) = + (F \ X guarantees Y)" by (blast intro: guarantees_imp_extend_guarantees extend_guarantees_imp_guarantees) diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Follows.thy --- a/src/HOL/UNITY/Follows.thy Mon Feb 03 11:45:05 2003 +0100 +++ b/src/HOL/UNITY/Follows.thy Tue Feb 04 18:12:40 2003 +0100 @@ -12,22 +12,22 @@ Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set" (infixl "Fols" 65) - "f Fols g == Increasing g Int Increasing f Int - Always {s. f s <= g s} Int - (INT k. {s. k <= g s} LeadsTo {s. k <= f s})" + "f Fols g == Increasing g \ Increasing f Int + Always {s. f s \ g s} Int + (\k. {s. k \ g s} LeadsTo {s. k \ f s})" (*Does this hold for "invariant"?*) lemma mono_Always_o: - "mono h ==> Always {s. f s <= g s} <= Always {s. h (f s) <= h (g s)}" + "mono h ==> Always {s. f s \ g s} \ Always {s. h (f s) \ h (g s)}" apply (simp add: Always_eq_includes_reachable) apply (blast intro: monoD) done lemma mono_LeadsTo_o: "mono (h::'a::order => 'b::order) - ==> (INT j. {s. j <= g s} LeadsTo {s. j <= f s}) <= - (INT k. {s. k <= h (g s)} LeadsTo {s. k <= h (f s)})" + ==> (\j. {s. j \ g s} LeadsTo {s. j \ f s}) \ + (\k. {s. k \ h (g s)} LeadsTo {s. k \ h (f s)})" apply auto apply (rule single_LeadsTo_I) apply (drule_tac x = "g s" in spec) @@ -35,10 +35,10 @@ apply (blast intro: monoD order_trans)+ done -lemma Follows_constant [iff]: "F : (%s. c) Fols (%s. c)" +lemma Follows_constant [iff]: "F \ (%s. c) Fols (%s. c)" by (unfold Follows_def, auto) -lemma mono_Follows_o: "mono h ==> f Fols g <= (h o f) Fols (h o g)" +lemma mono_Follows_o: "mono h ==> f Fols g \ (h o f) Fols (h o g)" apply (unfold Follows_def, clarify) apply (simp add: mono_Increasing_o [THEN [2] rev_subsetD] mono_Always_o [THEN [2] rev_subsetD] @@ -46,13 +46,13 @@ done lemma mono_Follows_apply: - "mono h ==> f Fols g <= (%x. h (f x)) Fols (%x. h (g x))" + "mono h ==> f Fols g \ (%x. h (f x)) Fols (%x. h (g x))" apply (drule mono_Follows_o) apply (force simp add: o_def) done lemma Follows_trans: - "[| F : f Fols g; F: g Fols h |] ==> F : f Fols h" + "[| F \ f Fols g; F \ g Fols h |] ==> F \ f Fols h" apply (unfold Follows_def) apply (simp add: Always_eq_includes_reachable) apply (blast intro: order_trans LeadsTo_Trans) @@ -61,24 +61,24 @@ subsection{*Destruction rules*} -lemma Follows_Increasing1: "F : f Fols g ==> F : Increasing f" +lemma Follows_Increasing1: "F \ f Fols g ==> F \ Increasing f" apply (unfold Follows_def, blast) done -lemma Follows_Increasing2: "F : f Fols g ==> F : Increasing g" +lemma Follows_Increasing2: "F \ f Fols g ==> F \ Increasing g" apply (unfold Follows_def, blast) done -lemma Follows_Bounded: "F : f Fols g ==> F : Always {s. f s <= g s}" +lemma Follows_Bounded: "F \ f Fols g ==> F \ Always {s. f s \ g s}" apply (unfold Follows_def, blast) done lemma Follows_LeadsTo: - "F : f Fols g ==> F : {s. k <= g s} LeadsTo {s. k <= f s}" + "F \ f Fols g ==> F \ {s. k \ g s} LeadsTo {s. k \ f s}" by (unfold Follows_def, blast) lemma Follows_LeadsTo_pfixLe: - "F : f Fols g ==> F : {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}" + "F \ f Fols g ==> F \ {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}" apply (rule single_LeadsTo_I, clarify) apply (drule_tac k="g s" in Follows_LeadsTo) apply (erule LeadsTo_weaken) @@ -87,7 +87,7 @@ done lemma Follows_LeadsTo_pfixGe: - "F : f Fols g ==> F : {s. k pfixGe g s} LeadsTo {s. k pfixGe f s}" + "F \ f Fols g ==> F \ {s. k pfixGe g s} LeadsTo {s. k pfixGe f s}" apply (rule single_LeadsTo_I, clarify) apply (drule_tac k="g s" in Follows_LeadsTo) apply (erule LeadsTo_weaken) @@ -97,21 +97,21 @@ lemma Always_Follows1: - "[| F : Always {s. f s = f' s}; F : f Fols g |] ==> F : f' Fols g" + "[| F \ Always {s. f s = f' s}; F \ f Fols g |] ==> F \ f' Fols g" apply (unfold Follows_def Increasing_def Stable_def, auto) apply (erule_tac [3] Always_LeadsTo_weaken) -apply (erule_tac A = "{s. z <= f s}" and A' = "{s. z <= f s}" +apply (erule_tac A = "{s. z \ f s}" and A' = "{s. z \ f s}" in Always_Constrains_weaken, auto) apply (drule Always_Int_I, assumption) apply (force intro: Always_weaken) done lemma Always_Follows2: - "[| F : Always {s. g s = g' s}; F : f Fols g |] ==> F : f Fols g'" + "[| F \ Always {s. g s = g' s}; F \ f Fols g |] ==> F \ f Fols g'" apply (unfold Follows_def Increasing_def Stable_def, auto) apply (erule_tac [3] Always_LeadsTo_weaken) -apply (erule_tac A = "{s. z <= g s}" and A' = "{s. z <= g s}" +apply (erule_tac A = "{s. z \ g s}" and A' = "{s. z \ g s}" in Always_Constrains_weaken, auto) apply (drule Always_Int_I, assumption) apply (force intro: Always_weaken) @@ -122,8 +122,8 @@ (*Can replace "Un" by any sup. But existing max only works for linorders.*) lemma increasing_Un: - "[| F : increasing f; F: increasing g |] - ==> F : increasing (%s. (f s) Un (g s))" + "[| F \ increasing f; F \ increasing g |] + ==> F \ increasing (%s. (f s) \ (g s))" apply (unfold increasing_def stable_def constrains_def, auto) apply (drule_tac x = "f xa" in spec) apply (drule_tac x = "g xa" in spec) @@ -131,8 +131,8 @@ done lemma Increasing_Un: - "[| F : Increasing f; F: Increasing g |] - ==> F : Increasing (%s. (f s) Un (g s))" + "[| F \ Increasing f; F \ Increasing g |] + ==> F \ Increasing (%s. (f s) \ (g s))" apply (auto simp add: Increasing_def Stable_def Constrains_def stable_def constrains_def) apply (drule_tac x = "f xa" in spec) @@ -142,17 +142,17 @@ lemma Always_Un: - "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] - ==> F : Always {s. f' s Un g' s <= f s Un g s}" + "[| F \ Always {s. f' s \ f s}; F \ Always {s. g' s \ g s} |] + ==> F \ Always {s. f' s \ g' s \ f s \ g s}" by (simp add: Always_eq_includes_reachable, blast) (*Lemma to re-use the argument that one variable increases (progress) while the other variable doesn't decrease (safety)*) lemma Follows_Un_lemma: - "[| F : Increasing f; F : Increasing g; - F : Increasing g'; F : Always {s. f' s <= f s}; - ALL k. F : {s. k <= f s} LeadsTo {s. k <= f' s} |] - ==> F : {s. k <= f s Un g s} LeadsTo {s. k <= f' s Un g s}" + "[| F \ Increasing f; F \ Increasing g; + F \ Increasing g'; F \ Always {s. f' s \ f s}; + \k. F \ {s. k \ f s} LeadsTo {s. k \ f' s} |] + ==> F \ {s. k \ f s \ g s} LeadsTo {s. k \ f' s \ g s}" apply (rule single_LeadsTo_I) apply (drule_tac x = "f s" in IncreasingD) apply (drule_tac x = "g s" in IncreasingD) @@ -164,8 +164,8 @@ done lemma Follows_Un: - "[| F : f' Fols f; F: g' Fols g |] - ==> F : (%s. (f' s) Un (g' s)) Fols (%s. (f s) Un (g s))" + "[| F \ f' Fols f; F \ g' Fols g |] + ==> F \ (%s. (f' s) \ (g' s)) Fols (%s. (f s) \ (g s))" apply (unfold Follows_def) apply (simp add: Increasing_Un Always_Un, auto) apply (rule LeadsTo_Trans) @@ -178,8 +178,8 @@ subsection{*Multiset union properties (with the multiset ordering)*} lemma increasing_union: - "[| F : increasing f; F: increasing g |] - ==> F : increasing (%s. (f s) + (g s :: ('a::order) multiset))" + "[| F \ increasing f; F \ increasing g |] + ==> F \ increasing (%s. (f s) + (g s :: ('a::order) multiset))" apply (unfold increasing_def stable_def constrains_def, auto) apply (drule_tac x = "f xa" in spec) apply (drule_tac x = "g xa" in spec) @@ -188,8 +188,8 @@ done lemma Increasing_union: - "[| F : Increasing f; F: Increasing g |] - ==> F : Increasing (%s. (f s) + (g s :: ('a::order) multiset))" + "[| F \ Increasing f; F \ Increasing g |] + ==> F \ Increasing (%s. (f s) + (g s :: ('a::order) multiset))" apply (auto simp add: Increasing_def Stable_def Constrains_def stable_def constrains_def) apply (drule_tac x = "f xa" in spec) @@ -199,19 +199,19 @@ done lemma Always_union: - "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] - ==> F : Always {s. f' s + g' s <= f s + (g s :: ('a::order) multiset)}" + "[| F \ Always {s. f' s \ f s}; F \ Always {s. g' s \ g s} |] + ==> F \ Always {s. f' s + g' s \ f s + (g s :: ('a::order) multiset)}" apply (simp add: Always_eq_includes_reachable) apply (blast intro: union_le_mono) done (*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*) lemma Follows_union_lemma: - "[| F : Increasing f; F : Increasing g; - F : Increasing g'; F : Always {s. f' s <= f s}; - ALL k::('a::order) multiset. - F : {s. k <= f s} LeadsTo {s. k <= f' s} |] - ==> F : {s. k <= f s + g s} LeadsTo {s. k <= f' s + g s}" + "[| F \ Increasing f; F \ Increasing g; + F \ Increasing g'; F \ Always {s. f' s \ f s}; + \k::('a::order) multiset. + F \ {s. k \ f s} LeadsTo {s. k \ f' s} |] + ==> F \ {s. k \ f s + g s} LeadsTo {s. k \ f' s + g s}" apply (rule single_LeadsTo_I) apply (drule_tac x = "f s" in IncreasingD) apply (drule_tac x = "g s" in IncreasingD) @@ -226,8 +226,8 @@ (*The !! is there to influence to effect of permutative rewriting at the end*) lemma Follows_union: "!!g g' ::'b => ('a::order) multiset. - [| F : f' Fols f; F: g' Fols g |] - ==> F : (%s. (f' s) + (g' s)) Fols (%s. (f s) + (g s))" + [| F \ f' Fols f; F \ g' Fols g |] + ==> F \ (%s. (f' s) + (g' s)) Fols (%s. (f s) + (g s))" apply (unfold Follows_def) apply (simp add: Increasing_union Always_union, auto) apply (rule LeadsTo_Trans) @@ -239,8 +239,8 @@ lemma Follows_setsum: "!!f ::['c,'b] => ('a::order) multiset. - [| ALL i: I. F : f' i Fols f i; finite I |] - ==> F : (%s. \i:I. f' i s) Fols (%s. \i:I. f i s)" + [| \i \ I. F \ f' i Fols f i; finite I |] + ==> F \ (%s. \i \ I. f' i s) Fols (%s. \i \ I. f i s)" apply (erule rev_mp) apply (erule finite_induct, simp) apply (simp add: Follows_union) @@ -249,7 +249,7 @@ (*Currently UNUSED, but possibly of interest*) lemma Increasing_imp_Stable_pfixGe: - "F : Increasing func ==> F : Stable {s. h pfixGe (func s)}" + "F \ Increasing func ==> F \ Stable {s. h pfixGe (func s)}" apply (simp add: Increasing_def Stable_def Constrains_def constrains_def) apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD] prefix_imp_pfixGe) @@ -257,8 +257,8 @@ (*Currently UNUSED, but possibly of interest*) lemma LeadsTo_le_imp_pfixGe: - "ALL z. F : {s. z <= f s} LeadsTo {s. z <= g s} - ==> F : {s. z pfixGe f s} LeadsTo {s. z pfixGe g s}" + "\z. F \ {s. z \ f s} LeadsTo {s. z \ g s} + ==> F \ {s. z pfixGe f s} LeadsTo {s. z pfixGe g s}" apply (rule single_LeadsTo_I) apply (drule_tac x = "f s" in spec) apply (erule LeadsTo_weaken) diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Guar.thy --- a/src/HOL/UNITY/Guar.thy Mon Feb 03 11:45:05 2003 +0100 +++ b/src/HOL/UNITY/Guar.thy Tue Feb 04 18:12:40 2003 +0100 @@ -32,57 +32,57 @@ case, proving equivalence with Chandy and Sanders's n-ary definitions*) ex_prop :: "'a program set => bool" - "ex_prop X == \F G. F ok G -->F:X | G: X --> (F Join G) : X" + "ex_prop X == \F G. F ok G -->F \ X | G \ X --> (F Join G) \ X" strict_ex_prop :: "'a program set => bool" - "strict_ex_prop X == \F G. F ok G --> (F:X | G: X) = (F Join G : X)" + "strict_ex_prop X == \F G. F ok G --> (F \ X | G \ X) = (F Join G \ X)" uv_prop :: "'a program set => bool" - "uv_prop X == SKIP : X & (\F G. F ok G --> F:X & G: X --> (F Join G) : X)" + "uv_prop X == SKIP \ X & (\F G. F ok G --> F \ X & G \ X --> (F Join G) \ X)" strict_uv_prop :: "'a program set => bool" "strict_uv_prop X == - SKIP : X & (\F G. F ok G --> (F:X & G: X) = (F Join G : X))" + SKIP \ X & (\F G. F ok G --> (F \ X & G \ X) = (F Join G \ X))" guar :: "['a program set, 'a program set] => 'a program set" (infixl "guarantees" 55) (*higher than membership, lower than Co*) - "X guarantees Y == {F. \G. F ok G --> F Join G : X --> F Join G : Y}" + "X guarantees Y == {F. \G. F ok G --> F Join G \ X --> F Join G \ Y}" (* Weakest guarantees *) wg :: "['a program, 'a program set] => 'a program set" - "wg F Y == Union({X. F:X guarantees Y})" + "wg F Y == Union({X. F \ X guarantees Y})" (* Weakest existential property stronger than X *) wx :: "('a program) set => ('a program)set" - "wx X == Union({Y. Y<=X & ex_prop Y})" + "wx X == Union({Y. Y \ X & ex_prop Y})" (*Ill-defined programs can arise through "Join"*) welldef :: "'a program set" - "welldef == {F. Init F ~= {}}" + "welldef == {F. Init F \ {}}" refines :: "['a program, 'a program, 'a program set] => bool" ("(3_ refines _ wrt _)" [10,10,10] 10) "G refines F wrt X == - \H. (F ok H & G ok H & F Join H : welldef Int X) --> - (G Join H : welldef Int X)" + \H. (F ok H & G ok H & F Join H \ welldef \ X) --> + (G Join H \ welldef \ X)" iso_refines :: "['a program, 'a program, 'a program set] => bool" ("(3_ iso'_refines _ wrt _)" [10,10,10] 10) "G iso_refines F wrt X == - F : welldef Int X --> G : welldef Int X" + F \ welldef \ X --> G \ welldef \ X" lemma OK_insert_iff: "(OK (insert i I) F) = - (if i:I then OK I F else OK I F & (F i ok JOIN I F))" + (if i \ I then OK I F else OK I F & (F i ok JOIN I F))" by (auto intro: ok_sym simp add: OK_iff_ok) (*** existential properties ***) lemma ex1 [rule_format]: "[| ex_prop X; finite GG |] ==> - GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X" + GG \ X \ {}--> OK GG (%G. G) --> (\G \ GG. G) \ X" apply (unfold ex_prop_def) apply (erule finite_induct) apply (auto simp add: OK_insert_iff Int_insert_left) @@ -90,7 +90,7 @@ lemma ex2: - "\GG. finite GG & GG Int X ~= {} --> OK GG (%G. G) -->(JN G:GG. G):X + "\GG. finite GG & GG \ X \ {} --> OK GG (%G. G) -->(\G \ GG. G):X ==> ex_prop X" apply (unfold ex_prop_def, clarify) apply (drule_tac x = "{F,G}" in spec) @@ -101,13 +101,13 @@ (*Chandy & Sanders take this as a definition*) lemma ex_prop_finite: "ex_prop X = - (\GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)" + (\GG. finite GG & GG \ X \ {} & OK GG (%G. G)--> (\G \ GG. G) \ X)" by (blast intro: ex1 ex2) (*Their "equivalent definition" given at the end of section 3*) lemma ex_prop_equiv: - "ex_prop X = (\G. G:X = (\H. (G component_of H) --> H: X))" + "ex_prop X = (\G. G \ X = (\H. (G component_of H) --> H \ X))" apply auto apply (unfold ex_prop_def component_of_def, safe) apply blast @@ -120,14 +120,14 @@ (*** universal properties ***) lemma uv1 [rule_format]: "[| uv_prop X; finite GG |] - ==> GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X" + ==> GG \ X & OK GG (%G. G) --> (\G \ GG. G) \ X" apply (unfold uv_prop_def) apply (erule finite_induct) apply (auto simp add: Int_insert_left OK_insert_iff) done lemma uv2: - "\GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X + "\GG. finite GG & GG \ X & OK GG (%G. G) --> (\G \ GG. G) \ X ==> uv_prop X" apply (unfold uv_prop_def) apply (rule conjI) @@ -141,37 +141,37 @@ (*Chandy & Sanders take this as a definition*) lemma uv_prop_finite: "uv_prop X = - (\GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G): X)" + (\GG. finite GG & GG \ X & OK GG (%G. G) --> (\G \ GG. G): X)" by (blast intro: uv1 uv2) (*** guarantees ***) lemma guaranteesI: - "(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y) - ==> F : X guarantees Y" + "(!!G. [| F ok G; F Join G \ X |] ==> F Join G \ Y) + ==> F \ X guarantees Y" by (simp add: guar_def component_def) lemma guaranteesD: - "[| F : X guarantees Y; F ok G; F Join G : X |] - ==> F Join G : Y" + "[| F \ X guarantees Y; F ok G; F Join G \ X |] + ==> F Join G \ 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<=H since we need to reason about G*) + The major premise can no longer be F \ H since we need to reason about G*) lemma component_guaranteesD: - "[| F : X guarantees Y; F Join G = H; H : X; F ok G |] - ==> H : Y" + "[| F \ X guarantees Y; F Join G = H; H \ X; F ok G |] + ==> H \ Y" by (unfold guar_def, blast) lemma guarantees_weaken: - "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'" + "[| F \ X guarantees X'; Y \ X; X' \ Y' |] ==> F \ Y guarantees Y'" by (unfold guar_def, blast) -lemma subset_imp_guarantees_UNIV: "X <= Y ==> X guarantees Y = UNIV" +lemma subset_imp_guarantees_UNIV: "X \ Y ==> X guarantees Y = UNIV" by (unfold guar_def, blast) (*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) -lemma subset_imp_guarantees: "X <= Y ==> F : X guarantees Y" +lemma subset_imp_guarantees: "X \ Y ==> F \ X guarantees Y" by (unfold guar_def, blast) (*Remark at end of section 4.1 *) @@ -201,31 +201,31 @@ (** Distributive laws. Re-orient to perform miniscoping **) lemma guarantees_UN_left: - "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)" + "(\i \ I. X i) guarantees Y = (\i \ I. X i guarantees Y)" by (unfold guar_def, blast) lemma guarantees_Un_left: - "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)" + "(X \ Y) guarantees Z = (X guarantees Z) \ (Y guarantees Z)" by (unfold guar_def, blast) lemma guarantees_INT_right: - "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)" + "X guarantees (\i \ I. Y i) = (\i \ I. X guarantees Y i)" by (unfold guar_def, blast) lemma guarantees_Int_right: - "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)" + "Z guarantees (X \ Y) = (Z guarantees X) \ (Z guarantees Y)" by (unfold guar_def, blast) lemma guarantees_Int_right_I: - "[| F : Z guarantees X; F : Z guarantees Y |] - ==> F : Z guarantees (X Int Y)" + "[| F \ Z guarantees X; F \ Z guarantees Y |] + ==> F \ Z guarantees (X \ Y)" by (simp add: guarantees_Int_right) lemma guarantees_INT_right_iff: - "(F : X guarantees (INTER I Y)) = (\i\I. F : X guarantees (Y i))" + "(F \ X guarantees (INTER I Y)) = (\i\I. F \ X guarantees (Y i))" by (simp add: guarantees_INT_right) -lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X Un Y))" +lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \ Y))" by (unfold guar_def, blast) lemma contrapositive: "(X guarantees Y) = -Y guarantees -X" @@ -236,35 +236,35 @@ **) lemma combining1: - "[| F : V guarantees X; F : (X Int Y) guarantees Z |] - ==> F : (V Int Y) guarantees Z" + "[| F \ V guarantees X; F \ (X \ Y) guarantees Z |] + ==> F \ (V \ Y) guarantees Z" by (unfold guar_def, blast) lemma combining2: - "[| F : V guarantees (X Un Y); F : Y guarantees Z |] - ==> F : V guarantees (X Un Z)" + "[| F \ V guarantees (X \ Y); F \ Y guarantees Z |] + ==> F \ V guarantees (X \ Z)" by (unfold guar_def, blast) (** The following two follow Chandy-Sanders, but the use of object-quantifiers does not suit Isabelle... **) -(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *) +(*Premise should be (!!i. i \ I ==> F \ X guarantees Y i) *) lemma all_guarantees: - "\i\I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)" + "\i\I. F \ X guarantees (Y i) ==> F \ X guarantees (\i \ I. Y i)" by (unfold guar_def, blast) -(*Premises should be [| F: X guarantees Y i; i: I |] *) +(*Premises should be [| F \ X guarantees Y i; i \ I |] *) lemma ex_guarantees: - "\i\I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)" + "\i\I. F \ X guarantees (Y i) ==> F \ X guarantees (\i \ I. Y i)" by (unfold guar_def, blast) (*** Additional guarantees laws, by lcp ***) lemma guarantees_Join_Int: - "[| F: U guarantees V; G: X guarantees Y; F ok G |] - ==> F Join G: (U Int X) guarantees (V Int Y)" + "[| F \ U guarantees V; G \ X guarantees Y; F ok G |] + ==> F Join G \ (U \ X) guarantees (V \ Y)" apply (unfold guar_def) apply (simp (no_asm)) apply safe @@ -275,8 +275,8 @@ done lemma guarantees_Join_Un: - "[| F: U guarantees V; G: X guarantees Y; F ok G |] - ==> F Join G: (U Un X) guarantees (V Un Y)" + "[| F \ U guarantees V; G \ X guarantees Y; F ok G |] + ==> F Join G \ (U \ X) guarantees (V \ Y)" apply (unfold guar_def) apply (simp (no_asm)) apply safe @@ -287,8 +287,8 @@ done lemma guarantees_JN_INT: - "[| \i\I. F i : X i guarantees Y i; OK I F |] - ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)" + "[| \i\I. F i \ X i guarantees Y i; OK I F |] + ==> (JOIN I F) \ (INTER I X) guarantees (INTER I Y)" apply (unfold guar_def, auto) apply (drule bspec, assumption) apply (rename_tac "i") @@ -298,8 +298,8 @@ done lemma guarantees_JN_UN: - "[| \i\I. F i : X i guarantees Y i; OK I F |] - ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)" + "[| \i\I. F i \ X i guarantees Y i; OK I F |] + ==> (JOIN I F) \ (UNION I X) guarantees (UNION I Y)" apply (unfold guar_def, auto) apply (drule bspec, assumption) apply (rename_tac "i") @@ -312,7 +312,7 @@ (*** guarantees laws for breaking down the program, by lcp ***) lemma guarantees_Join_I1: - "[| F: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y" + "[| F \ X guarantees Y; F ok G |] ==> F Join G \ X guarantees Y" apply (unfold guar_def) apply (simp (no_asm)) apply safe @@ -320,14 +320,14 @@ done lemma guarantees_Join_I2: - "[| G: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y" + "[| G \ X guarantees Y; F ok G |] ==> F Join G \ X guarantees Y" apply (simp add: Join_commute [of _ G] ok_commute [of _ G]) apply (blast intro: guarantees_Join_I1) done lemma guarantees_JN_I: - "[| i : I; F i: X guarantees Y; OK I F |] - ==> (JN i:I. (F i)) : X guarantees Y" + "[| i \ I; F i \ X guarantees Y; OK I F |] + ==> (\i \ I. (F i)) \ X guarantees Y" apply (unfold guar_def, clarify) apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec) apply (auto intro: OK_imp_ok simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric]) @@ -336,10 +336,10 @@ (*** well-definedness ***) -lemma Join_welldef_D1: "F Join G: welldef ==> F: welldef" +lemma Join_welldef_D1: "F Join G \ welldef ==> F \ welldef" by (unfold welldef_def, auto) -lemma Join_welldef_D2: "F Join G: welldef ==> G: welldef" +lemma Join_welldef_D2: "F Join G \ welldef ==> G \ welldef" by (unfold welldef_def, auto) (*** refinement ***) @@ -357,14 +357,14 @@ lemma strict_ex_refine_lemma: "strict_ex_prop X - ==> (\H. F ok H & G ok H & F Join H : X --> G Join H : X) - = (F:X --> G:X)" + ==> (\H. F ok H & G ok H & F Join H \ X --> G Join H \ X) + = (F \ X --> G \ X)" by (unfold strict_ex_prop_def, auto) lemma strict_ex_refine_lemma_v: "strict_ex_prop X - ==> (\H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = - (F: welldef Int X --> G:X)" + ==> (\H. F ok H & G ok H & F Join H \ welldef & F Join H \ X --> G Join H \ X) = + (F \ welldef \ X --> G \ X)" apply (unfold strict_ex_prop_def, safe) apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE) apply (auto dest: Join_welldef_D1 Join_welldef_D2) @@ -372,7 +372,7 @@ lemma ex_refinement_thm: "[| strict_ex_prop X; - \H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] + \H. F ok H & G ok H & F Join H \ welldef \ X --> G Join H \ 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) @@ -381,13 +381,13 @@ lemma strict_uv_refine_lemma: "strict_uv_prop X ==> - (\H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G:X)" + (\H. F ok H & G ok H & F Join H \ X --> G Join H \ X) = (F \ X --> G \ X)" by (unfold strict_uv_prop_def, blast) lemma strict_uv_refine_lemma_v: "strict_uv_prop X - ==> (\H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = - (F: welldef Int X --> G:X)" + ==> (\H. F ok H & G ok H & F Join H \ welldef & F Join H \ X --> G Join H \ X) = + (F \ welldef \ X --> G \ X)" apply (unfold strict_uv_prop_def, safe) apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE) apply (auto dest: Join_welldef_D1 Join_welldef_D2) @@ -395,8 +395,8 @@ lemma uv_refinement_thm: "[| strict_uv_prop X; - \H. F ok H & G ok H & F Join H : welldef Int X --> - G Join H : welldef |] + \H. F ok H & G ok H & F Join H \ welldef \ X --> + G Join H \ 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) @@ -404,17 +404,17 @@ (* Added by Sidi Ehmety from Chandy & Sander, section 6 *) lemma guarantees_equiv: - "(F:X guarantees Y) = (\H. H:X \ (F component_of H \ H:Y))" + "(F \ X guarantees Y) = (\H. H \ X \ (F component_of H \ H \ Y))" by (unfold guar_def component_of_def, auto) -lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X <= (wg F Y)" +lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X \ (wg F Y)" by (unfold wg_def, auto) lemma wg_guarantees: "F:((wg F Y) guarantees Y)" by (unfold wg_def guar_def, blast) lemma wg_equiv: - "(H: wg F X) = (F component_of H --> H:X)" + "(H \ wg F X) = (F component_of H --> H \ X)" apply (unfold wg_def) apply (simp (no_asm) add: guarantees_equiv) apply (rule iffI) @@ -423,21 +423,21 @@ done -lemma component_of_wg: "F component_of H ==> (H:wg F X) = (H:X)" +lemma component_of_wg: "F component_of H ==> (H \ wg F X) = (H \ X)" by (simp add: wg_equiv) lemma wg_finite: - "\FF. finite FF & FF Int X ~= {} --> OK FF (%F. F) - --> (\F\FF. ((JN F:FF. F): wg F X) = ((JN F:FF. F):X))" + "\FF. finite FF & FF \ X \ {} --> OK FF (%F. F) + --> (\F\FF. ((\F \ FF. F): wg F X) = ((\F \ FF. F):X))" apply clarify -apply (subgoal_tac "F component_of (JN F:FF. F) ") +apply (subgoal_tac "F component_of (\F \ FF. F) ") apply (drule_tac X = X in component_of_wg, simp) apply (simp add: component_of_def) -apply (rule_tac x = "JN F: (FF-{F}) . F" in exI) +apply (rule_tac x = "\F \ (FF-{F}) . F" in exI) apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok) done -lemma wg_ex_prop: "ex_prop X ==> (F:X) = (\H. H : wg F X)" +lemma wg_ex_prop: "ex_prop X ==> (F \ X) = (\H. H \ wg F X)" apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv) apply blast done @@ -455,11 +455,11 @@ apply auto done -lemma wx_weakest: "\Z. Z<= X --> ex_prop Z --> Z <= wx X" +lemma wx_weakest: "\Z. Z<= X --> ex_prop Z --> Z \ wx X" by (unfold wx_def, auto) (* Proposition 6 *) -lemma wx'_ex_prop: "ex_prop({F. \G. F ok G --> F Join G:X})" +lemma wx'_ex_prop: "ex_prop({F. \G. F ok G --> F Join G \ X})" apply (unfold ex_prop_def, safe) apply (drule_tac x = "G Join Ga" in spec) apply (force simp add: ok_Join_iff1 Join_assoc) @@ -483,7 +483,7 @@ apply (drule_tac x = G in spec) apply (frule_tac c = "x Join G" in subsetD, safe) apply (simp (no_asm)) -apply (rule_tac x = "{F. \G. F ok G --> F Join G:X}" in exI, safe) +apply (rule_tac x = "{F. \G. F ok G --> F Join G \ X}" in exI, safe) apply (rule_tac [2] wx'_ex_prop) apply (rotate_tac 1) apply (drule_tac x = SKIP in spec, auto) @@ -496,7 +496,7 @@ (* Proposition 12 *) (* Main result of the paper *) lemma guarantees_wx_eq: - "(X guarantees Y) = wx(-X Un Y)" + "(X guarantees Y) = wx(-X \ Y)" apply (unfold guar_def) apply (simp (no_asm) add: wx_equiv) done @@ -511,7 +511,7 @@ Reasoning About Program composition paper *) lemma stable_guarantees_Always: - "Init F <= A ==> F:(stable A) guarantees (Always A)" + "Init F \ A ==> F:(stable A) guarantees (Always A)" apply (rule guaranteesI) apply (simp (no_asm) add: Join_commute) apply (rule stable_Join_Always1) @@ -519,7 +519,7 @@ done (* To be moved to WFair.ML *) -lemma leadsTo_Basis': "[| F:A co A Un B; F:transient A |] ==> F:A leadsTo B" +lemma leadsTo_Basis': "[| F \ A co A \ B; F \ transient A |] ==> F \ A leadsTo B" apply (drule_tac B = "A-B" in constrains_weaken_L) apply (drule_tac [2] B = "A-B" in transient_strengthen) apply (rule_tac [3] ensuresI [THEN leadsTo_Basis]) @@ -529,7 +529,7 @@ lemma constrains_guarantees_leadsTo: - "F : transient A ==> F: (A co A Un B) guarantees (A leadsTo (B-A))" + "F \ transient A ==> F \ (A co A \ B) guarantees (A leadsTo (B-A))" apply (rule guaranteesI) apply (rule leadsTo_Basis') apply (drule constrains_weaken_R) diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Lift_prog.thy --- a/src/HOL/UNITY/Lift_prog.thy Mon Feb 03 11:45:05 2003 +0100 +++ b/src/HOL/UNITY/Lift_prog.thy Tue Feb 04 18:12:40 2003 +0100 @@ -116,23 +116,23 @@ lemma lift_set_empty [simp]: "lift_set i {} = {}" by (unfold lift_set_def, auto) -lemma lift_set_iff: "(lift_map i x : lift_set i A) = (x : A)" +lemma lift_set_iff: "(lift_map i x \ lift_set i A) = (x \ A)" apply (unfold lift_set_def) apply (rule inj_lift_map [THEN inj_image_mem_iff]) done (*Do we really need both this one and its predecessor?*) lemma lift_set_iff2 [iff]: - "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)" + "((f,uu) \ lift_set i A) = ((f i, (delete_map i f, uu)) \ A)" by (simp add: lift_set_def mem_rename_set_iff drop_map_def) -lemma lift_set_mono: "A<=B ==> lift_set i A <= lift_set i B" +lemma lift_set_mono: "A \ B ==> lift_set i A \ lift_set i B" apply (unfold lift_set_def) apply (erule image_mono) done -lemma lift_set_Un_distrib: "lift_set i (A Un B) = lift_set i A Un lift_set i B" +lemma lift_set_Un_distrib: "lift_set i (A \ B) = lift_set i A \ lift_set i B" apply (unfold lift_set_def) apply (simp add: image_Un) done @@ -154,39 +154,39 @@ lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G" by (simp add: lift_def) -lemma lift_JN [simp]: "lift j (JOIN I F) = (JN i:I. lift j (F i))" +lemma lift_JN [simp]: "lift j (JOIN I F) = (\i \ I. lift j (F i))" by (simp add: lift_def) (*** Safety: co, stable, invariant ***) lemma lift_constrains: - "(lift i F : (lift_set i A) co (lift_set i B)) = (F : A co B)" + "(lift i F \ (lift_set i A) co (lift_set i B)) = (F \ A co B)" by (simp add: lift_def lift_set_def rename_constrains) lemma lift_stable: - "(lift i F : stable (lift_set i A)) = (F : stable A)" + "(lift i F \ stable (lift_set i A)) = (F \ stable A)" by (simp add: lift_def lift_set_def rename_stable) lemma lift_invariant: - "(lift i F : invariant (lift_set i A)) = (F : invariant A)" + "(lift i F \ invariant (lift_set i A)) = (F \ invariant A)" apply (unfold lift_def lift_set_def) apply (simp add: rename_invariant) done lemma lift_Constrains: - "(lift i F : (lift_set i A) Co (lift_set i B)) = (F : A Co B)" + "(lift i F \ (lift_set i A) Co (lift_set i B)) = (F \ A Co B)" apply (unfold lift_def lift_set_def) apply (simp add: rename_Constrains) done lemma lift_Stable: - "(lift i F : Stable (lift_set i A)) = (F : Stable A)" + "(lift i F \ Stable (lift_set i A)) = (F \ Stable A)" apply (unfold lift_def lift_set_def) apply (simp add: rename_Stable) done lemma lift_Always: - "(lift i F : Always (lift_set i A)) = (F : Always A)" + "(lift i F \ Always (lift_set i A)) = (F \ Always A)" apply (unfold lift_def lift_set_def) apply (simp add: rename_Always) done @@ -194,37 +194,37 @@ (*** Progress: transient, ensures ***) lemma lift_transient: - "(lift i F : transient (lift_set i A)) = (F : transient A)" + "(lift i F \ transient (lift_set i A)) = (F \ transient A)" by (simp add: lift_def lift_set_def rename_transient) lemma lift_ensures: - "(lift i F : (lift_set i A) ensures (lift_set i B)) = - (F : A ensures B)" + "(lift i F \ (lift_set i A) ensures (lift_set i B)) = + (F \ A ensures B)" by (simp add: lift_def lift_set_def rename_ensures) lemma lift_leadsTo: - "(lift i F : (lift_set i A) leadsTo (lift_set i B)) = - (F : A leadsTo B)" + "(lift i F \ (lift_set i A) leadsTo (lift_set i B)) = + (F \ A leadsTo B)" by (simp add: lift_def lift_set_def rename_leadsTo) lemma lift_LeadsTo: - "(lift i F : (lift_set i A) LeadsTo (lift_set i B)) = - (F : A LeadsTo B)" + "(lift i F \ (lift_set i A) LeadsTo (lift_set i B)) = + (F \ A LeadsTo B)" by (simp add: lift_def lift_set_def rename_LeadsTo) (** guarantees **) lemma lift_lift_guarantees_eq: - "(lift i F : (lift i ` X) guarantees (lift i ` Y)) = - (F : X guarantees Y)" + "(lift i F \ (lift i ` X) guarantees (lift i ` Y)) = + (F \ X guarantees Y)" apply (unfold lift_def) apply (subst bij_lift_map [THEN rename_rename_guarantees_eq, symmetric]) apply (simp add: o_def) done -lemma lift_guarantees_eq_lift_inv: "(lift i F : X guarantees Y) = - (F : (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))" +lemma lift_guarantees_eq_lift_inv: "(lift i F \ X guarantees Y) = + (F \ (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))" by (simp add: bij_lift_map [THEN rename_guarantees_eq_rename_inv] lift_def) @@ -236,14 +236,14 @@ (*To preserve snd means that the second component is there just to allow guarantees properties to be stated. Converse fails, for lift i F can change function components other than i*) -lemma lift_preserves_snd_I: "F : preserves snd ==> lift i F : preserves snd" +lemma lift_preserves_snd_I: "F \ preserves snd ==> lift i F \ preserves snd" apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD]) apply (simp add: lift_def rename_preserves) apply (simp add: lift_map_def o_def split_def) done lemma delete_map_eqE': - "(delete_map i g) = (delete_map i g') ==> EX x. g = g'(i:=x)" + "(delete_map i g) = (delete_map i g') ==> \x. g = g'(i:=x)" apply (drule_tac f = "insert_map i (g i) " in arg_cong) apply (simp add: insert_map_delete_map_eq) apply (erule exI) @@ -252,7 +252,7 @@ lemmas delete_map_eqE = delete_map_eqE' [THEN exE, elim!] lemma delete_map_neq_apply: - "[| delete_map j g = delete_map j g'; i~=j |] ==> g i = g' i" + "[| delete_map j g = delete_map j g'; i\j |] ==> g i = g' i" by force (*A set of the form (A <*> UNIV) ignores the second (dummy) state component*) @@ -265,27 +265,27 @@ by auto lemma mem_lift_act_iff [iff]: - "((s,s') : extend_act (%(x,u::unit). lift_map i x) act) = - ((drop_map i s, drop_map i s') : act)" + "((s,s') \ extend_act (%(x,u::unit). lift_map i x) act) = + ((drop_map i s, drop_map i s') \ act)" apply (unfold extend_act_def, auto) apply (rule bexI, auto) done lemma preserves_snd_lift_stable: - "[| F : preserves snd; i~=j |] - ==> lift j F : stable (lift_set i (A <*> UNIV))" + "[| F \ preserves snd; i\j |] + ==> lift j F \ stable (lift_set i (A <*> UNIV))" apply (auto simp add: lift_def lift_set_def stable_def constrains_def rename_def extend_def mem_rename_set_iff) apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def) apply (drule_tac x = i in fun_cong, auto) done -(*If i~=j then lift j F does nothing to lift_set i, and the - premise ensures A<=B.*) +(*If i\j then lift j F does nothing to lift_set i, and the + premise ensures A \ B.*) lemma constrains_imp_lift_constrains: - "[| F i : (A <*> UNIV) co (B <*> UNIV); - F j : preserves snd |] - ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))" + "[| F i \ (A <*> UNIV) co (B <*> UNIV); + F j \ preserves snd |] + ==> lift j (F j) \ (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))" apply (case_tac "i=j") apply (simp add: lift_def lift_set_def rename_constrains) apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R], @@ -309,24 +309,24 @@ done lemma insert_map_eq_diff: - "[| insert_map i s f = insert_map j t g; i~=j |] - ==> EX g'. insert_map i s' f = insert_map j t g'" + "[| insert_map i s f = insert_map j t g; i\j |] + ==> \g'. insert_map i s' f = insert_map j t g'" apply (subst insert_map_upd_same [symmetric]) apply (erule ssubst) apply (simp only: insert_map_upd if_False split: split_if, blast) done lemma lift_map_eq_diff: - "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv)); i~=j |] - ==> EX g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))" + "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv)); i\j |] + ==> \g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))" apply (unfold lift_map_def, auto) apply (blast dest: insert_map_eq_diff) done lemma lift_transient_eq_disj: - "F : preserves snd - ==> (lift i F : transient (lift_set j (A <*> UNIV))) = - (i=j & F : transient (A <*> UNIV) | A={})" + "F \ preserves snd + ==> (lift i F \ transient (lift_set j (A <*> UNIV))) = + (i=j & F \ transient (A <*> UNIV) | A={})" apply (case_tac "i=j") apply (auto simp add: lift_transient) apply (auto simp add: lift_set_def lift_def transient_def rename_def @@ -346,21 +346,21 @@ (*USELESS??*) lemma lift_map_image_Times: "lift_map i ` (A <*> UNIV) = - (UN s:A. UN f. {insert_map i s f}) <*> UNIV" + (\s \ A. \f. {insert_map i s f}) <*> UNIV" apply (auto intro!: bexI image_eqI simp add: lift_map_def) apply (rule split_conv [symmetric]) done lemma lift_preserves_eq: - "(lift i F : preserves v) = (F : preserves (v o lift_map i))" + "(lift i F \ preserves v) = (F \ preserves (v o lift_map i))" by (simp add: lift_def rename_preserves) (*A useful rewrite. If o, sub have been rewritten out already then can also use it as rewrite_rule [sub_def, o_def] lift_preserves_sub*) lemma lift_preserves_sub: - "F : preserves snd - ==> lift i F : preserves (v o sub j o fst) = - (if i=j then F : preserves (v o fst) else True)" + "F \ preserves snd + ==> lift i F \ preserves (v o sub j o fst) = + (if i=j then F \ preserves (v o fst) else True)" apply (drule subset_preserves_o [THEN subsetD]) apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq) apply (auto cong del: if_weak_cong @@ -374,7 +374,7 @@ lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h" by (simp add: expand_fun_eq o_def) -lemma o_equiv_apply: "f o g = h ==> ALL x. f(g x) = h x" +lemma o_equiv_apply: "f o g = h ==> \x. f(g x) = h x" by (simp add: expand_fun_eq o_def) lemma fst_o_lift_map: "sub i o fst o lift_map i = fst" @@ -402,7 +402,7 @@ lemma project_act_extend_act: "project_act h (extend_act h' act) = - {(x,x'). EX s s' y y' z. (s,s') : act & + {(x,x'). \s s' y y' z. (s,s') \ act & h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}" by (simp add: extend_act_def project_act_def, blast) @@ -410,24 +410,24 @@ (*** OK and "lift" ***) lemma act_in_UNION_preserves_fst: - "act <= {(x,x'). fst x = fst x'} ==> act : UNION (preserves fst) Acts" + "act \ {(x,x'). fst x = fst x'} ==> act \ UNION (preserves fst) Acts" apply (rule_tac a = "mk_program (UNIV,{act},UNIV) " in UN_I) apply (auto simp add: preserves_def stable_def constrains_def) done lemma UNION_OK_lift_I: - "[| ALL i:I. F i : preserves snd; - ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |] + "[| \i \ I. F i \ preserves snd; + \i \ I. UNION (preserves fst) Acts \ AllowedActs (F i) |] ==> OK I (%i. lift i (F i))" apply (auto simp add: OK_def lift_def rename_def Extend.Acts_extend) apply (simp add: Extend.AllowedActs_extend project_act_extend_act) apply (rename_tac "act") apply (subgoal_tac "{(x, x'). \s f u s' f' u'. - ((s, f, u), s', f', u') : act & + ((s, f, u), s', f', u') \ act & lift_map j x = lift_map i (s, f, u) & lift_map j x' = lift_map i (s', f', u') } - <= { (x,x') . fst x = fst x'}") + \ { (x,x') . fst x = fst x'}") apply (blast intro: act_in_UNION_preserves_fst, clarify) apply (drule_tac x = j in fun_cong)+ apply (drule_tac x = i in bspec, assumption) @@ -435,8 +435,8 @@ done lemma OK_lift_I: - "[| ALL i:I. F i : preserves snd; - ALL i:I. preserves fst <= Allowed (F i) |] + "[| \i \ I. F i \ preserves snd; + \i \ I. preserves fst \ Allowed (F i) |] ==> OK I (%i. lift i (F i))" by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I) diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/PPROD.thy --- a/src/HOL/UNITY/PPROD.thy Mon Feb 03 11:45:05 2003 +0100 +++ b/src/HOL/UNITY/PPROD.thy Tue Feb 04 18:12:40 2003 +0100 @@ -15,19 +15,19 @@ PLam :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program] => ((nat=>'b) * 'c) program" - "PLam I F == JN i:I. lift i (F i)" + "PLam I F == \i \ I. lift i (F i)" syntax "@PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set" ("(3plam _:_./ _)" 10) translations - "plam x:A. B" == "PLam A (%x. B)" + "plam x : A. B" == "PLam A (%x. B)" (*** Basic properties ***) -lemma Init_PLam: "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))" +lemma Init_PLam: "Init (PLam I F) = (\i \ I. lift_set i (Init (F i)))" apply (simp (no_asm) add: PLam_def lift_def lift_set_def) done @@ -37,7 +37,7 @@ apply (simp (no_asm) add: PLam_def) done -lemma PLam_SKIP: "(plam i: I. SKIP) = SKIP" +lemma PLam_SKIP: "(plam i : I. SKIP) = SKIP" apply (simp (no_asm) add: PLam_def lift_SKIP JN_constant) done @@ -46,11 +46,11 @@ lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)" by (unfold PLam_def, auto) -lemma PLam_component_iff: "((PLam I F) <= H) = (ALL i: I. lift i (F i) <= H)" +lemma PLam_component_iff: "((PLam I F) \ H) = (\i \ I. lift i (F i) \ H)" apply (simp (no_asm) add: PLam_def JN_component_iff) done -lemma component_PLam: "i : I ==> lift i (F i) <= (PLam I F)" +lemma component_PLam: "i \ I ==> lift i (F i) \ (PLam I F)" apply (unfold PLam_def) (*blast_tac doesn't use HO unification*) apply (fast intro: component_JN) @@ -60,10 +60,10 @@ (** Safety & Progress: but are they used anywhere? **) lemma PLam_constrains: - "[| i : I; ALL j. F j : preserves snd |] ==> - (PLam I F : (lift_set i (A <*> UNIV)) co + "[| i \ I; \j. F j \ preserves snd |] ==> + (PLam I F \ (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))) = - (F i : (A <*> UNIV) co (B <*> UNIV))" + (F i \ (A <*> UNIV) co (B <*> UNIV))" apply (simp (no_asm_simp) add: PLam_def JN_constrains) apply (subst insert_Diff [symmetric], assumption) apply (simp (no_asm_simp) add: lift_constrains) @@ -71,33 +71,33 @@ done lemma PLam_stable: - "[| i : I; ALL j. F j : preserves snd |] - ==> (PLam I F : stable (lift_set i (A <*> UNIV))) = - (F i : stable (A <*> UNIV))" + "[| i \ I; \j. F j \ preserves snd |] + ==> (PLam I F \ stable (lift_set i (A <*> UNIV))) = + (F i \ stable (A <*> UNIV))" apply (simp (no_asm_simp) add: stable_def PLam_constrains) done lemma PLam_transient: - "i : I ==> - PLam I F : transient A = (EX i:I. lift i (F i) : transient A)" + "i \ I ==> + PLam I F \ transient A = (\i \ I. lift i (F i) \ transient A)" apply (simp (no_asm_simp) add: JN_transient PLam_def) done (*This holds because the F j cannot change (lift_set i)*) lemma PLam_ensures: - "[| i : I; F i : (A <*> UNIV) ensures (B <*> UNIV); - ALL j. F j : preserves snd |] ==> - PLam I F : lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)" + "[| i \ I; F i \ (A <*> UNIV) ensures (B <*> UNIV); + \j. F j \ preserves snd |] ==> + PLam I F \ lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)" apply (auto simp add: ensures_def PLam_constrains PLam_transient lift_transient_eq_disj lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric] Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric]) done lemma PLam_leadsTo_Basis: - "[| i : I; - F i : ((A <*> UNIV) - (B <*> UNIV)) co - ((A <*> UNIV) Un (B <*> UNIV)); - F i : transient ((A <*> UNIV) - (B <*> UNIV)); - ALL j. F j : preserves snd |] ==> - PLam I F : lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)" + "[| i \ I; + F i \ ((A <*> UNIV) - (B <*> UNIV)) co + ((A <*> UNIV) \ (B <*> UNIV)); + F i \ transient ((A <*> UNIV) - (B <*> UNIV)); + \j. F j \ preserves snd |] ==> + PLam I F \ lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)" by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI) @@ -105,20 +105,20 @@ (** invariant **) lemma invariant_imp_PLam_invariant: - "[| F i : invariant (A <*> UNIV); i : I; - ALL j. F j : preserves snd |] - ==> PLam I F : invariant (lift_set i (A <*> UNIV))" + "[| F i \ invariant (A <*> UNIV); i \ I; + \j. F j \ preserves snd |] + ==> PLam I F \ invariant (lift_set i (A <*> UNIV))" by (auto simp add: PLam_stable invariant_def) lemma PLam_preserves_fst [simp]: - "ALL j. F j : preserves snd - ==> (PLam I F : preserves (v o sub j o fst)) = - (if j: I then F j : preserves (v o fst) else True)" + "\j. F j \ preserves snd + ==> (PLam I F \ preserves (v o sub j o fst)) = + (if j \ I then F j \ preserves (v o fst) else True)" by (simp (no_asm_simp) add: PLam_def lift_preserves_sub) lemma PLam_preserves_snd [simp,intro]: - "ALL j. F j : preserves snd ==> PLam I F : preserves snd" + "\j. F j \ preserves snd ==> PLam I F \ preserves snd" by (simp (no_asm_simp) add: PLam_def lift_preserves_snd_I) @@ -130,44 +130,44 @@ something like lift_preserves_sub to rewrite the third. However there's no obvious way to alternative for the third premise.*) lemma guarantees_PLam_I: - "[| lift i (F i): X guarantees Y; i : I; + "[| lift i (F i): X guarantees Y; i \ I; OK I (%i. lift i (F i)) |] - ==> (PLam I F) : X guarantees Y" + ==> (PLam I F) \ X guarantees Y" apply (unfold PLam_def) apply (simp (no_asm_simp) add: guarantees_JN_I) done lemma Allowed_PLam [simp]: - "Allowed (PLam I F) = (INT i:I. lift i ` Allowed(F i))" + "Allowed (PLam I F) = (\i \ I. lift i ` Allowed(F i))" by (simp (no_asm) add: PLam_def) lemma PLam_preserves [simp]: - "(PLam I F) : preserves v = (ALL i:I. F i : preserves (v o lift_map i))" -by (simp (no_asm) add: PLam_def lift_def rename_preserves) + "(PLam I F) \ preserves v = (\i \ I. F i \ preserves (v o lift_map i))" +by (simp add: PLam_def lift_def rename_preserves) (**UNUSED (*The f0 premise ensures that the product is well-defined.*) lemma PLam_invariant_imp_invariant: - "[| PLam I F : invariant (lift_set i A); i : I; - f0: Init (PLam I F) |] ==> F i : invariant A" + "[| PLam I F \ invariant (lift_set i A); i \ I; + f0: Init (PLam I F) |] ==> F i \ invariant A" apply (auto simp add: invariant_def) apply (drule_tac c = "f0 (i:=x) " in subsetD) apply auto done lemma PLam_invariant: - "[| i : I; f0: Init (PLam I F) |] - ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)" + "[| i \ I; f0: Init (PLam I F) |] + ==> (PLam I F \ invariant (lift_set i A)) = (F i \ invariant A)" apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant) done (*The f0 premise isn't needed if F is a constant program because then we get an initial state by replicating that of F*) lemma reachable_PLam: - "i : I - ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)" + "i \ I + ==> ((plam x \ I. F) \ invariant (lift_set i A)) = (F \ invariant A)" apply (auto simp add: invariant_def) done **) @@ -176,25 +176,25 @@ (**UNUSED (** Reachability **) - Goal "[| f : reachable (PLam I F); i : I |] ==> f i : reachable (F i)" + Goal "[| f \ reachable (PLam I F); i \ I |] ==> f i \ reachable (F i)" apply (erule reachable.induct) apply (auto intro: reachable.intrs) done (*Result to justify a re-organization of this file*) - lemma "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))" + lemma "{f. \i \ I. f i \ R i} = (\i \ I. lift_set i (R i))" by auto lemma reachable_PLam_subset1: - "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))" + "reachable (PLam I F) \ (\i \ I. lift_set i (reachable (F i)))" apply (force dest!: reachable_PLam) done (*simplify using reachable_lift??*) lemma reachable_lift_Join_PLam [rule_format]: - "[| i ~: I; A : reachable (F i) |] - ==> ALL f. f : reachable (PLam I F) - --> f(i:=A) : reachable (lift i (F i) Join PLam I F)" + "[| i \ I; A \ reachable (F i) |] + ==> \f. f \ reachable (PLam I F) + --> f(i:=A) \ reachable (lift i (F i) Join PLam I F)" apply (erule reachable.induct) apply (ALLGOALS Clarify_tac) apply (erule reachable.induct) @@ -224,7 +224,7 @@ perform actions, and PLam can never catch up in finite time.*) lemma reachable_PLam_subset2: "finite I - ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)" + ==> (\i \ I. lift_set i (reachable (F i))) \ reachable (PLam I F)" apply (erule finite_induct) apply (simp (no_asm)) apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert) @@ -232,7 +232,7 @@ lemma reachable_PLam_eq: "finite I ==> - reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))" + reachable (PLam I F) = (\i \ I. lift_set i (reachable (F i)))" apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2])) done @@ -240,8 +240,8 @@ (** Co **) lemma Constrains_imp_PLam_Constrains: - "[| F i : A Co B; i: I; finite I |] - ==> PLam I F : (lift_set i A) Co (lift_set i B)" + "[| F i \ A Co B; i \ I; finite I |] + ==> PLam I F \ (lift_set i A) Co (lift_set i B)" apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq) apply (auto simp add: constrains_def PLam_def) apply (REPEAT (blast intro: reachable.intrs)) @@ -250,15 +250,15 @@ lemma PLam_Constrains: - "[| i: I; finite I; f0: Init (PLam I F) |] - ==> (PLam I F : (lift_set i A) Co (lift_set i B)) = - (F i : A Co B)" + "[| i \ I; finite I; f0: Init (PLam I F) |] + ==> (PLam I F \ (lift_set i A) Co (lift_set i B)) = + (F i \ A Co B)" apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains) done lemma PLam_Stable: - "[| i: I; finite I; f0: Init (PLam I F) |] - ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)" + "[| i \ I; finite I; f0: Init (PLam I F) |] + ==> (PLam I F \ Stable (lift_set i A)) = (F i \ Stable A)" apply (simp (no_asm_simp) del: Init_PLam add: Stable_def PLam_Constrains) done @@ -266,23 +266,23 @@ (** const_PLam (no dependence on i) doesn't require the f0 premise **) lemma const_PLam_Constrains: - "[| i: I; finite I |] - ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) = - (F : A Co B)" + "[| i \ I; finite I |] + ==> ((plam x \ I. F) \ (lift_set i A) Co (lift_set i B)) = + (F \ A Co B)" apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains) done lemma const_PLam_Stable: - "[| i: I; finite I |] - ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)" + "[| i \ I; finite I |] + ==> ((plam x \ I. F) \ Stable (lift_set i A)) = (F \ Stable A)" apply (simp (no_asm_simp) add: Stable_def const_PLam_Constrains) done lemma const_PLam_Increasing: - "[| i: I; finite I |] - ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)" + "[| i \ I; finite I |] + ==> ((plam x \ I. F) \ Increasing (f o sub i)) = (F \ Increasing f)" apply (unfold Increasing_def) - apply (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}") + apply (subgoal_tac "\z. {s. z \ (f o sub i) s} = lift_set i {s. z \ f s}") apply (asm_simp_tac (simpset () add: lift_set_sub) 2) apply (simp add: finite_lessThan const_PLam_Stable) done diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Rename.thy --- a/src/HOL/UNITY/Rename.thy Mon Feb 03 11:45:05 2003 +0100 +++ b/src/HOL/UNITY/Rename.thy Tue Feb 04 18:12:40 2003 +0100 @@ -31,7 +31,7 @@ apply (erule surj_f_inv_f) done -lemma mem_rename_set_iff: "bij h ==> z : h`A = (inv h z : A)" +lemma mem_rename_set_iff: "bij h ==> z \ h`A = (inv h z \ A)" by (force simp add: bij_is_inj bij_is_surj [THEN surj_f_inv_f]) @@ -176,31 +176,31 @@ by (simp add: rename_def Extend.extend_Join) lemma rename_JN [simp]: - "bij h ==> rename h (JOIN I F) = (JN i:I. rename h (F i))" + "bij h ==> rename h (JOIN I F) = (\i \ I. rename h (F i))" by (simp add: rename_def Extend.extend_JN) subsection{*Strong Safety: co, stable*} lemma rename_constrains: - "bij h ==> (rename h F : (h`A) co (h`B)) = (F : A co B)" + "bij h ==> (rename h F \ (h`A) co (h`B)) = (F \ A co B)" apply (unfold rename_def) apply (subst extend_set_eq_image [symmetric])+ apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_constrains]) done lemma rename_stable: - "bij h ==> (rename h F : stable (h`A)) = (F : stable A)" + "bij h ==> (rename h F \ stable (h`A)) = (F \ stable A)" apply (simp add: stable_def rename_constrains) done lemma rename_invariant: - "bij h ==> (rename h F : invariant (h`A)) = (F : invariant A)" + "bij h ==> (rename h F \ invariant (h`A)) = (F \ invariant A)" apply (simp add: invariant_def rename_stable bij_is_inj [THEN inj_image_subset_iff]) done lemma rename_increasing: - "bij h ==> (rename h F : increasing func) = (F : increasing (func o h))" + "bij h ==> (rename h F \ increasing func) = (F \ increasing (func o h))" apply (simp add: increasing_def rename_stable [symmetric] bij_image_Collect_eq bij_is_surj [THEN surj_f_inv_f]) done @@ -213,19 +213,19 @@ done lemma rename_Constrains: - "bij h ==> (rename h F : (h`A) Co (h`B)) = (F : A Co B)" + "bij h ==> (rename h F \ (h`A) Co (h`B)) = (F \ A Co B)" by (simp add: Constrains_def reachable_rename_eq rename_constrains bij_is_inj image_Int [symmetric]) lemma rename_Stable: - "bij h ==> (rename h F : Stable (h`A)) = (F : Stable A)" + "bij h ==> (rename h F \ Stable (h`A)) = (F \ Stable A)" by (simp add: Stable_def rename_Constrains) -lemma rename_Always: "bij h ==> (rename h F : Always (h`A)) = (F : Always A)" +lemma rename_Always: "bij h ==> (rename h F \ Always (h`A)) = (F \ Always A)" by (simp add: Always_def rename_Stable bij_is_inj [THEN inj_image_subset_iff]) lemma rename_Increasing: - "bij h ==> (rename h F : Increasing func) = (F : Increasing (func o h))" + "bij h ==> (rename h F \ Increasing func) = (F \ Increasing (func o h))" by (simp add: Increasing_def rename_Stable [symmetric] bij_image_Collect_eq bij_is_surj [THEN surj_f_inv_f]) @@ -233,52 +233,52 @@ subsection{*Progress: transient, ensures*} lemma rename_transient: - "bij h ==> (rename h F : transient (h`A)) = (F : transient A)" + "bij h ==> (rename h F \ transient (h`A)) = (F \ transient A)" apply (unfold rename_def) apply (subst extend_set_eq_image [symmetric]) apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_transient]) done lemma rename_ensures: - "bij h ==> (rename h F : (h`A) ensures (h`B)) = (F : A ensures B)" + "bij h ==> (rename h F \ (h`A) ensures (h`B)) = (F \ A ensures B)" apply (unfold rename_def) apply (subst extend_set_eq_image [symmetric])+ apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_ensures]) done lemma rename_leadsTo: - "bij h ==> (rename h F : (h`A) leadsTo (h`B)) = (F : A leadsTo B)" + "bij h ==> (rename h F \ (h`A) leadsTo (h`B)) = (F \ A leadsTo B)" apply (unfold rename_def) apply (subst extend_set_eq_image [symmetric])+ apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_leadsTo]) done lemma rename_LeadsTo: - "bij h ==> (rename h F : (h`A) LeadsTo (h`B)) = (F : A LeadsTo B)" + "bij h ==> (rename h F \ (h`A) LeadsTo (h`B)) = (F \ A LeadsTo B)" apply (unfold rename_def) apply (subst extend_set_eq_image [symmetric])+ apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_LeadsTo]) done lemma rename_rename_guarantees_eq: - "bij h ==> (rename h F : (rename h ` X) guarantees + "bij h ==> (rename h F \ (rename h ` X) guarantees (rename h ` Y)) = - (F : X guarantees Y)" + (F \ X guarantees Y)" apply (unfold rename_def) apply (subst good_map_bij [THEN Extend.intro, THEN Extend.extend_guarantees_eq [symmetric]], assumption) apply (simp (no_asm_simp) add: fst_o_inv_eq_inv o_def) done lemma rename_guarantees_eq_rename_inv: - "bij h ==> (rename h F : X guarantees Y) = - (F : (rename (inv h) ` X) guarantees + "bij h ==> (rename h F \ X guarantees Y) = + (F \ (rename (inv h) ` X) guarantees (rename (inv h) ` Y))" apply (subst rename_rename_guarantees_eq [symmetric], assumption) apply (simp add: image_eq_UN o_def bij_is_surj [THEN surj_f_inv_f]) done lemma rename_preserves: - "bij h ==> (rename h G : preserves v) = (G : preserves (v o h))" + "bij h ==> (rename h G \ preserves v) = (G \ preserves (v o h))" apply (subst good_map_bij [THEN Extend.intro, THEN Extend.extend_preserves [symmetric]], assumption) apply (simp add: o_def fst_o_inv_eq_inv rename_def bij_is_surj [THEN surj_f_inv_f]) done diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/SubstAx.thy --- a/src/HOL/UNITY/SubstAx.thy Mon Feb 03 11:45:05 2003 +0100 +++ b/src/HOL/UNITY/SubstAx.thy Tue Feb 04 18:12:40 2003 +0100 @@ -12,10 +12,10 @@ constdefs Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60) - "A Ensures B == {F. F : (reachable F Int A) ensures B}" + "A Ensures B == {F. F \ (reachable F \ A) ensures B}" LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) - "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}" + "A LeadsTo B == {F. F \ (reachable F \ A) leadsTo B}" syntax (xsymbols) "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \w " 60) @@ -23,7 +23,7 @@ (*Resembles the previous definition of LeadsTo*) lemma LeadsTo_eq_leadsTo: - "A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}" + "A LeadsTo B = {F. F \ (reachable F \ A) leadsTo (reachable F \ B)}" apply (unfold LeadsTo_def) apply (blast dest: psp_stable2 intro: leadsTo_weaken) done @@ -34,35 +34,37 @@ (** Conjoining an Always property **) lemma Always_LeadsTo_pre: - "F : Always INV ==> (F : (INV Int A) LeadsTo A') = (F : A LeadsTo A')" -by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric]) + "F \ Always INV ==> (F \ (INV \ A) LeadsTo A') = (F \ A LeadsTo A')" +by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 + Int_assoc [symmetric]) lemma Always_LeadsTo_post: - "F : Always INV ==> (F : A LeadsTo (INV Int A')) = (F : A LeadsTo A')" -by (simp add: LeadsTo_eq_leadsTo Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric]) + "F \ Always INV ==> (F \ A LeadsTo (INV \ A')) = (F \ A LeadsTo A')" +by (simp add: LeadsTo_eq_leadsTo Always_eq_includes_reachable Int_absorb2 + Int_assoc [symmetric]) -(* [| F : Always C; F : (C Int A) LeadsTo A' |] ==> F : A LeadsTo A' *) +(* [| F \ Always C; F \ (C \ A) LeadsTo A' |] ==> F \ A LeadsTo A' *) lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1, standard] -(* [| F : Always INV; F : A LeadsTo A' |] ==> F : A LeadsTo (INV Int A') *) +(* [| F \ Always INV; F \ A LeadsTo A' |] ==> F \ A LeadsTo (INV \ A') *) lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard] subsection{*Introduction rules: Basis, Trans, Union*} -lemma leadsTo_imp_LeadsTo: "F : A leadsTo B ==> F : A LeadsTo B" +lemma leadsTo_imp_LeadsTo: "F \ A leadsTo B ==> F \ A LeadsTo B" apply (simp add: LeadsTo_def) apply (blast intro: leadsTo_weaken_L) done lemma LeadsTo_Trans: - "[| F : A LeadsTo B; F : B LeadsTo C |] ==> F : A LeadsTo C" + "[| F \ A LeadsTo B; F \ B LeadsTo C |] ==> F \ A LeadsTo C" apply (simp add: LeadsTo_eq_leadsTo) apply (blast intro: leadsTo_Trans) done lemma LeadsTo_Union: - "(!!A. A : S ==> F : A LeadsTo B) ==> F : (Union S) LeadsTo B" + "(!!A. A \ S ==> F \ A LeadsTo B) ==> F \ (Union S) LeadsTo B" apply (simp add: LeadsTo_def) apply (subst Int_Union) apply (blast intro: leadsTo_UN) @@ -71,37 +73,37 @@ subsection{*Derived rules*} -lemma LeadsTo_UNIV [simp]: "F : A LeadsTo UNIV" +lemma LeadsTo_UNIV [simp]: "F \ A LeadsTo UNIV" by (simp add: LeadsTo_def) (*Useful with cancellation, disjunction*) lemma LeadsTo_Un_duplicate: - "F : A LeadsTo (A' Un A') ==> F : A LeadsTo A'" + "F \ A LeadsTo (A' \ A') ==> F \ A LeadsTo A'" by (simp add: Un_ac) lemma LeadsTo_Un_duplicate2: - "F : A LeadsTo (A' Un C Un C) ==> F : A LeadsTo (A' Un C)" + "F \ A LeadsTo (A' \ C \ C) ==> F \ A LeadsTo (A' \ C)" by (simp add: Un_ac) lemma LeadsTo_UN: - "(!!i. i : I ==> F : (A i) LeadsTo B) ==> F : (UN i:I. A i) LeadsTo B" + "(!!i. i \ I ==> F \ (A i) LeadsTo B) ==> F \ (\i \ I. A i) LeadsTo B" apply (simp only: Union_image_eq [symmetric]) apply (blast intro: LeadsTo_Union) done (*Binary union introduction rule*) lemma LeadsTo_Un: - "[| F : A LeadsTo C; F : B LeadsTo C |] ==> F : (A Un B) LeadsTo C" + "[| F \ A LeadsTo C; F \ B LeadsTo C |] ==> F \ (A \ B) LeadsTo C" apply (subst Un_eq_Union) apply (blast intro: LeadsTo_Union) done (*Lets us look at the starting state*) lemma single_LeadsTo_I: - "(!!s. s : A ==> F : {s} LeadsTo B) ==> F : A LeadsTo B" + "(!!s. s \ A ==> F \ {s} LeadsTo B) ==> F \ A LeadsTo B" by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast) -lemma subset_imp_LeadsTo: "A <= B ==> F : A LeadsTo B" +lemma subset_imp_LeadsTo: "A \ B ==> F \ A LeadsTo B" apply (simp add: LeadsTo_def) apply (blast intro: subset_imp_leadsTo) done @@ -109,73 +111,73 @@ lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, standard, simp] lemma LeadsTo_weaken_R [rule_format]: - "[| F : A LeadsTo A'; A' <= B' |] ==> F : A LeadsTo B'" -apply (simp (no_asm_use) add: LeadsTo_def) + "[| F \ A LeadsTo A'; A' \ B' |] ==> F \ A LeadsTo B'" +apply (simp add: LeadsTo_def) apply (blast intro: leadsTo_weaken_R) done lemma LeadsTo_weaken_L [rule_format]: - "[| F : A LeadsTo A'; B <= A |] - ==> F : B LeadsTo A'" -apply (simp (no_asm_use) add: LeadsTo_def) + "[| F \ A LeadsTo A'; B \ A |] + ==> F \ B LeadsTo A'" +apply (simp add: LeadsTo_def) apply (blast intro: leadsTo_weaken_L) done lemma LeadsTo_weaken: - "[| F : A LeadsTo A'; - B <= A; A' <= B' |] - ==> F : B LeadsTo B'" + "[| F \ A LeadsTo A'; + B \ A; A' \ B' |] + ==> F \ B LeadsTo B'" by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans) lemma Always_LeadsTo_weaken: - "[| F : Always C; F : A LeadsTo A'; - C Int B <= A; C Int A' <= B' |] - ==> F : B LeadsTo B'" + "[| F \ Always C; F \ A LeadsTo A'; + C \ B \ A; C \ A' \ B' |] + ==> F \ B LeadsTo B'" by (blast dest: Always_LeadsToI intro: LeadsTo_weaken intro: Always_LeadsToD) (** Two theorems for "proof lattices" **) -lemma LeadsTo_Un_post: "F : A LeadsTo B ==> F : (A Un B) LeadsTo B" +lemma LeadsTo_Un_post: "F \ A LeadsTo B ==> F \ (A \ B) LeadsTo B" by (blast intro: LeadsTo_Un subset_imp_LeadsTo) lemma LeadsTo_Trans_Un: - "[| F : A LeadsTo B; F : B LeadsTo C |] - ==> F : (A Un B) LeadsTo C" + "[| F \ A LeadsTo B; F \ B LeadsTo C |] + ==> F \ (A \ B) LeadsTo C" by (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans) (** Distributive laws **) lemma LeadsTo_Un_distrib: - "(F : (A Un B) LeadsTo C) = (F : A LeadsTo C & F : B LeadsTo C)" + "(F \ (A \ B) LeadsTo C) = (F \ A LeadsTo C & F \ B LeadsTo C)" by (blast intro: LeadsTo_Un LeadsTo_weaken_L) lemma LeadsTo_UN_distrib: - "(F : (UN i:I. A i) LeadsTo B) = (ALL i : I. F : (A i) LeadsTo B)" + "(F \ (\i \ I. A i) LeadsTo B) = (\i \ I. F \ (A i) LeadsTo B)" by (blast intro: LeadsTo_UN LeadsTo_weaken_L) lemma LeadsTo_Union_distrib: - "(F : (Union S) LeadsTo B) = (ALL A : S. F : A LeadsTo B)" + "(F \ (Union S) LeadsTo B) = (\A \ S. F \ A LeadsTo B)" by (blast intro: LeadsTo_Union LeadsTo_weaken_L) (** More rules using the premise "Always INV" **) -lemma LeadsTo_Basis: "F : A Ensures B ==> F : A LeadsTo B" +lemma LeadsTo_Basis: "F \ A Ensures B ==> F \ A LeadsTo B" by (simp add: Ensures_def LeadsTo_def leadsTo_Basis) lemma EnsuresI: - "[| F : (A-B) Co (A Un B); F : transient (A-B) |] - ==> F : A Ensures B" + "[| F \ (A-B) Co (A \ B); F \ transient (A-B) |] + ==> F \ A Ensures B" apply (simp add: Ensures_def Constrains_eq_constrains) apply (blast intro: ensuresI constrains_weaken transient_strengthen) done lemma Always_LeadsTo_Basis: - "[| F : Always INV; - F : (INV Int (A-A')) Co (A Un A'); - F : transient (INV Int (A-A')) |] - ==> F : A LeadsTo A'" + "[| F \ Always INV; + F \ (INV \ (A-A')) Co (A \ A'); + F \ transient (INV \ (A-A')) |] + ==> F \ A LeadsTo A'" apply (rule Always_LeadsToI, assumption) apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen) done @@ -183,14 +185,14 @@ (*Set difference: maybe combine with leadsTo_weaken_L?? This is the most useful form of the "disjunction" rule*) lemma LeadsTo_Diff: - "[| F : (A-B) LeadsTo C; F : (A Int B) LeadsTo C |] - ==> F : A LeadsTo C" + "[| F \ (A-B) LeadsTo C; F \ (A \ B) LeadsTo C |] + ==> F \ A LeadsTo C" by (blast intro: LeadsTo_Un LeadsTo_weaken) lemma LeadsTo_UN_UN: - "(!! i. i:I ==> F : (A i) LeadsTo (A' i)) - ==> F : (UN i:I. A i) LeadsTo (UN i:I. A' i)" + "(!! i. i \ I ==> F \ (A i) LeadsTo (A' i)) + ==> F \ (\i \ I. A i) LeadsTo (\i \ I. A' i)" apply (simp only: Union_image_eq [symmetric]) apply (blast intro: LeadsTo_Union LeadsTo_weaken_R) done @@ -198,48 +200,47 @@ (*Version with no index set*) lemma LeadsTo_UN_UN_noindex: - "(!! i. F : (A i) LeadsTo (A' i)) - ==> F : (UN i. A i) LeadsTo (UN i. A' i)" + "(!!i. F \ (A i) LeadsTo (A' i)) ==> F \ (\i. A i) LeadsTo (\i. A' i)" by (blast intro: LeadsTo_UN_UN) (*Version with no index set*) lemma all_LeadsTo_UN_UN: - "ALL i. F : (A i) LeadsTo (A' i) - ==> F : (UN i. A i) LeadsTo (UN i. A' i)" + "\i. F \ (A i) LeadsTo (A' i) + ==> F \ (\i. A i) LeadsTo (\i. A' i)" by (blast intro: LeadsTo_UN_UN) (*Binary union version*) lemma LeadsTo_Un_Un: - "[| F : A LeadsTo A'; F : B LeadsTo B' |] - ==> F : (A Un B) LeadsTo (A' Un B')" + "[| F \ A LeadsTo A'; F \ B LeadsTo B' |] + ==> F \ (A \ B) LeadsTo (A' \ B')" by (blast intro: LeadsTo_Un LeadsTo_weaken_R) (** The cancellation law **) lemma LeadsTo_cancel2: - "[| F : A LeadsTo (A' Un B); F : B LeadsTo B' |] - ==> F : A LeadsTo (A' Un B')" + "[| F \ A LeadsTo (A' \ B); F \ B LeadsTo B' |] + ==> F \ A LeadsTo (A' \ B')" by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans) lemma LeadsTo_cancel_Diff2: - "[| F : A LeadsTo (A' Un B); F : (B-A') LeadsTo B' |] - ==> F : A LeadsTo (A' Un B')" + "[| F \ A LeadsTo (A' \ B); F \ (B-A') LeadsTo B' |] + ==> F \ A LeadsTo (A' \ B')" apply (rule LeadsTo_cancel2) prefer 2 apply assumption apply (simp_all (no_asm_simp)) done lemma LeadsTo_cancel1: - "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |] - ==> F : A LeadsTo (B' Un A')" + "[| F \ A LeadsTo (B \ A'); F \ B LeadsTo B' |] + ==> F \ A LeadsTo (B' \ A')" apply (simp add: Un_commute) apply (blast intro!: LeadsTo_cancel2) done lemma LeadsTo_cancel_Diff1: - "[| F : A LeadsTo (B Un A'); F : (B-A') LeadsTo B' |] - ==> F : A LeadsTo (B' Un A')" + "[| F \ A LeadsTo (B \ A'); F \ (B-A') LeadsTo B' |] + ==> F \ A LeadsTo (B' \ A')" apply (rule LeadsTo_cancel1) prefer 2 apply assumption apply (simp_all (no_asm_simp)) @@ -249,8 +250,8 @@ (** The impossibility law **) (*The set "A" may be non-empty, but it contains no reachable states*) -lemma LeadsTo_empty: "F : A LeadsTo {} ==> F : Always (-A)" -apply (simp (no_asm_use) add: LeadsTo_def Always_eq_includes_reachable) +lemma LeadsTo_empty: "F \ A LeadsTo {} ==> F \ Always (-A)" +apply (simp add: LeadsTo_def Always_eq_includes_reachable) apply (drule leadsTo_empty, auto) done @@ -259,33 +260,33 @@ (*Special case of PSP: Misra's "stable conjunction"*) lemma PSP_Stable: - "[| F : A LeadsTo A'; F : Stable B |] - ==> F : (A Int B) LeadsTo (A' Int B)" -apply (simp (no_asm_use) add: LeadsTo_eq_leadsTo Stable_eq_stable) + "[| F \ A LeadsTo A'; F \ Stable B |] + ==> F \ (A \ B) LeadsTo (A' \ B)" +apply (simp add: LeadsTo_eq_leadsTo Stable_eq_stable) apply (drule psp_stable, assumption) apply (simp add: Int_ac) done lemma PSP_Stable2: - "[| F : A LeadsTo A'; F : Stable B |] - ==> F : (B Int A) LeadsTo (B Int A')" + "[| F \ A LeadsTo A'; F \ Stable B |] + ==> F \ (B \ A) LeadsTo (B \ A')" by (simp add: PSP_Stable Int_ac) lemma PSP: - "[| F : A LeadsTo A'; F : B Co B' |] - ==> F : (A Int B') LeadsTo ((A' Int B) Un (B' - B))" -apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains) + "[| F \ A LeadsTo A'; F \ B Co B' |] + ==> F \ (A \ B') LeadsTo ((A' \ B) \ (B' - B))" +apply (simp add: LeadsTo_def Constrains_eq_constrains) apply (blast dest: psp intro: leadsTo_weaken) done lemma PSP2: - "[| F : A LeadsTo A'; F : B Co B' |] - ==> F : (B' Int A) LeadsTo ((B Int A') Un (B' - B))" + "[| F \ A LeadsTo A'; F \ B Co B' |] + ==> F \ (B' \ A) LeadsTo ((B \ A') \ (B' - B))" by (simp add: PSP Int_ac) lemma PSP_Unless: - "[| F : A LeadsTo A'; F : B Unless B' |] - ==> F : (A Int B) LeadsTo ((A' Int B) Un B')" + "[| F \ A LeadsTo A'; F \ B Unless B' |] + ==> F \ (A \ B) LeadsTo ((A' \ B) \ B')" apply (unfold Unless_def) apply (drule PSP, assumption) apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo) @@ -293,8 +294,8 @@ lemma Stable_transient_Always_LeadsTo: - "[| F : Stable A; F : transient C; - F : Always (-A Un B Un C) |] ==> F : A LeadsTo B" + "[| F \ Stable A; F \ transient C; + F \ Always (-A \ B \ C) |] ==> F \ A LeadsTo B" apply (erule Always_LeadsTo_weaken) apply (rule LeadsTo_Diff) prefer 2 @@ -309,10 +310,10 @@ (** Meta or object quantifier ????? **) lemma LeadsTo_wf_induct: "[| wf r; - ALL m. F : (A Int f-`{m}) LeadsTo - ((A Int f-`(r^-1 `` {m})) Un B) |] - ==> F : A LeadsTo B" -apply (simp (no_asm_use) add: LeadsTo_eq_leadsTo) + \m. F \ (A \ f-`{m}) LeadsTo + ((A \ f-`(r^-1 `` {m})) \ B) |] + ==> F \ A LeadsTo B" +apply (simp add: LeadsTo_eq_leadsTo) apply (erule leadsTo_wf_induct) apply (blast intro: leadsTo_weaken) done @@ -320,28 +321,27 @@ lemma Bounded_induct: "[| wf r; - ALL m:I. F : (A Int f-`{m}) LeadsTo - ((A Int f-`(r^-1 `` {m})) Un B) |] - ==> F : A LeadsTo ((A - (f-`I)) Un B)" + \m \ I. F \ (A \ f-`{m}) LeadsTo + ((A \ f-`(r^-1 `` {m})) \ B) |] + ==> F \ A LeadsTo ((A - (f-`I)) \ B)" apply (erule LeadsTo_wf_induct, safe) -apply (case_tac "m:I") +apply (case_tac "m \ I") apply (blast intro: LeadsTo_weaken) apply (blast intro: subset_imp_LeadsTo) done lemma LessThan_induct: - "(!!m::nat. F : (A Int f-`{m}) LeadsTo ((A Int f-`(lessThan m)) Un B)) - ==> F : A LeadsTo B" -apply (rule wf_less_than [THEN LeadsTo_wf_induct], auto) -done + "(!!m::nat. F \ (A \ f-`{m}) LeadsTo ((A \ f-`(lessThan m)) \ B)) + ==> F \ A LeadsTo B" +by (rule wf_less_than [THEN LeadsTo_wf_induct], auto) (*Integer version. Could generalize from 0 to any lower bound*) lemma integ_0_le_induct: - "[| F : Always {s. (0::int) <= f s}; - !! z. F : (A Int {s. f s = z}) LeadsTo - ((A Int {s. f s < z}) Un B) |] - ==> F : A LeadsTo B" + "[| F \ Always {s. (0::int) \ f s}; + !! z. F \ (A \ {s. f s = z}) LeadsTo + ((A \ {s. f s < z}) \ B) |] + ==> F \ A LeadsTo B" apply (rule_tac f = "nat o f" in LessThan_induct) apply (simp add: vimage_def) apply (rule Always_LeadsTo_weaken, assumption+) @@ -349,42 +349,42 @@ done lemma LessThan_bounded_induct: - "!!l::nat. [| ALL m:(greaterThan l). F : (A Int f-`{m}) LeadsTo - ((A Int f-`(lessThan m)) Un B) |] - ==> F : A LeadsTo ((A Int (f-`(atMost l))) Un B)" -apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric]) -apply (rule wf_less_than [THEN Bounded_induct]) -apply (simp (no_asm_simp)) + "!!l::nat. \m \ greaterThan l. + F \ (A \ f-`{m}) LeadsTo ((A \ f-`(lessThan m)) \ B) + ==> F \ A LeadsTo ((A \ (f-`(atMost l))) \ B)" +apply (simp only: Diff_eq [symmetric] vimage_Compl + Compl_greaterThan [symmetric]) +apply (rule wf_less_than [THEN Bounded_induct], simp) done lemma GreaterThan_bounded_induct: - "!!l::nat. [| ALL m:(lessThan l). F : (A Int f-`{m}) LeadsTo - ((A Int f-`(greaterThan m)) Un B) |] - ==> F : A LeadsTo ((A Int (f-`(atLeast l))) Un B)" + "!!l::nat. \m \ lessThan l. + F \ (A \ f-`{m}) LeadsTo ((A \ f-`(greaterThan m)) \ B) + ==> F \ A LeadsTo ((A \ (f-`(atLeast l))) \ B)" apply (rule_tac f = f and f1 = "%k. l - k" in wf_less_than [THEN wf_inv_image, THEN LeadsTo_wf_induct]) apply (simp add: inv_image_def Image_singleton, clarify) apply (case_tac "m F : (A Int B) LeadsTo ((A' Int B') Un C)" -apply (simp (no_asm_use) add: LeadsTo_eq_leadsTo Constrains_eq_constrains Int_Un_distrib) + "[| F \ A LeadsTo (A' \ C); F \ A' Co (A' \ C); + F \ B LeadsTo (B' \ C); F \ B' Co (B' \ C) |] + ==> F \ (A \ B) LeadsTo ((A' \ B') \ C)" +apply (simp add: LeadsTo_eq_leadsTo Constrains_eq_constrains Int_Un_distrib) apply (blast intro: completion leadsTo_weaken) done lemma Finite_completion_lemma: "finite I - ==> (ALL i:I. F : (A i) LeadsTo (A' i Un C)) --> - (ALL i:I. F : (A' i) Co (A' i Un C)) --> - F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)" + ==> (\i \ I. F \ (A i) LeadsTo (A' i \ C)) --> + (\i \ I. F \ (A' i) Co (A' i \ C)) --> + F \ (\i \ I. A i) LeadsTo ((\i \ I. A' i) \ C)" apply (erule finite_induct, auto) apply (rule Completion) prefer 4 @@ -394,15 +394,15 @@ lemma Finite_completion: "[| finite I; - !!i. i:I ==> F : (A i) LeadsTo (A' i Un C); - !!i. i:I ==> F : (A' i) Co (A' i Un C) |] - ==> F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)" + !!i. i \ I ==> F \ (A i) LeadsTo (A' i \ C); + !!i. i \ I ==> F \ (A' i) Co (A' i \ C) |] + ==> F \ (\i \ I. A i) LeadsTo ((\i \ I. A' i) \ C)" by (blast intro: Finite_completion_lemma [THEN mp, THEN mp]) lemma Stable_completion: - "[| F : A LeadsTo A'; F : Stable A'; - F : B LeadsTo B'; F : Stable B' |] - ==> F : (A Int B) LeadsTo (A' Int B')" + "[| F \ A LeadsTo A'; F \ Stable A'; + F \ B LeadsTo B'; F \ Stable B' |] + ==> F \ (A \ B) LeadsTo (A' \ B')" apply (unfold Stable_def) apply (rule_tac C1 = "{}" in Completion [THEN LeadsTo_weaken_R]) apply (force+) @@ -410,14 +410,12 @@ lemma Finite_stable_completion: "[| finite I; - !!i. i:I ==> F : (A i) LeadsTo (A' i); - !!i. i:I ==> F : Stable (A' i) |] - ==> F : (INT i:I. A i) LeadsTo (INT i:I. A' i)" + !!i. i \ I ==> F \ (A i) LeadsTo (A' i); + !!i. i \ I ==> F \ Stable (A' i) |] + ==> F \ (\i \ I. A i) LeadsTo (\i \ I. A' i)" apply (unfold Stable_def) apply (rule_tac C1 = "{}" in Finite_completion [THEN LeadsTo_weaken_R]) -apply (simp_all (no_asm_simp)) -apply blast+ +apply (simp_all, blast+) done - end diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/UNITY.thy --- a/src/HOL/UNITY/UNITY.thy Mon Feb 03 11:45:05 2003 +0100 +++ b/src/HOL/UNITY/UNITY.thy Tue Feb 04 18:12:40 2003 +0100 @@ -14,15 +14,15 @@ typedef (Program) 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set, - allowed :: ('a * 'a)set set). Id:acts & Id: allowed}" + allowed :: ('a * 'a)set set). Id \ acts & Id: allowed}" by blast constdefs constrains :: "['a set, 'a set] => 'a program set" (infixl "co" 60) - "A co B == {F. ALL act: Acts F. act``A <= B}" + "A co B == {F. \act \ Acts F. act``A \ B}" unless :: "['a set, 'a set] => 'a program set" (infixl "unless" 60) - "A unless B == (A-B) co (A Un B)" + "A unless B == (A-B) co (A \ B)" mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set) => 'a program" @@ -39,20 +39,20 @@ "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)" Allowed :: "'a program => 'a program set" - "Allowed F == {G. Acts G <= AllowedActs F}" + "Allowed F == {G. Acts G \ AllowedActs F}" stable :: "'a set => 'a program set" "stable A == A co A" strongest_rhs :: "['a program, 'a set] => 'a set" - "strongest_rhs F A == Inter {B. F : A co B}" + "strongest_rhs F A == Inter {B. F \ A co B}" invariant :: "'a set => 'a program set" - "invariant A == {F. Init F <= A} Int stable A" + "invariant A == {F. Init F \ A} \ stable A" - (*Polymorphic in both states and the meaning of <= *) + (*Polymorphic in both states and the meaning of \ *) increasing :: "['a => 'b::{order}] => 'a program set" - "increasing f == INT z. stable {s. z <= f s}" + "increasing f == \z. stable {s. z \ f s}" (*Perhaps equalities.ML shouldn't add this in the first place!*) @@ -64,7 +64,7 @@ Rep_Program Rep_Program_inverse Abs_Program_inverse Program_def Init_def Acts_def AllowedActs_def mk_program_def -lemma Id_in_Acts [iff]: "Id : Acts F" +lemma Id_in_Acts [iff]: "Id \ Acts F" apply (cut_tac x = F in Rep_Program) apply (auto simp add: program_typedef) done @@ -72,7 +72,7 @@ lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F" by (simp add: insert_absorb Id_in_Acts) -lemma Id_in_AllowedActs [iff]: "Id : AllowedActs F" +lemma Id_in_AllowedActs [iff]: "Id \ AllowedActs F" apply (cut_tac x = F in Rep_Program) apply (auto simp add: program_typedef) done @@ -145,114 +145,114 @@ (*An action is expanded only if a pair of states is being tested against it*) lemma def_act_simp: - "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'" + "[| act == {(s,s'). P s s'} |] ==> ((s,s') \ act) = P s s'" by auto (*A set is expanded only if an element is being tested against it*) -lemma def_set_simp: "A == B ==> (x : A) = (x : B)" +lemma def_set_simp: "A == B ==> (x \ A) = (x \ B)" by auto (*** co ***) lemma constrainsI: - "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') - ==> F : A co A'" + "(!!act s s'. [| act: Acts F; (s,s') \ act; s \ A |] ==> s': A') + ==> F \ A co A'" by (simp add: constrains_def, blast) lemma constrainsD: - "[| F : A co A'; act: Acts F; (s,s'): act; s: A |] ==> s': A'" + "[| F \ A co A'; act: Acts F; (s,s'): act; s \ A |] ==> s': A'" by (unfold constrains_def, blast) -lemma constrains_empty [iff]: "F : {} co B" +lemma constrains_empty [iff]: "F \ {} co B" by (unfold constrains_def, blast) -lemma constrains_empty2 [iff]: "(F : A co {}) = (A={})" +lemma constrains_empty2 [iff]: "(F \ A co {}) = (A={})" by (unfold constrains_def, blast) -lemma constrains_UNIV [iff]: "(F : UNIV co B) = (B = UNIV)" +lemma constrains_UNIV [iff]: "(F \ UNIV co B) = (B = UNIV)" by (unfold constrains_def, blast) -lemma constrains_UNIV2 [iff]: "F : A co UNIV" +lemma constrains_UNIV2 [iff]: "F \ A co UNIV" by (unfold constrains_def, blast) (*monotonic in 2nd argument*) lemma constrains_weaken_R: - "[| F : A co A'; A'<=B' |] ==> F : A co B'" + "[| F \ A co A'; A'<=B' |] ==> F \ A co B'" by (unfold constrains_def, blast) (*anti-monotonic in 1st argument*) lemma constrains_weaken_L: - "[| F : A co A'; B<=A |] ==> F : B co A'" + "[| F \ A co A'; B \ A |] ==> F \ B co A'" by (unfold constrains_def, blast) lemma constrains_weaken: - "[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'" + "[| F \ A co A'; B \ A; A'<=B' |] ==> F \ B co B'" by (unfold constrains_def, blast) (** Union **) lemma constrains_Un: - "[| F : A co A'; F : B co B' |] ==> F : (A Un B) co (A' Un B')" + "[| F \ A co A'; F \ B co B' |] ==> F \ (A \ B) co (A' \ B')" by (unfold constrains_def, blast) lemma constrains_UN: - "(!!i. i:I ==> F : (A i) co (A' i)) - ==> F : (UN i:I. A i) co (UN i:I. A' i)" + "(!!i. i \ I ==> F \ (A i) co (A' i)) + ==> F \ (\i \ I. A i) co (\i \ I. A' i)" by (unfold constrains_def, blast) -lemma constrains_Un_distrib: "(A Un B) co C = (A co C) Int (B co C)" +lemma constrains_Un_distrib: "(A \ B) co C = (A co C) \ (B co C)" by (unfold constrains_def, blast) -lemma constrains_UN_distrib: "(UN i:I. A i) co B = (INT i:I. A i co B)" +lemma constrains_UN_distrib: "(\i \ I. A i) co B = (\i \ I. A i co B)" by (unfold constrains_def, blast) -lemma constrains_Int_distrib: "C co (A Int B) = (C co A) Int (C co B)" +lemma constrains_Int_distrib: "C co (A \ B) = (C co A) \ (C co B)" by (unfold constrains_def, blast) -lemma constrains_INT_distrib: "A co (INT i:I. B i) = (INT i:I. A co B i)" +lemma constrains_INT_distrib: "A co (\i \ I. B i) = (\i \ I. A co B i)" by (unfold constrains_def, blast) (** Intersection **) lemma constrains_Int: - "[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')" + "[| F \ A co A'; F \ B co B' |] ==> F \ (A \ B) co (A' \ B')" by (unfold constrains_def, blast) lemma constrains_INT: - "(!!i. i:I ==> F : (A i) co (A' i)) - ==> F : (INT i:I. A i) co (INT i:I. A' i)" + "(!!i. i \ I ==> F \ (A i) co (A' i)) + ==> F \ (\i \ I. A i) co (\i \ I. A' i)" by (unfold constrains_def, blast) -lemma constrains_imp_subset: "F : A co A' ==> A <= A'" +lemma constrains_imp_subset: "F \ A co A' ==> A \ A'" by (unfold constrains_def, auto) (*The reasoning is by subsets since "co" refers to single actions only. So this rule isn't that useful.*) lemma constrains_trans: - "[| F : A co B; F : B co C |] ==> F : A co C" + "[| F \ A co B; F \ B co C |] ==> F \ A co C" by (unfold constrains_def, blast) lemma constrains_cancel: - "[| F : A co (A' Un B); F : B co B' |] ==> F : A co (A' Un B')" + "[| F \ A co (A' \ B); F \ B co B' |] ==> F \ A co (A' \ B')" by (unfold constrains_def, clarify, blast) (*** unless ***) -lemma unlessI: "F : (A-B) co (A Un B) ==> F : A unless B" +lemma unlessI: "F \ (A-B) co (A \ B) ==> F \ A unless B" by (unfold unless_def, assumption) -lemma unlessD: "F : A unless B ==> F : (A-B) co (A Un B)" +lemma unlessD: "F \ A unless B ==> F \ (A-B) co (A \ B)" by (unfold unless_def, assumption) (*** stable ***) -lemma stableI: "F : A co A ==> F : stable A" +lemma stableI: "F \ A co A ==> F \ stable A" by (unfold stable_def, assumption) -lemma stableD: "F : stable A ==> F : A co A" +lemma stableD: "F \ stable A ==> F \ A co A" by (unfold stable_def, assumption) lemma stable_UNIV [simp]: "stable UNIV = UNIV" @@ -261,14 +261,14 @@ (** Union **) lemma stable_Un: - "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')" + "[| F \ stable A; F \ stable A' |] ==> F \ stable (A \ A')" apply (unfold stable_def) apply (blast intro: constrains_Un) done lemma stable_UN: - "(!!i. i:I ==> F : stable (A i)) ==> F : stable (UN i:I. A i)" + "(!!i. i \ I ==> F \ stable (A i)) ==> F \ stable (\i \ I. A i)" apply (unfold stable_def) apply (blast intro: constrains_UN) done @@ -276,75 +276,75 @@ (** Intersection **) lemma stable_Int: - "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')" + "[| F \ stable A; F \ stable A' |] ==> F \ stable (A \ A')" apply (unfold stable_def) apply (blast intro: constrains_Int) done lemma stable_INT: - "(!!i. i:I ==> F : stable (A i)) ==> F : stable (INT i:I. A i)" + "(!!i. i \ I ==> F \ stable (A i)) ==> F \ stable (\i \ I. A i)" apply (unfold stable_def) apply (blast intro: constrains_INT) done lemma stable_constrains_Un: - "[| F : stable C; F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')" + "[| F \ stable C; F \ A co (C \ A') |] ==> F \ (C \ A) co (C \ A')" by (unfold stable_def constrains_def, blast) lemma stable_constrains_Int: - "[| F : stable C; F : (C Int A) co A' |] ==> F : (C Int A) co (C Int A')" + "[| F \ stable C; F \ (C \ A) co A' |] ==> F \ (C \ A) co (C \ A')" by (unfold stable_def constrains_def, blast) -(*[| F : stable C; F : (C Int A) co A |] ==> F : stable (C Int A) *) +(*[| F \ stable C; F \ (C \ A) co A |] ==> F \ stable (C \ A) *) lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard] (*** invariant ***) -lemma invariantI: "[| Init F<=A; F: stable A |] ==> F : invariant A" +lemma invariantI: "[| Init F \ A; F \ stable A |] ==> F \ invariant A" by (simp add: invariant_def) -(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*) +(*Could also say "invariant A \ invariant B \ invariant (A \ B)"*) lemma invariant_Int: - "[| F : invariant A; F : invariant B |] ==> F : invariant (A Int B)" + "[| F \ invariant A; F \ invariant B |] ==> F \ invariant (A \ B)" by (auto simp add: invariant_def stable_Int) (*** increasing ***) lemma increasingD: - "F : increasing f ==> F : stable {s. z <= f s}" + "F \ increasing f ==> F \ stable {s. z \ f s}" by (unfold increasing_def, blast) -lemma increasing_constant [iff]: "F : increasing (%s. c)" +lemma increasing_constant [iff]: "F \ increasing (%s. c)" by (unfold increasing_def stable_def, auto) lemma mono_increasing_o: - "mono g ==> increasing f <= increasing (g o f)" + "mono g ==> increasing f \ increasing (g o f)" apply (unfold increasing_def stable_def constrains_def, auto) apply (blast intro: monoD order_trans) done -(*Holds by the theorem (Suc m <= n) = (m < n) *) +(*Holds by the theorem (Suc m \ n) = (m < n) *) lemma strict_increasingD: - "!!z::nat. F : increasing f ==> F: stable {s. z < f s}" + "!!z::nat. F \ increasing f ==> F \ stable {s. z < f s}" by (simp add: increasing_def Suc_le_eq [symmetric]) (** The Elimination Theorem. The "free" m has become universally quantified! - Should the premise be !!m instead of ALL m ? Would make it harder to use + Should the premise be !!m instead of \m ? Would make it harder to use in forward proof. **) lemma elimination: - "[| ALL m:M. F : {s. s x = m} co (B m) |] - ==> F : {s. s x : M} co (UN m:M. B m)" + "[| \m \ M. F \ {s. s x = m} co (B m) |] + ==> F \ {s. s x \ M} co (\m \ M. B m)" by (unfold constrains_def, blast) (*As above, but for the trivial case of a one-variable state, in which the state is identified with its one variable.*) lemma elimination_sing: - "(ALL m:M. F : {m} co (B m)) ==> F : M co (UN m:M. B m)" + "(\m \ M. F \ {m} co (B m)) ==> F \ M co (\m \ M. B m)" by (unfold constrains_def, blast) @@ -352,20 +352,20 @@ (*** Theoretical Results from Section 6 ***) lemma constrains_strongest_rhs: - "F : A co (strongest_rhs F A )" + "F \ A co (strongest_rhs F A )" by (unfold constrains_def strongest_rhs_def, blast) lemma strongest_rhs_is_strongest: - "F : A co B ==> strongest_rhs F A <= B" + "F \ A co B ==> strongest_rhs F A \ B" by (unfold constrains_def strongest_rhs_def, blast) (** Ad-hoc set-theory rules **) -lemma Un_Diff_Diff [simp]: "A Un B - (A - B) = B" +lemma Un_Diff_Diff [simp]: "A \ B - (A - B) = B" by blast -lemma Int_Union_Union: "Union(B) Int A = Union((%C. C Int A)`B)" +lemma Int_Union_Union: "Union(B) \ A = Union((%C. C \ A)`B)" by blast (** Needed for WF reasoning in WFair.ML **) diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Union.thy --- a/src/HOL/UNITY/Union.thy Mon Feb 03 11:45:05 2003 +0100 +++ b/src/HOL/UNITY/Union.thy Tue Feb 04 18:12:40 2003 +0100 @@ -12,36 +12,36 @@ constdefs - (*FIXME: conjoin Init F Int Init G ~= {} *) + (*FIXME: conjoin Init F \ Init G \ {} *) ok :: "['a program, 'a program] => bool" (infixl "ok" 65) - "F ok G == Acts F <= AllowedActs G & - Acts G <= AllowedActs F" + "F ok G == Acts F \ AllowedActs G & + Acts G \ AllowedActs F" - (*FIXME: conjoin (INT i:I. Init (F i)) ~= {} *) + (*FIXME: conjoin (\i \ I. Init (F i)) \ {} *) OK :: "['a set, 'a => 'b program] => bool" - "OK I F == (ALL i:I. ALL j: I-{i}. Acts (F i) <= AllowedActs (F j))" + "OK I F == (\i \ I. \j \ I-{i}. Acts (F i) \ AllowedActs (F j))" JOIN :: "['a set, 'a => 'b program] => 'b program" - "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i), - INT i:I. AllowedActs (F i))" + "JOIN I F == mk_program (\i \ I. Init (F i), \i \ I. Acts (F i), + \i \ I. AllowedActs (F i))" Join :: "['a program, 'a program] => 'a program" (infixl "Join" 65) - "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G, - AllowedActs F Int AllowedActs G)" + "F Join G == mk_program (Init F \ Init G, Acts F \ Acts G, + AllowedActs F \ AllowedActs G)" SKIP :: "'a program" "SKIP == mk_program (UNIV, {}, UNIV)" (*Characterizes safety properties. Used with specifying AllowedActs*) safety_prop :: "'a program set => bool" - "safety_prop X == SKIP: X & (ALL G. Acts G <= UNION X Acts --> G : X)" + "safety_prop X == SKIP: X & (\G. Acts G \ UNION X Acts --> G \ X)" syntax "@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10) "@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10) translations - "JN x:A. B" == "JOIN A (%x. B)" + "JN x : A. B" == "JOIN A (%x. B)" "JN x y. B" == "JN x. JN y. B" "JN x. B" == "JOIN UNIV (%x. B)" @@ -49,7 +49,7 @@ SKIP :: "'a program" ("\") "op Join" :: "['a program, 'a program] => 'a program" (infixl "\" 65) "@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\ _./ _)" 10) - "@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\ _:_./ _)" 10) + "@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\ _\_./ _)" 10) subsection{*SKIP*} @@ -68,13 +68,13 @@ subsection{*SKIP and safety properties*} -lemma SKIP_in_constrains_iff [iff]: "(SKIP : A co B) = (A<=B)" +lemma SKIP_in_constrains_iff [iff]: "(SKIP \ A co B) = (A \ B)" by (unfold constrains_def, auto) -lemma SKIP_in_Constrains_iff [iff]: "(SKIP : A Co B) = (A<=B)" +lemma SKIP_in_Constrains_iff [iff]: "(SKIP \ A Co B) = (A \ B)" by (unfold Constrains_def, auto) -lemma SKIP_in_stable [iff]: "SKIP : stable A" +lemma SKIP_in_stable [iff]: "SKIP \ stable A" by (unfold stable_def, auto) declare SKIP_in_stable [THEN stable_imp_Stable, iff] @@ -82,40 +82,40 @@ subsection{*Join*} -lemma Init_Join [simp]: "Init (F Join G) = Init F Int Init G" +lemma Init_Join [simp]: "Init (F Join G) = Init F \ Init G" by (simp add: Join_def) -lemma Acts_Join [simp]: "Acts (F Join G) = Acts F Un Acts G" +lemma Acts_Join [simp]: "Acts (F Join G) = Acts F \ Acts G" by (auto simp add: Join_def) lemma AllowedActs_Join [simp]: - "AllowedActs (F Join G) = AllowedActs F Int AllowedActs G" + "AllowedActs (F Join G) = AllowedActs F \ AllowedActs G" by (auto simp add: Join_def) subsection{*JN*} -lemma JN_empty [simp]: "(JN i:{}. F i) = SKIP" +lemma JN_empty [simp]: "(\i\{}. F i) = SKIP" by (unfold JOIN_def SKIP_def, auto) -lemma JN_insert [simp]: "(JN i:insert a I. F i) = (F a) Join (JN i:I. F i)" +lemma JN_insert [simp]: "(\i \ insert a I. F i) = (F a) Join (\i \ I. F i)" apply (rule program_equalityI) apply (auto simp add: JOIN_def Join_def) done -lemma Init_JN [simp]: "Init (JN i:I. F i) = (INT i:I. Init (F i))" +lemma Init_JN [simp]: "Init (\i \ I. F i) = (\i \ I. Init (F i))" by (simp add: JOIN_def) -lemma Acts_JN [simp]: "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))" +lemma Acts_JN [simp]: "Acts (\i \ I. F i) = insert Id (\i \ I. Acts (F i))" by (auto simp add: JOIN_def) lemma AllowedActs_JN [simp]: - "AllowedActs (JN i:I. F i) = (INT i:I. AllowedActs (F i))" + "AllowedActs (\i \ I. F i) = (\i \ I. AllowedActs (F i))" by (auto simp add: JOIN_def) lemma JN_cong [cong]: - "[| I=J; !!i. i:J ==> F i = G i |] ==> (JN i:I. F i) = (JN i:J. G i)" + "[| I=J; !!i. i \ J ==> F i = G i |] ==> (\i \ I. F i) = (\i \ J. G i)" by (simp add: JOIN_def) @@ -156,28 +156,28 @@ lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute -subsection{*JN laws*} +subsection{*\laws*} (*Also follows by JN_insert and insert_absorb, but the proof is longer*) -lemma JN_absorb: "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)" +lemma JN_absorb: "k \ I ==> F k Join (\i \ I. F i) = (\i \ I. F i)" by (auto intro!: program_equalityI) -lemma JN_Un: "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))" +lemma JN_Un: "(\i \ I \ J. F i) = ((\i \ I. F i) Join (\i \ J. F i))" by (auto intro!: program_equalityI) -lemma JN_constant: "(JN i:I. c) = (if I={} then SKIP else c)" +lemma JN_constant: "(\i \ I. c) = (if I={} then SKIP else c)" by (rule program_equalityI, auto) lemma JN_Join_distrib: - "(JN i:I. F i Join G i) = (JN i:I. F i) Join (JN i:I. G i)" + "(\i \ I. F i Join G i) = (\i \ I. F i) Join (\i \ I. G i)" by (auto intro!: program_equalityI) lemma JN_Join_miniscope: - "i : I ==> (JN i:I. F i Join G) = ((JN i:I. F i) Join G)" + "i \ I ==> (\i \ I. F i Join G) = ((\i \ I. F i) Join G)" by (auto simp add: JN_Join_distrib JN_constant) (*Used to prove guarantees_JN_I*) -lemma JN_Join_diff: "i: I ==> F i Join JOIN (I - {i}) F = JOIN I F" +lemma JN_Join_diff: "i \ I ==> F i Join JOIN (I - {i}) F = JOIN I F" apply (unfold JOIN_def Join_def) apply (rule program_equalityI, auto) done @@ -185,19 +185,19 @@ subsection{*Safety: co, stable, FP*} -(*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B. So an - alternative precondition is A<=B, but most proofs using this rule require +(*Fails if I={} because it collapses to SKIP \ A co B, i.e. to A \ B. So an + alternative precondition is A \ B, but most proofs using this rule require I to be nonempty for other reasons anyway.*) lemma JN_constrains: - "i : I ==> (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)" + "i \ I ==> (\i \ I. F i) \ A co B = (\i \ I. F i \ A co B)" by (simp add: constrains_def JOIN_def, blast) lemma Join_constrains [simp]: - "(F Join G : A co B) = (F : A co B & G : A co B)" + "(F Join G \ A co B) = (F \ A co B & G \ A co B)" by (auto simp add: constrains_def Join_def) lemma Join_unless [simp]: - "(F Join G : A unless B) = (F : A unless B & G : A unless B)" + "(F Join G \ A unless B) = (F \ A unless B & G \ A unless B)" by (simp add: Join_constrains unless_def) (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom. @@ -206,100 +206,100 @@ lemma Join_constrains_weaken: - "[| F : A co A'; G : B co B' |] - ==> F Join G : (A Int B) co (A' Un B')" + "[| F \ A co A'; G \ B co B' |] + ==> F Join G \ (A \ B) co (A' \ B')" by (simp, blast intro: constrains_weaken) -(*If I={}, it degenerates to SKIP : UNIV co {}, which is false.*) +(*If I={}, it degenerates to SKIP \ UNIV co {}, which is false.*) lemma JN_constrains_weaken: - "[| ALL i:I. F i : A i co A' i; i: I |] - ==> (JN i:I. F i) : (INT i:I. A i) co (UN i:I. A' i)" + "[| \i \ I. F i \ A i co A' i; i \ I |] + ==> (\i \ I. F i) \ (\i \ I. A i) co (\i \ I. A' i)" apply (simp (no_asm_simp) add: JN_constrains) apply (blast intro: constrains_weaken) done -lemma JN_stable: "(JN i:I. F i) : stable A = (ALL i:I. F i : stable A)" +lemma JN_stable: "(\i \ I. F i) \ stable A = (\i \ I. F i \ stable A)" by (simp add: stable_def constrains_def JOIN_def) lemma invariant_JN_I: - "[| !!i. i:I ==> F i : invariant A; i : I |] - ==> (JN i:I. F i) : invariant A" + "[| !!i. i \ I ==> F i \ invariant A; i \ I |] + ==> (\i \ I. F i) \ invariant A" by (simp add: invariant_def JN_stable, blast) lemma Join_stable [simp]: - "(F Join G : stable A) = - (F : stable A & G : stable A)" + "(F Join G \ stable A) = + (F \ stable A & G \ stable A)" by (simp add: stable_def) lemma Join_increasing [simp]: - "(F Join G : increasing f) = - (F : increasing f & G : increasing f)" + "(F Join G \ increasing f) = + (F \ increasing f & G \ increasing f)" by (simp add: increasing_def Join_stable, blast) lemma invariant_JoinI: - "[| F : invariant A; G : invariant A |] - ==> F Join G : invariant A" + "[| F \ invariant A; G \ invariant A |] + ==> F Join G \ invariant A" by (simp add: invariant_def, blast) -lemma FP_JN: "FP (JN i:I. F i) = (INT i:I. FP (F i))" +lemma FP_JN: "FP (\i \ I. F i) = (\i \ I. FP (F i))" by (simp add: FP_def JN_stable INTER_def) subsection{*Progress: transient, ensures*} lemma JN_transient: - "i : I ==> - (JN i:I. F i) : transient A = (EX i:I. F i : transient A)" + "i \ I ==> + (\i \ I. F i) \ transient A = (\i \ I. F i \ transient A)" by (auto simp add: transient_def JOIN_def) lemma Join_transient [simp]: - "F Join G : transient A = - (F : transient A | G : transient A)" + "F Join G \ transient A = + (F \ transient A | G \ transient A)" by (auto simp add: bex_Un transient_def Join_def) -lemma Join_transient_I1: "F : transient A ==> F Join G : transient A" +lemma Join_transient_I1: "F \ transient A ==> F Join G \ transient A" by (simp add: Join_transient) -lemma Join_transient_I2: "G : transient A ==> F Join G : transient A" +lemma Join_transient_I2: "G \ transient A ==> F Join G \ transient A" by (simp add: Join_transient) -(*If I={} it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *) +(*If I={} it degenerates to (SKIP \ A ensures B) = False, i.e. to ~(A \ B) *) lemma JN_ensures: - "i : I ==> - (JN i:I. F i) : A ensures B = - ((ALL i:I. F i : (A-B) co (A Un B)) & (EX i:I. F i : A ensures B))" + "i \ I ==> + (\i \ I. F i) \ A ensures B = + ((\i \ I. F i \ (A-B) co (A \ B)) & (\i \ I. F i \ A ensures B))" by (auto simp add: ensures_def JN_constrains JN_transient) lemma Join_ensures: - "F Join G : A ensures B = - (F : (A-B) co (A Un B) & G : (A-B) co (A Un B) & - (F : transient (A-B) | G : transient (A-B)))" + "F Join G \ A ensures B = + (F \ (A-B) co (A \ B) & G \ (A-B) co (A \ B) & + (F \ transient (A-B) | G \ transient (A-B)))" by (auto simp add: ensures_def Join_transient) lemma stable_Join_constrains: - "[| F : stable A; G : A co A' |] - ==> F Join G : A co A'" + "[| F \ stable A; G \ A co A' |] + ==> F Join G \ A co A'" apply (unfold stable_def constrains_def Join_def) apply (simp add: ball_Un, blast) done -(*Premise for G cannot use Always because F: Stable A is weaker than - G : stable A *) +(*Premise for G cannot use Always because F \ Stable A is weaker than + G \ stable A *) lemma stable_Join_Always1: - "[| F : stable A; G : invariant A |] ==> F Join G : Always A" + "[| F \ stable A; G \ invariant A |] ==> F Join G \ 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 : invariant A; G : stable A |] ==> F Join G : Always A" + "[| F \ invariant A; G \ stable A |] ==> F Join G \ Always A" apply (subst Join_commute) apply (blast intro: stable_Join_Always1) done lemma stable_Join_ensures1: - "[| F : stable A; G : A ensures B |] ==> F Join G : A ensures B" + "[| F \ stable A; G \ A ensures B |] ==> F Join G \ 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 : A ensures B; G : stable A |] ==> F Join G : A ensures B" + "[| F \ A ensures B; G \ stable A |] ==> F Join G \ A ensures B" apply (subst Join_commute) apply (blast intro: stable_Join_ensures1) done @@ -344,16 +344,16 @@ lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)" by (auto simp add: ok_def) -lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (ALL i:I. F ok G i)" +lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (\i \ I. F ok G i)" by (auto simp add: ok_def) -lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F = (ALL i:I. G i ok F)" +lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F = (\i \ I. G i ok F)" by (auto simp add: ok_def) -lemma OK_iff_ok: "OK I F = (ALL i: I. ALL j: I-{i}. (F i) ok (F j))" +lemma OK_iff_ok: "OK I F = (\i \ I. \j \ I-{i}. (F i) ok (F j))" by (auto simp add: ok_def OK_def) -lemma OK_imp_ok: "[| OK I F; i: I; j: I; i ~= j|] ==> (F i) ok (F j)" +lemma OK_imp_ok: "[| OK I F; i \ I; j \ I; i \ j|] ==> (F i) ok (F j)" by (auto simp add: OK_iff_ok) @@ -362,27 +362,27 @@ lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV" by (auto simp add: Allowed_def) -lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F Int Allowed G" +lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F \ Allowed G" by (auto simp add: Allowed_def) -lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (INT i:I. Allowed (F i))" +lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (\i \ I. Allowed (F i))" by (auto simp add: Allowed_def) -lemma ok_iff_Allowed: "F ok G = (F : Allowed G & G : Allowed F)" +lemma ok_iff_Allowed: "F ok G = (F \ Allowed G & G \ Allowed F)" by (simp add: ok_def Allowed_def) -lemma OK_iff_Allowed: "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))" +lemma OK_iff_Allowed: "OK I F = (\i \ I. \j \ I-{i}. F i \ Allowed(F j))" by (auto simp add: OK_iff_ok ok_iff_Allowed) subsection{*@{text safety_prop}, for reasoning about given instances of "ok"*} lemma safety_prop_Acts_iff: - "safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)" + "safety_prop X ==> (Acts G \ insert Id (UNION X Acts)) = (G \ X)" by (auto simp add: safety_prop_def) lemma safety_prop_AllowedActs_iff_Allowed: - "safety_prop X ==> (UNION X Acts <= AllowedActs F) = (X <= Allowed F)" + "safety_prop X ==> (UNION X Acts \ AllowedActs F) = (X \ Allowed F)" by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric]) lemma Allowed_eq: @@ -395,27 +395,27 @@ by (simp add: Allowed_eq) (*For safety_prop to hold, the property must be satisfiable!*) -lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A <= B)" +lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A \ B)" by (simp add: safety_prop_def constrains_def, blast) lemma safety_prop_stable [iff]: "safety_prop (stable A)" by (simp add: stable_def) lemma safety_prop_Int [simp]: - "[| safety_prop X; safety_prop Y |] ==> safety_prop (X Int Y)" + "[| safety_prop X; safety_prop Y |] ==> safety_prop (X \ Y)" by (simp add: safety_prop_def, blast) lemma safety_prop_INTER1 [simp]: - "(!!i. safety_prop (X i)) ==> safety_prop (INT i. X i)" + "(!!i. safety_prop (X i)) ==> safety_prop (\i. X i)" by (auto simp add: safety_prop_def, blast) lemma safety_prop_INTER [simp]: - "(!!i. i:I ==> safety_prop (X i)) ==> safety_prop (INT i:I. X i)" + "(!!i. i \ I ==> safety_prop (X i)) ==> safety_prop (\i \ I. X i)" by (auto simp add: safety_prop_def, blast) lemma def_UNION_ok_iff: "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |] - ==> F ok G = (G : X & acts <= AllowedActs G)" + ==> F ok G = (G \ X & acts \ AllowedActs G)" by (auto simp add: ok_def safety_prop_Acts_iff) end diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/WFair.thy --- a/src/HOL/UNITY/WFair.thy Mon Feb 03 11:45:05 2003 +0100 +++ b/src/HOL/UNITY/WFair.thy Tue Feb 04 18:12:40 2003 +0100 @@ -17,10 +17,10 @@ (*This definition specifies weak fairness. The rest of the theory is generic to all forms of fairness.*) transient :: "'a set => 'a program set" - "transient A == {F. EX act: Acts F. A <= Domain act & act``A <= -A}" + "transient A == {F. \act\Acts F. A \ Domain act & act``A \ -A}" ensures :: "['a set, 'a set] => 'a program set" (infixl "ensures" 60) - "A ensures B == (A-B co A Un B) Int transient (A-B)" + "A ensures B == (A-B co A \ B) \ transient (A-B)" consts @@ -32,22 +32,22 @@ inductive "leads F" intros - Basis: "F : A ensures B ==> (A,B) : leads F" + Basis: "F \ A ensures B ==> (A,B) \ leads F" - Trans: "[| (A,B) : leads F; (B,C) : leads F |] ==> (A,C) : leads F" + Trans: "[| (A,B) \ leads F; (B,C) \ leads F |] ==> (A,C) \ leads F" - Union: "ALL A: S. (A,B) : leads F ==> (Union S, B) : leads F" + Union: "\A \ S. (A,B) \ leads F ==> (Union S, B) \ leads F" constdefs (*visible version of the LEADS-TO relation*) leadsTo :: "['a set, 'a set] => 'a program set" (infixl "leadsTo" 60) - "A leadsTo B == {F. (A,B) : leads F}" + "A leadsTo B == {F. (A,B) \ leads F}" (*wlt F B is the largest set that leads to B*) wlt :: "['a program, 'a set] => 'a set" - "wlt F B == Union {A. F: A leadsTo B}" + "wlt F B == Union {A. F \ A leadsTo B}" syntax (xsymbols) "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\" 60) @@ -56,22 +56,22 @@ subsection{*transient*} lemma stable_transient_empty: - "[| F : stable A; F : transient A |] ==> A = {}" + "[| F \ stable A; F \ transient A |] ==> A = {}" by (unfold stable_def constrains_def transient_def, blast) lemma transient_strengthen: - "[| F : transient A; B<=A |] ==> F : transient B" + "[| F \ transient A; B \ A |] ==> F \ transient B" apply (unfold transient_def, clarify) apply (blast intro!: rev_bexI) done lemma transientI: - "[| act: Acts F; A <= Domain act; act``A <= -A |] ==> F : transient A" + "[| act: Acts F; A \ Domain act; act``A \ -A |] ==> F \ transient A" by (unfold transient_def, blast) lemma transientE: - "[| F : transient A; - !!act. [| act: Acts F; A <= Domain act; act``A <= -A |] ==> P |] + "[| F \ transient A; + !!act. [| act: Acts F; A \ Domain act; act``A \ -A |] ==> P |] ==> P" by (unfold transient_def, blast) @@ -85,23 +85,23 @@ subsection{*ensures*} lemma ensuresI: - "[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B" + "[| F \ (A-B) co (A \ B); F \ transient (A-B) |] ==> F \ A ensures B" by (unfold ensures_def, blast) lemma ensuresD: - "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)" + "F \ A ensures B ==> F \ (A-B) co (A \ B) & F \ transient (A-B)" by (unfold ensures_def, blast) lemma ensures_weaken_R: - "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'" + "[| F \ A ensures A'; A'<=B' |] ==> F \ A ensures B'" apply (unfold ensures_def) apply (blast intro: constrains_weaken transient_strengthen) done (*The L-version (precondition strengthening) fails, but we have this*) lemma stable_ensures_Int: - "[| F : stable C; F : A ensures B |] - ==> F : (C Int A) ensures (C Int B)" + "[| F \ stable C; F \ A ensures B |] + ==> F \ (C \ A) ensures (C \ B)" apply (unfold ensures_def) apply (auto simp add: ensures_def Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric]) prefer 2 apply (blast intro: transient_strengthen) @@ -109,78 +109,78 @@ done lemma stable_transient_ensures: - "[| F : stable A; F : transient C; A <= B Un C |] ==> F : A ensures B" + "[| F \ stable A; F \ transient C; A \ B \ C |] ==> F \ A ensures B" apply (simp add: ensures_def stable_def) apply (blast intro: constrains_weaken transient_strengthen) done -lemma ensures_eq: "(A ensures B) = (A unless B) Int transient (A-B)" +lemma ensures_eq: "(A ensures B) = (A unless B) \ transient (A-B)" by (simp (no_asm) add: ensures_def unless_def) subsection{*leadsTo*} -lemma leadsTo_Basis [intro]: "F : A ensures B ==> F : A leadsTo B" +lemma leadsTo_Basis [intro]: "F \ A ensures B ==> F \ A leadsTo B" apply (unfold leadsTo_def) apply (blast intro: leads.Basis) done lemma leadsTo_Trans: - "[| F : A leadsTo B; F : B leadsTo C |] ==> F : A leadsTo C" + "[| F \ A leadsTo B; F \ B leadsTo C |] ==> F \ A leadsTo C" apply (unfold leadsTo_def) apply (blast intro: leads.Trans) done -lemma transient_imp_leadsTo: "F : transient A ==> F : A leadsTo (-A)" +lemma transient_imp_leadsTo: "F \ transient A ==> F \ A leadsTo (-A)" by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition) (*Useful with cancellation, disjunction*) -lemma leadsTo_Un_duplicate: "F : A leadsTo (A' Un A') ==> F : A leadsTo A'" +lemma leadsTo_Un_duplicate: "F \ A leadsTo (A' \ A') ==> F \ A leadsTo A'" by (simp add: Un_ac) lemma leadsTo_Un_duplicate2: - "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)" + "F \ A leadsTo (A' \ C \ C) ==> F \ A leadsTo (A' \ C)" by (simp add: Un_ac) (*The Union introduction rule as we should have liked to state it*) lemma leadsTo_Union: - "(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B" + "(!!A. A \ S ==> F \ A leadsTo B) ==> F \ (Union S) leadsTo B" apply (unfold leadsTo_def) apply (blast intro: leads.Union) done lemma leadsTo_Union_Int: - "(!!A. A : S ==> F : (A Int C) leadsTo B) ==> F : (Union S Int C) leadsTo B" + "(!!A. A \ S ==> F \ (A \ C) leadsTo B) ==> F \ (Union S \ C) leadsTo B" apply (unfold leadsTo_def) apply (simp only: Int_Union_Union) apply (blast intro: leads.Union) done lemma leadsTo_UN: - "(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B" + "(!!i. i \ I ==> F \ (A i) leadsTo B) ==> F \ (\i \ I. A i) leadsTo B" apply (subst Union_image_eq [symmetric]) apply (blast intro: leadsTo_Union) done (*Binary union introduction rule*) lemma leadsTo_Un: - "[| F : A leadsTo C; F : B leadsTo C |] ==> F : (A Un B) leadsTo C" + "[| F \ A leadsTo C; F \ B leadsTo C |] ==> F \ (A \ B) leadsTo C" apply (subst Un_eq_Union) apply (blast intro: leadsTo_Union) done lemma single_leadsTo_I: - "(!!x. x : A ==> F : {x} leadsTo B) ==> F : A leadsTo B" + "(!!x. x \ A ==> F \ {x} leadsTo B) ==> F \ A leadsTo B" by (subst UN_singleton [symmetric], rule leadsTo_UN, blast) (*The INDUCTION rule as we should have liked to state it*) lemma leadsTo_induct: - "[| F : za leadsTo zb; - !!A B. F : A ensures B ==> P A B; - !!A B C. [| F : A leadsTo B; P A B; F : B leadsTo C; P B C |] + "[| F \ za leadsTo zb; + !!A B. F \ A ensures B ==> P A B; + !!A B C. [| F \ A leadsTo B; P A B; F \ B leadsTo C; P B C |] ==> P A C; - !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B + !!B S. \A \ S. F \ A leadsTo B & P A B ==> P (Union S) B |] ==> P za zb" apply (unfold leadsTo_def) apply (drule CollectD, erule leads.induct) @@ -188,7 +188,7 @@ done -lemma subset_imp_ensures: "A<=B ==> F : A ensures B" +lemma subset_imp_ensures: "A \ B ==> F \ A ensures B" by (unfold ensures_def constrains_def transient_def, blast) lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard] @@ -205,10 +205,10 @@ (*Lemma is the weak version: can't see how to do it in one step*) lemma leadsTo_induct_pre_lemma: - "[| F : za leadsTo zb; + "[| F \ za leadsTo zb; P zb; - !!A B. [| F : A ensures B; P B |] ==> P A; - !!S. ALL A:S. P A ==> P (Union S) + !!A B. [| F \ A ensures B; P B |] ==> P A; + !!S. \A \ S. P A ==> P (Union S) |] ==> P za" (*by induction on this formula*) apply (subgoal_tac "P zb --> P za") @@ -219,12 +219,12 @@ done lemma leadsTo_induct_pre: - "[| F : za leadsTo zb; + "[| F \ za leadsTo zb; P zb; - !!A B. [| F : A ensures B; F : B leadsTo zb; P B |] ==> P A; - !!S. ALL A:S. F : A leadsTo zb & P A ==> P (Union S) + !!A B. [| F \ A ensures B; F \ B leadsTo zb; P B |] ==> P A; + !!S. \A \ S. F \ A leadsTo zb & P A ==> P (Union S) |] ==> P za" -apply (subgoal_tac "F : za leadsTo zb & P za") +apply (subgoal_tac "F \ za leadsTo zb & P za") apply (erule conjunct2) apply (erule leadsTo_induct_pre_lemma) prefer 3 apply (blast intro: leadsTo_Union) @@ -233,76 +233,76 @@ done -lemma leadsTo_weaken_R: "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'" +lemma leadsTo_weaken_R: "[| F \ A leadsTo A'; A'<=B' |] ==> F \ A leadsTo B'" by (blast intro: subset_imp_leadsTo leadsTo_Trans) lemma leadsTo_weaken_L [rule_format]: - "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'" + "[| F \ A leadsTo A'; B \ A |] ==> F \ B leadsTo A'" by (blast intro: leadsTo_Trans subset_imp_leadsTo) (*Distributes over binary unions*) lemma leadsTo_Un_distrib: - "F : (A Un B) leadsTo C = (F : A leadsTo C & F : B leadsTo C)" + "F \ (A \ B) leadsTo C = (F \ A leadsTo C & F \ B leadsTo C)" by (blast intro: leadsTo_Un leadsTo_weaken_L) lemma leadsTo_UN_distrib: - "F : (UN i:I. A i) leadsTo B = (ALL i : I. F : (A i) leadsTo B)" + "F \ (\i \ I. A i) leadsTo B = (\i \ I. F \ (A i) leadsTo B)" by (blast intro: leadsTo_UN leadsTo_weaken_L) lemma leadsTo_Union_distrib: - "F : (Union S) leadsTo B = (ALL A : S. F : A leadsTo B)" + "F \ (Union S) leadsTo B = (\A \ S. F \ A leadsTo B)" by (blast intro: leadsTo_Union leadsTo_weaken_L) lemma leadsTo_weaken: - "[| F : A leadsTo A'; B<=A; A'<=B' |] ==> F : B leadsTo B'" + "[| F \ A leadsTo A'; B \ A; A'<=B' |] ==> F \ B leadsTo B'" by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans) (*Set difference: maybe combine with leadsTo_weaken_L?*) lemma leadsTo_Diff: - "[| F : (A-B) leadsTo C; F : B leadsTo C |] ==> F : A leadsTo C" + "[| F \ (A-B) leadsTo C; F \ B leadsTo C |] ==> F \ A leadsTo C" by (blast intro: leadsTo_Un leadsTo_weaken) lemma leadsTo_UN_UN: - "(!! i. i:I ==> F : (A i) leadsTo (A' i)) - ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)" + "(!! i. i \ I ==> F \ (A i) leadsTo (A' i)) + ==> F \ (\i \ I. A i) leadsTo (\i \ I. A' i)" apply (simp only: Union_image_eq [symmetric]) apply (blast intro: leadsTo_Union leadsTo_weaken_R) done (*Binary union version*) lemma leadsTo_Un_Un: - "[| F : A leadsTo A'; F : B leadsTo B' |] - ==> F : (A Un B) leadsTo (A' Un B')" + "[| F \ A leadsTo A'; F \ B leadsTo B' |] + ==> F \ (A \ B) leadsTo (A' \ B')" by (blast intro: leadsTo_Un leadsTo_weaken_R) (** The cancellation law **) lemma leadsTo_cancel2: - "[| F : A leadsTo (A' Un B); F : B leadsTo B' |] - ==> F : A leadsTo (A' Un B')" + "[| F \ A leadsTo (A' \ B); F \ B leadsTo B' |] + ==> F \ A leadsTo (A' \ B')" by (blast intro: leadsTo_Un_Un subset_imp_leadsTo leadsTo_Trans) lemma leadsTo_cancel_Diff2: - "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |] - ==> F : A leadsTo (A' Un B')" + "[| F \ A leadsTo (A' \ B); F \ (B-A') leadsTo B' |] + ==> F \ A leadsTo (A' \ B')" apply (rule leadsTo_cancel2) prefer 2 apply assumption apply (simp_all (no_asm_simp)) done lemma leadsTo_cancel1: - "[| F : A leadsTo (B Un A'); F : B leadsTo B' |] - ==> F : A leadsTo (B' Un A')" + "[| F \ A leadsTo (B \ A'); F \ B leadsTo B' |] + ==> F \ A leadsTo (B' \ A')" apply (simp add: Un_commute) apply (blast intro!: leadsTo_cancel2) done lemma leadsTo_cancel_Diff1: - "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |] - ==> F : A leadsTo (B' Un A')" + "[| F \ A leadsTo (B \ A'); F \ (B-A') leadsTo B' |] + ==> F \ A leadsTo (B' \ A')" apply (rule leadsTo_cancel1) prefer 2 apply assumption apply (simp_all (no_asm_simp)) @@ -312,7 +312,7 @@ (** The impossibility law **) -lemma leadsTo_empty: "F : A leadsTo {} ==> A={}" +lemma leadsTo_empty: "F \ A leadsTo {} ==> A={}" apply (erule leadsTo_induct_pre) apply (simp_all add: ensures_def constrains_def transient_def, blast) done @@ -322,8 +322,8 @@ (*Special case of PSP: Misra's "stable conjunction"*) lemma psp_stable: - "[| F : A leadsTo A'; F : stable B |] - ==> F : (A Int B) leadsTo (A' Int B)" + "[| F \ A leadsTo A'; F \ stable B |] + ==> F \ (A \ B) leadsTo (A' \ B)" apply (unfold stable_def) apply (erule leadsTo_induct) prefer 3 apply (blast intro: leadsTo_Union_Int) @@ -334,19 +334,19 @@ done lemma psp_stable2: - "[| F : A leadsTo A'; F : stable B |] ==> F : (B Int A) leadsTo (B Int A')" + "[| F \ A leadsTo A'; F \ stable B |] ==> F \ (B \ A) leadsTo (B \ A')" by (simp add: psp_stable Int_ac) lemma psp_ensures: - "[| F : A ensures A'; F : B co B' |] - ==> F : (A Int B') ensures ((A' Int B) Un (B' - B))" + "[| F \ A ensures A'; F \ B co B' |] + ==> F \ (A \ B') ensures ((A' \ B) \ (B' - B))" apply (unfold ensures_def constrains_def, clarify) (*speeds up the proof*) apply (blast intro: transient_strengthen) done lemma psp: - "[| F : A leadsTo A'; F : B co B' |] - ==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))" + "[| F \ A leadsTo A'; F \ B co B' |] + ==> F \ (A \ B') leadsTo ((A' \ B) \ (B' - B))" apply (erule leadsTo_induct) prefer 3 apply (blast intro: leadsTo_Union_Int) txt{*Basis case*} @@ -359,13 +359,13 @@ done lemma psp2: - "[| F : A leadsTo A'; F : B co B' |] - ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))" + "[| F \ A leadsTo A'; F \ B co B' |] + ==> F \ (B' \ A) leadsTo ((B \ A') \ (B' - B))" by (simp (no_asm_simp) add: psp Int_ac) lemma psp_unless: - "[| F : A leadsTo A'; F : B unless B' |] - ==> F : (A Int B) leadsTo ((A' Int B) Un B')" + "[| F \ A leadsTo A'; F \ B unless B' |] + ==> F \ (A \ B) leadsTo ((A' \ B) \ B')" apply (unfold unless_def) apply (drule psp, assumption) @@ -379,11 +379,11 @@ lemma leadsTo_wf_induct_lemma: "[| wf r; - ALL m. F : (A Int f-`{m}) leadsTo - ((A Int f-`(r^-1 `` {m})) Un B) |] - ==> F : (A Int f-`{m}) leadsTo B" + \m. F \ (A \ f-`{m}) leadsTo + ((A \ f-`(r^-1 `` {m})) \ B) |] + ==> F \ (A \ f-`{m}) leadsTo B" apply (erule_tac a = m in wf_induct) -apply (subgoal_tac "F : (A Int (f -` (r^-1 `` {x}))) leadsTo B") +apply (subgoal_tac "F \ (A \ (f -` (r^-1 `` {x}))) leadsTo B") apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate) apply (subst vimage_eq_UN) apply (simp only: UN_simps [symmetric]) @@ -394,9 +394,9 @@ (** Meta or object quantifier ? **) lemma leadsTo_wf_induct: "[| wf r; - ALL m. F : (A Int f-`{m}) leadsTo - ((A Int f-`(r^-1 `` {m})) Un B) |] - ==> F : A leadsTo B" + \m. F \ (A \ f-`{m}) leadsTo + ((A \ f-`(r^-1 `` {m})) \ B) |] + ==> F \ A leadsTo B" apply (rule_tac t = A in subst) defer 1 apply (rule leadsTo_UN) @@ -408,102 +408,102 @@ lemma bounded_induct: "[| wf r; - ALL m:I. F : (A Int f-`{m}) leadsTo - ((A Int f-`(r^-1 `` {m})) Un B) |] - ==> F : A leadsTo ((A - (f-`I)) Un B)" + \m \ I. F \ (A \ f-`{m}) leadsTo + ((A \ f-`(r^-1 `` {m})) \ B) |] + ==> F \ A leadsTo ((A - (f-`I)) \ B)" apply (erule leadsTo_wf_induct, safe) -apply (case_tac "m:I") +apply (case_tac "m \ I") apply (blast intro: leadsTo_weaken) apply (blast intro: subset_imp_leadsTo) done -(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*) +(*Alternative proof is via the lemma F \ (A \ f-`(lessThan m)) leadsTo B*) lemma lessThan_induct: - "[| !!m::nat. F : (A Int f-`{m}) leadsTo ((A Int f-`{..m(}) Un B) |] - ==> F : A leadsTo B" + "[| !!m::nat. F \ (A \ f-`{m}) leadsTo ((A \ f-`{..m(}) \ B) |] + ==> F \ A leadsTo B" apply (rule wf_less_than [THEN leadsTo_wf_induct]) apply (simp (no_asm_simp)) apply blast done lemma lessThan_bounded_induct: - "!!l::nat. [| ALL m:(greaterThan l). - F : (A Int f-`{m}) leadsTo ((A Int f-`(lessThan m)) Un B) |] - ==> F : A leadsTo ((A Int (f-`(atMost l))) Un B)" + "!!l::nat. [| \m \ greaterThan l. + F \ (A \ f-`{m}) leadsTo ((A \ f-`(lessThan m)) \ B) |] + ==> F \ A leadsTo ((A \ (f-`(atMost l))) \ B)" apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric]) apply (rule wf_less_than [THEN bounded_induct]) apply (simp (no_asm_simp)) done lemma greaterThan_bounded_induct: - "!!l::nat. [| ALL m:(lessThan l). - F : (A Int f-`{m}) leadsTo ((A Int f-`(greaterThan m)) Un B) |] - ==> F : A leadsTo ((A Int (f-`(atLeast l))) Un B)" + "(!!l::nat. \m \ lessThan l. + F \ (A \ f-`{m}) leadsTo ((A \ f-`(greaterThan m)) \ B)) + ==> F \ A leadsTo ((A \ (f-`(atLeast l))) \ B)" apply (rule_tac f = f and f1 = "%k. l - k" in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct]) apply (simp (no_asm) add: inv_image_def Image_singleton) apply clarify apply (case_tac "m (wlt F B) leadsTo B" apply (unfold wlt_def) apply (blast intro!: leadsTo_Union) done -lemma leadsTo_subset: "F : A leadsTo B ==> A <= wlt F B" +lemma leadsTo_subset: "F \ A leadsTo B ==> A \ wlt F B" apply (unfold wlt_def) apply (blast intro!: leadsTo_Union) done (*Misra's property W2*) -lemma leadsTo_eq_subset_wlt: "F : A leadsTo B = (A <= wlt F B)" +lemma leadsTo_eq_subset_wlt: "F \ A leadsTo B = (A \ wlt F B)" by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L]) (*Misra's property W4*) -lemma wlt_increasing: "B <= wlt F B" +lemma wlt_increasing: "B \ wlt F B" apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo) done (*Used in the Trans case below*) lemma lemma1: - "[| B <= A2; - F : (A1 - B) co (A1 Un B); - F : (A2 - C) co (A2 Un C) |] - ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)" + "[| B \ A2; + F \ (A1 - B) co (A1 \ B); + F \ (A2 - C) co (A2 \ C) |] + ==> F \ (A1 \ A2 - C) co (A1 \ A2 \ C)" by (unfold constrains_def, clarify, blast) (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) lemma leadsTo_123: - "F : A leadsTo A' - ==> EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')" + "F \ A leadsTo A' + ==> \B. A \ B & F \ B leadsTo A' & F \ (B-A') co (B \ A')" apply (erule leadsTo_induct) (*Basis*) apply (blast dest: ensuresD) (*Trans*) apply clarify -apply (rule_tac x = "Ba Un Bb" in exI) +apply (rule_tac x = "Ba \ Bb" in exI) apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate) (*Union*) apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice) -apply (rule_tac x = "UN A:S. f A" in exI) +apply (rule_tac x = "\A \ S. f A" in exI) apply (auto intro: leadsTo_UN) (*Blast_tac says PROOF FAILED*) -apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i Un B" +apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i \ B" in constrains_UN [THEN constrains_weaken], auto) done (*Misra's property W5*) -lemma wlt_constrains_wlt: "F : (wlt F B - B) co (wlt F B)" +lemma wlt_constrains_wlt: "F \ (wlt F B - B) co (wlt F B)" proof - from wlt_leadsTo [of F B, THEN leadsTo_123] show ?thesis @@ -527,28 +527,28 @@ subsection{*Completion: Binary and General Finite versions*} lemma completion_lemma : - "[| W = wlt F (B' Un C); - F : A leadsTo (A' Un C); F : A' co (A' Un C); - F : B leadsTo (B' Un C); F : B' co (B' Un C) |] - ==> F : (A Int B) leadsTo ((A' Int B') Un C)" -apply (subgoal_tac "F : (W-C) co (W Un B' Un C) ") + "[| W = wlt F (B' \ C); + F \ A leadsTo (A' \ C); F \ A' co (A' \ C); + F \ B leadsTo (B' \ C); F \ B' co (B' \ C) |] + ==> F \ (A \ B) leadsTo ((A' \ B') \ C)" +apply (subgoal_tac "F \ (W-C) co (W \ B' \ C) ") prefer 2 apply (blast intro: wlt_constrains_wlt [THEN [2] constrains_Un, THEN constrains_weaken]) -apply (subgoal_tac "F : (W-C) co W") +apply (subgoal_tac "F \ (W-C) co W") prefer 2 apply (simp add: wlt_increasing Un_assoc Un_absorb2) -apply (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C) ") +apply (subgoal_tac "F \ (A \ W - C) leadsTo (A' \ W \ C) ") prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken]) (** LEVEL 6 **) -apply (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C) ") +apply (subgoal_tac "F \ (A' \ W \ C) leadsTo (A' \ B' \ C) ") prefer 2 apply (rule leadsTo_Un_duplicate2) apply (blast intro: leadsTo_Un_Un wlt_leadsTo [THEN psp2, THEN leadsTo_weaken] leadsTo_refl) apply (drule leadsTo_Diff) apply (blast intro: subset_imp_leadsTo) -apply (subgoal_tac "A Int B <= A Int W") +apply (subgoal_tac "A \ B \ A \ W") prefer 2 apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono]) apply (blast intro: leadsTo_Trans subset_imp_leadsTo) @@ -557,9 +557,9 @@ lemmas completion = completion_lemma [OF refl] lemma finite_completion_lemma: - "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) --> - (ALL i:I. F : (A' i) co (A' i Un C)) --> - F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)" + "finite I ==> (\i \ I. F \ (A i) leadsTo (A' i \ C)) --> + (\i \ I. F \ (A' i) co (A' i \ C)) --> + F \ (\i \ I. A i) leadsTo ((\i \ I. A' i) \ C)" apply (erule finite_induct, auto) apply (rule completion) prefer 4 @@ -569,15 +569,15 @@ lemma finite_completion: "[| finite I; - !!i. i:I ==> F : (A i) leadsTo (A' i Un C); - !!i. i:I ==> F : (A' i) co (A' i Un C) |] - ==> F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)" + !!i. i \ I ==> F \ (A i) leadsTo (A' i \ C); + !!i. i \ I ==> F \ (A' i) co (A' i \ C) |] + ==> F \ (\i \ I. A i) leadsTo ((\i \ I. A' i) \ C)" by (blast intro: finite_completion_lemma [THEN mp, THEN mp]) lemma stable_completion: - "[| F : A leadsTo A'; F : stable A'; - F : B leadsTo B'; F : stable B' |] - ==> F : (A Int B) leadsTo (A' Int B')" + "[| F \ A leadsTo A'; F \ stable A'; + F \ B leadsTo B'; F \ stable B' |] + ==> F \ (A \ B) leadsTo (A' \ B')" apply (unfold stable_def) apply (rule_tac C1 = "{}" in completion [THEN leadsTo_weaken_R]) apply (force+) @@ -585,9 +585,9 @@ lemma finite_stable_completion: "[| finite I; - !!i. i:I ==> F : (A i) leadsTo (A' i); - !!i. i:I ==> F : stable (A' i) |] - ==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)" + !!i. i \ I ==> F \ (A i) leadsTo (A' i); + !!i. i \ I ==> F \ stable (A' i) |] + ==> F \ (\i \ I. A i) leadsTo (\i \ I. A' i)" apply (unfold stable_def) apply (rule_tac C1 = "{}" in finite_completion [THEN leadsTo_weaken_R]) apply (simp_all (no_asm_simp))