(* Title:  "MathEngBasic/MathEngBasic.thy"

   Author: Walther Neuper 110226

   (c) due to copyright terms

Definitions required for both, for Specify and for the Lucas-Interpreter.

Note (compare \<^ML>\<open>@{theory Know_Store}\<close> cf.03dea0a179d0):

The files ("xxxxx-def.sml") contain definitions required for ML_structure\<open>Ctree\<close>;

they also include minimal code required for other "xxxxx-def.sml" files.

These files have companion files "xxxxx.sml" with all further code,

located at appropriate positions in the file structure.

The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by

appropriate use of polymorphic high order functions.

*)

theory MathEngBasic

  imports "$ISABELLE_ISAC/ProgLang/ProgLang" "$ISABELLE_ISAC/Specify/Input_Descript"

  keywords "problem" "method" :: thy_decl

    and "Author" "Theory_Ref" "Problem_Ref" "Method_Ref" 

    "CAS" "Program" "Given" "Where" "Find" "Relate"

begin

  ML_file thmC.sml

  ML_file problem.sml

  ML_file method.sml

  ML_file rewrite.sml

  ML_file "model-def.sml"

  ML_file "istate-def.sml"

  ML_file "calc-tree-elem.sml"

  ML_file "pre-conds-def.sml"

  ML_file tactic.sml                                     

  ML_file applicable.sml

  ML_file position.sml

  ML_file "specification-def.sml"

  ML_file "ctree-basic.sml"

  ML_file "ctree-access.sml"

  ML_file "ctree-navi.sml"

  ML_file ctree.sml

  ML_file references.sml

  ML_file "state-steps.sml"

  ML_file calculation.sml

ML \<open>

\<close> ML \<open>

fun lev_up [] = raise Ctree.PTREE "lev_up []"

  | lev_up p = (drop_last p);

\<close> ML \<open>

\<close> ML \<open>

open Ctree

\<close> ML \<open> (*postpone after successful test*)

fun parent_node _ [] = (true, [], Rule_Set.Empty)

  | parent_node pt p =

    let

      fun par _ [] = (true, [], Rule_Set.Empty)

        | par pt p =

            if is_pblobj (get_obj I pt p)

            then (true, p, Rule_Set.Empty)

  		      else 

              let

                val ctxt = p |> get_obj g_loc pt |> snd |> the |> snd (*???*)

              in

                case get_obj g_tac pt p of

      				    Tactic.Rewrite_Set rls' => (false, p, get_rls ctxt rls')

      			    | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, get_rls ctxt rls')

      			    | _ => par pt (lev_up p)

              end

    in par pt (lev_up p) end; 

\<close> ML \<open>

\<close>

end