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