--- 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 \<open>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 = []}\<close>
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 \<open>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 = []}\<close>
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 \<open>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 = []}\<close>
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 \<open>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}}\<close>
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 \<open>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}}\<close>
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 \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
--- 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;