--- a/src/HOL/Library/Binomial.thy Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/Library/Binomial.thy Tue Jun 08 16:37:22 2010 +0200
@@ -235,7 +235,7 @@
have eq: "insert 0 {1 .. n} = {0..n}" by auto
have th1: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) =
(\<Prod>n\<in>{0\<Colon>nat..n - 1}. a + 1 + of_nat n)"
- apply (rule setprod_reindex_cong[where f = "Suc"])
+ apply (rule setprod_reindex_cong [where f = Suc])
using n0 by (auto simp add: expand_fun_eq field_simps)
have ?thesis apply (simp add: pochhammer_def)
unfolding setprod_insert[OF th0, unfolded eq]
--- a/src/HOL/Library/Countable.thy Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/Library/Countable.thy Tue Jun 08 16:37:22 2010 +0200
@@ -70,7 +70,7 @@
text {* Sums *}
-instance "+":: (countable, countable) countable
+instance "+" :: (countable, countable) countable
by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
| Inr b \<Rightarrow> to_nat (True, to_nat b))"])
(simp split: sum.split_asm)
--- a/src/HOL/Library/Diagonalize.thy Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/Library/Diagonalize.thy Tue Jun 08 16:37:22 2010 +0200
@@ -81,7 +81,7 @@
done
-subsection {* Diagonalization: an injective embedding of two @{typ "nat"}s to one @{typ "nat"} *}
+subsection {* Diagonalization: an injective embedding of two @{typ nat}s to one @{typ nat} *}
definition diagonalize :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
"diagonalize m n = sum (m + n) + m"
--- a/src/HOL/Library/Efficient_Nat.thy Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Tue Jun 08 16:37:22 2010 +0200
@@ -11,7 +11,7 @@
text {*
When generating code for functions on natural numbers, the
canonical representation using @{term "0::nat"} and
- @{term "Suc"} is unsuitable for computations involving large
+ @{term Suc} is unsuitable for computations involving large
numbers. The efficiency of the generated code can be improved
drastically by implementing natural numbers by target-language
integers. To do this, just include this theory.
@@ -362,7 +362,7 @@
Since natural numbers are implemented
using integers in ML, the coercion function @{const "of_nat"} of type
@{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
- For the @{const "nat"} function for converting an integer to a natural
+ For the @{const nat} function for converting an integer to a natural
number, we give a specific implementation using an ML function that
returns its input value, provided that it is non-negative, and otherwise
returns @{text "0"}.
--- a/src/HOL/Library/Formal_Power_Series.thy Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Tue Jun 08 16:37:22 2010 +0200
@@ -2031,7 +2031,7 @@
done
also have "\<dots> = setsum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (setsum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}"
unfolding fps_deriv_nth
- apply (rule setsum_reindex_cong[where f="Suc"])
+ apply (rule setsum_reindex_cong [where f = Suc])
by (auto simp add: mult_assoc)
finally have th0: "(fps_deriv (a oo b))$n = setsum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (setsum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" .
--- a/src/HOL/Nominal/Examples/Support.thy Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/Nominal/Examples/Support.thy Tue Jun 08 16:37:22 2010 +0200
@@ -31,7 +31,7 @@
text {* An atom is either even or odd. *}
lemma even_or_odd:
- fixes n::"nat"
+ fixes n :: nat
shows "\<exists>i. (n = 2*i) \<or> (n=2*i+1)"
by (induct n) (presburger)+
--- a/src/HOL/SetInterval.thy Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/SetInterval.thy Tue Jun 08 16:37:22 2010 +0200
@@ -770,7 +770,7 @@
qed
lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}"
-apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - Suc 0"])
+apply (rule card_bij_eq [of Suc _ _ "\<lambda>x. x - Suc 0"])
apply simp
apply fastsimp
apply auto
--- a/src/HOL/Sum_Type.thy Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/Sum_Type.thy Tue Jun 08 16:37:22 2010 +0200
@@ -17,21 +17,17 @@
definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
"Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
-global
-
-typedef (Sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
+typedef (sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
by auto
-local
-
-lemma Inl_RepI: "Inl_Rep a \<in> Sum"
- by (auto simp add: Sum_def)
+lemma Inl_RepI: "Inl_Rep a \<in> sum"
+ by (auto simp add: sum_def)
-lemma Inr_RepI: "Inr_Rep b \<in> Sum"
- by (auto simp add: Sum_def)
+lemma Inr_RepI: "Inr_Rep b \<in> sum"
+ by (auto simp add: sum_def)
-lemma inj_on_Abs_Sum: "A \<subseteq> Sum \<Longrightarrow> inj_on Abs_Sum A"
- by (rule inj_on_inverseI, rule Abs_Sum_inverse) auto
+lemma inj_on_Abs_sum: "A \<subseteq> sum \<Longrightarrow> inj_on Abs_sum A"
+ by (rule inj_on_inverseI, rule Abs_sum_inverse) auto
lemma Inl_Rep_inject: "inj_on Inl_Rep A"
proof (rule inj_onI)
@@ -49,28 +45,28 @@
by (auto simp add: Inl_Rep_def Inr_Rep_def expand_fun_eq)
definition Inl :: "'a \<Rightarrow> 'a + 'b" where
- "Inl = Abs_Sum \<circ> Inl_Rep"
+ "Inl = Abs_sum \<circ> Inl_Rep"
definition Inr :: "'b \<Rightarrow> 'a + 'b" where
- "Inr = Abs_Sum \<circ> Inr_Rep"
+ "Inr = Abs_sum \<circ> Inr_Rep"
lemma inj_Inl [simp]: "inj_on Inl A"
-by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_Sum Inl_RepI)
+by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_sum Inl_RepI)
lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y"
using inj_Inl by (rule injD)
lemma inj_Inr [simp]: "inj_on Inr A"
-by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_Sum Inr_RepI)
+by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_sum Inr_RepI)
lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y"
using inj_Inr by (rule injD)
lemma Inl_not_Inr: "Inl a \<noteq> Inr b"
proof -
- from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> Sum" by auto
- with inj_on_Abs_Sum have "inj_on Abs_Sum {Inl_Rep a, Inr_Rep b}" .
- with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_Sum (Inl_Rep a) \<noteq> Abs_Sum (Inr_Rep b)" by auto
+ from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum" by auto
+ with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" .
+ with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_sum (Inl_Rep a) \<noteq> Abs_sum (Inr_Rep b)" by auto
then show ?thesis by (simp add: Inl_def Inr_def)
qed
@@ -81,10 +77,10 @@
assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P"
and "\<And>y::'b. s = Inr y \<Longrightarrow> P"
shows P
-proof (rule Abs_Sum_cases [of s])
+proof (rule Abs_sum_cases [of s])
fix f
- assume "s = Abs_Sum f" and "f \<in> Sum"
- with assms show P by (auto simp add: Sum_def Inl_def Inr_def)
+ assume "s = Abs_sum f" and "f \<in> sum"
+ with assms show P by (auto simp add: sum_def Inl_def Inr_def)
qed
rep_datatype (sum) Inl Inr
--- a/src/HOL/Tools/Qelim/cooper.ML Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Tue Jun 08 16:37:22 2010 +0200
@@ -37,7 +37,7 @@
@{term "max :: int => _"}, @{term "max :: nat => _"},
@{term "min :: int => _"}, @{term "min :: nat => _"},
@{term "uminus :: int => _"}, (*@ {term "uminus :: nat => _"},*)
- @{term "Not"}, @{term "Suc"},
+ @{term "Not"}, @{term Suc},
@{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
@{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
@{term "nat"}, @{term "int"},
@@ -726,7 +726,7 @@
fun isnum t = case t of
Const(@{const_name Groups.zero},_) => true
| Const(@{const_name Groups.one},_) => true
- | @{term "Suc"}$s => isnum s
+ | @{term Suc}$s => isnum s
| @{term "nat"}$s => isnum s
| @{term "int"}$s => isnum s
| Const(@{const_name Groups.uminus},_)$s => isnum s
--- a/src/HOL/Tools/groebner.ML Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/Tools/groebner.ML Tue Jun 08 16:37:22 2010 +0200
@@ -698,7 +698,7 @@
val holify_polynomial =
let fun holify_varpow (v,n) =
- if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp "nat"} n) (* FIXME *)
+ if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp nat} n) (* FIXME *)
fun holify_monomial vars (c,m) =
let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m))
in end_itlist ring_mk_mul (mk_const c :: xps)
--- a/src/HOL/Tools/lin_arith.ML Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Tue Jun 08 16:37:22 2010 +0200
@@ -461,7 +461,7 @@
(* ?P ((?n::nat) mod (number_of ?k)) =
((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) -->
(ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
- | (Const ("Divides.div_class.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
+ | (Const ("Divides.div_class.mod", Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
let
val rev_terms = rev terms
val zero = Const (@{const_name Groups.zero}, split_type)
@@ -493,7 +493,7 @@
(* ?P ((?n::nat) div (number_of ?k)) =
((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) -->
(ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
- | (Const ("Divides.div_class.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
+ | (Const ("Divides.div_class.div", Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
let
val rev_terms = rev terms
val zero = Const (@{const_name Groups.zero}, split_type)
--- a/src/HOL/Tools/meson.ML Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/Tools/meson.ML Tue Jun 08 16:37:22 2010 +0200
@@ -395,7 +395,7 @@
since this code expects to be called on a clause form.*)
val is_conn = member (op =)
["Trueprop", "op &", "op |", "op -->", "Not",
- "All", "Ex", "Ball", "Bex"];
+ "All", "Ex", @{const_name Ball}, @{const_name Bex}];
(*True if the term contains a function--not a logical connective--where the type
of any argument contains bool.*)
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Tue Jun 08 16:37:22 2010 +0200
@@ -97,7 +97,7 @@
(*Split up a sum into the list of its constituent terms, on the way removing any
Sucs and counting them.*)
-fun dest_Suc_sum (Const ("Suc", _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
+fun dest_Suc_sum (Const (@{const_name Suc}, _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
| dest_Suc_sum (t, (k,ts)) =
let val (t1,t2) = dest_plus t
in dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts))) end
--- a/src/HOL/Tools/refute.ML Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/Tools/refute.ML Tue Jun 08 16:37:22 2010 +0200
@@ -657,14 +657,14 @@
(* other optimizations *)
| Const (@{const_name Finite_Set.card}, _) => t
| Const (@{const_name Finite_Set.finite}, _) => t
- | Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
- | Const (@{const_name Groups.plus}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
- | Const (@{const_name Groups.minus}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
- | Const (@{const_name Groups.times}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
+ | Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, Type ("bool", [])])])) => t
+ | Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) => t
+ | Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) => t
+ | Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) => t
| Const (@{const_name List.append}, _) => t
(* UNSOUND
| Const (@{const_name lfp}, _) => t
@@ -834,17 +834,17 @@
| Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
| Const (@{const_name Finite_Set.finite}, T) =>
collect_type_axioms T axs
- | Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
+ | Const (@{const_name Orderings.less}, T as Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, Type ("bool", [])])])) =>
collect_type_axioms T axs
- | Const (@{const_name Groups.plus}, T as Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
+ | Const (@{const_name Groups.plus}, T as Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) =>
collect_type_axioms T axs
- | Const (@{const_name Groups.minus}, T as Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
+ | Const (@{const_name Groups.minus}, T as Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) =>
collect_type_axioms T axs
- | Const (@{const_name Groups.times}, T as Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
+ | Const (@{const_name Groups.times}, T as Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) =>
collect_type_axioms T axs
| Const (@{const_name List.append}, T) => collect_type_axioms T axs
(* UNSOUND
@@ -2654,7 +2654,7 @@
case t of
Const (@{const_name Finite_Set.card},
Type ("fun", [Type ("fun", [T, Type ("bool", [])]),
- Type ("nat", [])])) =>
+ @{typ nat}])) =>
let
(* interpretation -> int *)
fun number_of_elements (Node xs) =
@@ -2670,7 +2670,7 @@
| number_of_elements (Leaf _) =
raise REFUTE ("Finite_Set_card_interpreter",
"interpretation for set type is a leaf")
- val size_of_nat = size_of_type thy model (Type ("nat", []))
+ val size_of_nat = size_of_type thy model (@{typ nat})
(* takes an interpretation for a set and returns an interpretation *)
(* for a 'nat' denoting the set's cardinality *)
(* interpretation -> interpretation *)
@@ -2730,10 +2730,10 @@
fun Nat_less_interpreter thy model args t =
case t of
- Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
+ Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, Type ("bool", [])])])) =>
let
- val size_of_nat = size_of_type thy model (Type ("nat", []))
+ val size_of_nat = size_of_type thy model (@{typ nat})
(* the 'n'-th nat is not less than the first 'n' nats, while it *)
(* is less than the remaining 'size_of_nat - n' nats *)
(* int -> interpretation *)
@@ -2753,10 +2753,10 @@
fun Nat_plus_interpreter thy model args t =
case t of
- Const (@{const_name Groups.plus}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
+ Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) =>
let
- val size_of_nat = size_of_type thy model (Type ("nat", []))
+ val size_of_nat = size_of_type thy model (@{typ nat})
(* int -> int -> interpretation *)
fun plus m n =
let
@@ -2784,10 +2784,10 @@
fun Nat_minus_interpreter thy model args t =
case t of
- Const (@{const_name Groups.minus}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
+ Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) =>
let
- val size_of_nat = size_of_type thy model (Type ("nat", []))
+ val size_of_nat = size_of_type thy model (@{typ nat})
(* int -> int -> interpretation *)
fun minus m n =
let
@@ -2812,10 +2812,10 @@
fun Nat_times_interpreter thy model args t =
case t of
- Const (@{const_name Groups.times}, Type ("fun", [Type ("nat", []),
- Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
+ Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
+ Type ("fun", [@{typ nat}, @{typ nat}])])) =>
let
- val size_of_nat = size_of_type thy model (Type ("nat", []))
+ val size_of_nat = size_of_type thy model (@{typ nat})
(* nat -> nat -> interpretation *)
fun mult m n =
let
--- a/src/HOL/ex/Dedekind_Real.thy Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Tue Jun 08 16:37:22 2010 +0200
@@ -2006,7 +2006,7 @@
qed
text {*
- There must be other proofs, e.g. @{text "Suc"} of the largest
+ There must be other proofs, e.g. @{text Suc} of the largest
integer in the cut representing @{text "x"}.
*}
--- a/src/HOL/ex/Refute_Examples.thy Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Tue Jun 08 16:37:22 2010 +0200
@@ -774,7 +774,7 @@
oops
lemma "P Suc"
- refute -- {* @{term "Suc"} is a partial function (regardless of the size
+ refute -- {* @{term Suc} is a partial function (regardless of the size
of the model), hence @{term "P Suc"} is undefined, hence no
model will be found *}
oops