|
walther@59728
|
1 |
(* Title: "MathEngBasic/tactic.sml"
|
|
walther@59728
|
2 |
Author: Walther Neuper
|
|
walther@59728
|
3 |
(c) due to copyright terms
|
|
walther@59728
|
4 |
*)
|
|
walther@59728
|
5 |
|
|
walther@59728
|
6 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59728
|
7 |
"table of contents -----------------------------------------------------------------------------";
|
|
walther@59728
|
8 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59728
|
9 |
"-----------------------------------------------------------------------------------------------";
|
|
Walther@60574
|
10 |
"----------- fun result, fun creates_assms -----------------------------------------------------";
|
|
Walther@60574
|
11 |
"----------- fun subst_adapt_to_type -----------------------------------------------------------";
|
|
walther@59728
|
12 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59728
|
13 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59728
|
14 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@59728
|
15 |
|
|
walther@59728
|
16 |
"----------- fun result, fun creates_assms ---------------------------------------------------";
|
|
walther@59728
|
17 |
"----------- fun result, fun creates_assms ---------------------------------------------------";
|
|
walther@59728
|
18 |
"----------- fun result, fun creates_assms ---------------------------------------------------";
|
|
walther@59728
|
19 |
val thm'' = ("real_mult_div_cancel2", @{thm real_mult_div_cancel2});
|
|
walther@59728
|
20 |
val (f, res) = (@{term "a * x / (b * x) :: real"}, (@{term "a / b :: real"}, [@{term "k \<noteq> (0 :: real)"}]: term list))
|
|
walther@59728
|
21 |
;
|
|
Walther@60509
|
22 |
Rewrite': ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Calc.result -> Tactic.T;
|
|
walther@59852
|
23 |
val tac = Rewrite' ("Diff", "dummy_ord", Rule_Set.empty, true, thm'', f, res)
|
|
walther@59728
|
24 |
;
|
|
Walther@60665
|
25 |
if (Tactic.result ctxt tac |> UnparseC.term_in_ctxt @{context}) = "a / b" then () else error "creates_assms CHANGED";
|
|
Walther@60655
|
26 |
if (Tactic.creates_assms ctxt tac |> UnparseC.terms) = "[\"k \<noteq> 0\"]" then () else error "creates_assms CHANGED";
|
|
Walther@60574
|
27 |
|
|
Walther@60574
|
28 |
|
|
Walther@60574
|
29 |
"----------- fun subst_adapt_to_type -----------------------------------------------------------";
|
|
Walther@60574
|
30 |
"----------- fun subst_adapt_to_type -----------------------------------------------------------";
|
|
Walther@60574
|
31 |
"----------- fun subst_adapt_to_type -----------------------------------------------------------";
|
|
Walther@60574
|
32 |
val subs = ["(''bdv'', x)"];
|
|
Walther@60574
|
33 |
|
|
Walther@60574
|
34 |
val [((Free ("bdv", T1)), Free ("x", T2))] = subst_adapt_to_type ctxt subs;
|
|
Walther@60574
|
35 |
if T1 = HOLogic.realT andalso T2 = HOLogic.realT
|
|
Walther@60574
|
36 |
then () else error "subst_adapt_to_type CHANGED";
|
|
Walther@60574
|
37 |
|