author  wenzelm 
Sat, 08 May 2010 22:29:44 +0200  
changeset 36771  3e08b6789e66 
parent 36754  5ce217fc769a 
child 36945  9bec62c10714 
permissions  rwrr 
23252  1 
(* Title: HOL/Tools/Groebner_Basis/normalizer.ML 
2 
Author: Amine Chaieb, TU Muenchen 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

3 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

4 
Normalization of expressions in semirings. 
23252  5 
*) 
6 

36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset

7 
signature SEMIRING_NORMALIZER = 
23252  8 
sig 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

9 
type entry 
36703
6e870d7f32e5
removed former algebra presimpset from signature
haftmann
parents:
36702
diff
changeset

10 
val get: Proof.context > (thm * entry) list 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

11 
val match: Proof.context > cterm > entry option 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

12 
val del: attribute 
36711  13 
val add: {semiring: cterm list * thm list, ring: cterm list * thm list, 
14 
field: cterm list * thm list, idom: thm list, ideal: thm list} > attribute 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

15 
val funs: thm > {is_const: morphism > cterm > bool, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

16 
dest_const: morphism > cterm > Rat.rat, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

17 
mk_const: morphism > ctyp > Rat.rat > cterm, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

18 
conv: morphism > Proof.context > cterm > thm} > declaration 
36720  19 
val semiring_funs: thm > declaration 
20 
val field_funs: thm > declaration 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

21 

36711  22 
val semiring_normalize_conv: Proof.context > conv 
23 
val semiring_normalize_ord_conv: Proof.context > (cterm > cterm > bool) > conv 

24 
val semiring_normalize_wrapper: Proof.context > entry > conv 

25 
val semiring_normalize_ord_wrapper: Proof.context > entry 

26 
> (cterm > cterm > bool) > conv 

27 
val semiring_normalizers_conv: cterm list > cterm list * thm list 

28 
> cterm list * thm list > cterm list * thm list > 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

29 
(cterm > bool) * conv * conv * conv > (cterm > cterm > bool) > 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

30 
{add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} 
36711  31 
val semiring_normalizers_ord_wrapper: Proof.context > entry > 
32 
(cterm > cterm > bool) > 

27222  33 
{add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

34 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

35 
val setup: theory > theory 
23252  36 
end 
37 

36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset

38 
structure Semiring_Normalizer: SEMIRING_NORMALIZER = 
23252  39 
struct 
23559  40 

36708  41 
(** data **) 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

42 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

43 
type entry = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

44 
{vars: cterm list, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

45 
semiring: cterm list * thm list, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

46 
ring: cterm list * thm list, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

47 
field: cterm list * thm list, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

48 
idom: thm list, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

49 
ideal: thm list} * 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

50 
{is_const: cterm > bool, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

51 
dest_const: cterm > Rat.rat, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

52 
mk_const: ctyp > Rat.rat > cterm, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

53 
conv: Proof.context > cterm > thm}; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

54 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

55 
structure Data = Generic_Data 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

56 
( 
36705  57 
type T = (thm * entry) list; 
58 
val empty = []; 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

59 
val extend = I; 
36771  60 
fun merge data = AList.merge Thm.eq_thm (K true) data; 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

61 
); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

62 

36705  63 
val get = Data.get o Context.Proof; 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

64 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

65 
fun match ctxt tm = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

66 
let 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

67 
fun match_inst 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

68 
({vars, semiring = (sr_ops, sr_rules), 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

69 
ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal}, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

70 
fns as {is_const, dest_const, mk_const, conv}) pat = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

71 
let 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

72 
fun h instT = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

73 
let 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

74 
val substT = Thm.instantiate (instT, []); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

75 
val substT_cterm = Drule.cterm_rule substT; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

76 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

77 
val vars' = map substT_cterm vars; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

78 
val semiring' = (map substT_cterm sr_ops, map substT sr_rules); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

79 
val ring' = (map substT_cterm r_ops, map substT r_rules); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

80 
val field' = (map substT_cterm f_ops, map substT f_rules); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

81 
val idom' = map substT idom; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

82 
val ideal' = map substT ideal; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

83 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

84 
val result = ({vars = vars', semiring = semiring', 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

85 
ring = ring', field = field', idom = idom', ideal = ideal'}, fns); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

86 
in SOME result end 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

87 
in (case try Thm.match (pat, tm) of 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

88 
NONE => NONE 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

89 
 SOME (instT, _) => h instT) 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

90 
end; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

91 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

92 
fun match_struct (_, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

93 
entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

94 
get_first (match_inst entry) (sr_ops @ r_ops @ f_ops); 
36704  95 
in get_first match_struct (get ctxt) end; 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

96 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

97 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

98 
(* logical content *) 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

99 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

100 
val semiringN = "semiring"; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

101 
val ringN = "ring"; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

102 
val idomN = "idom"; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

103 
val idealN = "ideal"; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

104 
val fieldN = "field"; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

105 

36706  106 
val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm); 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

107 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

108 
fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

109 
field = (f_ops, f_rules), idom, ideal} = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

