# HG changeset patch # User haftmann # Date 1276007842 -7200 # Node ID 793618618f7800674f8f6c4900ad7fb5c36c6ca9 # Parent 3581483cca6c96fcc7b343d1800bda2f5f203879 tuned quotes, antiquotations and whitespace diff -r 3581483cca6c -r 793618618f78 src/HOL/Library/Binomial.thy --- 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: "(\n\{1\nat..n}. a + of_nat n) = (\n\{0\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] diff -r 3581483cca6c -r 793618618f78 src/HOL/Library/Countable.thy --- 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 "(\x. case x of Inl a \ to_nat (False, to_nat a) | Inr b \ to_nat (True, to_nat b))"]) (simp split: sum.split_asm) diff -r 3581483cca6c -r 793618618f78 src/HOL/Library/Diagonalize.thy --- 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 \ nat \ nat" where "diagonalize m n = sum (m + n) + m" diff -r 3581483cca6c -r 793618618f78 src/HOL/Library/Efficient_Nat.thy --- 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 \ 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"}. diff -r 3581483cca6c -r 793618618f78 src/HOL/Library/Formal_Power_Series.thy --- 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 "\ = setsum (\i. of_nat (i + 1) * a$(i+1) * (setsum (\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 (\i. of_nat (i + 1) * a$(i+1) * (setsum (\j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" . diff -r 3581483cca6c -r 793618618f78 src/HOL/Nominal/Examples/Support.thy --- 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 "\i. (n = 2*i) \ (n=2*i+1)" by (induct n) (presburger)+ diff -r 3581483cca6c -r 793618618f78 src/HOL/SetInterval.thy --- 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 \ M \ card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}" -apply (rule card_bij_eq [of "Suc" _ _ "\x. x - Suc 0"]) +apply (rule card_bij_eq [of Suc _ _ "\x. x - Suc 0"]) apply simp apply fastsimp apply auto diff -r 3581483cca6c -r 793618618f78 src/HOL/Sum_Type.thy --- 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 \ 'a \ 'b \ bool \ bool" where "Inr_Rep b x y p \ y = b \ \ p" -global - -typedef (Sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\a. f = Inl_Rep (a::'a)) \ (\b. f = Inr_Rep (b::'b))}" +typedef (sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\a. f = Inl_Rep (a::'a)) \ (\b. f = Inr_Rep (b::'b))}" by auto -local - -lemma Inl_RepI: "Inl_Rep a \ Sum" - by (auto simp add: Sum_def) +lemma Inl_RepI: "Inl_Rep a \ sum" + by (auto simp add: sum_def) -lemma Inr_RepI: "Inr_Rep b \ Sum" - by (auto simp add: Sum_def) +lemma Inr_RepI: "Inr_Rep b \ sum" + by (auto simp add: sum_def) -lemma inj_on_Abs_Sum: "A \ Sum \ inj_on Abs_Sum A" - by (rule inj_on_inverseI, rule Abs_Sum_inverse) auto +lemma inj_on_Abs_sum: "A \ sum \ 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 \ 'a + 'b" where - "Inl = Abs_Sum \ Inl_Rep" + "Inl = Abs_sum \ Inl_Rep" definition Inr :: "'b \ 'a + 'b" where - "Inr = Abs_Sum \ Inr_Rep" + "Inr = Abs_sum \ 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 \ 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 \ x = y" using inj_Inr by (rule injD) lemma Inl_not_Inr: "Inl a \ Inr b" proof - - from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \ 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) \ Abs_Sum (Inr_Rep b)" by auto + from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \ 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) \ Abs_sum (Inr_Rep b)" by auto then show ?thesis by (simp add: Inl_def Inr_def) qed @@ -81,10 +77,10 @@ assumes "\x::'a. s = Inl x \ P" and "\y::'b. s = Inr y \ 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 \ Sum" - with assms show P by (auto simp add: Sum_def Inl_def Inr_def) + assume "s = Abs_sum f" and "f \ sum" + with assms show P by (auto simp add: sum_def Inl_def Inr_def) qed rep_datatype (sum) Inl Inr diff -r 3581483cca6c -r 793618618f78 src/HOL/Tools/Qelim/cooper.ML --- 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 diff -r 3581483cca6c -r 793618618f78 src/HOL/Tools/groebner.ML --- 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) diff -r 3581483cca6c -r 793618618f78 src/HOL/Tools/lin_arith.ML --- 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) diff -r 3581483cca6c -r 793618618f78 src/HOL/Tools/meson.ML --- 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.*) diff -r 3581483cca6c -r 793618618f78 src/HOL/Tools/nat_numeral_simprocs.ML --- 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 diff -r 3581483cca6c -r 793618618f78 src/HOL/Tools/refute.ML --- 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 diff -r 3581483cca6c -r 793618618f78 src/HOL/ex/Dedekind_Real.thy --- 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"}. *} diff -r 3581483cca6c -r 793618618f78 src/HOL/ex/Refute_Examples.thy --- 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