18 "----------- ### thes2file ... Exception- Match raised -----------"; |
18 "----------- ### thes2file ... Exception- Match raised -----------"; |
19 "----------- search for data error in thes2file ------------------"; |
19 "----------- search for data error in thes2file ------------------"; |
20 "----------- thes2file: thy_containing_rls : rls '...' not in ! --"; |
20 "----------- thes2file: thy_containing_rls : rls '...' not in ! --"; |
21 "----------- fun Thm.make_thm ------------------------------------"; |
21 "----------- fun Thm.make_thm ------------------------------------"; |
22 "----------- correct theIDs for Rule_Set.empty -------------------"; |
22 "----------- correct theIDs for Rule_Set.empty -------------------"; |
23 "----------- fun revert_sym --------------------------------------"; |
23 "----------- fun revert_sym_rule --------------------------------------"; |
24 "----------- fun thms_of_rlss ------------------------------------"; |
24 "----------- fun thms_of_rlss ------------------------------------"; |
25 "----------- repair thydata2xml for rls --------------------------"; |
25 "----------- repair thydata2xml for rls --------------------------"; |
26 "-----------------------------------------------------------------"; |
26 "-----------------------------------------------------------------"; |
27 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy"; |
27 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy"; |
28 "----------- ..CONTINUED: we adapt some required MINIfunctions ---"; |
28 "----------- ..CONTINUED: we adapt some required MINIfunctions ---"; |
39 (*WN160112 WE REPLACED vvv BY "fun thms_of" in src/../thy-hierarchy.sml |
39 (*WN160112 WE REPLACED vvv BY "fun thms_of" in src/../thy-hierarchy.sml |
40 val ths = MutabelleExtra.thms_of false @{theory Biegelinie}; |
40 val ths = MutabelleExtra.thms_of false @{theory Biegelinie}; |
41 (*val it = |
41 (*val it = |
42 ["Q' ?x = - qq ?x", "- qq ?x = Q' ?x", "\<not> ?a =!= 0 \<Longrightarrow> (?a * ?f ?x = ?b) = (?f ?x = 1 / ?a * ?b)", |
42 ["Q' ?x = - qq ?x", "- qq ?x = Q' ?x", "\<not> ?a =!= 0 \<Longrightarrow> (?a * ?f ?x = ?b) = (?f ?x = 1 / ?a * ?b)", |
43 "Q ?x = M_b' ?x", "M_b' ?x = Q ?x", "y'' ?x = - M_b ?x / EI", "M_b ?x = - EI * y'' ?x"]*) |
43 "Q ?x = M_b' ?x", "M_b' ?x = Q ?x", "y'' ?x = - M_b ?x / EI", "M_b ?x = - EI * y'' ?x"]*) |
44 map ThmC.thmID_of_derivation_name' (thms_of thy) = |
44 map ThmC.id_of_thm (thms_of thy) = |
45 ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", |
45 ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", |
46 "Querkraft_Moment", "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] |
46 "Querkraft_Moment", "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] |
47 *) |
47 *) |
48 val thy = @{theory Biegelinie}; |
48 val thy = @{theory Biegelinie}; |
49 val thms = thms_of thy; |
49 val thms = thms_of thy; |
50 if map ThmC.thmID_of_derivation_name' thms = |
50 if map ThmC.id_of_thm thms = |
51 ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", "Querkraft_Moment", |
51 ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", "Querkraft_Moment", |
52 "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] then () |
52 "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] then () |
53 else error "fun thms_of ...changed"; |
53 else error "fun thms_of ...changed"; |
54 |
54 |
55 val without_partial_functions = thms_of @{theory Biegelinie}; |
55 val without_partial_functions = thms_of @{theory Biegelinie}; |
166 (*shows different assignment for "empty"... |
166 (*shows different assignment for "empty"... |
167 : |
167 : |
168 ["IsacScripts", "KEStore", "Rulesets", "empty"], |
168 ["IsacScripts", "KEStore", "Rulesets", "empty"], |
169 :*) |
169 :*) |
170 |
170 |
171 "----------- fun revert_sym --------------------------------------"; |
171 "----------- fun revert_sym_rule --------------------------------------"; |
172 "----------- fun revert_sym --------------------------------------"; |
172 "----------- fun revert_sym_rule --------------------------------------"; |
173 "----------- fun revert_sym --------------------------------------"; |
173 "----------- fun revert_sym_rule --------------------------------------"; |
174 val thy = @{theory Isac_Knowledge} |
174 val thy = @{theory Isac_Knowledge} |
175 val (Thm (thmID, thm)) = ThmC.revert_sym thy |
175 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy |
176 (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym}))) |
176 (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym}))) |
177 ; |
177 ; |
178 if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z" |
178 if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z" |
179 then () else error "fun revert_sym changed 1"; |
179 then () else error "fun revert_sym_rule changed 1"; |
180 |
180 |
181 val (Thm (thmID, thm)) = ThmC.revert_sym thy |
181 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy |
182 (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus})) |
182 (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus})) |
183 ; |
183 ; |
184 if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b" |
184 if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b" |
185 then () else error "fun revert_sym changed 2" |
185 then () else error "fun revert_sym_rule changed 2" |
186 |
186 |
187 "----------- fun thms_of_rlss ------------------------------------"; |
187 "----------- fun thms_of_rlss ------------------------------------"; |
188 "----------- fun thms_of_rlss ------------------------------------"; |
188 "----------- fun thms_of_rlss ------------------------------------"; |
189 "----------- fun thms_of_rlss ------------------------------------"; |
189 "----------- fun thms_of_rlss ------------------------------------"; |
190 val rlss = |
190 val rlss = |
203 (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"), |
203 (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"), |
204 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*) |
204 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*) |
205 |> flat |
205 |> flat |
206 (* = [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"), |
206 (* = [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"), |
207 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]*) |
207 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]*) |
208 |> map (ThmC.revert_sym thy) |
208 |> map (ThmC.revert_sym_rule thy) |
209 (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"), |
209 (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"), |
210 Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*) |
210 Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*) |
211 |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm)) |
211 |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm)) |
212 (* = [("Poly.real_diff_minus", Const ("HOL.Trueprop", "bool \<Rightarrow> prop") $ ..., |
212 (* = [("Poly.real_diff_minus", Const ("HOL.Trueprop", "bool \<Rightarrow> prop") $ ..., |
213 ("Delete.real_mult_minus1", Const ("HOL.Trueprop", ...)] : (string * term) list*) |
213 ("Delete.real_mult_minus1", Const ("HOL.Trueprop", ...)] : (string * term) list*) |