--- a/src/HOL/Complex/ex/Sqrt.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Complex/ex/Sqrt.thy Thu Feb 16 21:12:00 2006 +0100
@@ -17,17 +17,17 @@
theorem.
*}
-constdefs
- rationals :: "real set" ("\<rat>")
- "\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
+definition
+ rationals ("\<rat>")
+ "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
-theorem rationals_rep: "x \<in> \<rat> \<Longrightarrow>
- \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real m / real n \<and> gcd (m, n) = 1"
+theorem rationals_rep [elim?]:
+ assumes "x \<in> \<rat>"
+ obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd (m, n) = 1"
proof -
- assume "x \<in> \<rat>"
- then obtain m n :: nat where
+ from `x \<in> \<rat>` obtain m n :: nat where
n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n"
- by (unfold rationals_def) blast
+ unfolding rationals_def by blast
let ?gcd = "gcd (m, n)"
from n have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
let ?k = "m div ?gcd"
@@ -58,14 +58,9 @@
with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
with gcd show ?thesis by simp
qed
- ultimately show ?thesis by blast
+ ultimately show ?thesis ..
qed
-lemma [elim?]: "r \<in> \<rat> \<Longrightarrow>
- (\<And>m n. n \<noteq> 0 \<Longrightarrow> \<bar>r\<bar> = real m / real n \<Longrightarrow> gcd (m, n) = 1 \<Longrightarrow> C)
- \<Longrightarrow> C"
- using rationals_rep by blast
-
subsection {* Main theorem *}
@@ -74,10 +69,11 @@
irrational.
*}
-theorem sqrt_prime_irrational: "prime p \<Longrightarrow> sqrt (real p) \<notin> \<rat>"
+theorem sqrt_prime_irrational:
+ assumes "prime p"
+ shows "sqrt (real p) \<notin> \<rat>"
proof
- assume p_prime: "prime p"
- then have p: "1 < p" by (simp add: prime_def)
+ from `prime p` have p: "1 < p" by (simp add: prime_def)
assume "sqrt (real p) \<in> \<rat>"
then obtain m n where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
@@ -94,12 +90,12 @@
have "p dvd m \<and> p dvd n"
proof
from eq have "p dvd m\<twosuperior>" ..
- with p_prime show "p dvd m" by (rule prime_dvd_power_two)
+ with `prime p` show "p dvd m" by (rule prime_dvd_power_two)
then obtain k where "m = p * k" ..
with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
then have "p dvd n\<twosuperior>" ..
- with p_prime show "p dvd n" by (rule prime_dvd_power_two)
+ with `prime p` show "p dvd n" by (rule prime_dvd_power_two)
qed
then have "p dvd gcd (m, n)" ..
with gcd have "p dvd 1" by simp
@@ -119,10 +115,11 @@
structure, it is probably closer to proofs seen in mathematics.
*}
-theorem "prime p \<Longrightarrow> sqrt (real p) \<notin> \<rat>"
+theorem
+ assumes "prime p"
+ shows "sqrt (real p) \<notin> \<rat>"
proof
- assume p_prime: "prime p"
- then have p: "1 < p" by (simp add: prime_def)
+ from `prime p` have p: "1 < p" by (simp add: prime_def)
assume "sqrt (real p) \<in> \<rat>"
then obtain m n where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
@@ -134,12 +131,12 @@
also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
finally have eq: "m\<twosuperior> = p * n\<twosuperior>" ..
then have "p dvd m\<twosuperior>" ..
- with p_prime have dvd_m: "p dvd m" by (rule prime_dvd_power_two)
+ with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_two)
then obtain k where "m = p * k" ..
with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
then have "p dvd n\<twosuperior>" ..
- with p_prime have "p dvd n" by (rule prime_dvd_power_two)
+ with `prime p` have "p dvd n" by (rule prime_dvd_power_two)
with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest)
with gcd have "p dvd 1" by simp
then have "p \<le> 1" by (simp add: dvd_imp_le)
--- a/src/HOL/Lambda/Commutation.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/Commutation.thy Thu Feb 16 21:12:00 2006 +0100
@@ -10,25 +10,24 @@
subsection {* Basic definitions *}
-constdefs
+definition
square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
- "square R S T U ==
- \<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U))"
+ "square R S T U =
+ (\<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U)))"
commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
- "commute R S == square R S S R"
+ "commute R S = square R S S R"
diamond :: "('a \<times> 'a) set => bool"
- "diamond R == commute R R"
+ "diamond R = commute R R"
Church_Rosser :: "('a \<times> 'a) set => bool"
- "Church_Rosser R ==
- \<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*)"
+ "Church_Rosser R =
+ (\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*))"
-syntax
+abbreviation (output)
confluent :: "('a \<times> 'a) set => bool"
-translations
- "confluent R" == "diamond (R^*)"
+ "confluent R = diamond (R^*)"
subsection {* Basic lemmas *}
--- a/src/HOL/Lambda/Eta.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/Eta.thy Thu Feb 16 21:12:00 2006 +0100
@@ -21,14 +21,13 @@
consts
eta :: "(dB \<times> dB) set"
-syntax
- "_eta" :: "[dB, dB] => bool" (infixl "-e>" 50)
- "_eta_rtrancl" :: "[dB, dB] => bool" (infixl "-e>>" 50)
- "_eta_reflcl" :: "[dB, dB] => bool" (infixl "-e>=" 50)
-translations
- "s -e> t" == "(s, t) \<in> eta"
- "s -e>> t" == "(s, t) \<in> eta^*"
- "s -e>= t" == "(s, t) \<in> eta^="
+abbreviation (output)
+ eta_red :: "[dB, dB] => bool" (infixl "-e>" 50)
+ "(s -e> t) = ((s, t) \<in> eta)"
+ eta_reds :: "[dB, dB] => bool" (infixl "-e>>" 50)
+ "(s -e>> t) = ((s, t) \<in> eta^*)"
+ eta_red0 :: "[dB, dB] => bool" (infixl "-e>=" 50)
+ "(s -e>= t) = ((s, t) \<in> eta^=)"
inductive eta
intros
@@ -225,13 +224,12 @@
consts
par_eta :: "(dB \<times> dB) set"
-syntax
- "_par_eta" :: "[dB, dB] => bool" (infixl "=e>" 50)
-translations
- "s =e> t" == "(s, t) \<in> par_eta"
+abbreviation (output)
+ par_eta_red :: "[dB, dB] => bool" (infixl "=e>" 50)
+ "(s =e> t) = ((s, t) \<in> par_eta)"
syntax (xsymbols)
- "_par_eta" :: "[dB, dB] => bool" (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
+ par_eta_red :: "[dB, dB] => bool" (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
inductive par_eta
intros
--- a/src/HOL/Lambda/Lambda.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/Lambda.thy Thu Feb 16 21:12:00 2006 +0100
@@ -56,15 +56,15 @@
consts
beta :: "(dB \<times> dB) set"
-syntax
- "_beta" :: "[dB, dB] => bool" (infixl "->" 50)
- "_beta_rtrancl" :: "[dB, dB] => bool" (infixl "->>" 50)
+abbreviation (output)
+ beta_red :: "[dB, dB] => bool" (infixl "->" 50)
+ "(s -> t) = ((s, t) \<in> beta)"
+ beta_reds :: "[dB, dB] => bool" (infixl "->>" 50)
+ "(s ->> t) = ((s, t) \<in> beta^*)"
+
syntax (latex)
- "_beta" :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
- "_beta_rtrancl" :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
-translations
- "s \<rightarrow>\<^sub>\<beta> t" == "(s, t) \<in> beta"
- "s \<rightarrow>\<^sub>\<beta>\<^sup>* t" == "(s, t) \<in> beta^*"
+ beta_red :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+ beta_reds :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
inductive beta
intros
--- a/src/HOL/Lambda/ListApplication.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/ListApplication.thy Thu Feb 16 21:12:00 2006 +0100
@@ -8,10 +8,9 @@
theory ListApplication imports Lambda begin
-syntax
- "_list_application" :: "dB => dB list => dB" (infixl "\<degree>\<degree>" 150)
-translations
- "t \<degree>\<degree> ts" == "foldl (op \<degree>) t ts"
+abbreviation (output)
+ list_application :: "dB => dB list => dB" (infixl "\<degree>\<degree>" 150)
+ "t \<degree>\<degree> ts = foldl (op \<degree>) t ts"
lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
by (induct ts rule: rev_induct) auto
--- a/src/HOL/Lambda/ListBeta.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/ListBeta.thy Thu Feb 16 21:12:00 2006 +0100
@@ -12,10 +12,9 @@
Lifting beta-reduction to lists of terms, reducing exactly one element.
*}
-syntax
- "_list_beta" :: "dB => dB => bool" (infixl "=>" 50)
-translations
- "rs => ss" == "(rs, ss) : step1 beta"
+abbreviation (output)
+ list_beta :: "dB list => dB list => bool" (infixl "=>" 50)
+ "(rs => ss) = ((rs, ss) : step1 beta)"
lemma head_Var_reduction:
"Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
--- a/src/HOL/Lambda/ListOrder.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/ListOrder.thy Thu Feb 16 21:12:00 2006 +0100
@@ -13,9 +13,9 @@
element.
*}
-constdefs
+definition
step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
- "step1 r ==
+ "step1 r =
{(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys =
us @ z' # vs}"
--- a/src/HOL/Lambda/ParRed.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/ParRed.thy Thu Feb 16 21:12:00 2006 +0100
@@ -17,10 +17,9 @@
consts
par_beta :: "(dB \<times> dB) set"
-syntax
- par_beta :: "[dB, dB] => bool" (infixl "=>" 50)
-translations
- "s => t" == "(s, t) \<in> par_beta"
+abbreviation (output)
+ par_beta_red :: "[dB, dB] => bool" (infixl "=>" 50)
+ "(s => t) = ((s, t) \<in> par_beta)"
inductive par_beta
intros
--- a/src/HOL/Lambda/Type.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/Type.thy Thu Feb 16 21:12:00 2006 +0100
@@ -11,9 +11,9 @@
subsection {* Environments *}
-constdefs
+definition
shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_<_:_>" [90, 0, 0] 91)
- "e<i:a> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
+ "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
syntax (xsymbols)
shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
syntax (HTML output)
@@ -47,21 +47,23 @@
typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
-syntax
- "_funs" :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "=>>" 200)
- "_typing" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |- _ : _" [50, 50, 50] 50)
- "_typings" :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
+abbreviation (output)
+ funs :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "=>>" 200)
+ "Ts =>> T = foldr Fun Ts T"
+
+ typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |- _ : _" [50, 50, 50] 50)
+ "(env |- t : T) = ((env, t, T) \<in> typing)"
+
+ typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
("_ ||- _ : _" [50, 50, 50] 50)
+ "(env ||- ts : Ts) = typings env ts Ts"
+
syntax (xsymbols)
- "_typing" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50)
+ typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50)
syntax (latex)
- "_funs" :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "\<Rrightarrow>" 200)
- "_typings" :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
+ funs :: "type list \<Rightarrow> type \<Rightarrow> type" (infixr "\<Rrightarrow>" 200)
+ typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
("_ \<tturnstile> _ : _" [50, 50, 50] 50)
-translations
- "Ts \<Rrightarrow> T" \<rightleftharpoons> "foldr Fun Ts T"
- "env \<turnstile> t : T" \<rightleftharpoons> "(env, t, T) \<in> typing"
- "env \<tturnstile> ts : Ts" \<rightleftharpoons> "typings env ts Ts"
inductive typing
intros
--- a/src/HOL/Lambda/WeakNorm.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy Thu Feb 16 21:12:00 2006 +0100
@@ -16,9 +16,9 @@
subsection {* Terms in normal form *}
-constdefs
+definition
listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
- "listall P xs \<equiv> (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
+ "listall P xs == (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
declare listall_def [extraction_expand]
@@ -361,12 +361,11 @@
consts -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
rtyping :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
-syntax
- "_rtyping" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |-\<^sub>R _ : _" [50, 50, 50] 50)
+abbreviation (output)
+ 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)"
syntax (xsymbols)
- "_rtyping" :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
-translations
- "e \<turnstile>\<^sub>R t : T" \<rightleftharpoons> "(e, t, T) \<in> rtyping"
+ rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
inductive rtyping
intros
--- a/src/HOL/Library/Accessible_Part.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Library/Accessible_Part.thy Thu Feb 16 21:12:00 2006 +0100
@@ -23,10 +23,9 @@
intros
accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
-syntax
+abbreviation (output)
termi :: "('a \<times> 'a) set => 'a set"
-translations
- "termi r" == "acc (r\<inverse>)"
+ "termi r == acc (r\<inverse>)"
subsection {* Induction rules *}
--- a/src/HOL/Library/Coinductive_List.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Library/Coinductive_List.thy Thu Feb 16 21:12:00 2006 +0100
@@ -11,12 +11,9 @@
subsection {* List constructors over the datatype universe *}
-constdefs
- NIL :: "'a Datatype_Universe.item"
- "NIL \<equiv> Datatype_Universe.In0 (Datatype_Universe.Numb 0)"
- CONS :: "'a Datatype_Universe.item \<Rightarrow> 'a Datatype_Universe.item
- \<Rightarrow> 'a Datatype_Universe.item"
- "CONS M N \<equiv> Datatype_Universe.In1 (Datatype_Universe.Scons M N)"
+definition
+ "NIL = Datatype_Universe.In0 (Datatype_Universe.Numb 0)"
+ "CONS M N = Datatype_Universe.In1 (Datatype_Universe.Scons M N)"
lemma CONS_not_NIL [iff]: "CONS M N \<noteq> NIL"
and NIL_not_CONS [iff]: "NIL \<noteq> CONS M N"
@@ -30,9 +27,8 @@
-- {* A continuity result? *}
by (simp add: CONS_def In1_UN1 Scons_UN1_y)
-constdefs
- List_case where
- "List_case c h \<equiv> Datatype_Universe.Case (\<lambda>_. c) (Datatype_Universe.Split h)"
+definition
+ "List_case c h = Datatype_Universe.Case (\<lambda>_. c) (Datatype_Universe.Split h)"
lemma List_case_NIL [simp]: "List_case c h NIL = c"
and List_case_CONS [simp]: "List_case c h (CONS M N) = h M N"
@@ -63,10 +59,8 @@
None \<Rightarrow> NIL
| Some (z, w) \<Rightarrow> CONS z (LList_corec_aux k f w))"
-constdefs
- LList_corec :: "'a \<Rightarrow> ('a \<Rightarrow> ('b Datatype_Universe.item \<times> 'a) option) \<Rightarrow>
- 'b Datatype_Universe.item"
- "LList_corec a f \<equiv> \<Union>k. LList_corec_aux k f a"
+definition
+ "LList_corec a f = (\<Union>k. LList_corec_aux k f a)"
text {*
Note: the subsequent recursion equation for @{text LList_corec} may
@@ -150,12 +144,9 @@
finally show ?thesis .
qed
-constdefs
- LNil :: "'a llist"
- "LNil \<equiv> Abs_llist NIL"
-
- LCons :: "'a \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
- "LCons x xs \<equiv> Abs_llist (CONS (Datatype_Universe.Leaf x) (Rep_llist xs))"
+definition
+ "LNil = Abs_llist NIL"
+ "LCons x xs = Abs_llist (CONS (Datatype_Universe.Leaf x) (Rep_llist xs))"
lemma LCons_not_LNil [iff]: "LCons x xs \<noteq> LNil"
apply (simp add: LNil_def LCons_def)
@@ -202,11 +193,9 @@
qed
-constdefs
- llist_case :: "'b \<Rightarrow> ('a \<Rightarrow> 'a llist \<Rightarrow> 'b) \<Rightarrow> 'a llist \<Rightarrow> 'b"
- "llist_case c d l \<equiv>
+definition
+ "llist_case c d l =
List_case c (\<lambda>x y. d (inv Datatype_Universe.Leaf x) (Abs_llist y)) (Rep_llist l)"
-
translations
"case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "llist_case a (\<lambda>x l. b) p"
@@ -219,9 +208,8 @@
CONS_type Abs_llist_inverse Rep_llist Rep_llist_inverse inj_Leaf)
-constdefs
- llist_corec :: "'a \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'a) option) \<Rightarrow> 'b llist"
- "llist_corec a f \<equiv>
+definition
+ "llist_corec a f =
Abs_llist (LList_corec a
(\<lambda>z.
case f z of None \<Rightarrow> None
@@ -539,8 +527,7 @@
subsubsection {* @{text Lconst} *}
-constdefs
- Lconst where
+definition
"Lconst M \<equiv> lfp (\<lambda>N. CONS M N)"
lemma Lconst_fun_mono: "mono (CONS M)"
@@ -580,12 +567,9 @@
subsubsection {* @{text Lmap} and @{text lmap} *}
-constdefs
- Lmap where
- "Lmap f M \<equiv> LList_corec M (List_case None (\<lambda>x M'. Some (f x, M')))"
-
- lmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a llist \<Rightarrow> 'b llist"
- "lmap f l \<equiv> llist_corec l
+definition
+ "Lmap f M = LList_corec M (List_case None (\<lambda>x M'. Some (f x, M')))"
+ "lmap f l = llist_corec l
(\<lambda>z.
case z of LNil \<Rightarrow> None
| LCons y z \<Rightarrow> Some (f y, z))"
@@ -678,15 +662,12 @@
subsubsection {* @{text Lappend} *}
-constdefs
- Lappend where
- "Lappend M N \<equiv> LList_corec (M, N)
+definition
+ "Lappend M N = LList_corec (M, N)
(split (List_case
(List_case None (\<lambda>N1 N2. Some (N1, (NIL, N2))))
(\<lambda>M1 M2 N. Some (M1, (M2, N)))))"
-
- lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
- "lappend l n \<equiv> llist_corec (l, n)
+ "lappend l n = llist_corec (l, n)
(split (llist_case
(llist_case None (\<lambda>n1 n2. Some (n1, (LNil, n2))))
(\<lambda>l1 l2 n. Some (l1, (l2, n)))))"
@@ -760,9 +741,9 @@
text {* @{text llist_fun_equalityI} cannot be used here! *}
-constdefs
+definition
iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist"
- "iterates f a \<equiv> llist_corec a (\<lambda>x. Some (x, f x))"
+ "iterates f a = llist_corec a (\<lambda>x. Some (x, f x))"
lemma iterates: "iterates f x = LCons x (iterates f (f x))"
apply (unfold iterates_def)
--- a/src/HOL/Library/List_Prefix.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Library/List_Prefix.thy Thu Feb 16 21:12:00 2006 +0100
@@ -155,9 +155,9 @@
subsection {* Parallel lists *}
-constdefs
+definition
parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50)
- "xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs"
+ "(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)"
lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
unfolding parallel_def by blast
@@ -215,9 +215,9 @@
subsection {* Postfix order on lists *}
-constdefs
+definition
postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50)
- "xs >>= ys == \<exists>zs. xs = zs @ ys"
+ "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)"
lemma postfix_refl [simp, intro!]: "xs >>= xs"
by (auto simp add: postfix_def)
--- a/src/HOL/Library/Multiset.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Feb 16 21:12:00 2006 +0100
@@ -20,29 +20,31 @@
Abs_multiset_inverse Rep_multiset_inverse Rep_multiset
and [simp] = Rep_multiset_inject [symmetric]
-constdefs
+definition
Mempty :: "'a multiset" ("{#}")
- "{#} == Abs_multiset (\<lambda>a. 0)"
+ "{#} = Abs_multiset (\<lambda>a. 0)"
single :: "'a => 'a multiset" ("{#_#}")
- "{#a#} == Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
+ "{#a#} = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
count :: "'a multiset => 'a => nat"
- "count == Rep_multiset"
+ "count = Rep_multiset"
MCollect :: "'a multiset => ('a => bool) => 'a multiset"
- "MCollect M P == Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
+ "MCollect M P = Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
+
+abbreviation (output)
+ Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50)
+ "(a :# M) = (0 < count M a)"
syntax
- "_Melem" :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50)
"_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ : _./ _#})")
translations
- "a :# M" == "0 < count M a"
"{#x:M. P#}" == "MCollect M (\<lambda>x. P)"
-constdefs
+definition
set_of :: "'a multiset => 'a set"
- "set_of M == {x. x :# M}"
+ "set_of M = {x. x :# M}"
instance multiset :: (type) "{plus, minus, zero}" ..
@@ -52,9 +54,9 @@
Zero_multiset_def [simp]: "0 == {#}"
size_def: "size M == setsum (count M) (set_of M)"
-constdefs
- multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70)
- "multiset_inter A B \<equiv> A - (A - B)"
+definition
+ multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70)
+ "multiset_inter A B = A - (A - B)"
text {*
@@ -377,14 +379,14 @@
subsubsection {* Well-foundedness *}
-constdefs
+definition
mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
- "mult1 r ==
+ "mult1 r =
{(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
(\<forall>b. b :# K --> (b, a) \<in> r)}"
mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
- "mult r == (mult1 r)\<^sup>+"
+ "mult r = (mult1 r)\<^sup>+"
lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
by (simp add: mult1_def)
@@ -793,16 +795,9 @@
subsection {* Pointwise ordering induced by count *}
-consts
- mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool"
-
-syntax
- "_mset_le" :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" ("_ \<le># _" [50,51] 50)
-translations
- "x \<le># y" == "mset_le x y"
-
-defs
- mset_le_def: "xs \<le># ys == (\<forall>a. count xs a \<le> count ys a)"
+definition
+ mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool" ("_ \<le># _" [50,51] 50)
+ "(xs \<le># ys) = (\<forall>a. count xs a \<le> count ys a)"
lemma mset_le_refl[simp]: "xs \<le># xs"
unfolding mset_le_def by auto
--- a/src/HOL/Library/Primes.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Library/Primes.thy Thu Feb 16 21:12:00 2006 +0100
@@ -10,12 +10,12 @@
imports Main
begin
-constdefs
+definition
coprime :: "nat => nat => bool"
- "coprime m n == gcd (m, n) = 1"
+ "coprime m n = (gcd (m, n) = 1)"
prime :: "nat \<Rightarrow> bool"
- "prime p == 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)"
+ "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
lemma two_is_prime: "prime 2"
--- a/src/HOL/Library/Quotient.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Library/Quotient.thy Thu Feb 16 21:12:00 2006 +0100
@@ -74,9 +74,9 @@
representation of elements of a quotient type.
*}
-constdefs
+definition
"class" :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>")
- "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
+ "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
proof (cases A)
@@ -133,9 +133,9 @@
subsection {* Picking representing elements *}
-constdefs
+definition
pick :: "'a::equiv quot => 'a"
- "pick A == SOME a. A = \<lfloor>a\<rfloor>"
+ "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
proof (unfold pick_def)
--- a/src/HOL/Unix/Unix.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Unix/Unix.thy Thu Feb 16 21:12:00 2006 +0100
@@ -160,15 +160,13 @@
\cite{Nipkow-et-al:2000:HOL}.
*}
-constdefs
- attributes :: "file \<Rightarrow> att"
- "attributes file \<equiv>
+definition
+ "attributes file =
(case file of
Val (att, text) \<Rightarrow> att
| Env att dir \<Rightarrow> att)"
- attributes_update :: "att \<Rightarrow> file \<Rightarrow> file"
- "attributes_update att file \<equiv>
+ "attributes_update att file =
(case file of
Val (att', text) \<Rightarrow> Val (att, text)
| Env att' dir \<Rightarrow> Env att dir)"
@@ -201,9 +199,8 @@
has user id 0).
*}
-constdefs
- init :: "uid set \<Rightarrow> file"
- "init users \<equiv>
+definition
+ "init users =
Env \<lparr>owner = 0, others = {Readable}\<rparr>
(\<lambda>u. if u \<in> users then Some (Env \<lparr>owner = u, others = {Readable}\<rparr> empty)
else None)"
@@ -223,8 +220,7 @@
access a file unconditionally (in our simplified model).
*}
-constdefs
- access :: "file \<Rightarrow> path \<Rightarrow> uid \<Rightarrow> perms \<Rightarrow> file option"
+definition
"access root path uid perms \<equiv>
(case lookup root path of
None \<Rightarrow> None
@@ -648,8 +644,7 @@
transition.
*}
-constdefs
- can_exec :: "file \<Rightarrow> operation list \<Rightarrow> bool"
+definition
"can_exec root xs \<equiv> \<exists>root'. root =xs\<Rightarrow> root'"
lemma can_exec_nil: "can_exec root []"
@@ -843,13 +838,12 @@
notes facts = user\<^isub>1_known user\<^isub>1_not_root users_neq
perms\<^isub>1_writable perms\<^isub>2_not_writable
- fixes bogus :: "operation list"
- and bogus_path :: path
- defines "bogus \<equiv>
+definition (in situation)
+ "bogus =
[Mkdir user\<^isub>1 perms\<^isub>1 [user\<^isub>1, name\<^isub>1],
Mkdir user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2],
Creat user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2, name\<^isub>3]]"
- and "bogus_path \<equiv> [user\<^isub>1, name\<^isub>1, name\<^isub>2]"
+ "bogus_path = [user\<^isub>1, name\<^isub>1, name\<^isub>2]"
text {*
The @{term bogus} operations are the ones that lead into the uncouth
@@ -867,9 +861,8 @@
neither owned and nor writable by @{term user\<^isub>1}.
*}
-locale invariant = situation +
- fixes invariant :: "file \<Rightarrow> path \<Rightarrow> bool"
- defines "invariant root path \<equiv>
+definition (in situation)
+ "invariant root path \<equiv>
(\<exists>att dir.
access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>
user\<^isub>1 \<noteq> owner att \<and>
@@ -907,7 +900,7 @@
we just have to inspect rather special cases.
*}
-lemma (in invariant) cannot_rmdir:
+lemma (in situation) cannot_rmdir:
assumes inv: "invariant root bogus_path"
and rmdir: "root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root'"
shows False
@@ -923,7 +916,7 @@
ultimately show False by (simp add: bogus_path_def)
qed
-lemma (in invariant)
+lemma (in situation)
assumes init: "init users =bogus\<Rightarrow> root"
notes eval = facts access_def init_def
shows init_invariant: "invariant root bogus_path"
@@ -946,7 +939,7 @@
required here.
*}
-lemma (in invariant) preserve_invariant:
+lemma (in situation) preserve_invariant:
assumes tr: "root \<midarrow>x\<rightarrow> root'"
and inv: "invariant root path"
and uid: "uid_of x = user\<^isub>1"
@@ -1090,8 +1083,7 @@
overall procedure (see \secref{sec:unix-inv-procedure}).
*}
-corollary result:
- includes invariant
+corollary (in situation)
assumes bogus: "init users =bogus\<Rightarrow> root"
shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user\<^isub>1) \<and>
can_exec root (xs @ [Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1]]))"
@@ -1100,11 +1092,4 @@
and bogus show ?thesis by (rule general_procedure)
qed
-text {*
- So this is our final result:
-
- @{thm [display, show_question_marks = false] result [OF
- invariant.intro, OF situation.intro]}
-*}
-
end