1.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Sun Oct 09 06:53:03 2022 +0200
1.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Sun Oct 09 07:44:22 2022 +0200
1.3 @@ -64,9 +64,9 @@
1.4 "----------- fun transfer_asms_from_to ---------------------------------------------------------";
1.5 val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}
1.6 val from_ctxt = ContextC.insert_assumptions
1.7 - [TermC.str2term "a < (fro::int)", TermC.str2term "b < (fro::int)"] ctxt
1.8 + [TermC.parse_test @{context} "a < (fro::int)", TermC.parse_test @{context} "b < (fro::int)"] ctxt
1.9 val to_ctxt = ContextC.insert_assumptions
1.10 - [TermC.str2term "b < (to::int)", TermC.str2term "c < (to::int)"] ctxt
1.11 + [TermC.parse_test @{context} "b < (to::int)", TermC.parse_test @{context} "c < (to::int)"] ctxt
1.12 val new_ctxt = transfer_asms_from_to from_ctxt to_ctxt;
1.13 if UnparseC.terms_to_strings (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"]
1.14 then () else error "fun transfer_asms_from_to changed"
1.15 @@ -76,34 +76,34 @@
1.16 "----------- fun avoid_contradict --------------------------------------------------------------";
1.17 "----------- fun avoid_contradict --------------------------------------------------------------";
1.18 val preds = [
1.19 -(*0.pre*)TermC.str2term "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
1.20 -(*1.pre*)TermC.str2term ("\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) \<or>\n"
1.21 +(*0.pre*)TermC.parse_test @{context} "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
1.22 +(*1.pre*)TermC.parse_patt_test @{theory} ("\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) \<or>\n"
1.23 (*1.pre*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) is_poly_in x"),
1.24 -(*0.asm*)TermC.str2term "x \<noteq> 0", (* <-------------- "x \<noteq> 0" would contradict "x = 0" ---\*)
1.25 -(*0.asm*)TermC.str2term "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
1.26 +(*0.asm*)TermC.parse_test @{context} "x \<noteq> 0", (* <-------------- "x \<noteq> 0" would contradict "x = 0" ---\*)
1.27 +(*0.asm*)TermC.parse_test @{context} "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
1.28 ];
1.29
1.30 -val t = TermC.str2term "[x = 0, x = 6 / 5]";
1.31 +val t = TermC.parse_test @{context} "[x = 0, x = 6 / 5]";
1.32 val (t', for_asm) = avoid_contradict t preds;
1.33 if UnparseC.term t' = "[x = 6 / 5]" andalso map UnparseC.term for_asm = ["x = 6 / 5"]
1.34 then () else error "avoid_contradict [x = 0, x = 6 / 5] CHANGED";
1.35
1.36 -val t = TermC.str2term "x = 0";
1.37 +val t = TermC.parse_test @{context} "x = 0";
1.38 val (t', for_asm) = avoid_contradict t preds;
1.39 if UnparseC.term t' = "bool_undef" andalso map UnparseC.term for_asm = []
1.40 then () else error "avoid_contradict x = 0 CHANGED"; (* "x \<noteq> 0" in preds *)
1.41
1.42 -val t = TermC.str2term "x = 1";
1.43 +val t = TermC.parse_test @{context} "x = 1";
1.44 val (t', for_asm) = avoid_contradict t preds;
1.45 if UnparseC.term t' = "x = 1" andalso map UnparseC.term for_asm = ["x = 1"]
1.46 then () else error "avoid_contradict x = 1 CHANGED"; (* "x \<noteq> 1" NOT in preds *)
1.47
1.48 -val t = TermC.str2term "a + b";
1.49 +val t = TermC.parse_test @{context} "a + b";
1.50 val (t', for_asm) = avoid_contradict t preds;
1.51 if UnparseC.term t' = "a + b" andalso map UnparseC.term for_asm = []
1.52 then () else error "avoid_contradict a + b CHANGED"; (* NOT a predicate *)
1.53
1.54 -val t = TermC.str2term "[a + b]";
1.55 +val t = TermC.parse_test @{context} "[a + b]";
1.56 val (t', for_asm) = avoid_contradict t preds;
1.57 if UnparseC.term t' = "[a + b]" andalso map UnparseC.term for_asm = []
1.58 then () else error "avoid_contradict [a + b] CHANGED"; (* NOT a predicate *)
1.59 @@ -115,12 +115,12 @@
1.60 val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}
1.61
1.62 val sub_ctxt = ContextC.insert_assumptions
1.63 - [TermC.str2term "a < (fro::int)", TermC.str2term "b < (fro::int)"] ctxt
1.64 -val prog_res = TermC.str2term "[x_1 = 1, x_2 = (2::int), x_3 = 3]";
1.65 + [TermC.parse_test @{context} "a < (fro::int)", TermC.parse_test @{context} "b < (fro::int)"] ctxt
1.66 +val prog_res = TermC.parse_test @{context} "[x_1 = 1, x_2 = (2::int), x_3 = 3]";
1.67
1.68 (* NO contradiction ..*)
1.69 val caller_ctxt = ContextC.insert_assumptions
1.70 - [TermC.str2term "b < (to::int)", TermC.str2term "c < (to::int)"] ctxt
1.71 + [TermC.parse_test @{context} "b < (to::int)", TermC.parse_test @{context} "c < (to::int)"] ctxt
1.72 val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt;
1.73
1.74 if UnparseC.term t = "[x_1 = 1, x_2 = 2, x_3 = 3]" andalso map UnparseC.term (get_assumptions new_ctxt) =
1.75 @@ -129,7 +129,7 @@
1.76
1.77 (* a contradiction ..*)
1.78 val caller_ctxt = ContextC.insert_assumptions
1.79 - [TermC.str2term "b < (to::int)", TermC.str2term "x_2 \<noteq> (2::int)"] ctxt
1.80 + [TermC.parse_test @{context} "b < (to::int)", TermC.parse_test @{context} "x_2 \<noteq> (2::int)"] ctxt
1.81 val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt;
1.82
1.83 if UnparseC.term t = "[x_1 = 1, x_3 = 3]" andalso map UnparseC.term (get_assumptions new_ctxt) =