110 
Thm.declaration_attribute (fn key => fn context => context > Data.map 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

111 
let 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

112 
val ctxt = Context.proof_of context; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

113 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

114 
fun check kind name xs n = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

115 
null xs orelse length xs = n orelse 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

116 
error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

117 
val check_ops = check "operations"; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

118 
val check_rules = check "rules"; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

119 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

120 
val _ = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

121 
check_ops semiringN sr_ops 5 andalso 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

122 
check_rules semiringN sr_rules 37 andalso 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

123 
check_ops ringN r_ops 2 andalso 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

124 
check_rules ringN r_rules 2 andalso 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

125 
check_ops fieldN f_ops 2 andalso 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

126 
check_rules fieldN f_rules 2 andalso 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

127 
check_rules idomN idom 2; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

128 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

129 
val mk_meta = Local_Defs.meta_rewrite_rule ctxt; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

130 
val sr_rules' = map mk_meta sr_rules; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

131 
val r_rules' = map mk_meta r_rules; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

132 
val f_rules' = map mk_meta f_rules; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

133 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

134 
fun rule i = nth sr_rules' (i  1); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

135 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

136 
val (cx, cy) = Thm.dest_binop (hd sr_ops); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

137 
val cz = rule 34 > Thm.rhs_of > Thm.dest_arg > Thm.dest_arg; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

138 
val cn = rule 36 > Thm.rhs_of > Thm.dest_arg > Thm.dest_arg; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

139 
val ((clx, crx), (cly, cry)) = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

140 
rule 13 > Thm.rhs_of > Thm.dest_binop > pairself Thm.dest_binop; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

141 
val ((ca, cb), (cc, cd)) = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

142 
rule 20 > Thm.lhs_of > Thm.dest_binop > pairself Thm.dest_binop; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

143 
val cm = rule 1 > Thm.rhs_of > Thm.dest_arg; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

144 
val (cp, cq) = rule 26 > Thm.lhs_of > Thm.dest_binop > pairself Thm.dest_arg; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

145 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

146 
val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry]; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

147 
val semiring = (sr_ops, sr_rules'); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

148 
val ring = (r_ops, r_rules'); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

149 
val field = (f_ops, f_rules'); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

150 
val ideal' = map (symmetric o mk_meta) ideal 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

151 
in 
36706  152 
AList.delete Thm.eq_thm key #> 
36705  153 
cons (key, ({vars = vars, semiring = semiring, 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

154 
ring = ring, field = field, idom = idom, ideal = ideal'}, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

155 
{is_const = undefined, dest_const = undefined, mk_const = undefined, 
36705  156 
conv = undefined})) 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

157 
end); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

158 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

159 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

160 
(* extralogical functions *) 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

161 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

162 
fun funs raw_key {is_const, dest_const, mk_const, conv} phi = 
36705  163 
Data.map (fn data => 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

164 
let 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

165 
val key = Morphism.thm phi raw_key; 
36706  166 
val _ = AList.defined Thm.eq_thm data key orelse 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

167 
raise THM ("No data entry for structure key", 0, [key]); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

168 
val fns = {is_const = is_const phi, dest_const = dest_const phi, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

169 
mk_const = mk_const phi, conv = conv phi}; 
36706  170 
in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end); 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

171 

36720  172 
fun semiring_funs key = funs key 
173 
{is_const = fn phi => can HOLogic.dest_number o Thm.term_of, 

174 
dest_const = fn phi => fn ct => 

175 
Rat.rat_of_int (snd 

176 
(HOLogic.dest_number (Thm.term_of ct) 

177 
handle TERM _ => error "ring_dest_const")), 

178 
mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT 

179 
(case Rat.quotient_of_rat x of (i, 1) => i  _ => error "int_of_rat: bad int"), 

180 
conv = fn phi => fn _ => Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm}) 

181 
then_conv Simplifier.rewrite (HOL_basic_ss addsimps 

182 
(@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(12)}))}; 

183 

184 
fun field_funs key = 

185 
let 

186 
fun numeral_is_const ct = 

187 
case term_of ct of 

188 
Const (@{const_name Rings.divide},_) $ a $ b => 

189 
can HOLogic.dest_number a andalso can HOLogic.dest_number b 

190 
 Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t 

191 
 t => can HOLogic.dest_number t 

