--- a/src/FOL/IFOL.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/FOL/IFOL.thy Tue May 16 21:33:01 2006 +0200
@@ -49,13 +49,11 @@
not_equal :: "['a, 'a] => o" (infixl "~=" 50)
"x ~= y == ~ (x = y)"
-abbreviation (xsymbols)
- not_equal1 (infixl "\<noteq>" 50)
- "x \<noteq> y == ~ (x = y)"
+const_syntax (xsymbols)
+ not_equal (infixl "\<noteq>" 50)
-abbreviation (HTML output)
- not_equal2 (infixl "\<noteq>" 50)
- "not_equal2 == not_equal"
+const_syntax (HTML output)
+ not_equal (infixl "\<noteq>" 50)
syntax (xsymbols)
Not :: "o => o" ("\<not> _" [40] 40)
--- a/src/HOL/Fun.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Fun.thy Tue May 16 21:33:01 2006 +0200
@@ -48,17 +48,15 @@
comp :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "o" 55)
"f o g == %x. f(g(x))"
+const_syntax (xsymbols)
+ comp (infixl "\<circ>" 55)
+
+const_syntax (HTML output)
+ comp (infixl "\<circ>" 55)
+
text{*compatibility*}
lemmas o_def = comp_def
-abbreviation (xsymbols)
- comp1 (infixl "\<circ>" 55)
- "comp1 == comp"
-
-abbreviation (HTML output)
- comp2 (infixl "\<circ>" 55)
- "comp2 == comp"
-
constdefs
inj_on :: "['a => 'b, 'a set] => bool" (*injective*)
"inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
--- a/src/HOL/HOL.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/HOL.thy Tue May 16 21:33:01 2006 +0200
@@ -52,14 +52,45 @@
consts
If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)
+
subsubsection {* Additional concrete syntax *}
+const_syntax (output)
+ "op =" (infix "=" 50)
+
+abbreviation
+ not_equal :: "['a, 'a] => bool" (infixl "~=" 50)
+ "x ~= y == ~ (x = y)"
+
+const_syntax (output)
+ not_equal (infix "~=" 50)
+
+const_syntax (xsymbols)
+ Not ("\<not> _" [40] 40)
+ "op &" (infixr "\<and>" 35)
+ "op |" (infixr "\<or>" 30)
+ "op -->" (infixr "\<longrightarrow>" 25)
+ not_equal (infix "\<noteq>" 50)
+
+const_syntax (HTML output)
+ Not ("\<not> _" [40] 40)
+ "op &" (infixr "\<and>" 35)
+ "op |" (infixr "\<or>" 30)
+ not_equal (infix "\<noteq>" 50)
+
+abbreviation (iff)
+ iff :: "[bool, bool] => bool" (infixr "<->" 25)
+ "A <-> B == A = B"
+
+const_syntax (xsymbols)
+ iff (infixr "\<longleftrightarrow>" 25)
+
+
nonterminals
letbinds letbind
case_syn cases_syn
syntax
- "_not_equal" :: "['a, 'a] => bool" (infixl "~=" 50)
"_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10)
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10)
@@ -73,7 +104,6 @@
"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _")
translations
- "x ~= y" == "~ (x = y)"
"THE x. P" == "The (%x. P)"
"_Let (_binds b bs) e" == "_Let b (_Let bs e)"
"let x = a in e" == "Let a (%x. e)"
@@ -85,31 +115,14 @@
in Syntax.const "_The" $ x $ t end)]
*}
-syntax (output)
- "=" :: "['a, 'a] => bool" (infix 50)
- "_not_equal" :: "['a, 'a] => bool" (infix "~=" 50)
-
syntax (xsymbols)
- Not :: "bool => bool" ("\<not> _" [40] 40)
- "op &" :: "[bool, bool] => bool" (infixr "\<and>" 35)
- "op |" :: "[bool, bool] => bool" (infixr "\<or>" 30)
- "op -->" :: "[bool, bool] => bool" (infixr "\<longrightarrow>" 25)
- "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50)
"ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10)
"EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10)
"EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10)
"_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10)
(*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \<orelse> _")*)
-syntax (xsymbols output)
- "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50)
-
syntax (HTML output)
- "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50)
- Not :: "bool => bool" ("\<not> _" [40] 40)
- "op &" :: "[bool, bool] => bool" (infixr "\<and>" 35)
- "op |" :: "[bool, bool] => bool" (infixr "\<or>" 30)
- "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50)
"ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10)
"EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10)
"EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10)
@@ -119,14 +132,6 @@
"EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10)
"EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10)
-abbreviation (iff)
- iff :: "[bool, bool] => bool" (infixr "<->" 25)
- "A <-> B == A = B"
-
-abbreviation (xsymbols)
- iff1 (infixr "\<longleftrightarrow>" 25)
- "A \<longleftrightarrow> B == A <-> B"
-
subsubsection {* Axioms and basic definitions *}
@@ -181,6 +186,7 @@
The
arbitrary
+
subsubsection {* Generic algebraic operations *}
axclass zero < type
--- a/src/HOL/Infinite_Set.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Infinite_Set.thy Tue May 16 21:33:01 2006 +0200
@@ -346,29 +346,24 @@
so we introduce corresponding binders and their proof rules.
*}
-consts
+definition
Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "INF " 10)
+ INF_def: "Inf_many P \<equiv> infinite {x. P x}"
Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "MOST " 10)
-
-defs
- INF_def: "Inf_many P \<equiv> infinite {x. P x}"
MOST_def: "Alm_all P \<equiv> \<not>(INF x. \<not> P x)"
-abbreviation (xsymbols)
- Inf_many1 (binder "\<exists>\<^sub>\<infinity>" 10)
- "Inf_many1 == Inf_many"
- Alm_all1 (binder "\<forall>\<^sub>\<infinity>" 10)
- "Alm_all1 == Alm_all"
+const_syntax (xsymbols)
+ Inf_many (binder "\<exists>\<^sub>\<infinity>" 10)
+ Alm_all (binder "\<forall>\<^sub>\<infinity>" 10)
-abbreviation (HTML output)
- Inf_many2 (binder "\<exists>\<^sub>\<infinity>" 10)
- "Inf_many2 == Inf_many"
- Alm_all2 (binder "\<forall>\<^sub>\<infinity>" 10)
- "Alm_all2 == Alm_all"
+const_syntax (HTML output)
+ Inf_many (binder "\<exists>\<^sub>\<infinity>" 10)
+ Alm_all (binder "\<forall>\<^sub>\<infinity>" 10)
lemma INF_EX:
"(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
-proof (unfold INF_def, rule ccontr)
+ unfolding INF_def
+proof (rule ccontr)
assume inf: "infinite {x. P x}"
and notP: "\<not>(\<exists>x. P x)"
from notP have "{x. P x} = {}" by simp
@@ -418,7 +413,7 @@
These simplify the reasoning about deterministic automata.
*}
-constdefs
+definition
atmost_one :: "'a set \<Rightarrow> bool"
"atmost_one S \<equiv> \<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y"
--- a/src/HOL/Integ/IntDef.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy Tue May 16 21:33:01 2006 +0200
@@ -567,9 +567,8 @@
Nats :: "'a::comm_semiring_1_cancel set"
"Nats == range of_nat"
-abbreviation (xsymbols)
- Nats1 ("\<nat>")
- "\<nat> == Nats"
+const_syntax (xsymbols)
+ Nats ("\<nat>")
lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
by (simp add: Nats_def)
@@ -701,9 +700,8 @@
Ints :: "'a::comm_ring_1 set"
"Ints == range of_int"
-abbreviation (xsymbols)
- Ints1 ("\<int>")
- "\<int> == Ints"
+const_syntax (xsymbols)
+ Ints ("\<int>")
lemma Ints_0 [simp]: "0 \<in> Ints"
apply (simp add: Ints_def)
--- a/src/HOL/Integ/NatBin.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy Tue May 16 21:33:01 2006 +0200
@@ -24,13 +24,11 @@
square :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999)
"x\<twosuperior> == x^2"
-abbreviation (latex output)
- square1 ("(_\<twosuperior>)" [1000] 999)
- "square1 x == x^2"
+const_syntax (latex output)
+ square ("(_\<twosuperior>)" [1000] 999)
-abbreviation (HTML output)
- square2 ("(_\<twosuperior>)" [1000] 999)
- "square2 x == x^2"
+const_syntax (HTML output)
+ square ("(_\<twosuperior>)" [1000] 999)
subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
--- a/src/HOL/Lambda/Eta.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Lambda/Eta.thy Tue May 16 21:33:01 2006 +0200
@@ -228,9 +228,8 @@
par_eta_red :: "[dB, dB] => bool" (infixl "=e>" 50)
"s =e> t == (s, t) \<in> par_eta"
-abbreviation (xsymbols)
- par_eta_red1 :: "[dB, dB] => bool" (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
- "op \<Rightarrow>\<^sub>\<eta> == op =e>"
+const_syntax (xsymbols)
+ par_eta_red (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
inductive par_eta
intros
@@ -300,7 +299,8 @@
assumes u: "u => u'"
shows "t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]"
proof (induct k fixing: t t')
- case 0 with u show ?case by simp
+ case 0
+ with u show ?case by simp
next
case (Suc k)
hence "Abs (lift t (Suc 0)) \<degree> Var 0 => lift t' (Suc 0)[Var 0/0]"
@@ -387,7 +387,7 @@
subsection {* Eta-postponement theorem *}
text {*
-Based on a proof by Masako Takahashi \cite{Takahashi-IandC}.
+ Based on a proof by Masako Takahashi \cite{Takahashi-IandC}.
*}
theorem par_eta_beta: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u"
@@ -428,7 +428,7 @@
and qq: "q \<Rightarrow>\<^sub>\<eta> q'" and rr: "r \<Rightarrow>\<^sub>\<eta> r'"
by (blast dest: par_eta_elim_app par_eta_elim_abs)
from beta have "size q' < size t" and "size r' < size t" by simp_all
- with beta(2,3) qq rr obtain t' t'' where "q => t'" and
+ with beta(2-3) qq rr obtain t' t'' where "q => t'" and
"t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''"
by (blast dest: less(1))
with s beta show ?thesis
--- a/src/HOL/Lambda/Lambda.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Lambda/Lambda.thy Tue May 16 21:33:01 2006 +0200
@@ -62,11 +62,9 @@
beta_reds :: "[dB, dB] => bool" (infixl "->>" 50)
"s ->> t == (s, t) \<in> beta^*"
-abbreviation (latex)
- beta_red1 :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
- "op \<rightarrow>\<^sub>\<beta> == op ->"
- beta_reds1 :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
- "op \<rightarrow>\<^sub>\<beta>\<^sup>* == op ->>"
+const_syntax (latex)
+ beta_red (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+ beta_reds (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
inductive beta
intros
@@ -100,9 +98,7 @@
lemma rtrancl_beta_App [intro]:
"[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
- apply (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR
- intro: rtrancl_trans)
- done
+ by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtrancl_trans)
subsection {* Substitution-lemmas *}
--- a/src/HOL/Lambda/Type.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Lambda/Type.thy Tue May 16 21:33:01 2006 +0200
@@ -15,13 +15,11 @@
shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_<_:_>" [90, 0, 0] 91)
"e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
-abbreviation (xsymbols)
- shift1 ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
- "e\<langle>i:a\<rangle> == e<i:a>"
+const_syntax (xsymbols)
+ shift ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
-abbreviation (HTML output)
- shift2 ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
- "shift2 == shift"
+const_syntax (HTML output)
+ shift ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
by (simp add: shift_def)
@@ -62,16 +60,12 @@
("_ ||- _ : _" [50, 50, 50] 50)
"env ||- ts : Ts == typings env ts Ts"
-abbreviation (xsymbols)
- typing_rel1 :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50)
- "env \<turnstile> t : T == env |- t : T"
+const_syntax (xsymbols)
+ typing_rel ("_ \<turnstile> _ : _" [50, 50, 50] 50)
-abbreviation (latex)
- funs2 :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "\<Rrightarrow>" 200)
- "op \<Rrightarrow> == op =>>"
- typings_rel2 :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
- ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
- "env \<tturnstile> ts : Ts == env ||- ts : Ts"
+const_syntax (latex)
+ funs (infixr "\<Rrightarrow>" 200)
+ typings_rel ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
inductive typing
intros
--- a/src/HOL/Lambda/WeakNorm.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Tue May 16 21:33:01 2006 +0200
@@ -365,9 +365,8 @@
rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |-\<^sub>R _ : _" [50, 50, 50] 50)
"e |-\<^sub>R t : T == (e, t, T) \<in> rtyping"
-abbreviation (xsymbols)
- rtyping_rel1 :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
- "e \<turnstile>\<^sub>R t : T == e |-\<^sub>R t : T"
+const_syntax (xsymbols)
+ rtyping_rel ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
inductive rtyping
intros
--- a/src/HOL/Library/FuncSet.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Library/FuncSet.thy Tue May 16 21:33:01 2006 +0200
@@ -23,9 +23,8 @@
funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "->" 60)
"A -> B == Pi A (%_. B)"
-abbreviation (xsymbols)
- funcset1 (infixr "\<rightarrow>" 60)
- "funcset1 == funcset"
+const_syntax (xsymbols)
+ funcset (infixr "\<rightarrow>" 60)
syntax
"@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10)
--- a/src/HOL/Library/SetsAndFunctions.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Library/SetsAndFunctions.thy Tue May 16 21:33:01 2006 +0200
@@ -58,7 +58,7 @@
elt_set_times :: "'a::times => 'a set => 'a set" (infixl "*o" 80)
"a *o B == {c. EX b:B. c = a * b}"
-abbreviation (inout)
+abbreviation (input)
elt_set_eq :: "'a => 'a set => bool" (infix "=o" 50)
"x =o A == x : A"
--- a/src/HOL/Map.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Map.thy Tue May 16 21:33:01 2006 +0200
@@ -15,14 +15,20 @@
types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
translations (type) "a ~=> b " <= (type) "a => b option"
+syntax (xsymbols)
+ "~=>" :: "[type, type] => type" (infixr "\<rightharpoonup>" 0)
+
abbreviation
empty :: "'a ~=> 'b"
"empty == %x. None"
-constdefs
+definition
map_comp :: "('b ~=> 'c) => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
"f o_m g == (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
+const_syntax (xsymbols)
+ map_comp (infixl "\<circ>\<^sub>m" 55)
+
consts
map_add :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" (infixl "|`" 110)
@@ -32,6 +38,9 @@
map_upds:: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
map_le :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
+const_syntax (latex output)
+ restrict_map ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
+
nonterminals
maplets maplet
@@ -44,17 +53,9 @@
"_Map" :: "maplets => 'a ~=> 'b" ("(1[_])")
syntax (xsymbols)
- "~=>" :: "[type, type] => type" (infixr "\<rightharpoonup>" 0)
-
- map_comp :: "('b ~=> 'c) => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "\<circ>\<^sub>m" 55)
-
"_maplet" :: "['a, 'a] => maplet" ("_ /\<mapsto>/ _")
"_maplets" :: "['a, 'a] => maplet" ("_ /[\<mapsto>]/ _")
-syntax (latex output)
- restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
- --"requires amssymb!"
-
translations
"_MapUpd m (_Maplets xy ms)" == "_MapUpd (_MapUpd m xy) ms"
"_MapUpd m (_maplet x y)" == "m(x:=Some y)"
--- a/src/HOL/Orderings.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Orderings.thy Tue May 16 21:33:01 2006 +0200
@@ -17,21 +17,23 @@
axclass
ord < type
-syntax
- "less" :: "['a::ord, 'a] => bool" ("op <")
- "less_eq" :: "['a::ord, 'a] => bool" ("op <=")
-
consts
- "less" :: "['a::ord, 'a] => bool" ("(_/ < _)" [50, 51] 50)
- "less_eq" :: "['a::ord, 'a] => bool" ("(_/ <= _)" [50, 51] 50)
+ less :: "['a::ord, 'a] => bool"
+ less_eq :: "['a::ord, 'a] => bool"
-syntax (xsymbols)
- "less_eq" :: "['a::ord, 'a] => bool" ("op \<le>")
- "less_eq" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50)
+const_syntax
+ less ("op <")
+ less ("(_/ < _)" [50, 51] 50)
+ less_eq ("op <=")
+ less_eq ("(_/ <= _)" [50, 51] 50)
-syntax (HTML output)
- "less_eq" :: "['a::ord, 'a] => bool" ("op \<le>")
- "less_eq" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50)
+const_syntax (xsymbols)
+ less_eq ("op \<le>")
+ less_eq ("(_/ \<le> _)" [50, 51] 50)
+
+const_syntax (HTML output)
+ less_eq ("op \<le>")
+ less_eq ("(_/ \<le> _)" [50, 51] 50)
abbreviation (input)
greater (infixl ">" 50)
@@ -39,13 +41,8 @@
greater_eq (infixl ">=" 50)
"x >= y == y <= x"
-abbreviation (xsymbols)
- greater_eq1 (infixl "\<ge>" 50)
- "x \<ge> y == x >= y"
-
-abbreviation (HTML output)
- greater_eq2 (infixl "\<ge>" 50)
- "greater_eq2 == greater_eq"
+const_syntax (xsymbols)
+ greater_eq (infixl "\<ge>" 50)
subsection {* Monotonicity *}
--- a/src/HOL/Product_Type.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Product_Type.thy Tue May 16 21:33:01 2006 +0200
@@ -113,13 +113,11 @@
Times :: "['a set, 'b set] => ('a * 'b) set" (infixr "<*>" 80)
"A <*> B == Sigma A (%_. B)"
-abbreviation (xsymbols)
- Times1 (infixr "\<times>" 80)
- "Times1 == Times"
+const_syntax (xsymbols)
+ Times (infixr "\<times>" 80)
-abbreviation (HTML output)
- Times2 (infixr "\<times>" 80)
- "Times2 == Times"
+const_syntax (HTML output)
+ Times (infixr "\<times>" 80)
subsubsection {* Concrete syntax *}
--- a/src/HOL/Relation.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Relation.thy Tue May 16 21:33:01 2006 +0200
@@ -12,13 +12,14 @@
subsection {* Definitions *}
-constdefs
+definition
converse :: "('a * 'b) set => ('b * 'a) set" ("(_^-1)" [1000] 999)
"r^-1 == {(y, x). (x, y) : r}"
-syntax (xsymbols)
- converse :: "('a * 'b) set => ('b * 'a) set" ("(_\<inverse>)" [1000] 999)
-constdefs
+const_syntax (xsymbols)
+ converse ("(_\<inverse>)" [1000] 999)
+
+definition
rel_comp :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set" (infixr "O" 60)
"r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
--- a/src/HOL/Set.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Set.thy Tue May 16 21:33:01 2006 +0200
@@ -34,11 +34,11 @@
Ball :: "'a set => ('a => bool) => bool" -- "bounded universal quantifiers"
Bex :: "'a set => ('a => bool) => bool" -- "bounded existential quantifiers"
image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90)
-
-syntax
- "op :" :: "'a => 'a set => bool" ("op :")
-consts
- "op :" :: "'a => 'a set => bool" ("(_/ : _)" [50, 51] 50) -- "membership"
+ "op :" :: "'a => 'a set => bool" -- "membership"
+
+const_syntax
+ "op :" ("op :")
+ "op :" ("(_/ : _)" [50, 51] 50)
local
@@ -51,10 +51,62 @@
range :: "('a => 'b) => 'b set" -- "of function"
"range f == f ` UNIV"
+abbreviation
+ "not_mem x A == ~ (x : A)" -- "non-membership"
+
+const_syntax
+ not_mem ("op ~:")
+ not_mem ("(_/ ~: _)" [50, 51] 50)
+
+const_syntax (xsymbols)
+ "op Int" (infixl "\<inter>" 70)
+ "op Un" (infixl "\<union>" 65)
+ "op :" ("op \<in>")
+ "op :" ("(_/ \<in> _)" [50, 51] 50)
+ not_mem ("op \<notin>")
+ not_mem ("(_/ \<notin> _)" [50, 51] 50)
+ Union ("\<Union>_" [90] 90)
+ Inter ("\<Inter>_" [90] 90)
+
+const_syntax (HTML output)
+ "op Int" (infixl "\<inter>" 70)
+ "op Un" (infixl "\<union>" 65)
+ "op :" ("op \<in>")
+ "op :" ("(_/ \<in> _)" [50, 51] 50)
+ not_mem ("op \<notin>")
+ not_mem ("(_/ \<notin> _)" [50, 51] 50)
+
+abbreviation
+ subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+ "subset == less"
+ subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+ "subset_eq == less_eq"
+
+const_syntax (output)
+ subset ("op <")
+ subset ("(_/ < _)" [50, 51] 50)
+ subset_eq ("op <=")
+ subset_eq ("(_/ <= _)" [50, 51] 50)
+
+const_syntax (xsymbols)
+ subset ("op \<subset>")
+ subset ("(_/ \<subset> _)" [50, 51] 50)
+ subset_eq ("op \<subseteq>")
+ subset_eq ("(_/ \<subseteq> _)" [50, 51] 50)
+
+const_syntax (HTML output)
+ subset ("op \<subset>")
+ subset ("(_/ \<subset> _)" [50, 51] 50)
+ subset_eq ("op \<subseteq>")
+ subset_eq ("(_/ \<subseteq> _)" [50, 51] 50)
+
+abbreviation (input)
+ supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "\<supset>" 50)
+ "supset == greater"
+ supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "\<supseteq>" 50)
+ "supset_eq == greater_eq"
+
syntax
- "op ~:" :: "'a => 'a set => bool" ("op ~:") -- "non-membership"
- "op ~:" :: "'a => 'a set => bool" ("(_/ ~: _)" [50, 51] 50)
-
"@Finset" :: "args => 'a set" ("{(_)}")
"@Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})")
"@SetCompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})")
@@ -63,18 +115,15 @@
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" 10)
"@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" 10)
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" 10)
-
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10)
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3EX _:_./ _)" [0, 0, 10] 10)
"_Bleast" :: "id => 'a set => bool => 'a" ("(3LEAST _:_./ _)" [0, 0, 10] 10)
-
syntax (HOL)
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3! _:_./ _)" [0, 0, 10] 10)
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3? _:_./ _)" [0, 0, 10] 10)
translations
- "x ~: y" == "~ (x : y)"
"{x, xs}" == "insert x {xs}"
"{x}" == "insert x {}"
"{x. P}" == "Collect (%x. P)"
@@ -91,41 +140,12 @@
"EX x:A. P" == "Bex A (%x. P)"
"LEAST x:A. P" => "LEAST x. x:A & P"
-
-syntax (output)
- "_setle" :: "'a set => 'a set => bool" ("op <=")
- "_setle" :: "'a set => 'a set => bool" ("(_/ <= _)" [50, 51] 50)
- "_setless" :: "'a set => 'a set => bool" ("op <")
- "_setless" :: "'a set => 'a set => bool" ("(_/ < _)" [50, 51] 50)
-
syntax (xsymbols)
- "_setle" :: "'a set => 'a set => bool" ("op \<subseteq>")
- "_setle" :: "'a set => 'a set => bool" ("(_/ \<subseteq> _)" [50, 51] 50)
- "_setless" :: "'a set => 'a set => bool" ("op \<subset>")
- "_setless" :: "'a set => 'a set => bool" ("(_/ \<subset> _)" [50, 51] 50)
- "op Int" :: "'a set => 'a set => 'a set" (infixl "\<inter>" 70)
- "op Un" :: "'a set => 'a set => 'a set" (infixl "\<union>" 65)
- "op :" :: "'a => 'a set => bool" ("op \<in>")
- "op :" :: "'a => 'a set => bool" ("(_/ \<in> _)" [50, 51] 50)
- "op ~:" :: "'a => 'a set => bool" ("op \<notin>")
- "op ~:" :: "'a => 'a set => bool" ("(_/ \<notin> _)" [50, 51] 50)
- Union :: "'a set set => 'a set" ("\<Union>_" [90] 90)
- Inter :: "'a set set => 'a set" ("\<Inter>_" [90] 90)
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
"_Bleast" :: "id => 'a set => bool => 'a" ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
syntax (HTML output)
- "_setle" :: "'a set => 'a set => bool" ("op \<subseteq>")
- "_setle" :: "'a set => 'a set => bool" ("(_/ \<subseteq> _)" [50, 51] 50)
- "_setless" :: "'a set => 'a set => bool" ("op \<subset>")
- "_setless" :: "'a set => 'a set => bool" ("(_/ \<subset> _)" [50, 51] 50)
- "op Int" :: "'a set => 'a set => 'a set" (infixl "\<inter>" 70)
- "op Un" :: "'a set => 'a set => 'a set" (infixl "\<union>" 65)
- "op :" :: "'a => 'a set => bool" ("op \<in>")
- "op :" :: "'a => 'a set => bool" ("(_/ \<in> _)" [50, 51] 50)
- "op ~:" :: "'a => 'a set => bool" ("op \<notin>")
- "op ~:" :: "'a => 'a set => bool" ("(_/ \<notin> _)" [50, 51] 50)
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
@@ -135,47 +155,25 @@
"@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" 10)
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" 10)
"@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" 10)
-(*
-syntax (xsymbols)
- "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" 10)
- "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" 10)
- "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
- "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
-*)
+
syntax (latex output)
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" 10)
"@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" 10)
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
"@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
-text{* Note the difference between ordinary xsymbol syntax of indexed
-unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
-and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
-former does not make the index expression a subscript of the
-union/intersection symbol because this leads to problems with nested
-subscripts in Proof General. *}
-
-
-translations
- "op \<subseteq>" => "op <= :: _ set => _ set => bool"
- "op \<subset>" => "op < :: _ set => _ set => bool"
-
-typed_print_translation {*
- let
- fun le_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
- list_comb (Syntax.const "_setle", ts)
- | le_tr' _ _ _ = raise Match;
-
- fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
- list_comb (Syntax.const "_setless", ts)
- | less_tr' _ _ _ = raise Match;
- in [("less_eq", le_tr'), ("less", less_tr')] end
-*}
+text{*
+ Note the difference between ordinary xsymbol syntax of indexed
+ unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
+ and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
+ former does not make the index expression a subscript of the
+ union/intersection symbol because this leads to problems with nested
+ subscripts in Proof General. *}
subsubsection "Bounded quantifiers"
-syntax
+syntax (output)
"_setlessAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10)
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10)
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10)
@@ -187,7 +185,7 @@
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
"_setleEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
-syntax (HOL)
+syntax (HOL output)
"_setlessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10)
"_setlessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10)
"_setleAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10)
--- a/src/HOL/Transitive_Closure.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Transitive_Closure.thy Tue May 16 21:33:01 2006 +0200
@@ -36,20 +36,19 @@
r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+"
-syntax
- "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^=)" [1000] 999)
-translations
- "r^=" == "r \<union> Id"
+abbreviation
+ reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^=)" [1000] 999)
+ "r^= == r \<union> Id"
-syntax (xsymbols)
- rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>*)" [1000] 999)
- trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>+)" [1000] 999)
- "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>=)" [1000] 999)
+const_syntax (xsymbols)
+ rtrancl ("(_\<^sup>*)" [1000] 999)
+ trancl ("(_\<^sup>+)" [1000] 999)
+ reflcl ("(_\<^sup>=)" [1000] 999)
-syntax (HTML output)
- rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>*)" [1000] 999)
- trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>+)" [1000] 999)
- "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_\<^sup>=)" [1000] 999)
+const_syntax (HTML output)
+ rtrancl ("(_\<^sup>*)" [1000] 999)
+ trancl ("(_\<^sup>+)" [1000] 999)
+ reflcl ("(_\<^sup>=)" [1000] 999)
subsection {* Reflexive-transitive closure *}