--- a/src/HOL/Algebra/FiniteProduct.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Thu Jul 23 22:13:42 2015 +0200
@@ -296,15 +296,9 @@
syntax
"_finprod" :: "index => idt => 'a set => 'b => 'b"
- ("(3\<Otimes>__:_. _)" [1000, 0, 51, 10] 10)
-syntax (xsymbols)
- "_finprod" :: "index => idt => 'a set => 'b => 'b"
- ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
-syntax (HTML output)
- "_finprod" :: "index => idt => 'a set => 'b => 'b"
("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
translations
- "\<Otimes>\<index>i:A. b" == "CONST finprod \<struct>\<index> (%i. b) A"
+ "\<Otimes>\<index>i\<in>A. b" \<rightleftharpoons> "CONST finprod \<struct>\<index> (%i. b) A"
-- {* Beware of argument permutation! *}
lemma (in comm_monoid) finprod_empty [simp]:
@@ -338,8 +332,7 @@
apply (auto simp add: finprod_def)
done
-lemma finprod_one [simp]:
- "(\<Otimes>i:A. \<one>) = \<one>"
+lemma finprod_one [simp]: "(\<Otimes>i\<in>A. \<one>) = \<one>"
proof (induct A rule: infinite_finite_induct)
case empty show ?case by simp
next
--- a/src/HOL/Algebra/Ring.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/Algebra/Ring.thy Thu Jul 23 22:13:42 2015 +0200
@@ -36,15 +36,9 @@
syntax
"_finsum" :: "index => idt => 'a set => 'b => 'b"
- ("(3\<Oplus>__:_. _)" [1000, 0, 51, 10] 10)
-syntax (xsymbols)
- "_finsum" :: "index => idt => 'a set => 'b => 'b"
- ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
-syntax (HTML output)
- "_finsum" :: "index => idt => 'a set => 'b => 'b"
("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
translations
- "\<Oplus>\<index>i:A. b" == "CONST finsum \<struct>\<index> (%i. b) A"
+ "\<Oplus>\<index>i\<in>A. b" \<rightleftharpoons> "CONST finsum \<struct>\<index> (%i. b) A"
-- {* Beware of argument permutation! *}
--- a/src/HOL/MicroJava/BV/Correct.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy Thu Jul 23 22:13:42 2015 +0200
@@ -42,7 +42,7 @@
correct_frames G hp phi rT sig frs))))"
definition correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
- ("_,_ |-JVM _ [ok]" [51,51] 50) where
+ ("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50) where
"correct_state G phi == \<lambda>(xp,hp,frs).
case xp of
None \<Rightarrow> (case frs of
@@ -59,10 +59,6 @@
| Some x \<Rightarrow> frs = []"
-notation (xsymbols)
- correct_state ("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50)
-
-
lemma sup_ty_opt_OK:
"(G \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')"
by (cases X) auto
--- a/src/HOL/MicroJava/Comp/TranslCompTp.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy Thu Jul 23 22:13:42 2015 +0200
@@ -8,7 +8,9 @@
(**********************************************************************)
-definition comb :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd" where
+definition comb :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd"
+ (infixr "\<box>" 55)
+where
"comb == (\<lambda> f1 f2 x0. let (xs1, x1) = f1 x0;
(xs2, x2) = f2 x1
in (xs1 @ xs2, x2))"
@@ -16,9 +18,6 @@
definition comb_nil :: "'a \<Rightarrow> 'b list \<times> 'a" where
"comb_nil a == ([], a)"
-notation (xsymbols)
- comb (infixr "\<box>" 55)
-
lemma comb_nil_left [simp]: "comb_nil \<box> f = f"
by (simp add: comb_def comb_nil_def split_beta)
--- a/src/HOL/Number_Theory/MiscAlgebra.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy Thu Jul 23 22:13:42 2015 +0200
@@ -155,12 +155,12 @@
and a [simp]: "a : carrier G"
shows "a (^) card(carrier G) = one G"
proof -
- have "(\<Otimes>x:carrier G. x) = (\<Otimes>x:carrier G. a \<otimes> x)"
+ have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
by (subst (2) finprod_reindex [symmetric],
auto simp add: Pi_def inj_on_const_mult surj_const_mult)
- also have "\<dots> = (\<Otimes>x:carrier G. a) \<otimes> (\<Otimes>x:carrier G. x)"
+ also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
by (auto simp add: finprod_multf Pi_def)
- also have "(\<Otimes>x:carrier G. a) = a (^) card(carrier G)"
+ also have "(\<Otimes>x\<in>carrier G. a) = a (^) card(carrier G)"
by (auto simp add: finprod_const)
finally show ?thesis
(* uses the preceeding lemma *)
--- a/src/HOL/UNITY/Comp/Alloc.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy Thu Jul 23 22:13:42 2015 +0200
@@ -247,7 +247,7 @@
where Network: "Network : network_spec"
definition System :: "'a systemState program"
- where "System = rename sysOfAlloc Alloc Join Network Join
+ where "System = rename sysOfAlloc Alloc \<squnion> Network \<squnion>
(rename sysOfClient
(plam x: lessThan Nclients. rename client_map Client))"
@@ -268,9 +268,9 @@
defines
System_def
"System == rename sysOfAlloc Alloc
- Join
+ \<squnion>
Network
- Join
+ \<squnion>
(rename sysOfClient
(plam x: lessThan Nclients. rename client_map Client))"
**)
@@ -631,20 +631,20 @@
subsection{*Components Lemmas [MUST BE AUTOMATED]*}
-lemma Network_component_System: "Network Join
+lemma Network_component_System: "Network \<squnion>
((rename sysOfClient
- (plam x: (lessThan Nclients). rename client_map Client)) Join
+ (plam x: (lessThan Nclients). rename client_map Client)) \<squnion>
rename sysOfAlloc Alloc)
= System"
by (simp add: System_def Join_ac)
lemma Client_component_System: "(rename sysOfClient
- (plam x: (lessThan Nclients). rename client_map Client)) Join
- (Network Join rename sysOfAlloc Alloc) = System"
+ (plam x: (lessThan Nclients). rename client_map Client)) \<squnion>
+ (Network \<squnion> rename sysOfAlloc Alloc) = System"
by (simp add: System_def Join_ac)
-lemma Alloc_component_System: "rename sysOfAlloc Alloc Join
- ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join
+lemma Alloc_component_System: "rename sysOfAlloc Alloc \<squnion>
+ ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) \<squnion>
Network) = System"
by (simp add: System_def Join_ac)
--- a/src/HOL/UNITY/Comp/AllocImpl.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy Thu Jul 23 22:13:42 2015 +0200
@@ -258,21 +258,21 @@
lemma Merge_Always_Out_eq_iOut:
"[| G \<in> preserves merge.Out; G \<in> preserves merge.iOut; M \<in> Allowed G |]
- ==> M Join G \<in> Always {s. length (merge.Out s) = length (merge.iOut s)}"
+ ==> M \<squnion> G \<in> Always {s. length (merge.Out s) = length (merge.iOut s)}"
apply (cut_tac Merge_spec)
apply (force dest: guaranteesD simp add: merge_spec_def merge_eqOut_def)
done
lemma Merge_Bounded:
"[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
- ==> M Join G \<in> Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
+ ==> M \<squnion> G \<in> Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
apply (cut_tac Merge_spec)
apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
done
lemma Merge_Bag_Follows_lemma:
"[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
- ==> M Join G \<in> Always
+ ==> M \<squnion> G \<in> Always
{s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (merge.Out s)
{k. k < length (iOut s) & iOut s ! k = i})) =
(bag_of o merge.Out) s}"
@@ -325,8 +325,8 @@
lemma Distr_Bag_Follows_lemma:
"[| G \<in> preserves distr.Out;
- D Join G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]
- ==> D Join G \<in> Always
+ D \<squnion> G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]
+ ==> D \<squnion> G \<in> Always
{s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (distr.In s)
{k. k < length (iIn s) & iIn s ! k = i})) =
bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}"
--- a/src/HOL/UNITY/Comp/Client.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Comp/Client.thy Thu Jul 23 22:13:42 2015 +0200
@@ -98,7 +98,7 @@
simultaneously. *}
lemma ask_bounded_lemma:
"Client ok G
- ==> Client Join G \<in>
+ ==> Client \<squnion> G \<in>
Always ({s. tok s \<le> NbT} Int
{s. \<forall>elt \<in> set (ask s). elt \<le> NbT})"
apply auto
@@ -125,13 +125,13 @@
by (simp add: Client_def, safety, auto)
lemma Join_Stable_rel_le_giv:
- "[| Client Join G \<in> Increasing giv; G \<in> preserves rel |]
- ==> Client Join G \<in> Stable {s. rel s \<le> giv s}"
+ "[| Client \<squnion> G \<in> Increasing giv; G \<in> preserves rel |]
+ ==> Client \<squnion> G \<in> Stable {s. rel s \<le> giv s}"
by (rule stable_rel_le_giv [THEN Increasing_preserves_Stable], auto)
lemma Join_Always_rel_le_giv:
- "[| Client Join G \<in> Increasing giv; G \<in> preserves rel |]
- ==> Client Join G \<in> Always {s. rel s \<le> giv s}"
+ "[| Client \<squnion> G \<in> Increasing giv; G \<in> preserves rel |]
+ ==> Client \<squnion> G \<in> Always {s. rel s \<le> giv s}"
by (force intro: AlwaysI Join_Stable_rel_le_giv)
lemma transient_lemma:
@@ -146,8 +146,8 @@
lemma induct_lemma:
- "[| Client Join G \<in> Increasing giv; Client ok G |]
- ==> Client Join G \<in> {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}
+ "[| Client \<squnion> G \<in> Increasing giv; Client ok G |]
+ ==> Client \<squnion> G \<in> {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}
LeadsTo {s. k < rel s & rel s \<le> giv s &
h \<le> giv s & h pfixGe ask s}"
apply (rule single_LeadsTo_I)
@@ -165,8 +165,8 @@
lemma rel_progress_lemma:
- "[| Client Join G \<in> Increasing giv; Client ok G |]
- ==> Client Join G \<in> {s. rel s < h & h \<le> giv s & h pfixGe ask s}
+ "[| Client \<squnion> G \<in> Increasing giv; Client ok G |]
+ ==> Client \<squnion> G \<in> {s. rel s < h & h \<le> giv s & h pfixGe ask s}
LeadsTo {s. h \<le> rel s}"
apply (rule_tac f = "%s. size h - size (rel s) " in LessThan_induct)
apply (auto simp add: vimage_def)
@@ -179,8 +179,8 @@
lemma client_progress_lemma:
- "[| Client Join G \<in> Increasing giv; Client ok G |]
- ==> Client Join G \<in> {s. h \<le> giv s & h pfixGe ask s}
+ "[| Client \<squnion> G \<in> Increasing giv; Client ok G |]
+ ==> Client \<squnion> G \<in> {s. h \<le> giv s & h pfixGe ask s}
LeadsTo {s. h \<le> rel s}"
apply (rule Join_Always_rel_le_giv [THEN Always_LeadsToI], simp_all)
apply (rule LeadsTo_Un [THEN LeadsTo_weaken_L])
--- a/src/HOL/UNITY/Comp/Handshake.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Comp/Handshake.thy Thu Jul 23 22:13:42 2015 +0200
@@ -47,7 +47,7 @@
invFG_def [THEN def_set_simp, simp]
-lemma invFG: "(F Join G) : Always invFG"
+lemma invFG: "(F \<squnion> G) : Always invFG"
apply (rule AlwaysI)
apply force
apply (rule constrains_imp_Constrains [THEN StableI])
@@ -56,25 +56,25 @@
apply (unfold G_def, safety)
done
-lemma lemma2_1: "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo
+lemma lemma2_1: "(F \<squnion> G) : ({s. NF s = k} - {s. BB s}) LeadsTo
({s. NF s = k} Int {s. BB s})"
apply (rule stable_Join_ensures1[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
apply (unfold F_def, safety)
apply (unfold G_def, ensures_tac "cmdG")
done
-lemma lemma2_2: "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo
+lemma lemma2_2: "(F \<squnion> G) : ({s. NF s = k} Int {s. BB s}) LeadsTo
{s. k < NF s}"
apply (rule stable_Join_ensures2[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
apply (unfold F_def, ensures_tac "cmdF")
apply (unfold G_def, safety)
done
-lemma progress: "(F Join G) : UNIV LeadsTo {s. m < NF s}"
+lemma progress: "(F \<squnion> G) : UNIV LeadsTo {s. m < NF s}"
apply (rule LeadsTo_weaken_R)
apply (rule_tac f = "NF" and l = "Suc m" and B = "{}"
in GreaterThan_bounded_induct)
-(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
+(*The inductive step is (F \<squnion> G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
apply (auto intro!: lemma2_1 lemma2_2
intro: LeadsTo_Trans LeadsTo_Diff simp add: vimage_def)
done
--- a/src/HOL/UNITY/Comp/Priority.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Comp/Priority.thy Thu Jul 23 22:13:42 2015 +0200
@@ -65,7 +65,7 @@
the vertex 'UNIV' is finite by assumption *)
definition system :: "state program"
- where "system = (JN i. Component i)"
+ where "system = (\<Squnion>i. Component i)"
declare highest_def [simp] lowest_def [simp]
--- a/src/HOL/UNITY/Lift_prog.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy Thu Jul 23 22:13:42 2015 +0200
@@ -178,7 +178,7 @@
lemma lift_SKIP [simp]: "lift i SKIP = SKIP"
by (simp add: lift_def)
-lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G"
+lemma lift_Join [simp]: "lift i (F \<squnion> G) = lift i F \<squnion> lift i G"
by (simp add: lift_def)
lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i \<in> I. lift j (F i))"
--- a/src/HOL/UNITY/PPROD.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/PPROD.thy Thu Jul 23 22:13:42 2015 +0200
@@ -31,7 +31,7 @@
lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
by (simp add: PLam_def JN_constant)
-lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
+lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) \<squnion> (PLam I F)"
by (unfold PLam_def, auto)
lemma PLam_component_iff: "((PLam I F) \<le> H) = (\<forall>i \<in> I. lift i (F i) \<le> H)"
@@ -184,7 +184,7 @@
lemma reachable_lift_Join_PLam [rule_format]:
"[| i \<notin> I; A \<in> reachable (F i) |]
==> \<forall>f. f \<in> reachable (PLam I F)
- --> f(i:=A) \<in> reachable (lift i (F i) Join PLam I F)"
+ --> f(i:=A) \<in> reachable (lift i (F i) \<squnion> PLam I F)"
apply (erule reachable.induct)
apply (ALLGOALS Clarify_tac)
apply (erule reachable.induct)
--- a/src/HOL/UNITY/Rename.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Rename.thy Thu Jul 23 22:13:42 2015 +0200
@@ -170,7 +170,7 @@
by (simp add: rename_def Extend.extend_SKIP)
lemma rename_Join [simp]:
- "bij h ==> rename h (F Join G) = rename h F Join rename h G"
+ "bij h ==> rename h (F \<squnion> G) = rename h F \<squnion> rename h G"
by (simp add: rename_def Extend.extend_Join)
lemma rename_JN [simp]:
--- a/src/HOL/UNITY/SubstAx.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/SubstAx.thy Thu Jul 23 22:13:42 2015 +0200
@@ -15,8 +15,7 @@
definition LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) where
"A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}"
-notation (xsymbols)
- LeadsTo (infixl " \<longmapsto>w " 60)
+notation LeadsTo (infixl "\<longmapsto>w" 60)
text{*Resembles the previous definition of LeadsTo*}
--- a/src/HOL/UNITY/Union.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Union.thy Thu Jul 23 22:13:42 2015 +0200
@@ -26,34 +26,25 @@
\<Inter>i \<in> I. AllowedActs (F i))"
definition
- Join :: "['a program, 'a program] => 'a program" (infixl "Join" 65)
- where "F Join G = mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
+ Join :: "['a program, 'a program] => 'a program" (infixl "\<squnion>" 65)
+ where "F \<squnion> G = mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
AllowedActs F \<inter> AllowedActs G)"
-definition
- SKIP :: "'a program"
- where "SKIP = mk_program (UNIV, {}, UNIV)"
+definition SKIP :: "'a program" ("\<bottom>")
+ where "\<bottom> = mk_program (UNIV, {}, UNIV)"
(*Characterizes safety properties. Used with specifying Allowed*)
definition
safety_prop :: "'a program set => bool"
where "safety_prop X <-> SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
-notation (xsymbols)
- SKIP ("\<bottom>") and
- Join (infixl "\<squnion>" 65)
-
syntax
- "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10)
- "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10)
-syntax (xsymbols)
"_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion>_./ _)" 10)
"_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion>_\<in>_./ _)" 10)
-
translations
- "JN x: A. B" == "CONST JOIN A (%x. B)"
- "JN x y. B" == "JN x. JN y. B"
- "JN x. B" == "CONST JOIN (CONST UNIV) (%x. B)"
+ "\<Squnion>x \<in> A. B" == "CONST JOIN A (\<lambda>x. B)"
+ "\<Squnion>x y. B" == "\<Squnion>x. \<Squnion>y. B"
+ "\<Squnion>x. B" == "CONST JOIN (CONST UNIV) (\<lambda>x. B)"
subsection{*SKIP*}
--- a/src/HOL/UNITY/WFair.thy Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/WFair.thy Thu Jul 23 22:13:42 2015 +0200
@@ -67,8 +67,7 @@
--{*predicate transformer: the largest set that leads to @{term B}*}
"wlt F B == Union {A. F \<in> A leadsTo B}"
-notation (xsymbols)
- leadsTo (infixl "\<longmapsto>" 60)
+notation leadsTo (infixl "\<longmapsto>" 60)
subsection{*transient*}