192 
fun dest_const ct = ((case term_of ct of 

193 
Const (@{const_name Rings.divide},_) $ a $ b=> 

194 
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) 

195 
 Const (@{const_name Rings.inverse},_)$t => 

196 
Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t))) 

197 
 t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 

198 
handle TERM _ => error "ring_dest_const") 

199 
fun mk_const phi cT x = 

200 
let val (a, b) = Rat.quotient_of_rat x 

201 
in if b = 1 then Numeral.mk_cnumber cT a 

202 
else Thm.capply 

203 
(Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) 

204 
(Numeral.mk_cnumber cT a)) 

205 
(Numeral.mk_cnumber cT b) 

206 
end 

207 
in funs key 

208 
{is_const = K numeral_is_const, 

209 
dest_const = K dest_const, 

210 
mk_const = mk_const, 

36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36720
diff
changeset

211 
conv = K (K Numeral_Simprocs.field_comp_conv)} 
36720  212 
end; 
213 

214 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

215 

36710  216 
(** auxiliary **) 
25253  217 

218 
fun is_comb ct = 

219 
(case Thm.term_of ct of 

220 
_ $ _ => true 

221 
 _ => false); 

222 

223 
val concl = Thm.cprop_of #> Thm.dest_arg; 

224 

225 
fun is_binop ct ct' = 

226 
(case Thm.term_of ct' of 

227 
c $ _ $ _ => term_of ct aconv c 

228 
 _ => false); 

229 

230 
fun dest_binop ct ct' = 

231 
if is_binop ct ct' then Thm.dest_binop ct' 

232 
else raise CTERM ("dest_binop: bad binop", [ct, ct']) 

233 

234 
fun inst_thm inst = Thm.instantiate ([], inst); 

235 

23252  236 
val dest_numeral = term_of #> HOLogic.dest_number #> snd; 
237 
val is_numeral = can dest_numeral; 

238 

239 
val numeral01_conv = Simplifier.rewrite 

25481  240 
(HOL_basic_ss addsimps [@{thm numeral_1_eq_1}, @{thm numeral_0_eq_0}]); 
23252  241 
val zero1_numeral_conv = 
25481  242 
Simplifier.rewrite (HOL_basic_ss addsimps [@{thm numeral_1_eq_1} RS sym, @{thm numeral_0_eq_0} RS sym]); 
23580
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

243 
fun zerone_conv cv = zero1_numeral_conv then_conv cv then_conv numeral01_conv; 
23252  244 
val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"}, 
245 
@{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, 

246 
@{thm "less_nat_number_of"}]; 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

247 

23252  248 
val nat_add_conv = 
249 
zerone_conv 

250 
(Simplifier.rewrite 

251 
(HOL_basic_ss 

25481  252 
addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps} 
35410  253 
@ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}, 
31790  254 
@{thm add_number_of_left}, @{thm Suc_eq_plus1}] 
25481  255 
@ map (fn th => th RS sym) @{thms numerals})); 
23252  256 

257 
val zeron_tm = @{cterm "0::nat"}; 

258 
val onen_tm = @{cterm "1::nat"}; 

259 
val true_tm = @{cterm "True"}; 

260 

261 

36710  262 
(** normalizing conversions **) 
263 

264 
(* core conversion *) 

265 

30866  266 
fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules) 
23252  267 
(is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) = 
268 
let 

269 

270 
val [pthm_02, pthm_03, pthm_04, pthm_05, pthm_07, pthm_08, 

271 
pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16, 

272 
pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24, 

273 
pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32, 

274 
pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38,pthm_39,pthm_40] = sr_rules; 

275 

276 
val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars; 

277 
val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops; 

278 
val [add_tm, mul_tm, pow_tm] = map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat]; 

279 

280 
val dest_add = dest_binop add_tm 

281 
val dest_mul = dest_binop mul_tm 

282 
fun dest_pow tm = 

283 
let val (l,r) = dest_binop pow_tm tm 

284 
in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm]) 

285 
end; 

286 
val is_add = is_binop add_tm 

287 
val is_mul = is_binop mul_tm 

288 
fun is_pow tm = is_binop pow_tm tm andalso is_numeral(Thm.dest_arg tm); 

289 

290 
val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') = 

291 
(case (r_ops, r_rules) of 

30866  292 
([sub_pat, neg_pat], [neg_mul, sub_add]) => 
23252  293 
let 
294 
val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat) 

295 
val neg_tm = Thm.dest_fun neg_pat 

296 
val dest_sub = dest_binop sub_tm 

297 
val is_sub = is_binop sub_tm 

298 
in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul > concl > Thm.dest_arg, 

