tuned quotes, antiquotations and whitespace
authorhaftmann
Tue, 08 Jun 2010 16:37:22 +0200
changeset 37388 793618618f78
parent 37387 3581483cca6c
child 37389 09467cdfa198
tuned quotes, antiquotations and whitespace
src/HOL/Library/Binomial.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Diagonalize.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Nominal/Examples/Support.thy
src/HOL/SetInterval.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/nat_numeral_simprocs.ML
src/HOL/Tools/refute.ML
src/HOL/ex/Dedekind_Real.thy
src/HOL/ex/Refute_Examples.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: "(\<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