# HG changeset patch # User haftmann # Date 1424296007 -3600 # Node ID e87974cd9b868f987c30f605f4b5456e3988f97a # Parent ae50c9b824440538353a532bf4ea8a8ee0c6be38 explicit declaration allows cumulative declaration diff -r ae50c9b82444 -r e87974cd9b86 src/HOL/Semiring_Normalization.thy --- a/src/HOL/Semiring_Normalization.thy Tue Feb 17 17:22:45 2015 +0100 +++ b/src/HOL/Semiring_Normalization.thy Wed Feb 18 22:46:47 2015 +0100 @@ -72,10 +72,6 @@ context comm_semiring_1 begin -lemma normalizing_semiring_ops: - shows "TERM (x + y)" and "TERM (x * y)" and "TERM (x ^ n)" - and "TERM 0" and "TERM 1" . - lemma normalizing_semiring_rules: "(a * m) + (b * m) = (a + b) * m" "(a * m) + m = (a + 1) * m" @@ -116,85 +112,65 @@ by (simp_all add: algebra_simps power_add power2_eq_square power_mult_distrib power_mult del: one_add_one) -lemmas normalizing_comm_semiring_1_axioms = - comm_semiring_1_axioms [normalizer - semiring ops: normalizing_semiring_ops - semiring rules: normalizing_semiring_rules] +declaration \Semiring_Normalizer.declare @{thm comm_semiring_1_axioms} + {semiring = ([@{cpat "?x + ?y"}, @{cpat "?x * ?y"}, @{cpat "?x ^ ?n"}, @{cpat 0}, @{cpat 1}], + @{thms normalizing_semiring_rules}), ring = ([], []), field = ([], []), idom = [], ideal = []}\ end context comm_ring_1 begin -lemma normalizing_ring_ops: shows "TERM (x- y)" and "TERM (- x)" . - lemma normalizing_ring_rules: "- x = (- 1) * x" "x - y = x + (- y)" by simp_all -lemmas normalizing_comm_ring_1_axioms = - comm_ring_1_axioms [normalizer - semiring ops: normalizing_semiring_ops - semiring rules: normalizing_semiring_rules - ring ops: normalizing_ring_ops - ring rules: normalizing_ring_rules] +declaration \Semiring_Normalizer.declare @{thm comm_ring_1_axioms} + {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms}, + ring = ([@{cpat "?x - ?y"}, @{cpat "- ?x"}], @{thms normalizing_ring_rules}), field = ([], []), idom = [], ideal = []}\ end context comm_semiring_1_cancel_crossproduct begin -lemmas - normalizing_comm_semiring_1_cancel_crossproduct_axioms = - comm_semiring_1_cancel_crossproduct_axioms [normalizer - semiring ops: normalizing_semiring_ops - semiring rules: normalizing_semiring_rules - idom rules: crossproduct_noteq add_scale_eq_noteq] +declaration \Semiring_Normalizer.declare @{thm comm_semiring_1_cancel_crossproduct_axioms} + {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms}, + ring = ([], []), field = ([], []), idom = @{thms crossproduct_noteq add_scale_eq_noteq}, ideal = []}\ end context idom begin -lemmas normalizing_idom_axioms = idom_axioms [normalizer - semiring ops: normalizing_semiring_ops - semiring rules: normalizing_semiring_rules - ring ops: normalizing_ring_ops - ring rules: normalizing_ring_rules - idom rules: crossproduct_noteq add_scale_eq_noteq - ideal rules: right_minus_eq add_0_iff] +declaration \Semiring_Normalizer.declare @{thm idom_axioms} + {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_ring_1_axioms}, + ring = Semiring_Normalizer.the_ring @{context} @{thm comm_ring_1_axioms}, + field = ([], []), idom = @{thms crossproduct_noteq add_scale_eq_noteq}, + ideal = @{thms right_minus_eq add_0_iff}}\ end context field begin -lemma normalizing_field_ops: - shows "TERM (x / y)" and "TERM (inverse x)" . - lemmas normalizing_field_rules = divide_inverse inverse_eq_divide -lemmas normalizing_field_axioms = - field_axioms [normalizer - semiring ops: normalizing_semiring_ops - semiring rules: normalizing_semiring_rules - ring ops: normalizing_ring_ops - ring rules: normalizing_ring_rules - field ops: normalizing_field_ops - field rules: normalizing_field_rules - idom rules: crossproduct_noteq add_scale_eq_noteq - ideal rules: right_minus_eq add_0_iff] +declaration \Semiring_Normalizer.declare @{thm field_axioms} + {semiring = Semiring_Normalizer.the_semiring @{context} @{thm idom_axioms}, + ring = Semiring_Normalizer.the_ring @{context} @{thm idom_axioms}, + field = ([@{cpat "?x / ?y"}, @{cpat "inverse ?x"}], @{thms normalizing_field_rules}), + idom = Semiring_Normalizer.the_idom @{context} @{thm idom_axioms}, + ideal = Semiring_Normalizer.the_ideal @{context} @{thm idom_axioms}}\ end -hide_fact (open) normalizing_comm_semiring_1_axioms - normalizing_comm_semiring_1_cancel_crossproduct_axioms normalizing_semiring_ops normalizing_semiring_rules +hide_fact (open) normalizing_semiring_rules -hide_fact (open) normalizing_comm_ring_1_axioms - normalizing_idom_axioms normalizing_ring_ops normalizing_ring_rules +hide_fact (open) normalizing_ring_rules -hide_fact (open) normalizing_field_axioms normalizing_field_ops normalizing_field_rules +hide_fact (open) normalizing_field_rules code_identifier code_module Semiring_Normalization \ (SML) Arith and (OCaml) Arith and (Haskell) Arith diff -r ae50c9b82444 -r e87974cd9b86 src/HOL/Tools/semiring_normalizer.ML --- a/src/HOL/Tools/semiring_normalizer.ML Tue Feb 17 17:22:45 2015 +0100 +++ b/src/HOL/Tools/semiring_normalizer.ML Wed Feb 18 22:46:47 2015 +0100 @@ -8,8 +8,13 @@ sig type entry val match: Proof.context -> cterm -> entry option - val add: {semiring: cterm list * thm list, ring: cterm list * thm list, - field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute + val the_semiring: Proof.context -> thm -> cterm list * thm list + val the_ring: Proof.context -> thm -> cterm list * thm list + val the_field: Proof.context -> thm -> cterm list * thm list + val the_idom: Proof.context -> thm -> thm list + val the_ideal: Proof.context -> thm -> thm list + val declare: thm -> {semiring: cterm list * thm list, ring: cterm list * thm list, + field: cterm list * thm list, idom: thm list, ideal: thm list} -> declaration val semiring_normalize_conv: Proof.context -> conv val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv @@ -60,6 +65,14 @@ fun merge data = AList.merge Thm.eq_thm (K true) data; ); +fun the_rules ctxt = fst o the o AList.lookup Thm.eq_thm (Data.get (Context.Proof ctxt)) + +val the_semiring = #semiring oo the_rules +val the_ring = #ring oo the_rules +val the_field = #field oo the_rules +val the_idom = #idom oo the_rules +val the_ideal = #ideal oo the_rules + fun match ctxt tm = let fun match_inst @@ -93,7 +106,7 @@ in get_first match_struct (Data.get (Context.Proof ctxt)) end; - (* extra-logical functions *) +(* extra-logical functions *) val semiring_norm_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms semiring_norm}); @@ -145,59 +158,64 @@ val semiringN = "semiring"; val ringN = "ring"; +val fieldN = "field"; val idomN = "idom"; -val idealN = "ideal"; -val fieldN = "field"; -fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), - field = (f_ops, f_rules), idom, ideal} = - Thm.declaration_attribute (fn key => fn context => context |> Data.map - let - val ctxt = Context.proof_of context; +fun declare raw_key raw_entry = fn phi => fn context => + let + val ctxt = Context.proof_of context; + val key = Morphism.thm phi raw_key; + fun morphism_ops_rules (ops, rules) = (map (Morphism.cterm phi) ops, Morphism.fact phi rules); + val (sr_ops, sr_rules) = morphism_ops_rules (#semiring raw_entry); + val (r_ops, r_rules) = morphism_ops_rules (#ring raw_entry); + val (f_ops, f_rules) = morphism_ops_rules (#field raw_entry); + val idom = Morphism.fact phi (#idom raw_entry); + val ideal = Morphism.fact phi (#ideal raw_entry); - fun check kind name xs n = - null xs orelse length xs = n orelse - error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name); - val check_ops = check "operations"; - val check_rules = check "rules"; - - val _ = - check_ops semiringN sr_ops 5 andalso - check_rules semiringN sr_rules 36 andalso - check_ops ringN r_ops 2 andalso - check_rules ringN r_rules 2 andalso - check_ops fieldN f_ops 2 andalso - check_rules fieldN f_rules 2 andalso - check_rules idomN idom 2; + fun check kind name xs n = + null xs orelse length xs = n orelse + error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name); + val check_ops = check "operations"; + val check_rules = check "rules"; + val _ = + check_ops semiringN sr_ops 5 andalso + check_rules semiringN sr_rules 36 andalso + check_ops ringN r_ops 2 andalso + check_rules ringN r_rules 2 andalso + check_ops fieldN f_ops 2 andalso + check_rules fieldN f_rules 2 andalso + check_rules idomN idom 2; - val mk_meta = Local_Defs.meta_rewrite_rule ctxt; - val sr_rules' = map mk_meta sr_rules; - val r_rules' = map mk_meta r_rules; - val f_rules' = map mk_meta f_rules; - - fun rule i = nth sr_rules' (i - 1); + val mk_meta = Local_Defs.meta_rewrite_rule ctxt; + val sr_rules' = map mk_meta sr_rules; + val r_rules' = map mk_meta r_rules; + val f_rules' = map mk_meta f_rules; - val (cx, cy) = Thm.dest_binop (hd sr_ops); - val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; - val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; - val ((clx, crx), (cly, cry)) = - rule 13 |> Thm.rhs_of |> Thm.dest_binop |> apply2 Thm.dest_binop; - val ((ca, cb), (cc, cd)) = - rule 20 |> Thm.lhs_of |> Thm.dest_binop |> apply2 Thm.dest_binop; - val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg; - val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> apply2 Thm.dest_arg; + fun rule i = nth sr_rules' (i - 1); + + val (cx, cy) = Thm.dest_binop (hd sr_ops); + val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; + val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; + val ((clx, crx), (cly, cry)) = + rule 13 |> Thm.rhs_of |> Thm.dest_binop |> apply2 Thm.dest_binop; + val ((ca, cb), (cc, cd)) = + rule 20 |> Thm.lhs_of |> Thm.dest_binop |> apply2 Thm.dest_binop; + val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg; + val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> apply2 Thm.dest_arg; - val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry]; - val semiring = (sr_ops, sr_rules'); - val ring = (r_ops, r_rules'); - val field = (f_ops, f_rules'); - val ideal' = map (Thm.symmetric o mk_meta) ideal - - in - AList.update Thm.eq_thm (key, + val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry]; + + val semiring = (sr_ops, sr_rules'); + val ring = (r_ops, r_rules'); + val field = (f_ops, f_rules'); + val ideal' = map (Thm.symmetric o mk_meta) ideal + + in + context + |> Data.map (AList.update Thm.eq_thm (key, ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal'}, - (if null f_ops then semiring_funs else field_funs))) - end) + (if null f_ops then semiring_funs else field_funs)))) + end (** auxiliary **) @@ -849,46 +867,4 @@ fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord; - -(** Isar setup **) - -local - -fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K (); - -val opsN = "ops"; -val rulesN = "rules"; - -val delN = "del"; - -val any_keyword = - keyword2 semiringN opsN || keyword2 semiringN rulesN || - keyword2 ringN opsN || keyword2 ringN rulesN || - keyword2 fieldN opsN || keyword2 fieldN rulesN || - keyword2 idomN rulesN || keyword2 idealN rulesN; - -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; -val terms = thms >> map Drule.dest_term; - -fun optional scan = Scan.optional scan []; - -in - -val _ = - Theory.setup - (Attrib.setup @{binding normalizer} - (((keyword2 semiringN opsN |-- terms) -- - (keyword2 semiringN rulesN |-- thms)) -- - (optional (keyword2 ringN opsN |-- terms) -- - optional (keyword2 ringN rulesN |-- thms)) -- - (optional (keyword2 fieldN opsN |-- terms) -- - optional (keyword2 fieldN rulesN |-- thms)) -- - optional (keyword2 idomN rulesN |-- thms) -- - optional (keyword2 idealN rulesN |-- thms) - >> (fn ((((sr, r), f), id), idl) => - add {semiring = sr, ring = r, field = f, idom = id, ideal = idl})) - "semiring normalizer data"); - end; - -end;