--- a/NEWS Thu Nov 29 07:55:46 2007 +0100
+++ b/NEWS Thu Nov 29 17:08:26 2007 +0100
@@ -4,6 +4,14 @@
New in this Isabelle version
----------------------------
+*** Pure ***
+
+* Command "instance" now takes list of definitions in the same
+manner as the "definition" command. Most notably, object equality is now
+possible. Type inference is more canonical than it used to be.
+INCOMPATIBILITY: in some cases explicit type annotations are required.
+
+
*** HOL ***
* Constant "card" now with authentic syntax.
--- a/src/HOL/Complex/Complex.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Complex/Complex.thy Thu Nov 29 17:08:26 2007 +0100
@@ -45,7 +45,7 @@
complex_minus_def:
"- x \<equiv> Complex (- Re x) (- Im x)"
complex_diff_def:
- "x - y \<equiv> x + - y" ..
+ "x - (y\<Colon>complex) \<equiv> x + - y" ..
lemma Complex_eq_0 [simp]: "(Complex a b = 0) = (a = 0 \<and> b = 0)"
by (simp add: complex_zero_def)
@@ -116,7 +116,7 @@
"inverse x \<equiv>
Complex (Re x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>)) (- Im x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>))"
complex_divide_def:
- "x / y \<equiv> x * inverse y" ..
+ "x / (y\<Colon>complex) \<equiv> x * inverse y" ..
lemma Complex_eq_1 [simp]: "(Complex a b = 1) = (a = 1 \<and> b = 0)"
by (simp add: complex_one_def)
@@ -195,7 +195,7 @@
instance complex :: number
complex_number_of_def:
- "number_of w \<equiv> of_int w" ..
+ "number_of w \<equiv> of_int w \<Colon> complex" ..
instance complex :: number_ring
by (intro_classes, simp only: complex_number_of_def)
@@ -213,10 +213,10 @@
by (cases z rule: int_diff_cases) simp
lemma complex_Re_number_of [simp]: "Re (number_of v) = number_of v"
-unfolding number_ring_class.axioms by (rule complex_Re_of_int)
+unfolding number_of_eq by (rule complex_Re_of_int)
lemma complex_Im_number_of [simp]: "Im (number_of v) = 0"
-unfolding number_ring_class.axioms by (rule complex_Im_of_int)
+unfolding number_of_eq by (rule complex_Im_of_int)
lemma Complex_eq_number_of [simp]:
"(Complex a b = number_of w) = (a = number_of w \<and> b = 0)"
--- a/src/HOL/Finite_Set.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Finite_Set.thy Thu Nov 29 17:08:26 2007 +0100
@@ -2689,7 +2689,7 @@
lemmas [code func] = univ_bool
instance * :: (finite, finite) finite
- "itself \<equiv> TYPE('a\<Colon>finite)"
+ "itself \<equiv> TYPE('a \<times> 'b)"
proof
show "finite (UNIV :: ('a \<times> 'b) set)"
proof (rule finite_Prod_UNIV)
@@ -2703,7 +2703,7 @@
unfolding UNIV_Times_UNIV ..
instance "+" :: (finite, finite) finite
- "itself \<equiv> TYPE('a\<Colon>finite + 'b\<Colon>finite)"
+ "itself \<equiv> TYPE('a + 'b)"
proof
have a: "finite (UNIV :: 'a set)" by (rule finite)
have b: "finite (UNIV :: 'b set)" by (rule finite)
@@ -2717,7 +2717,7 @@
unfolding UNIV_Plus_UNIV ..
instance set :: (finite) finite
- "itself \<equiv> TYPE('a\<Colon>finite set)"
+ "itself \<equiv> TYPE('a set)"
proof
have "finite (UNIV :: 'a set)" by (rule finite)
hence "finite (Pow (UNIV :: 'a set))"
@@ -2732,7 +2732,7 @@
by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
instance "fun" :: (finite, finite) finite
- "itself \<equiv> TYPE('a\<Colon>finite \<Rightarrow> 'b\<Colon>finite)"
+ "itself \<equiv> TYPE('a \<Rightarrow> 'b)"
proof
show "finite (UNIV :: ('a => 'b) set)"
proof (rule finite_imageD)
--- a/src/HOL/IntDef.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/IntDef.thy Thu Nov 29 17:08:26 2007 +0100
@@ -36,7 +36,7 @@
instance int :: minus
minus_int_def:
"- z \<equiv> Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
- diff_int_def: "z - w \<equiv> z + (-w)" ..
+ diff_int_def: "z - w \<equiv> z + (-w \<Colon> int)" ..
instance int :: times
mult_int_def: "z * w \<equiv> Abs_Integ
@@ -46,7 +46,7 @@
instance int :: ord
le_int_def:
"z \<le> w \<equiv> \<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w"
- less_int_def: "z < w \<equiv> z \<le> w \<and> z \<noteq> w" ..
+ less_int_def: "(z\<Colon>int) < w \<equiv> z \<le> w \<and> z \<noteq> w" ..
lemmas [code func del] = Zero_int_def One_int_def add_int_def
minus_int_def mult_int_def le_int_def less_int_def
@@ -218,8 +218,8 @@
zsgn_def: "sgn(i\<Colon>int) \<equiv> (if i=0 then 0 else if 0<i then 1 else - 1)" ..
instance int :: distrib_lattice
- "inf \<equiv> min"
- "sup \<equiv> max"
+ "inf \<Colon> int \<Rightarrow> int \<Rightarrow> int \<equiv> min"
+ "sup \<Colon> int \<Rightarrow> int \<Rightarrow> int \<equiv> max"
by intro_classes
(auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
--- a/src/HOL/Library/Char_ord.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Library/Char_ord.thy Thu Nov 29 17:08:26 2007 +0100
@@ -39,8 +39,8 @@
qed
instance nibble :: distrib_lattice
- "inf \<equiv> min"
- "sup \<equiv> max"
+ "(inf \<Colon> nibble \<Rightarrow> _) = min"
+ "(sup \<Colon> nibble \<Rightarrow> _) = max"
by default (auto simp add:
inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
@@ -54,8 +54,8 @@
lemmas [code func del] = char_less_eq_def char_less_def
instance char :: distrib_lattice
- "inf \<equiv> min"
- "sup \<equiv> max"
+ "(inf \<Colon> char \<Rightarrow> _) = min"
+ "(sup \<Colon> char \<Rightarrow> _) = max"
by default (auto simp add:
inf_char_def sup_char_def min_max.sup_inf_distrib1)
--- a/src/HOL/Library/Code_Index.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Library/Code_Index.thy Thu Nov 29 17:08:26 2007 +0100
@@ -143,7 +143,7 @@
by simp
instance index :: abs
- "\<bar>k\<bar> \<equiv> if k < 0 then -k else k" ..
+ "\<bar>k\<Colon>index\<bar> \<equiv> if k < 0 then -k else k" ..
lemma index_of_int [code func]:
"index_of_int k = (if k = 0 then 0
--- a/src/HOL/Library/Eval.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Library/Eval.thy Thu Nov 29 17:08:26 2007 +0100
@@ -35,16 +35,16 @@
*}
instance "prop" :: typ_of
- "typ_of T \<equiv> STR ''prop'' {\<struct>} []" ..
+ "typ_of (T\<Colon>prop itself) \<equiv> STR ''prop'' {\<struct>} []" ..
instance itself :: (typ_of) typ_of
- "typ_of T \<equiv> STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
+ "typ_of (T\<Colon>'a itself itself) \<equiv> STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
instance set :: (typ_of) typ_of
- "typ_of T \<equiv> STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
+ "typ_of (T\<Colon>'a set itself) \<equiv> STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
instance int :: typ_of
- "typ_of T \<equiv> STR ''IntDef.int'' {\<struct>} []" ..
+ "typ_of (T\<Colon>int itself) \<equiv> STR ''IntDef.int'' {\<struct>} []" ..
setup {*
let
--- a/src/HOL/Library/List_lexord.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Library/List_lexord.thy Thu Nov 29 17:08:26 2007 +0100
@@ -10,13 +10,11 @@
begin
instance list :: (ord) ord
- list_le_def: "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
- list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}" ..
-
-lemmas list_ord_defs [code func del] = list_less_def list_le_def
+ list_less_def [code func del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
+ list_le_def [code func del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)" ..
instance list :: (order) order
- apply (intro_classes, unfold list_ord_defs)
+ apply (intro_classes, unfold list_less_def list_le_def)
apply safe
apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
apply simp
@@ -35,13 +33,11 @@
done
instance list :: (linorder) distrib_lattice
- "inf \<equiv> min"
- "sup \<equiv> max"
+ [code func del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
+ [code func del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
by intro_classes
(auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
-lemmas [code func del] = inf_list_def sup_list_def
-
lemma not_less_Nil [simp]: "\<not> (x < [])"
by (unfold list_less_def) simp
@@ -52,13 +48,13 @@
by (unfold list_less_def) simp
lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
- by (unfold list_ord_defs, cases x) auto
+ by (unfold list_le_def, cases x) auto
lemma Nil_le_Cons [simp]: "[] \<le> x"
- by (unfold list_ord_defs, cases x) auto
+ by (unfold list_le_def, cases x) auto
lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
- by (unfold list_ord_defs) auto
+ by (unfold list_le_def) auto
lemma less_code [code func]:
"xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
--- a/src/HOL/Library/Parity.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Library/Parity.thy Thu Nov 29 17:08:26 2007 +0100
@@ -17,7 +17,7 @@
"odd x \<equiv> \<not> even x"
instance int :: even_odd
- even_def[presburger]: "even x \<equiv> x mod 2 = 0" ..
+ even_def[presburger]: "even x \<equiv> (x\<Colon>int) mod 2 = 0" ..
instance nat :: even_odd
even_nat_def[presburger]: "even x \<equiv> even (int x)" ..
--- a/src/HOL/Library/Product_ord.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Library/Product_ord.thy Thu Nov 29 17:08:26 2007 +0100
@@ -10,30 +10,28 @@
begin
instance "*" :: (ord, ord) ord
- prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x \<le> snd y)"
- prod_less_def: "(x < y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x < snd y)" ..
-
-lemmas prod_ord_defs [code func del] = prod_less_def prod_le_def
+ prod_le_def [code func del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
+ prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y" ..
lemma [code func]:
"(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
"(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
- unfolding prod_ord_defs by simp_all
+ unfolding prod_le_def prod_less_def by simp_all
lemma [code]:
"(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
"(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
- unfolding prod_ord_defs by simp_all
+ unfolding prod_le_def prod_less_def by simp_all
instance * :: (order, order) order
- by default (auto simp: prod_ord_defs intro: order_less_trans)
+ by default (auto simp: prod_le_def prod_less_def intro: order_less_trans)
instance * :: (linorder, linorder) linorder
by default (auto simp: prod_le_def)
instance * :: (linorder, linorder) distrib_lattice
- inf_prod_def: "inf \<equiv> min"
- sup_prod_def: "sup \<equiv> max"
+ inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
+ sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
by intro_classes
(auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
--- a/src/HOL/List.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/List.thy Thu Nov 29 17:08:26 2007 +0100
@@ -2691,7 +2691,7 @@
text{* The integers are an instance of the above class: *}
instance int:: finite_intvl_succ
- successor_int_def: "successor == (%i. i+1)"
+ successor_int_def: "successor == (%i\<Colon>int. i+1)"
by intro_classes (simp_all add: successor_int_def)
text{* Now @{term"[i..j::int]"} is defined for integers. *}
--- a/src/HOL/Matrix/Matrix.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Matrix/Matrix.thy Thu Nov 29 17:08:26 2007 +0100
@@ -23,7 +23,7 @@
times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
instance matrix :: (lordered_ab_group_add) abs
- abs_matrix_def: "abs A \<equiv> sup A (- A)" ..
+ abs_matrix_def: "abs (A \<Colon> 'a matrix) \<equiv> sup A (- A)" ..
instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet
proof
--- a/src/HOL/Matrix/MatrixGeneral.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Matrix/MatrixGeneral.thy Thu Nov 29 17:08:26 2007 +0100
@@ -1281,7 +1281,7 @@
instance matrix :: ("{ord, zero}") ord
le_matrix_def: "A \<le> B \<equiv> \<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i"
- less_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
+ less_def: "A < (B\<Colon>'a matrix) \<equiv> A \<le> B \<and> A \<noteq> B" ..
instance matrix :: ("{order, zero}") order
apply intro_classes
--- a/src/HOL/Nat.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Nat.thy Thu Nov 29 17:08:26 2007 +0100
@@ -1488,8 +1488,8 @@
text {* the lattice order on @{typ nat} *}
instance nat :: distrib_lattice
- "inf \<equiv> min"
- "sup \<equiv> max"
+ "inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat \<equiv> min"
+ "sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat \<equiv> max"
by intro_classes
(simp_all add: inf_nat_def sup_nat_def)
--- a/src/HOL/Numeral.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Numeral.thy Thu Nov 29 17:08:26 2007 +0100
@@ -203,16 +203,15 @@
unfolding numeral_simps int_distrib by simp
-
subsection {* Converting Numerals to Rings: @{term number_of} *}
-axclass number_ring \<subseteq> number, comm_ring_1
- number_of_eq: "number_of k = of_int k"
+class number_ring = number + comm_ring_1 +
+ assumes number_of_eq: "number_of k = of_int k"
text {* self-embedding of the integers *}
instance int :: number_ring
- int_number_of_def: "number_of w \<equiv> of_int w"
+ int_number_of_def: "number_of w \<equiv> of_int w \<Colon> int"
by intro_classes (simp only: int_number_of_def)
lemmas [code func del] = int_number_of_def
--- a/src/HOL/Orderings.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Orderings.thy Thu Nov 29 17:08:26 2007 +0100
@@ -930,7 +930,7 @@
instance bool :: order
le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
- less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
+ less_bool_def: "(P\<Colon>bool) < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
by intro_classes (auto simp add: le_bool_def less_bool_def)
lemmas [code func del] = le_bool_def less_bool_def
@@ -968,7 +968,7 @@
instance "fun" :: (type, ord) ord
le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
- less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
+ less_fun_def: "(f\<Colon>'a \<Rightarrow> 'b) < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
lemmas [code func del] = le_fun_def less_fun_def
--- a/src/HOL/Real/PReal.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Real/PReal.thy Thu Nov 29 17:08:26 2007 +0100
@@ -212,8 +212,8 @@
by intro_classes (rule preal_le_linear)
instance preal :: distrib_lattice
- "inf \<equiv> min"
- "sup \<equiv> max"
+ "inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal \<equiv> min"
+ "sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal \<equiv> max"
by intro_classes
(auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
--- a/src/HOL/Real/Rational.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Real/Rational.thy Thu Nov 29 17:08:26 2007 +0100
@@ -362,8 +362,8 @@
qed
instance rat :: distrib_lattice
- "inf r s \<equiv> min r s"
- "sup r s \<equiv> max r s"
+ "inf \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat \<equiv> min"
+ "sup \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat \<equiv> max"
by default (auto simp add: min_max.sup_inf_distrib1 inf_rat_def sup_rat_def)
instance rat :: ordered_field
--- a/src/HOL/Real/RealDef.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Real/RealDef.thy Thu Nov 29 17:08:26 2007 +0100
@@ -66,7 +66,7 @@
real_abs_def: "abs (r::real) == (if r < 0 then - r else r)" ..
instance real :: sgn
- real_sgn_def: "sgn x == (if x=0 then 0 else if 0<x then 1 else - 1)" ..
+ real_sgn_def: "sgn (x::real) == (if x=0 then 0 else if 0<x then 1 else - 1)" ..
subsection {* Equivalence relation over positive reals *}
@@ -401,8 +401,8 @@
done
instance real :: distrib_lattice
- "inf x y \<equiv> min x y"
- "sup x y \<equiv> max x y"
+ "inf \<Colon> real \<Rightarrow> real \<Rightarrow> real \<equiv> min"
+ "sup \<Colon> real \<Rightarrow> real \<Rightarrow> real \<equiv> max"
by default (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
--- a/src/HOL/Set.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Set.thy Thu Nov 29 17:08:26 2007 +0100
@@ -145,7 +145,7 @@
instance set :: (type) ord
subset_def: "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
- psubset_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
+ psubset_def: "(A\<Colon>'a set) < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
lemmas [code func del] = subset_def psubset_def
abbreviation
--- a/src/HOL/SizeChange/Graphs.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/SizeChange/Graphs.thy Thu Nov 29 17:08:26 2007 +0100
@@ -79,7 +79,7 @@
graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H"
graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H"
"inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
- "sup G H \<equiv> G + H"
+ "sup (G \<Colon> ('a, 'b) graph) H \<equiv> G + H"
Inf_graph_def: "Inf \<equiv> \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
Sup_graph_def: "Sup \<equiv> \<lambda>Gs. Graph (\<Union>(dest_graph ` Gs))"
proof
@@ -195,10 +195,10 @@
"grpow 0 A = 1"
| "grpow (Suc n) A = A * (grpow n A)"
-instance graph :: (type, monoid_mult)
+instance graph :: (type, monoid_mult)
"{semiring_1,idem_add,recpower,star}"
graph_pow_def: "A ^ n == grpow n A"
- graph_star_def: "star G == (SUP n. G ^ n)"
+ graph_star_def: "star (G \<Colon> ('a, 'b) graph) == (SUP n. G ^ n)"
proof
fix a b c :: "('a, 'b) graph"
--- a/src/HOL/Tools/datatype_codegen.ML Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML Thu Nov 29 17:08:26 2007 +0100
@@ -544,7 +544,7 @@
|> not (null arities) ? (
f arities css
#-> (fn defs =>
- Class.prove_instance tac arities defs
+ Instance.prove_instance tac arities defs
#-> (fn defs =>
after_qed arities css defs)))
end;
--- a/src/HOL/Tools/function_package/size.ML Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Tools/function_package/size.ML Thu Nov 29 17:08:26 2007 +0100
@@ -38,7 +38,7 @@
val n = Sign.arity_number thy tyco;
in
thy
- |> Class.prove_instance (Class.intro_classes_tac [])
+ |> Instance.prove_instance (Class.intro_classes_tac [])
[(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
|> snd
end
--- a/src/HOL/ex/Classpackage.thy Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/ex/Classpackage.thy Thu Nov 29 17:08:26 2007 +0100
@@ -13,14 +13,14 @@
assumes assoc: "x \<otimes> y \<otimes> z = x \<otimes> (y \<otimes> z)"
instance nat :: semigroup
- "m \<otimes> n \<equiv> m + n"
+ "m \<otimes> n \<equiv> (m\<Colon>nat) + n"
proof
fix m n q :: nat
from mult_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp
qed
instance int :: semigroup
- "k \<otimes> l \<equiv> k + l"
+ "k \<otimes> l \<equiv> (k\<Colon>int) + l"
proof
fix k l j :: int
from mult_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp
@@ -47,8 +47,8 @@
assumes neutl: "\<one> \<otimes> x = x"
instance nat :: monoidl and int :: monoidl
- "\<one> \<equiv> 0"
- "\<one> \<equiv> 0"
+ "\<one> \<equiv> (0\<Colon>nat)"
+ "\<one> \<equiv> (0\<Colon>int)"
proof
fix n :: nat
from mult_nat_def one_nat_def show "\<one> \<otimes> n = n" by simp
--- a/src/Pure/Isar/class.ML Thu Nov 29 07:55:46 2007 +0100
+++ b/src/Pure/Isar/class.ML Thu Nov 29 17:08:26 2007 +0100
@@ -57,16 +57,7 @@
(*old instance layer*)
val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
- val instance: arity list -> ((bstring * Attrib.src list) * term) list
- -> (thm list -> theory -> theory)
- -> theory -> Proof.state
- val instance_cmd: (bstring * xstring list * xstring) list
- -> ((bstring * Attrib.src list) * xstring) list
- -> (thm list -> theory -> theory)
- -> theory -> Proof.state
- val prove_instance: tactic -> arity list
- -> ((bstring * Attrib.src list) * term) list
- -> theory -> thm list * theory
+ val instance_arity_cmd: (bstring * xstring list * xstring) list -> theory -> Proof.state
end;
structure Class : CLASS =
@@ -150,6 +141,8 @@
val instance_arity =
gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
+val instance_arity_cmd =
+ gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity I;
val classrel =
gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel))
AxClass.add_classrel I o single;
@@ -221,7 +214,7 @@
val SOME class = AxClass.class_of_param thy c;
val SOME tyco = inst_tyco thy (c, ty);
val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
- val c' = NameSpace.base c;
+ val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
val ty' = Type.strip_sorts ty;
in
thy
@@ -253,137 +246,6 @@
end;
-(* legacy *)
-
-fun add_inst_def (class, tyco) (c, ty) thy =
- let
- val tyco_base = Sign.base_name tyco;
- val name_inst = Sign.base_name class ^ "_" ^ tyco_base ^ "_inst";
- val c_inst_base = Sign.base_name c ^ "_" ^ tyco_base;
- in
- thy
- |> Sign.sticky_prefix name_inst
- |> Sign.declare_const [] (c_inst_base, ty, NoSyn)
- |-> (fn const as Const (c_inst, _) =>
- PureThy.add_defs_i false
- [((Thm.def_name c_inst_base, Logic.mk_equals (const, Const (c, ty))), [])]
- #-> (fn [thm] => add_inst (c, tyco) (c_inst, Thm.symmetric thm)))
- |> Sign.restore_naming thy
- end;
-
-fun add_inst_def' (class, tyco) (c, ty) thy =
- if case Symtab.lookup (fst (InstData.get thy)) c
- of NONE => true
- | SOME tab => is_none (Symtab.lookup tab tyco)
- then add_inst_def (class, tyco) (c, Logic.unvarifyT ty) thy
- else thy;
-
-fun add_def ((class, tyco), ((name, prop), atts)) thy =
- let
- val ((lhs as Const (c, ty), args), rhs) =
- (apfst Term.strip_comb o Logic.dest_equals) prop;
- in
- thy
- |> PureThy.add_defs_i true [((name, prop), map (Attrib.attribute_i thy) atts)]
- |-> (fn [def] => add_inst_def (class, tyco) (c, ty) #> pair def)
- end;
-
-
-(** instances with implicit parameter handling **)
-
-local
-
-fun gen_read_def thy prep_att parse_prop ((raw_name, raw_atts), raw_t) =
- let
- val ctxt = ProofContext.init thy;
- val t = parse_prop ctxt raw_t |> Syntax.check_prop ctxt;
- val ((c, ty), _) = Sign.cert_def ctxt t;
- val atts = map (prep_att thy) raw_atts;
- val insts = Consts.typargs (Sign.consts_of thy) (c, ty);
- val name = case raw_name
- of "" => NONE
- | _ => SOME raw_name;
- in (c, (insts, ((name, t), atts))) end;
-
-fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Syntax.parse_prop;
-fun read_def thy = gen_read_def thy (K I) (K I);
-
-fun gen_instance prep_arity read_def do_proof raw_arities raw_defs after_qed theory =
- let
- val arities = map (prep_arity theory) raw_arities;
- val _ = if null arities then error "At least one arity must be given" else ();
- val _ = case (duplicates (op =) o map #1) arities
- of [] => ()
- | dupl_tycos => error ("Type constructors occur more than once in arities: "
- ^ commas_quote dupl_tycos);
- fun get_consts_class tyco ty class =
- let
- val cs = (these o try (#params o AxClass.get_info theory)) class;
- val subst_ty = map_type_tfree (K ty);
- in
- map (fn (c, ty) => (c, ((class, tyco), subst_ty ty))) cs
- end;
- fun get_consts_sort (tyco, asorts, sort) =
- let
- val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort))
- (Name.names Name.context Name.aT asorts))
- in maps (get_consts_class tyco ty) (Sign.complete_sort theory sort) end;
- val cs = maps get_consts_sort arities;
- fun mk_typnorm thy (ty, ty_sc) =
- case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty
- of SOME env => SOME (Logic.varifyT #> Envir.typ_subst_TVars env #> Logic.unvarifyT)
- | NONE => NONE;
- fun read_defs defs cs thy_read =
- let
- fun read raw_def cs =
- let
- val (c, (inst, ((name_opt, t), atts))) = read_def thy_read raw_def;
- val ty = Consts.instance (Sign.consts_of thy_read) (c, inst);
- val ((class, tyco), ty') = case AList.lookup (op =) cs c
- of NONE => error ("Illegal definition for constant " ^ quote c)
- | SOME class_ty => class_ty;
- val name = case name_opt
- of NONE => Thm.def_name (Logic.name_arity (tyco, [], c))
- | SOME name => name;
- val t' = case mk_typnorm thy_read (ty', ty)
- of NONE => error ("Illegal definition for constant " ^
- quote (c ^ "::" ^ setmp show_sorts true
- (Sign.string_of_typ thy_read) ty))
- | SOME norm => map_types norm t
- in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;
- in fold_map read defs cs end;
- val (defs, other_cs) = read_defs raw_defs cs
- (fold Sign.primitive_arity arities (Theory.copy theory));
- fun after_qed' cs defs =
- fold Sign.add_const_constraint (map (apsnd SOME) cs)
- #> after_qed defs;
- in
- theory
- |> fold_map get_remove_global_constraint (map fst cs |> distinct (op =))
- ||>> fold_map add_def defs
- ||> fold (fn (c, ((class, tyco), ty)) => add_inst_def' (class, tyco) (c, ty)) other_cs
- |-> (fn (cs, defs) => do_proof (after_qed' cs defs) arities defs)
- end;
-
-fun tactic_proof tac f arities defs =
- fold (fn arity => AxClass.prove_arity arity tac) arities
- #> f
- #> pair defs;
-
-in
-
-val instance = gen_instance Sign.cert_arity read_def
- (fn f => fn arities => fn defs => instance_arity f arities);
-val instance_cmd = gen_instance Sign.read_arity read_def_cmd
- (fn f => fn arities => fn defs => instance_arity f arities);
-fun prove_instance tac arities defs =
- gen_instance Sign.cert_arity read_def
- (tactic_proof tac) arities defs (K I);
-
-end; (*local*)
-
-
-
(** class data **)
datatype class_data = ClassData of {
@@ -1008,7 +870,7 @@
fun check_improve (Const (c, ty)) = (case inst_tyco thy (c, ty)
of SOME tyco => (case AList.lookup (op =) params (c, tyco)
- of SOME (_, ty') => Type.typ_match tsig (ty, ty')
+ of SOME (_, ty') => perhaps (try (Type.typ_match tsig (ty, ty')))
| NONE => I)
| NONE => I)
| check_improve _ = I;
@@ -1057,6 +919,7 @@
of [] => ()
| dupl_tycos => error ("Type constructors occur more than once in arities: "
^ commas_quote dupl_tycos);
+ val _ = map (map (the_class_data thy) o #3) arities;
val ty_insts = map (fn (tyco, sorts, _) =>
(tyco, Type (tyco, map TFree (Name.names Name.context Name.aT sorts))))
arities;
@@ -1064,12 +927,11 @@
fun type_name "*" = "prod"
| type_name "+" = "sum"
| type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
- fun get_param tyco sorts (param, (c, ty)) =
- ((unoverload_const thy (c, ty), tyco),
- (param ^ "_" ^ type_name tyco,
- map_atyps (K (ty_inst tyco)) ty));
+ fun get_param tyco sorts (param, (c, ty)) = if can (inst thy) (c, tyco)
+ then NONE else SOME ((unoverload_const thy (c, ty), tyco),
+ (param ^ "_" ^ type_name tyco, map_atyps (K (ty_inst tyco)) ty));
fun get_params (tyco, sorts, sort) =
- map (get_param tyco sorts) (these_params thy sort)
+ map_filter (get_param tyco sorts) (these_params thy sort)
val params = maps get_params arities;
in
thy
@@ -1099,8 +961,8 @@
Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
- fn ts => fn lthy => after_qed (Goal.prove_multi lthy [] [] ts
- (fn {context, ...} => tac context)) lthy) I;
+ fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
+ (fn {context, ...} => tac context)) ts) lthy) I;
fun conclude_instantiation lthy =
let
@@ -1121,7 +983,7 @@
let
val SOME class = AxClass.class_of_param thy c;
val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
- val c' = NameSpace.base c;
+ val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy tyco) []);
val ty = map_atyps (fn _ => Type (tyco, map TFree vs)) ty0;
in
--- a/src/Pure/Isar/instance.ML Thu Nov 29 07:55:46 2007 +0100
+++ b/src/Pure/Isar/instance.ML Thu Nov 29 17:08:26 2007 +0100
@@ -10,7 +10,6 @@
val instantiate: arity list -> (local_theory -> local_theory)
-> (Proof.context -> tactic) -> theory -> theory
val instance: arity list -> ((bstring * Attrib.src list) * term) list
- -> (thm list -> theory -> theory)
-> theory -> Proof.state
val prove_instance: tactic -> arity list -> ((bstring * Attrib.src list) * term) list
-> theory -> thm list * theory
@@ -18,7 +17,6 @@
val instantiation_cmd: (xstring * sort * xstring) list
-> theory -> local_theory
val instance_cmd: (xstring * sort * xstring) list -> ((bstring * Attrib.src list) * xstring) list
- -> (thm list -> theory -> theory)
-> theory -> Proof.state
end;
@@ -35,8 +33,9 @@
#> LocalTheory.exit
#> ProofContext.theory_of;
-fun gen_instance prep_arity prep_attr parse_term do_proof raw_arities defs after_qed thy =
+fun gen_instance prep_arity prep_attr parse_term do_proof do_proof' raw_arities defs thy =
let
+ val arities = map (prep_arity thy) raw_arities;
fun export_defs ctxt =
let
val ctxt_thy = ProofContext.init (ProofContext.theory_of ctxt);
@@ -54,8 +53,9 @@
let
val def' = (apsnd o apsnd) (Syntax.check_prop ctxt) def;
in Specification.definition def' ctxt end;
- val arities = map (prep_arity thy) raw_arities;
- in
+ in if not (null defs) orelse forall (fn (_, _, sort) =>
+ forall (Class.is_class thy) sort) arities
+ then
thy
|> TheoryTarget.instantiation arities
|> `(fn ctxt => map (mk_def ctxt) defs)
@@ -64,15 +64,21 @@
||> LocalTheory.exit
||> ProofContext.theory_of
||> TheoryTarget.instantiation arities
- |-> (fn defs => do_proof defs (LocalTheory.theory (after_qed defs)))
+ |-> (fn defs => do_proof defs)
+ else
+ thy
+ |> do_proof' arities
end;
val instance = gen_instance Sign.cert_arity (K I) (K I)
- (fn _ => fn after_qed => Class.instantiation_instance (after_qed #> Class.conclude_instantiation));
+ (fn _ => Class.instantiation_instance Class.conclude_instantiation) (Class.instance_arity I);
val instance_cmd = gen_instance Sign.read_arity Attrib.intern_src Syntax.parse_prop
- (fn _ => fn after_qed => Class.instantiation_instance (after_qed #> Class.conclude_instantiation));
+ (fn _ => Class.instantiation_instance Class.conclude_instantiation) (Class.instance_arity I);
fun prove_instance tac arities defs = gen_instance Sign.cert_arity (K I) (K I)
- (fn defs => fn after_qed => Class.prove_instantiation_instance (K tac)
- #> after_qed #> Class.conclude_instantiation #> ProofContext.theory_of #> pair defs) arities defs (K I);
+ (fn defs => Class.prove_instantiation_instance (K tac)
+ #> Class.conclude_instantiation #> ProofContext.theory_of #> pair defs)
+ (pair [] o ProofContext.theory_of o Proof.global_terminal_proof
+ (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
+ oo Class.instance_arity I) arities defs;
end;
--- a/src/Pure/Isar/isar_syn.ML Thu Nov 29 07:55:46 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML Thu Nov 29 17:08:26 2007 +0100
@@ -453,10 +453,8 @@
val _ =
OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
- P.$$$ "advanced" |-- P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
- >> (fn (arities, defs) => Instance.instance_cmd arities defs (K I)) ||
P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
- >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func)))
+ >> (fn (arities, defs) => Instance.instance_cmd arities defs))
>> (Toplevel.print oo Toplevel.theory_to_proof)
|| Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));