299 
sub_add > concl > Thm.dest_arg > Thm.dest_arg) 

30866  300 
end 
301 
 _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm)); 

302 

303 
val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) = 

304 
(case (f_ops, f_rules) of 

305 
([divide_pat, inverse_pat], [div_inv, inv_div]) => 

306 
let val div_tm = funpow 2 Thm.dest_fun divide_pat 

307 
val inv_tm = Thm.dest_fun inverse_pat 

308 
in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm) 

309 
end 

310 
 _ => (TrueI, TrueI, true_tm, true_tm, K false)); 

311 

23252  312 
in fn variable_order => 
313 
let 

314 

315 
(* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible. *) 

316 
(* Also deals with "const * const", but both terms must involve powers of *) 

317 
(* the same variable, or both be constants, or behaviour may be incorrect. *) 

318 

319 
fun powvar_mul_conv tm = 

320 
let 

321 
val (l,r) = dest_mul tm 

322 
in if is_semiring_constant l andalso is_semiring_constant r 

323 
then semiring_mul_conv tm 

324 
else 

325 
((let 

326 
val (lx,ln) = dest_pow l 

327 
in 

328 
((let val (rx,rn) = dest_pow r 

329 
val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29 

330 
val (tm1,tm2) = Thm.dest_comb(concl th1) in 

331 
transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end) 

332 
handle CTERM _ => 

333 
(let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31 

334 
val (tm1,tm2) = Thm.dest_comb(concl th1) in 

335 
transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end) 

336 
handle CTERM _ => 

337 
((let val (rx,rn) = dest_pow r 

338 
val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30 

339 
val (tm1,tm2) = Thm.dest_comb(concl th1) in 

340 
transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end) 

341 
handle CTERM _ => inst_thm [(cx,l)] pthm_32 

342 

343 
)) 

344 
end; 

345 

346 
(* Remove "1 * m" from a monomial, and just leave m. *) 

347 

348 
fun monomial_deone th = 

349 
(let val (l,r) = dest_mul(concl th) in 

350 
if l aconvc one_tm 

351 
then transitive th (inst_thm [(ca,r)] pthm_13) else th end) 

352 
handle CTERM _ => th; 

353 

354 
(* Conversion for "(monomial)^n", where n is a numeral. *) 

355 

356 
val monomial_pow_conv = 

357 
let 

358 
fun monomial_pow tm bod ntm = 

359 
if not(is_comb bod) 

360 
then reflexive tm 

361 
else 

362 
if is_semiring_constant bod 

363 
then semiring_pow_conv tm 

364 
else 

365 
let 

366 
val (lopr,r) = Thm.dest_comb bod 

367 
in if not(is_comb lopr) 

368 
then reflexive tm 

369 
else 

370 
let 

371 
val (opr,l) = Thm.dest_comb lopr 

372 
in 

373 
if opr aconvc pow_tm andalso is_numeral r 

374 
then 

375 
let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34 

376 
val (l,r) = Thm.dest_comb(concl th1) 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

377 
in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r)) 
23252  378 
end 
379 
else 

380 
if opr aconvc mul_tm 

381 
then 

382 
let 

383 
val th1 = inst_thm [(cx,l),(cy,r),(cq,ntm)] pthm_33 

384 
val (xy,z) = Thm.dest_comb(concl th1) 

385 
val (x,y) = Thm.dest_comb xy 

386 
val thl = monomial_pow y l ntm 

387 
val thr = monomial_pow z r ntm 

388 
in transitive th1 (combination (Drule.arg_cong_rule x thl) thr) 

389 
end 

390 
else reflexive tm 

391 
end 

392 
end 

393 
in fn tm => 

394 
let 

395 
val (lopr,r) = Thm.dest_comb tm 

396 
val (opr,l) = Thm.dest_comb lopr 

397 
in if not (opr aconvc pow_tm) orelse not(is_numeral r) 

398 
then raise CTERM ("monomial_pow_conv", [tm]) 

399 
else if r aconvc zeron_tm 

400 
then inst_thm [(cx,l)] pthm_35 

401 
else if r aconvc onen_tm 

402 
then inst_thm [(cx,l)] pthm_36 

403 
else monomial_deone(monomial_pow tm l r) 

404 
end 

405 
end; 

406 

407 
(* Multiplication of canonical monomials. *) 

408 
val monomial_mul_conv = 

409 
let 

410 
fun powvar tm = 

411 
if is_semiring_constant tm then one_tm 

412 
else 

413 
((let val (lopr,r) = Thm.dest_comb tm 

414 
val (opr,l) = Thm.dest_comb lopr 

415 
in if opr aconvc pow_tm andalso is_numeral r then l 

416 
else raise CTERM ("monomial_mul_conv",[tm]) end) 

417 
handle CTERM _ => tm) (* FIXME !? *) 

