1 (* Title: "BaseDefinitions/rewrite-order.sml"
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------";
10 "-------- check simple terms -------------------------------------------------------------------";
11 "-------- check all 'not >' in trace of Test_simplify on: x + 1 + - 1 * 2 = 0 ------------------";
12 "-----------------------------------------------------------------------------------------------";
13 "-----------------------------------------------------------------------------------------------";
14 "-----------------------------------------------------------------------------------------------";
17 "-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------";
18 "-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------";
19 "-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------";
20 val form = TermC.parse_test @{context} "x + -2 ::real"
21 val Repeat {rew_ord = ("sqrt_right", rew_ord_), erls, ...} = Test_simplify;
22 val ctxt = Proof_Context.init_global @{theory Test};
23 (*Rewrite.trace_on := false; (*true false*)*)
24 (** )val NONE = ( *isa*)
25 (**)val SOME (form', _) = (*isa2*)
26 rewrite_ ctxt rew_ord_ erls true @{thm radd_commute} form;
28 -------------------- code in rew_sub -------------------------------------------------------
30 @{print}{a = "@@@rew_sub.ord.rew: ", perm = TermC.perm lhs rhs, tless = not (tless bdv (t', t))};
31 if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
32 then (trace_eq2 i "not >" thy t t'; raise NO_REWRITE)
33 else (t'', p'', [], true)
35 -------------------- output with Rewrite.trace_on := true; ---------------------------------
36 ## eval asms: "x + -2 = -2 + x"
37 {a = "@@@rew_sub.ord.rew: ", b = true, c = false}
39 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
40 (@{theory Test}, rew_ord_, erls, true, @{thm radd_commute}, form);
42 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
43 (thy, 1, []: Subst.T, rew_ord, erls, bool, thm, term);
45 val (t', asms, _(*lrd*), rew) =
46 rew_sub ctxt i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
47 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct;
48 "~~~~~ fun rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
49 (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
50 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))), ct);
51 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
52 val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)
53 handle Pattern.MATCH => raise NO_REWRITE
54 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
55 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
56 val _ = trace_in2 ctxt i "eval asms" r';
57 val (t'', p'') = (*conditional rewriting*)
58 let val (simpl_p', nofalse) = Rewrite.eval__true ctxt (i + 1) p' bdv rls
61 then (trace_in4 ctxt i "asms accepted" p' simpl_p'; (t',simpl_p'))(* uncond.rew.from above*)
62 else (trace_in5 ctxt i "asms false" p'; raise NO_REWRITE) (* don't go into subtm.of cond*)
64 (*if*) TermC.perm lhs rhs andalso not (tless bdv (t', t)); (*ordered rewriting*)
65 not (tless bdv (t', t)); (*isa = true , isa2 = false*)
66 (tless bdv (t', t)); (*isa = false, isa2 = true*)
68 tless <-- Repeat {rew_ord = ("sqrt_right", rew_ord_), erls, ...} = Test_simplify; ..in Test_Some.thy
69 rew_ord_ <-- sqrt_right false @{theory "Pure"} ..in Test.thy
70 sqrt_right ..in Root.thy
71 CHECK THIS ...(same error as with ^^^^^^^^^tless
72 CHECK THIS ...(same error as with code copied into Test_Some.thy
74 if (sqrt_right false @{theory "Pure"} bdv (t', t)) (*isa = false, isa2 = true*)
75 (** )then error "sqrt_right: special case NOT ok" else (); ( *isa*)
76 (**)then () else error "sqrt_right: special case OK"; (*isa2*)
77 "~~~~~ fun sqrt_right , args:"; val ((pr:bool), thy, (_: subst), tu) =
78 (false, @{theory "Pure"}, bdv, (t', t));
80 "~~~~~ fun term_ord' , args:"; val (pr, _(*thy*), (t, u)) = (pr, thy(***), tu);
81 (*//----------------------------- open local ------------------------------------------------\\* )
83 (*case*) int_ord (size_of_term' t, size_of_term' u) (*of*);
84 val (f, ts) = strip_comb t and (g, us) = strip_comb u
86 (*case*) hd_ord (f, g) (*of*);
88 (**)val GREATER = (*isa*)
89 (** )val LESS = ( *isa2*)
90 terms_ord str pr (ts, us)
91 "~~~~~ and terms_ord , args:"; val (_(*str*), pr, (ts, us)) = (str, pr, (ts, us));
93 list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge")) (ts, us);
94 (*+*)list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order;
95 (*+*)term_ord' pr (ThyC.get_theory "Isac_Knowledge"): term * term -> order;
96 "~~~~~ fun list_ord , args:"; val (elem_ord, (xs, ys)) =
97 ((term_ord' pr (ThyC.get_theory "Isac_Knowledge")), (ts, us));
98 (*+*)UnparseC.terms xs = "[\"- 2\", \"x\"]"; (*isa == ?*)
99 (*+*)UnparseC.terms ys = "[\"x\", \"- 2\"]"; (*isa == ?*)
101 (*case*) int_ord (length xs, length ys) (*of*);
104 dict_ord elem_ord (xs, ys);
105 "~~~~~ fun dict_ord , args:"; val ( elem_ord, (x :: xs, y :: ys)) = (elem_ord, (xs, ys))
107 (*case*) elem_ord (x, y) (*of*);
108 val return = GREATER;
109 ( *\\----------------------------- open local ------------------------------------------------//*)
112 "-------- check simple terms -------------------------------------------------------------------";
113 "-------- check simple terms -------------------------------------------------------------------";
114 "-------- check simple terms -------------------------------------------------------------------";
115 val rew_ord_ = sqrt_right false @{theory "Pure"};
117 if rew_ord_ [] (@{term "1::real"}, @{term "2::real"}) = true then () else error "";
118 if rew_ord_ [] (@{term "3::real"}, @{term "2::real"}) = false then () else error "";
120 if rew_ord_ [] (@{term "-1::real"}, @{term "-2::real"}) = true then () else error "";
121 if rew_ord_ [] (@{term "-3::real"}, @{term "-2::real"}) = false then () else error "";
123 if rew_ord_ [] (@{term "1::real"}, @{term "-1::real"}) = false then () else error "";
124 if rew_ord_ [] (@{term "-1::real"}, @{term "1::real"}) = true then () else error "";
126 if rew_ord_ [] (@{term "x::real"}, @{term "2::real"}) = false then () else error "";
127 if rew_ord_ [] (@{term "3::real"}, @{term "x::real"}) = true then () else error "";
130 "-------- check all 'not >' in trace of Test_simplify on: x + 1 + - 1 * 2 = 0 ------------------";
131 "-------- check all 'not >' in trace of Test_simplify on: x + 1 + - 1 * 2 = 0 ------------------";
132 "-------- check all 'not >' in trace of Test_simplify on: x + 1 + - 1 * 2 = 0 ------------------";
133 (* the rewrite-order for rewriting single theorems in a Rule_Set is taken from
135 val Repeat {rew_ord = ("sqrt_right", rew_ord_), erls, ...} = Test_simplify;
136 (*# rls: Test_simplify on: x + 1 + - 1 * 2 = 0 ..selected "not >:" from trace:*)
138 (*## not >: "x + 1 + - 1 * 2" > "x + 1 + - 1 * 2" *)
139 if rew_ord_ [] (@{term "x + 1 + - 1 * 2::real"}, @{term "x + 1 + - 1 * 2::real"}) = false
140 then () else error "term_ord' 1";
142 (*## not >: "1 + x + - 1 * 2" > "- 1 * 2 + (1 + x)" *)
143 if rew_ord_ [] (@{term "1 + x + - 1 * 2::real"}, @{term "- 1 * 2 + (1 + x)::real"}) = true
144 then () else error "term_ord' 2";
146 (*## not >: "1 + x" > "x + 1" *)
147 if rew_ord_ [] (@{term "1 + x::real"}, @{term "x + 1::real"}) = true
148 then () else error "term_ord' 3";
150 (*## not >: "- 1 * 2" > "2 * - 1" *)
151 if rew_ord_ [] (@{term "- 1 * 2::real"}, @{term "2 * - 1::real"}) = true
152 then () else error "term_ord' 4";
154 (*## not >: "1 + (x + - 2)" > "x + - 2 + 1" *)
155 if rew_ord_ [] (@{term "1 + (x + - 2)::real"}, @{term "x + - 2 + 1::real"}) = true
156 then () else error "term_ord' 5";
158 (*## not >: "x + - 2" > "- 2 + x"*)
159 if rew_ord_ [] (@{term "x + - 2::real"}, @{term "- 2 + x ::real"}) = false
160 then () else error "term_ord' 5a"; (*<<<<<<<<<<<<<<----------------- false in trace isa2*)
162 (*--------------------------------- ordered rew. (NOT) inhibited*)
164 (*## not >: "1 + (-2 + x)" > "-2 + x + 1" *)
165 if rew_ord_ [] (@{term "1 + (-2 + x)::real"}, @{term "-2 + x + 1::real"}) = true
166 then () else error "term_ord' 6";
168 (*## not >: "- 2 + x" > "x + - 2" *)
169 if rew_ord_ [] (@{term "- 2 + x::real"}, @{term "x + - 2::real"}) = true
170 then () else error "term_ord' 7";
172 (*## not >: "- 2 + (1 + x)" > "1 + (- 2 + x)" *)
173 if rew_ord_ [] (@{term "- 2 + (1 + x)::real"}, @{term "1 + (- 2 + x)::real"}) = true
174 then () else error "term_ord' 8";
176 (*## not > "- 1 + x" > "x + - 1" *)
177 if rew_ord_ [] (@{term "- 1 + x::real"}, @{term "x + - 1::real"}) = true
178 then () else error "term_ord' 9";