24 "----------- occurs_in -------------------------------------------"; |
24 "----------- occurs_in -------------------------------------------"; |
25 "----------- occurs_in -------------------------------------------"; |
25 "----------- occurs_in -------------------------------------------"; |
26 fun str2term str = (term_of o the o (parse thy )) str; |
26 fun str2term str = (term_of o the o (parse thy )) str; |
27 fun term2s t = Syntax.string_of_term (thy2ctxt thy) t; |
27 fun term2s t = Syntax.string_of_term (thy2ctxt thy) t; |
28 val t = str2term "x"; |
28 val t = str2term "x"; |
29 if occurs_in t t then "OK" else raise error "atools.sml: occurs_in x x -> f"; |
29 if occurs_in t t then "OK" else error "atools.sml: occurs_in x x -> f"; |
30 |
30 |
31 val t = str2term "x occurs_in x"; |
31 val t = str2term "x occurs_in x"; |
32 val SOME (str, t') = eval_occurs_in 0 "Atools.occurs'_in" t 0; |
32 val SOME (str, t') = eval_occurs_in 0 "Atools.occurs'_in" t 0; |
33 if (term2s t') = "x occurs_in x = True" then () |
33 if (term2s t') = "x occurs_in x = True" then () |
34 else raise error "atools.sml: x occurs_in x = True ???"; |
34 else error "atools.sml: x occurs_in x = True ???"; |
35 |
35 |
36 "------- some_occur_in"; |
36 "------- some_occur_in"; |
37 some_occur_in [str2term"c",str2term"c_2"] (str2term"a + b + c"); |
37 some_occur_in [str2term"c",str2term"c_2"] (str2term"a + b + c"); |
38 val t = str2term "some_of [c, c_2, c_3, c_4] occur_in \ |
38 val t = str2term "some_of [c, c_2, c_3, c_4] occur_in \ |
39 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2"; |
39 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2"; |
40 val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0; |
40 val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0; |
41 if term2str t' = |
41 if term2str t' = |
42 "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 =\nTrue" then () |
42 "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 =\nTrue" then () |
43 else raise error "atools.sml: some_occur_in true"; |
43 else error "atools.sml: some_occur_in true"; |
44 |
44 |
45 val t = str2term "some_of [c_3, c_4] occur_in \ |
45 val t = str2term "some_of [c_3, c_4] occur_in \ |
46 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2"; |
46 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2"; |
47 val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0; |
47 val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0; |
48 if term2str t' = |
48 if term2str t' = |
49 "some_of [c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then () |
49 "some_of [c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then () |
50 else raise error "atools.sml: some_occur_in false"; |
50 else error "atools.sml: some_occur_in false"; |
51 |
51 |
52 |
52 |
53 "----------- argument_of -----------------------------------------"; |
53 "----------- argument_of -----------------------------------------"; |
54 "----------- argument_of -----------------------------------------"; |
54 "----------- argument_of -----------------------------------------"; |
55 "----------- argument_of -----------------------------------------"; |
55 "----------- argument_of -----------------------------------------"; |
56 val t = str2term "argument_in (M_b x)"; |
56 val t = str2term "argument_in (M_b x)"; |
57 val SOME (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0; |
57 val SOME (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0; |
58 if term2s t' = "(argument_in M_b x) = x" then () |
58 if term2s t' = "(argument_in M_b x) = x" then () |
59 else raise error "atools.sml:(argument_in M_b x) = x ???"; |
59 else error "atools.sml:(argument_in M_b x) = x ???"; |
60 |
60 |
61 "----------- sameFunId -------------------------------------------"; |
61 "----------- sameFunId -------------------------------------------"; |
62 "----------- sameFunId -------------------------------------------"; |
62 "----------- sameFunId -------------------------------------------"; |
63 "----------- sameFunId -------------------------------------------"; |
63 "----------- sameFunId -------------------------------------------"; |
64 val t = str2term "M_b L"; atomty t; |
64 val t = str2term "M_b L"; atomty t; |
89 val (p as Const ("Atools.filter'_sameFunId",_) $ (fid $ _) $ fs) = |
89 val (p as Const ("Atools.filter'_sameFunId",_) $ (fid $ _) $ fs) = |
90 str2term "filter_sameFunId (y' L) \ |
90 str2term "filter_sameFunId (y' L) \ |
91 \[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]"; |
91 \[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]"; |
92 val SOME (str, es) = eval_filter_sameFunId "" "Atools.filter'_sameFunId" p ""; |
92 val SOME (str, es) = eval_filter_sameFunId "" "Atools.filter'_sameFunId" p ""; |
93 if term2str es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n y x = c + L * x]) =\n[y' x = c + L * x]" then () |
93 if term2str es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n y x = c + L * x]) =\n[y' x = c + L * x]" then () |
94 else raise error "atools.slm diff.behav. in filter_sameFunId"; |
94 else error "atools.slm diff.behav. in filter_sameFunId"; |
95 |
95 |
96 |
96 |
97 "----------- boollist2sum ----------------------------------------"; |
97 "----------- boollist2sum ----------------------------------------"; |
98 "----------- boollist2sum ----------------------------------------"; |
98 "----------- boollist2sum ----------------------------------------"; |
99 "----------- boollist2sum ----------------------------------------"; |
99 "----------- boollist2sum ----------------------------------------"; |
112 _ $ _) = t; |
112 _ $ _) = t; |
113 |
113 |
114 |
114 |
115 val SOME (str, pred) = eval_boollist2sum "" "Atools.boollist2sum" t ""; |
115 val SOME (str, pred) = eval_boollist2sum "" "Atools.boollist2sum" t ""; |
116 if term2str pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then () |
116 if term2str pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then () |
117 else raise error "atools.sml diff.behav. in eval_boollist2sum"; |
117 else error "atools.sml diff.behav. in eval_boollist2sum"; |
118 |
118 |
119 trace_rewrite:=true; |
119 trace_rewrite:=true; |
120 val srls_ = append_rls "srls_..Berechnung-erstSymbolisch" e_rls |
120 val srls_ = append_rls "srls_..Berechnung-erstSymbolisch" e_rls |
121 [Calc ("Atools.boollist2sum", eval_boollist2sum "")]; |
121 [Calc ("Atools.boollist2sum", eval_boollist2sum "")]; |
122 val t = str2term |
122 val t = str2term |
123 "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"; |
123 "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"; |
124 case rewrite_set_ thy false srls_ t of SOME _ => () |
124 case rewrite_set_ thy false srls_ t of SOME _ => () |
125 | _ => raise error "atools.sml diff.rewrite boollist2sum"; |
125 | _ => error "atools.sml diff.rewrite boollist2sum"; |
126 trace_rewrite:=false; |
126 trace_rewrite:=false; |
127 |
127 |
128 |
128 |
129 (* use"IsacKnowledge/Atools.ML"; |
129 (* use"IsacKnowledge/Atools.ML"; |
130 use"../smltest/IsacKnowledge/atools.sml"; |
130 use"../smltest/IsacKnowledge/atools.sml"; |