59 here we partly check consistency libisabelle/Isac -- Isabelle/Isac: *) |
59 here we partly check consistency libisabelle/Isac -- Isabelle/Isac: *) |
60 Protocol.Protocol |
60 Protocol.Protocol |
61 |
61 |
62 begin |
62 begin |
63 |
63 |
64 text {* |
64 text \<open> |
65 show theory dependencies using the graph browser, |
65 show theory dependencies using the graph browser, |
66 open "browser_info/HOL/Isac/session.graph" |
66 open "browser_info/HOL/Isac/session.graph" |
67 and proceed from the ancestors towards the siblings. |
67 and proceed from the ancestors towards the siblings. |
68 *} |
68 \<close> |
69 |
69 |
70 section {*check presence of definitions from directories*} |
70 section \<open>check presence of definitions from directories\<close> |
71 |
71 |
72 (*declare [[ML_print_depth = 999]]*) |
72 (*declare [[ML_print_depth = 999]]*) |
73 ML {* |
73 ML \<open> |
74 *} ML {* |
74 \<close> ML \<open> |
75 *} |
75 \<close> |
76 |
76 |
77 (*============================================================================================== |
77 (*============================================================================================== |
78 The test below from calculate.sml raises an exception with the cleaned Rewrite. |
78 The test below from calculate.sml raises an exception with the cleaned Rewrite. |
79 The differences to the working 'fun rewrite' are that significant, |
79 The differences to the working 'fun rewrite' are that significant, |
80 that we want to rely on 'hg revert'. |
80 that we want to rely on 'hg revert'. |
81 For that purpose we save this changeset with a broken 'fun rewrite' and tests not running. |
81 For that purpose we save this changeset with a broken 'fun rewrite' and tests not running. |
82 *) |
82 *) |
83 ML {* |
83 ML \<open> |
84 *} ML {* |
84 \<close> ML \<open> |
85 (*--------------(2): does divide work in Test_simplify ?: ------*) |
85 (*--------------(2): does divide work in Test_simplify ?: ------*) |
86 val thy = @{theory Test}; |
86 val thy = @{theory Test}; |
87 val t = (Thm.term_of o the o (TermC.parse thy)) "6 / 2"; |
87 val t = (Thm.term_of o the o (TermC.parse thy)) "6 / 2"; |
88 val rls = Test_simplify; |
88 val rls = Test_simplify; |
89 *} ML {* |
89 \<close> ML \<open> |
90 val (t,_) = the (Rewrite.rewrite_set_ thy false rls t); |
90 val (t,_) = the (Rewrite.rewrite_set_ thy false rls t); |
91 (*val t = Free ("3","Real.real") : term*) |
91 (*val t = Free ("3","Real.real") : term*) |
92 *} ML {* |
92 \<close> ML \<open> |
93 |
93 |
94 (*--------------(3): is_const works ?: -------------------------------------*) |
94 (*--------------(3): is_const works ?: -------------------------------------*) |
95 val t = (Thm.term_of o the o (TermC.parse @{theory})) "2 is_const"; |
95 val t = (Thm.term_of o the o (TermC.parse @{theory})) "2 is_const"; |
96 *} ML {* |
96 \<close> ML \<open> |
97 Rewrite.rewrite_set_ @{theory Test} false tval_rls t; |
97 Rewrite.rewrite_set_ @{theory Test} false tval_rls t; |
98 |
98 |
99 (* exception TERM raised (line 270 of "~~/src/HOL/Tools/hologic.ML"): |
99 (* exception TERM raised (line 270 of "~~/src/HOL/Tools/hologic.ML"): |
100 dest_eq |
100 dest_eq |
101 0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True*) |
101 0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True*) |
102 *} ML {* |
102 \<close> ML \<open> |
103 *} |
103 \<close> |
104 (*==============================================================================================*) |
104 (*==============================================================================================*) |
105 |
105 |
106 ML {* Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *) *} |
106 ML \<open>Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *)\<close> |
107 ML {* Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *) *} |
107 ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close> |
108 ML {* LTool.is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *} |
108 ML \<open>LTool.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\<close> |
109 ML {* Math_Engine.me; (*from "Interpret/mathengine.sml"*) *} |
109 ML \<open>Math_Engine.me; (*from "Interpret/mathengine.sml"*)\<close> |
110 ML {* contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*) *} |
110 ML \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close> |
111 ML {* print_exn_unit *} |
111 ML \<open>print_exn_unit\<close> |
112 ML {* list_rls (*from Atools.thy WN130615??? or ProgLang???*) *} |
112 ML \<open>list_rls (*from Atools.thy WN130615??? or ProgLang???*)\<close> |
113 |
113 |
114 ML {* eval_occurs_in (*from Atools.thy*) *} |
114 ML \<open>eval_occurs_in (*from Atools.thy*)\<close> |
115 ML {* @{thm last_thmI} (*from Atools.thy*) *} |
115 ML \<open>@{thm last_thmI} (*from Atools.thy*)\<close> |
116 ML {*@{thm Querkraft_Belastung}*} |
116 ML \<open>@{thm Querkraft_Belastung}\<close> |
117 |
117 |
118 ML {* Celem.check_guhs_unique := false; *} |
118 ML \<open>Celem.check_guhs_unique := false;\<close> |
119 ML {* writeln "**** isac kernel = math-engine + Knowledge complete ******" *} |
119 ML \<open>writeln "**** isac kernel = math-engine + Knowledge complete ******"\<close> |
120 ML {* @{theory "Isac"} *} |
120 ML \<open>@{theory "Isac"}\<close> |
121 ML {* (*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"] |
121 ML \<open>(*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"] |
122 ERROR: app_py: not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*) *} |
122 ERROR: app_py: not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)\<close> |
123 |
123 |
124 section {* State of approaching Isabelle by Isac *} |
124 section \<open>State of approaching Isabelle by Isac\<close> |
125 text {* |
125 text \<open> |
126 Mathias Lehnfeld gives the following list in his thesis in section |
126 Mathias Lehnfeld gives the following list in his thesis in section |
127 4.2.3 Relation to Ongoing Isabelle Development. |
127 4.2.3 Relation to Ongoing Isabelle Development. |
128 *} |
128 \<close> |
129 subsection {* (0) Survey on remaining Unsynchronized.ref *} |
129 subsection \<open>(0) Survey on remaining Unsynchronized.ref\<close> |
130 text {* |
130 text \<open> |
131 REPLACE BY KEStore... (has been overlooked) |
131 REPLACE BY KEStore... (has been overlooked) |
132 calcelems.sml:val rew_ord' = Unsynchronized.ref ... |
132 calcelems.sml:val rew_ord' = Unsynchronized.ref ... |
133 KEEP FOR TRACING |
133 KEEP FOR TRACING |
134 calcelems.sml:val trace_rewrite = Unsynchronized.ref false; |
134 calcelems.sml:val trace_rewrite = Unsynchronized.ref false; |
135 calcelems.sml:val depth = Unsynchronized.ref 99999; |
135 calcelems.sml:val depth = Unsynchronized.ref 99999; |
140 calcelems.sml:val check_guhs_unique = Unsynchronized.ref true; |
140 calcelems.sml:val check_guhs_unique = Unsynchronized.ref true; |
141 KEEP FOR DEMOS |
141 KEEP FOR DEMOS |
142 Knowledge/GCD_Poly_ML.thy: val trace_div = Unsynchronized.ref true; |
142 Knowledge/GCD_Poly_ML.thy: val trace_div = Unsynchronized.ref true; |
143 Knowledge/GCD_Poly_ML.thy: val trace_div_invariant = Unsynchronized.ref false; |
143 Knowledge/GCD_Poly_ML.thy: val trace_div_invariant = Unsynchronized.ref false; |
144 Knowledge/GCD_Poly_ML.thy: val trace_Euclid = Unsynchronized.ref true; |
144 Knowledge/GCD_Poly_ML.thy: val trace_Euclid = Unsynchronized.ref true; |
145 *} |
145 \<close> |
146 subsection {* (1) Exploit parallelism for concurrent session management *} |
146 subsection \<open>(1) Exploit parallelism for concurrent session management\<close> |
147 subsection {* (2) Make Isac’s programming language usable *} |
147 subsection \<open>(2) Make Isac’s programming language usable\<close> |
148 subsection {* (3) Adopt Isabelle’s numeral computation for Isac *} |
148 subsection \<open>(3) Adopt Isabelle’s numeral computation for Isac\<close> |
149 text {* |
149 text \<open> |
150 In 2002 isac already strived for floating point numbers. Since that time |
150 In 2002 isac already strived for floating point numbers. Since that time |
151 isac represents numerals as "Free", see below (*1*). These experiments are |
151 isac represents numerals as "Free", see below (*1*). These experiments are |
152 unsatisfactory with respect to logical soundness. |
152 unsatisfactory with respect to logical soundness. |
153 Since Isabelle now has started to care about floating point numbers, it is high |
153 Since Isabelle now has started to care about floating point numbers, it is high |
154 time to adopt these together with the other numerals. Isabelle2012/13's numerals |
154 time to adopt these together with the other numerals. Isabelle2012/13's numerals |