418 
fun vorder x y = 

419 
if x aconvc y then 0 

420 
else 

421 
if x aconvc one_tm then ~1 

422 
else if y aconvc one_tm then 1 

423 
else if variable_order x y then ~1 else 1 

424 
fun monomial_mul tm l r = 

425 
((let val (lx,ly) = dest_mul l val vl = powvar lx 

426 
in 

427 
((let 

428 
val (rx,ry) = dest_mul r 

429 
val vr = powvar rx 

430 
val ord = vorder vl vr 

431 
in 

432 
if ord = 0 

433 
then 

434 
let 

435 
val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] pthm_15 

436 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

437 
val (tm3,tm4) = Thm.dest_comb tm1 

438 
val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2 

439 
val th3 = transitive th1 th2 

440 
val (tm5,tm6) = Thm.dest_comb(concl th3) 

441 
val (tm7,tm8) = Thm.dest_comb tm6 

442 
val th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8 

443 
in transitive th3 (Drule.arg_cong_rule tm5 th4) 

444 
end 

445 
else 

446 
let val th0 = if ord < 0 then pthm_16 else pthm_17 

447 
val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0 

448 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

449 
val (tm3,tm4) = Thm.dest_comb tm2 

450 
in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) 

451 
end 

452 
end) 

453 
handle CTERM _ => 

454 
(let val vr = powvar r val ord = vorder vl vr 

455 
in 

456 
if ord = 0 then 

457 
let 

458 
val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_18 

459 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

460 
val (tm3,tm4) = Thm.dest_comb tm1 

461 
val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2 

462 
in transitive th1 th2 

463 
end 

464 
else 

465 
if ord < 0 then 

466 
let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19 

467 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

468 
val (tm3,tm4) = Thm.dest_comb tm2 

469 
in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) 

470 
end 

471 
else inst_thm [(ca,l),(cb,r)] pthm_09 

472 
end)) end) 

473 
handle CTERM _ => 

474 
(let val vl = powvar l in 

475 
((let 

476 
val (rx,ry) = dest_mul r 

477 
val vr = powvar rx 

478 
val ord = vorder vl vr 

479 
in if ord = 0 then 

480 
let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21 

481 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

482 
val (tm3,tm4) = Thm.dest_comb tm1 

483 
in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2) 

484 
end 

485 
else if ord > 0 then 

486 
let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22 

487 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

488 
val (tm3,tm4) = Thm.dest_comb tm2 

489 
in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) 

490 
end 

491 
else reflexive tm 

492 
end) 

493 
handle CTERM _ => 

494 
(let val vr = powvar r 

495 
val ord = vorder vl vr 

496 
in if ord = 0 then powvar_mul_conv tm 

497 
else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09 

498 
else reflexive tm 

499 
end)) end)) 

500 
in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r) 

501 
end 

502 
end; 

503 
(* Multiplication by monomial of a polynomial. *) 

504 

505 
val polynomial_monomial_mul_conv = 

506 
let 

507 
fun pmm_conv tm = 

508 
let val (l,r) = dest_mul tm 

509 
in 

510 
((let val (y,z) = dest_add r 

511 
val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37 

512 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

513 
val (tm3,tm4) = Thm.dest_comb tm1 

514 
val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2) 

515 
in transitive th1 th2 

516 
end) 

517 
handle CTERM _ => monomial_mul_conv tm) 

518 
end 

519 
in pmm_conv 

520 
end; 

521 

522 
(* Addition of two monomials identical except for constant multiples. *) 

523 

524 
fun monomial_add_conv tm = 

525 
let val (l,r) = dest_add tm 

526 
in if is_semiring_constant l andalso is_semiring_constant r 

527 
then semiring_add_conv tm 

528 
else 

529 
let val th1 = 

530 
if is_mul l andalso is_semiring_constant(Thm.dest_arg1 l) 

531 
then if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) then 

532 
inst_thm [(ca,Thm.dest_arg1 l),(cm,Thm.dest_arg r), (cb,Thm.dest_arg1 r)] pthm_02 

533 
else inst_thm [(ca,Thm.dest_arg1 l),(cm,r)] pthm_03 

534 
else if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) 

535 
then inst_thm [(cm,l),(ca,Thm.dest_arg1 r)] pthm_04 

536 
else inst_thm [(cm,r)] pthm_05 

537 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

538 
val (tm3,tm4) = Thm.dest_comb tm1 

539 
val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4) 

540 
val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2) 

541 
val tm5 = concl th3 

