62 "----------- fun transfer_asms_from_to ---------------------------------------------------------"; |
62 "----------- fun transfer_asms_from_to ---------------------------------------------------------"; |
63 "----------- fun transfer_asms_from_to ---------------------------------------------------------"; |
63 "----------- fun transfer_asms_from_to ---------------------------------------------------------"; |
64 "----------- fun transfer_asms_from_to ---------------------------------------------------------"; |
64 "----------- fun transfer_asms_from_to ---------------------------------------------------------"; |
65 val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"} |
65 val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"} |
66 val from_ctxt = ContextC.insert_assumptions |
66 val from_ctxt = ContextC.insert_assumptions |
67 [TermC.str2term "a < (fro::int)", TermC.str2term "b < (fro::int)"] ctxt |
67 [TermC.parse_test @{context} "a < (fro::int)", TermC.parse_test @{context} "b < (fro::int)"] ctxt |
68 val to_ctxt = ContextC.insert_assumptions |
68 val to_ctxt = ContextC.insert_assumptions |
69 [TermC.str2term "b < (to::int)", TermC.str2term "c < (to::int)"] ctxt |
69 [TermC.parse_test @{context} "b < (to::int)", TermC.parse_test @{context} "c < (to::int)"] ctxt |
70 val new_ctxt = transfer_asms_from_to from_ctxt to_ctxt; |
70 val new_ctxt = transfer_asms_from_to from_ctxt to_ctxt; |
71 if UnparseC.terms_to_strings (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"] |
71 if UnparseC.terms_to_strings (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"] |
72 then () else error "fun transfer_asms_from_to changed" |
72 then () else error "fun transfer_asms_from_to changed" |
73 |
73 |
74 |
74 |
75 "----------- fun avoid_contradict --------------------------------------------------------------"; |
75 "----------- fun avoid_contradict --------------------------------------------------------------"; |
76 "----------- fun avoid_contradict --------------------------------------------------------------"; |
76 "----------- fun avoid_contradict --------------------------------------------------------------"; |
77 "----------- fun avoid_contradict --------------------------------------------------------------"; |
77 "----------- fun avoid_contradict --------------------------------------------------------------"; |
78 val preds = [ |
78 val preds = [ |
79 (*0.pre*)TermC.str2term "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x", |
79 (*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", |
80 (*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" |
80 (*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" |
81 (*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"), |
81 (*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"), |
82 (*0.asm*)TermC.str2term "x \<noteq> 0", (* <-------------- "x \<noteq> 0" would contradict "x = 0" ---\*) |
82 (*0.asm*)TermC.parse_test @{context} "x \<noteq> 0", (* <-------------- "x \<noteq> 0" would contradict "x = 0" ---\*) |
83 (*0.asm*)TermC.str2term "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0" |
83 (*0.asm*)TermC.parse_test @{context} "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0" |
84 ]; |
84 ]; |
85 |
85 |
86 val t = TermC.str2term "[x = 0, x = 6 / 5]"; |
86 val t = TermC.parse_test @{context} "[x = 0, x = 6 / 5]"; |
87 val (t', for_asm) = avoid_contradict t preds; |
87 val (t', for_asm) = avoid_contradict t preds; |
88 if UnparseC.term t' = "[x = 6 / 5]" andalso map UnparseC.term for_asm = ["x = 6 / 5"] |
88 if UnparseC.term t' = "[x = 6 / 5]" andalso map UnparseC.term for_asm = ["x = 6 / 5"] |
89 then () else error "avoid_contradict [x = 0, x = 6 / 5] CHANGED"; |
89 then () else error "avoid_contradict [x = 0, x = 6 / 5] CHANGED"; |
90 |
90 |
91 val t = TermC.str2term "x = 0"; |
91 val t = TermC.parse_test @{context} "x = 0"; |
92 val (t', for_asm) = avoid_contradict t preds; |
92 val (t', for_asm) = avoid_contradict t preds; |
93 if UnparseC.term t' = "bool_undef" andalso map UnparseC.term for_asm = [] |
93 if UnparseC.term t' = "bool_undef" andalso map UnparseC.term for_asm = [] |
94 then () else error "avoid_contradict x = 0 CHANGED"; (* "x \<noteq> 0" in preds *) |
94 then () else error "avoid_contradict x = 0 CHANGED"; (* "x \<noteq> 0" in preds *) |
95 |
95 |
96 val t = TermC.str2term "x = 1"; |
96 val t = TermC.parse_test @{context} "x = 1"; |
97 val (t', for_asm) = avoid_contradict t preds; |
97 val (t', for_asm) = avoid_contradict t preds; |
98 if UnparseC.term t' = "x = 1" andalso map UnparseC.term for_asm = ["x = 1"] |
98 if UnparseC.term t' = "x = 1" andalso map UnparseC.term for_asm = ["x = 1"] |
99 then () else error "avoid_contradict x = 1 CHANGED"; (* "x \<noteq> 1" NOT in preds *) |
99 then () else error "avoid_contradict x = 1 CHANGED"; (* "x \<noteq> 1" NOT in preds *) |
100 |
100 |
101 val t = TermC.str2term "a + b"; |
101 val t = TermC.parse_test @{context} "a + b"; |
102 val (t', for_asm) = avoid_contradict t preds; |
102 val (t', for_asm) = avoid_contradict t preds; |
103 if UnparseC.term t' = "a + b" andalso map UnparseC.term for_asm = [] |
103 if UnparseC.term t' = "a + b" andalso map UnparseC.term for_asm = [] |
104 then () else error "avoid_contradict a + b CHANGED"; (* NOT a predicate *) |
104 then () else error "avoid_contradict a + b CHANGED"; (* NOT a predicate *) |
105 |
105 |
106 val t = TermC.str2term "[a + b]"; |
106 val t = TermC.parse_test @{context} "[a + b]"; |
107 val (t', for_asm) = avoid_contradict t preds; |
107 val (t', for_asm) = avoid_contradict t preds; |
108 if UnparseC.term t' = "[a + b]" andalso map UnparseC.term for_asm = [] |
108 if UnparseC.term t' = "[a + b]" andalso map UnparseC.term for_asm = [] |
109 then () else error "avoid_contradict [a + b] CHANGED"; (* NOT a predicate *) |
109 then () else error "avoid_contradict [a + b] CHANGED"; (* NOT a predicate *) |
110 |
110 |
111 |
111 |
113 "----------- fun subpbl_to_caller --------------------------------------------------------------"; |
113 "----------- fun subpbl_to_caller --------------------------------------------------------------"; |
114 "----------- fun subpbl_to_caller --------------------------------------------------------------"; |
114 "----------- fun subpbl_to_caller --------------------------------------------------------------"; |
115 val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"} |
115 val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"} |
116 |
116 |
117 val sub_ctxt = ContextC.insert_assumptions |
117 val sub_ctxt = ContextC.insert_assumptions |
118 [TermC.str2term "a < (fro::int)", TermC.str2term "b < (fro::int)"] ctxt |
118 [TermC.parse_test @{context} "a < (fro::int)", TermC.parse_test @{context} "b < (fro::int)"] ctxt |
119 val prog_res = TermC.str2term "[x_1 = 1, x_2 = (2::int), x_3 = 3]"; |
119 val prog_res = TermC.parse_test @{context} "[x_1 = 1, x_2 = (2::int), x_3 = 3]"; |
120 |
120 |
121 (* NO contradiction ..*) |
121 (* NO contradiction ..*) |
122 val caller_ctxt = ContextC.insert_assumptions |
122 val caller_ctxt = ContextC.insert_assumptions |
123 [TermC.str2term "b < (to::int)", TermC.str2term "c < (to::int)"] ctxt |
123 [TermC.parse_test @{context} "b < (to::int)", TermC.parse_test @{context} "c < (to::int)"] ctxt |
124 val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt; |
124 val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt; |
125 |
125 |
126 if UnparseC.term t = "[x_1 = 1, x_2 = 2, x_3 = 3]" andalso map UnparseC.term (get_assumptions new_ctxt) = |
126 if UnparseC.term t = "[x_1 = 1, x_2 = 2, x_3 = 3]" andalso map UnparseC.term (get_assumptions new_ctxt) = |
127 ["b < fro", "x_1 = 1", "x_2 = 2", "x_3 = 3", "b < to", "c < to"] |
127 ["b < fro", "x_1 = 1", "x_2 = 2", "x_3 = 3", "b < to", "c < to"] |
128 then () else error "fun subpbl_to_caller changed 1"; |
128 then () else error "fun subpbl_to_caller changed 1"; |
129 |
129 |
130 (* a contradiction ..*) |
130 (* a contradiction ..*) |
131 val caller_ctxt = ContextC.insert_assumptions |
131 val caller_ctxt = ContextC.insert_assumptions |
132 [TermC.str2term "b < (to::int)", TermC.str2term "x_2 \<noteq> (2::int)"] ctxt |
132 [TermC.parse_test @{context} "b < (to::int)", TermC.parse_test @{context} "x_2 \<noteq> (2::int)"] ctxt |
133 val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt; |
133 val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt; |
134 |
134 |
135 if UnparseC.term t = "[x_1 = 1, x_3 = 3]" andalso map UnparseC.term (get_assumptions new_ctxt) = |
135 if UnparseC.term t = "[x_1 = 1, x_3 = 3]" andalso map UnparseC.term (get_assumptions new_ctxt) = |
136 ["b < fro", "x_1 = 1", "x_3 = 3", "b < to", "x_2 \<noteq> 2"] |
136 ["b < fro", "x_1 = 1", "x_3 = 3", "b < to", "x_2 \<noteq> 2"] |
137 then () else error "fun subpbl_to_caller changed 2"; |
137 then () else error "fun subpbl_to_caller changed 2"; |