# HG changeset patch # User wenzelm # Date 1263247891 -3600 # Node ID 45aa70e7e7b625bb65c9307baf7b531e6e506448 # Parent 89c230bf8febc967e80559e4745ec4ab4c46ff1d# Parent e596a0b71f3cff52f5153e424fb3e94d6246c46d merged diff -r e596a0b71f3c -r 45aa70e7e7b6 src/HOL/HOL.thy --- 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 \ P) \ Trueprop True" - and "(True \ PROP Q) \ PROP Q" - and "(P \ False) \ Trueprop (\ P)" - and "(PROP Q \ True) \ Trueprop True" by (auto intro!: equal_intr_rule) + shows "(True \ PROP Q) \ PROP Q" + and "(PROP Q \ True) \ Trueprop True" + and "(P \ R) \ Trueprop (P \ R)" by (auto intro!: equal_intr_rule) lemma [code]: shows "False \ P \ False" diff -r e596a0b71f3c -r 45aa70e7e7b6 src/HOL/Matrix/Matrix.thy --- 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 \ (A::('a::{ring_1}) matrix) * (one_matrix n) = A" +lemma one_matrix_mult_right[simp]: "ncols A <= n \ (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 \ (one_matrix n) * A = (A::('a::ring_1) matrix)" +lemma one_matrix_mult_left[simp]: "nrows A <= n \ (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 \ a * b = 0" +lemma zero_imp_mult_zero: "(a::'a::semiring_0) = 0 | b = 0 \ 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 diff -r e596a0b71f3c -r 45aa70e7e7b6 src/Pure/Isar/code.ML --- 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 *)