--- a/src/HOL/HOL.thy Mon Jan 11 23:00:05 2010 +0100
+++ b/src/HOL/HOL.thy Mon Jan 11 23:11:31 2010 +0100
@@ -1816,10 +1816,9 @@
text {* Code equations *}
lemma [code]:
- shows "(False \<Longrightarrow> P) \<equiv> Trueprop True"
- and "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
- and "(P \<Longrightarrow> False) \<equiv> Trueprop (\<not> P)"
- and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True" by (auto intro!: equal_intr_rule)
+ shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
+ and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
+ and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" by (auto intro!: equal_intr_rule)
lemma [code]:
shows "False \<and> P \<longleftrightarrow> False"
--- a/src/HOL/Matrix/Matrix.thy Mon Jan 11 23:00:05 2010 +0100
+++ b/src/HOL/Matrix/Matrix.thy Mon Jan 11 23:11:31 2010 +0100
@@ -1559,7 +1559,7 @@
instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet ..
instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_join ..
-instance matrix :: (ring) ring
+instance matrix :: (semiring_0) semiring_0
proof
fix A B C :: "'a matrix"
show "A * B * C = A * (B * C)"
@@ -1577,7 +1577,11 @@
apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])
apply (simp_all add: associative_def commutative_def algebra_simps)
done
-qed
+ show "0 * A = 0" by (simp add: times_matrix_def)
+ show "A * 0 = 0" by (simp add: times_matrix_def)
+qed
+
+instance matrix :: (ring) ring ..
instance matrix :: (pordered_ring) pordered_ring
proof
@@ -1607,7 +1611,7 @@
"Rep_matrix ((a::('a::monoid_add)matrix)+b) j i = (Rep_matrix a j i) + (Rep_matrix b j i)"
by (simp add: plus_matrix_def)
-lemma Rep_matrix_mult: "Rep_matrix ((a::('a::ring) matrix) * b) j i =
+lemma Rep_matrix_mult: "Rep_matrix ((a::('a::semiring_0) matrix) * b) j i =
foldseq (op +) (% k. (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))"
apply (simp add: times_matrix_def)
apply (simp add: Rep_mult_matrix)
@@ -1626,10 +1630,10 @@
apply (simp)
done
-lemma nrows_mult: "nrows ((A::('a::ring) matrix) * B) <= nrows A"
+lemma nrows_mult: "nrows ((A::('a::semiring_0) matrix) * B) <= nrows A"
by (simp add: times_matrix_def mult_nrows)
-lemma ncols_mult: "ncols ((A::('a::ring) matrix) * B) <= ncols B"
+lemma ncols_mult: "ncols ((A::('a::semiring_0) matrix) * B) <= ncols B"
by (simp add: times_matrix_def mult_ncols)
definition
@@ -1656,7 +1660,7 @@
ultimately show "?r = n" by simp
qed
-lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{ring_1}) matrix) * (one_matrix n) = A"
+lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{semiring_1}) matrix) * (one_matrix n) = A"
apply (subst Rep_matrix_inject[THEN sym])
apply (rule ext)+
apply (simp add: times_matrix_def Rep_mult_matrix)
@@ -1664,7 +1668,7 @@
apply (simp_all)
by (simp add: ncols)
-lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::ring_1) matrix)"
+lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::semiring_1) matrix)"
apply (subst Rep_matrix_inject[THEN sym])
apply (rule ext)+
apply (simp add: times_matrix_def Rep_mult_matrix)
@@ -1730,7 +1734,7 @@
lemma one_matrix_inverse: "inverse_matrix (one_matrix n) (one_matrix n)"
by (simp add: inverse_matrix_def left_inverse_matrix_def right_inverse_matrix_def)
-lemma zero_imp_mult_zero: "(a::'a::ring) = 0 | b = 0 \<Longrightarrow> a * b = 0"
+lemma zero_imp_mult_zero: "(a::'a::semiring_0) = 0 | b = 0 \<Longrightarrow> a * b = 0"
by auto
lemma Rep_matrix_zero_imp_mult_zero:
@@ -1746,7 +1750,7 @@
apply (simp_all)
done
-lemma move_matrix_row_mult: "move_matrix ((A::('a::ring) matrix) * B) j 0 = (move_matrix A j 0) * B"
+lemma move_matrix_row_mult: "move_matrix ((A::('a::semiring_0) matrix) * B) j 0 = (move_matrix A j 0) * B"
apply (subst Rep_matrix_inject[symmetric])
apply (rule ext)+
apply (auto simp add: Rep_matrix_mult foldseq_zero)
@@ -1757,7 +1761,7 @@
apply (simp add: max1)
done
-lemma move_matrix_col_mult: "move_matrix ((A::('a::ring) matrix) * B) 0 i = A * (move_matrix B 0 i)"
+lemma move_matrix_col_mult: "move_matrix ((A::('a::semiring_0) matrix) * B) 0 i = A * (move_matrix B 0 i)"
apply (subst Rep_matrix_inject[symmetric])
apply (rule ext)+
apply (auto simp add: Rep_matrix_mult foldseq_zero)
@@ -1774,7 +1778,7 @@
apply (simp)
done
-lemma move_matrix_mult: "move_matrix ((A::('a::ring) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)"
+lemma move_matrix_mult: "move_matrix ((A::('a::semiring_0) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)"
by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult)
constdefs
--- a/src/Pure/Isar/code.ML Mon Jan 11 23:00:05 2010 +0100
+++ b/src/Pure/Isar/code.ML Mon Jan 11 23:11:31 2010 +0100
@@ -23,7 +23,7 @@
val constrset_of_consts: theory -> (string * typ) list
-> string * ((string * sort) list * (string * typ list) list)
- (*code equations*)
+ (*code equations and certificates*)
val mk_eqn: theory -> thm * bool -> thm * bool
val mk_eqn_warning: theory -> thm -> (thm * bool) option
val mk_eqn_liberal: theory -> thm -> (thm * bool) option
@@ -34,6 +34,11 @@
val typscheme_eqn: theory -> thm -> (string * sort) list * typ
val typscheme_eqns: theory -> string -> thm list -> (string * sort) list * typ
val standard_typscheme: theory -> thm list -> thm list
+ type cert = thm * bool list
+ val cert_of_eqns: theory -> (thm * bool) list -> cert
+ val constrain_cert: theory -> sort list -> cert -> cert
+ val dest_cert: theory -> cert -> (string * ((string * sort) list * typ)) * ((term list * term) * bool) list
+ val eqns_of_cert: theory -> cert -> (thm * bool) list
(*executable code*)
val add_type: string -> theory -> theory
@@ -57,7 +62,7 @@
val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
val get_datatype_of_constr: theory -> string -> string option
val these_eqns: theory -> string -> (thm * bool) list
- val all_eqns: theory -> (thm * bool) list
+ val eqn_cert: theory -> string -> cert
val get_case_scheme: theory -> string -> (int * (int * string list)) option
val undefineds: theory -> string list
val print_codesetup: theory -> unit
@@ -414,7 +419,7 @@
fun is_constr thy = is_some o get_datatype_of_constr thy;
-(* code equations *)
+(* bare code equations *)
exception BAD_THM of string;
fun bad_thm msg = raise BAD_THM msg;
@@ -521,10 +526,10 @@
fun const_eqn thy = fst o const_typ_eqn thy;
-fun raw_typscheme thy (c, ty) =
+fun logical_typscheme thy (c, ty) =
(map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
-fun typscheme thy (c, ty) = raw_typscheme thy (c, subst_signature thy c ty);
+fun typscheme thy (c, ty) = logical_typscheme thy (c, subst_signature thy c ty);
fun typscheme_eqn thy = typscheme thy o apsnd Logic.unvarifyT o const_typ_eqn thy;
@@ -537,7 +542,7 @@
| NONE => Name.invent_list [] Name.aT (length tvars)
|> map (fn v => TFree (v, []));
val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
- in raw_typscheme thy (c, ty) end
+ in logical_typscheme thy (c, ty) end
| typscheme_eqns thy c (thm :: _) = typscheme_eqn thy thm;
fun assert_eqns_const thy c eqns =
@@ -547,6 +552,9 @@
^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)
in map (cert o assert_eqn thy) eqns end;
+
+(* code equation certificates *)
+
fun standard_typscheme thy thms =
let
fun tvars_of T = rev (Term.add_tvarsT T []);
@@ -558,6 +566,69 @@
|> map (fn (v, sort) => TVar ((v, 0), sort));
in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end;
+type cert = thm * bool list;
+
+fun cert_of_eqns thy [] = (Drule.dummy_thm, [])
+ | cert_of_eqns thy eqns =
+ let
+ val propers = map snd eqns;
+ val thms as thm :: _ = (map Thm.freezeT o standard_typscheme thy o map fst) eqns; (*FIXME*)
+ val (c, ty) = head_eqn thm;
+ val head_thm = Thm.assume (Thm.cterm_of thy (Logic.mk_equals
+ (Free ("HEAD", ty), Const (c, ty)))) |> Thm.symmetric;
+ fun head_conv ct = if can Thm.dest_comb ct
+ then Conv.fun_conv head_conv ct
+ else Conv.rewr_conv head_thm ct;
+ val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv);
+ val cert = Conjunction.intr_balanced (map rewrite_head thms);
+ in (cert, propers) end;
+
+fun head_cert thy cert =
+ let
+ val [head] = Thm.hyps_of cert;
+ val (Free (h, _), Const (c, ty)) = (Logic.dest_equals o the_single o Thm.hyps_of) cert;
+ in ((c, typscheme thy (AxClass.unoverload_const thy (c, ty), ty)), (head, h)) end;
+
+fun constrain_cert thy sorts (cert, []) = (cert, [])
+ | constrain_cert thy sorts (cert, propers) =
+ let
+ val ((c, (vs, _)), (head, _)) = head_cert thy cert;
+ val subst = map2 (fn (v, _) => fn sort => (v, sort)) vs sorts;
+ val head' = (map_types o map_atyps)
+ (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) subst v))) head;
+ val inst = (map2 (fn (v, sort) => fn sort' =>
+ pairself (Thm.ctyp_of thy) (TVar ((v, 0), sort), TFree (v, sort'))) vs sorts ,[]);
+ val cert' = cert
+ |> Thm.implies_intr (Thm.cterm_of thy head)
+ |> Thm.varifyT
+ |> Thm.instantiate inst
+ |> Thm.elim_implies (Thm.assume (Thm.cterm_of thy head'))
+ in (cert', propers) end;
+
+fun dest_cert thy (cert, propers) =
+ let
+ val (c_vs_ty, (head, h)) = head_cert thy cert;
+ val equations = cert
+ |> Thm.prop_of
+ |> Logic.dest_conjunction_balanced (length propers)
+ |> map Logic.dest_equals
+ |> (map o apfst) strip_comb
+ |> (map o apfst) (fn (Free (h', _), ts) => case h = h' of True => ts)
+ in (c_vs_ty, equations ~~ propers) end;
+
+fun eqns_of_cert thy (cert, []) = []
+ | eqns_of_cert thy (cert, propers) =
+ let
+ val (_, (head, _)) = head_cert thy cert;
+ val thms = cert
+ |> LocalDefs.expand [Thm.cterm_of thy head]
+ |> Thm.varifyT
+ |> Conjunction.elim_balanced (length propers)
+ in thms ~~ propers end;
+
+
+(* code equation access *)
+
fun these_eqns thy c =
Symtab.lookup ((the_eqns o the_exec) thy) c
|> Option.map (snd o snd o fst)
@@ -565,9 +636,12 @@
|> (map o apfst) (Thm.transfer thy)
|> burrow_fst (standard_typscheme thy);
-fun all_eqns thy =
- Symtab.dest ((the_eqns o the_exec) thy)
- |> maps (snd o snd o fst o snd);
+fun eqn_cert thy c =
+ Symtab.lookup ((the_eqns o the_exec) thy) c
+ |> Option.map (snd o snd o fst)
+ |> these
+ |> (map o apfst) (Thm.transfer thy)
+ |> cert_of_eqns thy;
(* cases *)