author | wneuper <Walther.Neuper@jku.at> |
Wed, 19 Oct 2022 10:43:04 +0200 | |
changeset 60567 | bb3140a02f3d |
parent 60545 | 30b1475b2295 |
child 60569 | f5454fd2e013 |
permissions | -rw-r--r-- |
walther@59814 | 1 |
(* Title: Interpret/Interpret.thy |
neuper@41905 | 2 |
Author: Walther Neuper 110226 |
neuper@41905 | 3 |
(c) due to copyright terms |
walther@59814 | 4 |
|
walther@59814 | 5 |
Collect all defitions for the Lucas-Interpreter |
walther@59814 | 6 |
*) |
neuper@41905 | 7 |
|
neuper@48761 | 8 |
theory Interpret |
walther@60182 | 9 |
imports Specify.Specify |
neuper@41905 | 10 |
begin |
walther@59737 | 11 |
ML_file istate.sml |
walther@59817 | 12 |
ML_file "sub-problem.sml" |
walther@59916 | 13 |
ML_file "thy-read.sml" |
Walther@60544 | 14 |
ML_file "li-tool.sml" |
walther@59920 | 15 |
ML_file "solve-step.sml" |
walther@59909 | 16 |
ML_file "error-pattern.sml" |
walther@59906 | 17 |
ML_file derive.sml |
wneuper@59594 | 18 |
ML_file "lucas-interpreter.sml" |
walther@59748 | 19 |
ML_file "step-solve.sml" |
walther@60081 | 20 |
|
wneuper@59472 | 21 |
ML \<open> |
walther@60081 | 22 |
local |
wenzelm@60282 | 23 |
val thys_known_sofar = Theory.nodes_of @{theory} |
walther@60182 | 24 |
val isac_thys_known_sofar = take ( |
walther@60182 | 25 |
find_index (curry Context.eq_thy ThyC.last_isabelle_thy) thys_known_sofar, |
walther@60182 | 26 |
thys_known_sofar) |
walther@60182 | 27 |
val isac_names_known_sofar = map Context.theory_name isac_thys_known_sofar |
walther@60081 | 28 |
in |
walther@60182 | 29 |
val compare_dependencies__ThyC = |
walther@60182 | 30 |
if isac_names_known_sofar = ThyC.session_interpret_names @ ThyC.session_specify_names then () |
walther@60182 | 31 |
else raise ERROR "theory dependencies not as anticipated in ThyC" |
walther@60081 | 32 |
end |
walther@59664 | 33 |
\<close> ML \<open> |
walther@59729 | 34 |
\<close> ML \<open> |
Walther@60567 | 35 |
\<close> ML \<open> |
Walther@60567 | 36 |
fun tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ sub $ thmID $ _) = |
Walther@60567 | 37 |
let |
Walther@60567 | 38 |
val tid = HOLogic.dest_string thmID |
Walther@60567 | 39 |
val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub |
Walther@60567 | 40 |
in (Tactic.Rewrite_Inst (sub', (tid, ThmC.thm_from_thy thy tid))) end |
Walther@60567 | 41 |
| tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls $ _) = |
Walther@60567 | 42 |
(Tactic.Rewrite_Set (HOLogic.dest_string rls)) |
Walther@60567 | 43 |
| tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) = |
Walther@60567 | 44 |
let |
Walther@60567 | 45 |
val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub |
Walther@60567 | 46 |
in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end |
Walther@60567 | 47 |
\<close> ML \<open> |
Walther@60567 | 48 |
\<close> ML \<open> |
Walther@60567 | 49 |
\<close> ML \<open> |
wneuper@59472 | 50 |
\<close> |
wneuper@59283 | 51 |
end |