542 
in 

543 
if (Thm.dest_arg1 tm5) aconvc zero_tm 

544 
then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11) 

545 
else monomial_deone th3 

546 
end 

547 
end; 

548 

549 
(* Ordering on monomials. *) 

550 

551 
fun striplist dest = 

552 
let fun strip x acc = 

553 
((let val (l,r) = dest x in 

554 
strip l (strip r acc) end) 

555 
handle CTERM _ => x::acc) (* FIXME !? *) 

556 
in fn x => strip x [] 

557 
end; 

558 

559 

560 
fun powervars tm = 

561 
let val ptms = striplist dest_mul tm 

562 
in if is_semiring_constant (hd ptms) then tl ptms else ptms 

563 
end; 

564 
val num_0 = 0; 

565 
val num_1 = 1; 

566 
fun dest_varpow tm = 

567 
((let val (x,n) = dest_pow tm in (x,dest_numeral n) end) 

568 
handle CTERM _ => 

569 
(tm,(if is_semiring_constant tm then num_0 else num_1))); 

570 

571 
val morder = 

572 
let fun lexorder l1 l2 = 

573 
case (l1,l2) of 

574 
([],[]) => 0 

575 
 (vps,[]) => ~1 

576 
 ([],vps) => 1 

577 
 (((x1,n1)::vs1),((x2,n2)::vs2)) => 

578 
if variable_order x1 x2 then 1 

579 
else if variable_order x2 x1 then ~1 

580 
else if n1 < n2 then ~1 

581 
else if n2 < n1 then 1 

582 
else lexorder vs1 vs2 

583 
in fn tm1 => fn tm2 => 

584 
let val vdegs1 = map dest_varpow (powervars tm1) 

585 
val vdegs2 = map dest_varpow (powervars tm2) 

33002  586 
val deg1 = fold (Integer.add o snd) vdegs1 num_0 
587 
val deg2 = fold (Integer.add o snd) vdegs2 num_0 

23252  588 
in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1 
589 
else lexorder vdegs1 vdegs2 

590 
end 

591 
end; 

592 

593 
(* Addition of two polynomials. *) 

594 

595 
val polynomial_add_conv = 

596 
let 

597 
fun dezero_rule th = 

598 
let 

599 
val tm = concl th 

600 
in 

601 
if not(is_add tm) then th else 

602 
let val (lopr,r) = Thm.dest_comb tm 

603 
val l = Thm.dest_arg lopr 

604 
in 

605 
if l aconvc zero_tm 

606 
then transitive th (inst_thm [(ca,r)] pthm_07) else 

607 
if r aconvc zero_tm 

608 
then transitive th (inst_thm [(ca,l)] pthm_08) else th 

609 
end 

610 
end 

611 
fun padd tm = 

612 
let 

613 
val (l,r) = dest_add tm 

614 
in 

615 
if l aconvc zero_tm then inst_thm [(ca,r)] pthm_07 

616 
else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_08 

617 
else 

618 
if is_add l 

619 
then 

620 
let val (a,b) = dest_add l 

621 
in 

622 
if is_add r then 

623 
let val (c,d) = dest_add r 

624 
val ord = morder a c 

625 
in 

626 
if ord = 0 then 

627 
let val th1 = inst_thm [(ca,a),(cb,b),(cc,c),(cd,d)] pthm_23 

628 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

629 
val (tm3,tm4) = Thm.dest_comb tm1 

630 
val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4) 

631 
in dezero_rule (transitive th1 (combination th2 (padd tm2))) 

632 
end 

633 
else (* ord <> 0*) 

634 
let val th1 = 

635 
if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24 

636 
else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25 

637 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

638 
in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) 

639 
end 

640 
end 

641 
else (* not (is_add r)*) 

642 
let val ord = morder a r 

643 
in 

644 
if ord = 0 then 

645 
let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_26 

646 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

647 
val (tm3,tm4) = Thm.dest_comb tm1 

648 
val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2 

649 
in dezero_rule (transitive th1 th2) 

650 
end 

651 
else (* ord <> 0*) 

652 
if ord > 0 then 

653 
let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24 

654 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

655 
in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) 

656 
end 

657 
else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27) 

658 
end 

659 
end 

660 
else (* not (is_add l)*) 

661 
if is_add r then 

662 
let val (c,d) = dest_add r 

663 
val ord = morder l c 

664 
in 

665 
if ord = 0 then 

666 
let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_28 

667 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

668 
val (tm3,tm4) = Thm.dest_comb tm1 

669 
val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2 

670 
in dezero_rule (transitive th1 th2) 

671 
end 

672 
else 

673 
if ord > 0 then reflexive tm 

