(* 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