equal
deleted
inserted
replaced
156 qed |
156 qed |
157 |
157 |
158 ML {* |
158 ML {* |
159 local |
159 local |
160 val lhss = |
160 val lhss = |
161 [read_cterm (sign_of (the_context ())) |
161 ["t + u::'a::ring", |
162 ("?t + ?u::'a::ring", TVar (("'z", 0), [])), |
162 "t - u::'a::ring", |
163 read_cterm (sign_of (the_context ())) |
163 "t * u::'a::ring", |
164 ("?t - ?u::'a::ring", TVar (("'z", 0), [])), |
164 "- t::'a::ring"]; |
165 read_cterm (sign_of (the_context ())) |
|
166 ("?t * ?u::'a::ring", TVar (("'z", 0), [])), |
|
167 read_cterm (sign_of (the_context ())) |
|
168 ("- ?t::'a::ring", TVar (("'z", 0), [])) |
|
169 ]; |
|
170 fun proc sg _ t = |
165 fun proc sg _ t = |
171 let val rew = Tactic.prove sg [] [] |
166 let val rew = Tactic.prove sg [] [] |
172 (HOLogic.mk_Trueprop |
167 (HOLogic.mk_Trueprop |
173 (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t)))) |
168 (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t)))) |
174 (fn _ => simp_tac ring_ss 1) |
169 (fn _ => simp_tac ring_ss 1) |
177 in if t' aconv u |
172 in if t' aconv u |
178 then None |
173 then None |
179 else Some rew |
174 else Some rew |
180 end; |
175 end; |
181 in |
176 in |
182 val ring_simproc = mk_simproc "ring" lhss proc; |
177 val ring_simproc = Simplifier.simproc (sign_of (the_context ())) "ring" lhss proc; |
183 end; |
178 end; |
184 *} |
179 *} |
185 |
180 |
186 ML_setup {* Addsimprocs [ring_simproc] *} |
181 ML_setup {* Addsimprocs [ring_simproc] *} |
187 |
182 |