674 
else 

675 
let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25 

676 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

677 
in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) 

678 
end 

679 
end 

680 
else 

681 
let val ord = morder l r 

682 
in 

683 
if ord = 0 then monomial_add_conv tm 

684 
else if ord > 0 then dezero_rule(reflexive tm) 

685 
else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27) 

686 
end 

687 
end 

688 
in padd 

689 
end; 

690 

691 
(* Multiplication of two polynomials. *) 

692 

693 
val polynomial_mul_conv = 

694 
let 

695 
fun pmul tm = 

696 
let val (l,r) = dest_mul tm 

697 
in 

698 
if not(is_add l) then polynomial_monomial_mul_conv tm 

699 
else 

700 
if not(is_add r) then 

701 
let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09 

702 
in transitive th1 (polynomial_monomial_mul_conv(concl th1)) 

703 
end 

704 
else 

705 
let val (a,b) = dest_add l 

706 
val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_10 

707 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

708 
val (tm3,tm4) = Thm.dest_comb tm1 

709 
val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4) 

710 
val th3 = transitive th1 (combination th2 (pmul tm2)) 

711 
in transitive th3 (polynomial_add_conv (concl th3)) 

712 
end 

713 
end 

714 
in fn tm => 

715 
let val (l,r) = dest_mul tm 

716 
in 

717 
if l aconvc zero_tm then inst_thm [(ca,r)] pthm_11 

718 
else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_12 

719 
else if l aconvc one_tm then inst_thm [(ca,r)] pthm_13 

720 
else if r aconvc one_tm then inst_thm [(ca,l)] pthm_14 

721 
else pmul tm 

722 
end 

723 
end; 

724 

725 
(* Power of polynomial (optimized for the monomial and trivial cases). *) 

726 

23580
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

727 
fun num_conv n = 
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

728 
nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n  1))) 
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

729 
> Thm.symmetric; 
23252  730 

731 

732 
val polynomial_pow_conv = 

733 
let 

734 
fun ppow tm = 

735 
let val (l,n) = dest_pow tm 

736 
in 

737 
if n aconvc zeron_tm then inst_thm [(cx,l)] pthm_35 

738 
else if n aconvc onen_tm then inst_thm [(cx,l)] pthm_36 

739 
else 

740 
let val th1 = num_conv n 

741 
val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38 

742 
val (tm1,tm2) = Thm.dest_comb(concl th2) 

743 
val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2)) 

744 
val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3 

745 
in transitive th4 (polynomial_mul_conv (concl th4)) 

746 
end 

747 
end 

748 
in fn tm => 

749 
if is_add(Thm.dest_arg1 tm) then ppow tm else monomial_pow_conv tm 

750 
end; 

751 

752 
(* Negation. *) 

753 

23580
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

754 
fun polynomial_neg_conv tm = 
23252  755 
let val (l,r) = Thm.dest_comb tm in 
756 
if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else 

757 
let val th1 = inst_thm [(cx',r)] neg_mul 

36709  758 
val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1)) 
23252  759 
in transitive th2 (polynomial_monomial_mul_conv (concl th2)) 
760 
end 

761 
end; 

762 

763 

764 
(* Subtraction. *) 

23580
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

765 
fun polynomial_sub_conv tm = 
23252  766 
let val (l,r) = dest_sub tm 
767 
val th1 = inst_thm [(cx',l),(cy',r)] sub_add 

768 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

769 
val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2) 

770 
in transitive th1 (transitive th2 (polynomial_add_conv (concl th2))) 

771 
end; 

772 

773 
(* Conversion from HOL term. *) 

774 

775 
fun polynomial_conv tm = 

23407
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

776 
if is_semiring_constant tm then semiring_add_conv tm 
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

777 
else if not(is_comb tm) then reflexive tm 
23252  778 
else 
779 
let val (lopr,r) = Thm.dest_comb tm 

780 
in if lopr aconvc neg_tm then 

781 
let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r) 

782 
in transitive th1 (polynomial_neg_conv (concl th1)) 

783 
end 

30866  784 
else if lopr aconvc inverse_tm then 
785 
let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r) 

786 
in transitive th1 (semiring_mul_conv (concl th1)) 

787 
end 

23252  788 
else 
789 
if not(is_comb lopr) then reflexive tm 

790 
else 

791 
let val (opr,l) = Thm.dest_comb lopr 

792 
in if opr aconvc pow_tm andalso is_numeral r 

793 
then 

794 
let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r 

795 
in transitive th1 (polynomial_pow_conv (concl th1)) 

796 
end 

30866  797 
else if opr aconvc divide_tm 
798 
then 

799 
let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) 

800 
(polynomial_conv r) 

36709  801 
val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv) 
30866  802 
(Thm.rhs_of th1) 
803 
in transitive th1 th2 

804 
end 

23252  805 
else 
806 
if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm 

807 
then 

808 
let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r) 

809 
val f = if opr aconvc add_tm then polynomial_add_conv 

810 
else if opr aconvc mul_tm then polynomial_mul_conv 

811 
else polynomial_sub_conv 

812 
in transitive th1 (f (concl th1)) 

813 
end 

814 
else reflexive tm 

815 
end 

816 
end; 

817 
in 

818 
{main = polynomial_conv, 

819 
add = polynomial_add_conv, 

820 
mul = polynomial_mul_conv, 

821 
pow = polynomial_pow_conv, 

822 
neg = polynomial_neg_conv, 

823 
sub = polynomial_sub_conv} 

824 
end 

825 
end; 

826 

35410  827 
val nat_exp_ss = 
828 
HOL_basic_ss addsimps (@{thms nat_number} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps}) 

829 
addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]; 

23252  830 

35408  831 
fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS; 
27222  832 

36710  833 

834 
(* various normalizing conversions *) 

835 

30866  836 
fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, 
23407
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

837 
{conv, dest_const, mk_const, is_const}) ord = 
23252  838 
let 
839 
val pow_conv = 

36709  840 
Conv.arg_conv (Simplifier.rewrite nat_exp_ss) 
23252  841 
then_conv Simplifier.rewrite 
842 
(HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34]) 

23330
01c09922ce59
Conversion for computation on constants now depends on the context
chaieb
parents:
23259
diff
changeset

843 
then_conv conv ctxt 
01c09922ce59
Conversion for computation on constants now depends on the context
chaieb
parents:
23259
diff
changeset

844 
val dat = (is_const, conv ctxt, conv ctxt, pow_conv) 
30866  845 
in semiring_normalizers_conv vars semiring ring field dat ord end; 
27222  846 

30866  847 
fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord = 
848 
#main (semiring_normalizers_ord_wrapper ctxt ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal},{conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) ord); 

23252  849 

23407
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

850 
fun semiring_normalize_wrapper ctxt data = 
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

851 
semiring_normalize_ord_wrapper ctxt data simple_cterm_ord; 
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

852 

0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

853 
fun semiring_normalize_ord_conv ctxt ord tm = 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

854 
(case match ctxt tm of 
23252  855 
NONE => reflexive tm 
23407
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

856 
 SOME res => semiring_normalize_ord_wrapper ctxt res ord tm); 
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

857 

0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

858 
fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord; 
23252  859 

36708  860 

861 
(** Isar setup **) 

862 

863 
local 

864 

865 
fun keyword k = Scan.lift (Args.$$$ k  Args.colon) >> K (); 

866 
fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1  Args.$$$ k2  Args.colon) >> K (); 

867 
fun keyword3 k1 k2 k3 = 

868 
Scan.lift (Args.$$$ k1  Args.$$$ k2  Args.$$$ k3  Args.colon) >> K (); 

869 

870 
val opsN = "ops"; 

871 
val rulesN = "rules"; 

872 

873 
val normN = "norm"; 

874 
val constN = "const"; 

875 
val delN = "del"; 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

876 

36708  877 
val any_keyword = 
878 
keyword2 semiringN opsN  keyword2 semiringN rulesN  

879 
keyword2 ringN opsN  keyword2 ringN rulesN  

880 
keyword2 fieldN opsN  keyword2 fieldN rulesN  

881 
keyword2 idomN rulesN  keyword2 idealN rulesN; 

882 

883 
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; 

884 
val terms = thms >> map Drule.dest_term; 

885 

886 
fun optional scan = Scan.optional scan []; 

887 

888 
in 

889 

890 
val setup = 

891 
Attrib.setup @{binding normalizer} 

892 
(Scan.lift (Args.$$$ delN >> K del)  

893 
((keyword2 semiringN opsN  terms)  

894 
(keyword2 semiringN rulesN  thms))  

895 
(optional (keyword2 ringN opsN  terms)  

896 
optional (keyword2 ringN rulesN  thms))  

897 
(optional (keyword2 fieldN opsN  terms)  

898 
optional (keyword2 fieldN rulesN  thms))  

899 
optional (keyword2 idomN rulesN  thms)  

900 
optional (keyword2 idealN rulesN  thms) 

901 
>> (fn ((((sr, r), f), id), idl) => 

902 
add {semiring = sr, ring = r, field = f, idom = id, ideal = idl})) 

903 
"semiring normalizer data"; 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

904 

23252  905 
end; 
36708  906 

907 
end; 