1.1 --- a/TODO.md Sun Oct 09 09:01:29 2022 +0200
1.2 +++ b/TODO.md Wed Oct 19 10:43:04 2022 +0200
1.3 @@ -69,6 +69,9 @@
1.4
1.5 * WN: improve naming in refine.sml, m-match.sml
1.6 * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store›
1.7 +* WN: review Prog_Tac:
1.8 + (*+isa==isa2*)@{term "Substitution []"}; (*Free ("Subproblem",.. ALSO Subproblem, ?!*)
1.9 + (*+isa==isa2*)@{term "Rewrite_Set ''norm_Rational''"}; (*Const ("Prog_Tac.Rewrite_Set",..*)
1.10 * WN: KEStore_Elems.get_thes, add_thes still required for Error_Patterns, we want to eliminate thes:
1.11 (1) Error_Pattern.T are already stored by MethodC -- place them in respective thys
1.12 (2) Error_Pattern.fill_in stored with thm (in thes): instead introduce new Thy_Data for them.
2.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Sun Oct 09 09:01:29 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Wed Oct 19 10:43:04 2022 +0200
2.3 @@ -64,5 +64,7 @@
2.4 ML \<open>
2.5 \<close> ML \<open>
2.6 \<close> ML \<open>
2.7 +\<close> ML \<open>
2.8 +\<close> ML \<open>
2.9 \<close>
2.10 end
3.1 --- a/src/Tools/isac/BaseDefinitions/substitution.sml Sun Oct 09 09:01:29 2022 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/substitution.sml Wed Oct 19 10:43:04 2022 +0200
3.3 @@ -27,7 +27,7 @@
3.4 val T_from_string_eqs: theory -> as_string_eqs -> T
3.5 val T_from_input: Proof.context -> input -> T
3.6
3.7 - val input_to_terms: input -> term list
3.8 + val input_to_terms: Proof.context -> input -> as_eqs
3.9 val eqs_to_input: as_eqs -> as_string_eqs
3.10 val program_to_input: program -> input
3.11 val for_bdv: program -> T -> input option * T
3.12 @@ -78,8 +78,11 @@
3.13 handle TERM _ => raise TERM ("T_from_input: wrong argument " ^ strs2str' input, [])
3.14
3.15 val eqs_to_input = map UnparseC.term;
3.16 -(*TODO: input requires parse _: _ -> _ option*)
3.17 -val input_to_terms = map TermC.str2term;
3.18 +
3.19 +(* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type *)
3.20 +fun input_to_terms ctxt strs = strs
3.21 + |> map (TermC.parse ctxt)
3.22 + |> map (Model_Pattern.adapt_term_to_type ctxt)
3.23
3.24 fun program_to_input sub = (sub
3.25 |> HOLogic.dest_list
4.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Sun Oct 09 09:01:29 2022 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Wed Oct 19 10:43:04 2022 +0200
4.3 @@ -83,7 +83,6 @@
4.4 (*for test/* *)
4.5 (*goal*)val parse_test: Proof.context -> string -> term
4.6 (*goal*)val parse_patt_test: theory -> string -> term
4.7 - val str2term: string -> term (*to be replaced by parse/_patt in src*, by parse/_patt in test/**)
4.8
4.9 val str_of_free_opt: term -> string option
4.10 val str_of_int: int -> string
4.11 @@ -590,7 +589,6 @@
4.12 |>> Proof_Context.init_global
4.13 |-> Proof_Context.read_term_pattern
4.14 |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)
4.15 -fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
4.16
4.17
4.18 fun is_atom (Const _) = true
5.1 --- a/src/Tools/isac/BridgeLibisabelle/mathml.sml Sun Oct 09 09:01:29 2022 +0200
5.2 +++ b/src/Tools/isac/BridgeLibisabelle/mathml.sml Wed Oct 19 10:43:04 2022 +0200
5.3 @@ -67,7 +67,7 @@
5.4 indt (j+i) ^ "<MATHML>\n" ^
5.5 indt (j+2*i) ^ "<ISA> " ^ (decode o UnparseC.term) t ^ " </ISA>\n" ^
5.6 indt (j+i) ^ "</MATHML>";
5.7 -(*val t = str2term "equality e_";
5.8 +(*val t = TermC.parse_test @{context} "equality e_";
5.9 writeln (term2xml 8 t);
5.10 <MATHML>
5.11 <ISA> equality e_ </ISA>
6.1 --- a/src/Tools/isac/Build_Isac.thy Sun Oct 09 09:01:29 2022 +0200
6.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Oct 19 10:43:04 2022 +0200
6.3 @@ -109,10 +109,10 @@
6.4 ML_file istate.sml
6.5 ML_file "sub-problem.sml"
6.6 ML_file "thy-read.sml"
6.7 + ML_file "li-tool.sml"
6.8 ML_file "solve-step.sml"
6.9 ML_file "error-pattern.sml"
6.10 ML_file derive.sml
6.11 - ML_file "li-tool.sml"
6.12 ML_file "lucas-interpreter.sml"
6.13 ML_file "step-solve.sml"
6.14 ( ** ) "Interpret/Interpret"( **)
7.1 --- a/src/Tools/isac/Interpret/Interpret.thy Sun Oct 09 09:01:29 2022 +0200
7.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Wed Oct 19 10:43:04 2022 +0200
7.3 @@ -32,5 +32,20 @@
7.4 end
7.5 \<close> ML \<open>
7.6 \<close> ML \<open>
7.7 +\<close> ML \<open>
7.8 +fun tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ sub $ thmID $ _) =
7.9 + let
7.10 + val tid = HOLogic.dest_string thmID
7.11 + val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub
7.12 + in (Tactic.Rewrite_Inst (sub', (tid, ThmC.thm_from_thy thy tid))) end
7.13 + | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls $ _) =
7.14 + (Tactic.Rewrite_Set (HOLogic.dest_string rls))
7.15 + | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) =
7.16 + let
7.17 + val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub
7.18 + in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end
7.19 +\<close> ML \<open>
7.20 +\<close> ML \<open>
7.21 +\<close> ML \<open>
7.22 \<close>
7.23 end
8.1 --- a/src/Tools/isac/Interpret/li-tool.sml Sun Oct 09 09:01:29 2022 +0200
8.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Oct 19 10:43:04 2022 +0200
8.3 @@ -73,16 +73,19 @@
8.4 | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ sub $ thmID $ _) =
8.5 let
8.6 val tid = HOLogic.dest_string thmID
8.7 - in (Tactic.Rewrite_Inst (Subst.program_to_input sub, (tid, ThmC.thm_from_thy thy tid))) end
8.8 + val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub
8.9 + in (Tactic.Rewrite_Inst (sub', (tid, ThmC.thm_from_thy thy tid))) end
8.10 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls $ _) =
8.11 (Tactic.Rewrite_Set (HOLogic.dest_string rls))
8.12 - | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) =
8.13 - (Tactic.Rewrite_Set_Inst (Subst.program_to_input sub, HOLogic.dest_string rls))
8.14 + | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) =
8.15 + let
8.16 + val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub
8.17 + in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end
8.18 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>, _) $ op_ $ _) =
8.19 (Tactic.Calculate (HOLogic.dest_string op_))
8.20 | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ t) = (Tactic.Take (UnparseC.term t))
8.21 - | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>, _) $ isasub $ _) =
8.22 - (Tactic.Substitute ((Subst.eqs_to_input o TermC.isalist2list) isasub))
8.23 + | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>, _) $ isasub $ _) =
8.24 + Tactic.Substitute (Prog_Tac.Substitute_adapt_to_type thy isasub)
8.25 | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Check_elementwise\<close>, _) $ _ $
8.26 (Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _, pred))) =
8.27 (Tactic.Check_elementwise (UnparseC.term_in_thy thy pred))
8.28 @@ -341,7 +344,7 @@
8.29 else ();
8.30 (*
8.31 check a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr.
8.32 - snd of return value is the formal arguments in case of currying.
8.33 + snd of return value are the formal arguments in case of currying.
8.34 *)
8.35 fun check_leaf call ctxt srls (E, (a, v)) t =
8.36 case Prog_Tac.eval_leaf E a v t of
9.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sun Oct 09 09:01:29 2022 +0200
9.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Oct 19 10:43:04 2022 +0200
9.3 @@ -175,15 +175,16 @@
9.4 then scan_dn cc (ist |> path_down [L, R]) e1
9.5 else scan_dn cc (ist |> path_down [R]) e2
9.6
9.7 - | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t =
9.8 + | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t (*fall-through*) =
9.9 if Tactical.contained_in t
9.10 then raise TERM ("scan_dn expects Prog_Tac or Prog_Expr", [t])
9.11 else
9.12 case LItool.check_leaf "next " ctxt eval (get_subst ist) t of
9.13 (Program.Expr s, _) => Term_Val s (*TODO?: include set_found here and drop those after call*)
9.14 | (Program.Tac prog_tac, form_arg) =>
9.15 - check_tac cc ist (prog_tac, form_arg)
9.16 -
9.17 + (tracing ("### scan_dn fall-through, prog_tac = " ^ quote (UnparseC.term prog_tac) ^ " |");
9.18 +check_tac cc ist (prog_tac, form_arg))
9.19 +
9.20 fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept, ...}) =
9.21 if path = [R] (*root of the program body*) then
9.22 if found_accept then
10.1 --- a/src/Tools/isac/Interpret/solve-step.sml Sun Oct 09 09:01:29 2022 +0200
10.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Wed Oct 19 10:43:04 2022 +0200
10.3 @@ -21,6 +21,7 @@
10.4 val get_eval: string -> Pos.pos' -> Ctree.ctree -> string * ThyC.id * Eval.ml
10.5
10.6 \<^isac_test>\<open>
10.7 + val get_ctxt: Ctree.ctree -> Pos.pos' -> Proof.context
10.8 val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Eval.ml_from_prog list
10.9 \<close>
10.10 end
10.11 @@ -84,6 +85,31 @@
10.12 end
10.13 end;
10.14
10.15 +(** get context reliably at switch_specify_solve **)
10.16 +
10.17 +fun at_begin_program (is, Pos.Res) = last_elem is = 0
10.18 + | at_begin_program _ = false;
10.19 +
10.20 +(* strange special case at Apply_Method *)
10.21 +fun get_ctxt_from_PblObj pt (p_, Pos.Res) =
10.22 + let
10.23 + val pp = Ctree.par_pblobj pt p_ (*drops the "0"*)
10.24 + val {ctxt, ...} = Ctree.get_obj I pt pp |> Ctree.rep_specify_data
10.25 + in ctxt end
10.26 + | get_ctxt_from_PblObj _ _ = raise ERROR "get_ctxt_from_PblObj called by PrfObj or EmptyPtree";
10.27 +
10.28 +fun get_ctxt pt (p_, Pos.Pbl) =
10.29 + let
10.30 + val pp = Ctree.par_pblobj pt p_ (*drops the "0"*)
10.31 + val {ctxt, ...} = Ctree.get_obj I pt pp |> Ctree.rep_specify_data
10.32 + in ctxt end
10.33 + | get_ctxt pt pos =
10.34 + if at_begin_program pos
10.35 + then get_ctxt_from_PblObj pt pos
10.36 + else Ctree.get_ctxt pt pos
10.37 +
10.38 +
10.39 +
10.40 (** Solve_Step.check **)
10.41
10.42 (*
10.43 @@ -94,7 +120,7 @@
10.44 let
10.45 val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
10.46 Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
10.47 - | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
10.48 + | _ => raise ERROR "Solve_Step.check Apply_Method: uncovered case Ctree.get_obj"
10.49 val {where_, ...} = Problem.from_store ctxt pI
10.50 val pres = map (I_Model.environment probl |> subst_atomic) where_
10.51 val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
10.52 @@ -196,7 +222,7 @@
10.53 val thy = Proof_Context.theory_of ctxt
10.54 val f = Calc.current_formula cs;
10.55 val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp)
10.56 - val subte = Subst.input_to_terms sube (*?TODO: input requires parse _: _ -> _ option?*)
10.57 + val subte = Subst.input_to_terms ctxt sube (*?TODO: input requires parse _: _ -> _ option?*)
10.58 val ro = get_rew_ord ctxt rew_ord'
10.59 in
10.60 if foldl and_ (true, map TermC.contains_Var subte)
10.61 @@ -218,7 +244,17 @@
10.62 in
10.63 Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
10.64 end
10.65 - | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
10.66 +(*/----------------- updated----------------------------------* )
10.67 + | check (Tactic.Take str) (pt, pos) =
10.68 + Applicable.Yes (Tactic.Take'
10.69 + (TermC.parse ((*Solve_Step.*)get_ctxt pt pos) str)) (*always applicable*)
10.70 +( *------------------- updated----------------------------------*)
10.71 + | check (Tactic.Take str) (pt, pos) =
10.72 + let
10.73 + val ctxt = (*Solve_Step.*)get_ctxt pt pos
10.74 + val t = Prog_Tac.Take_adapt_to_type ctxt str
10.75 + in Applicable.Yes (Tactic.Take' t) end
10.76 +(*\----------------- updated----------------------------------*)
10.77 | check (Tactic.Begin_Trans) cs =
10.78 Applicable.Yes (Tactic.Begin_Trans' (Calc.current_formula cs))
10.79 | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)
10.80 @@ -327,9 +363,11 @@
10.81 Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete
10.82 in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term t'), pt)
10.83 end
10.84 - | add (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) =
10.85 + | add (Tactic.Tac_ (_, f, id, f')) l (pt, pos as (p, _)) =
10.86 let
10.87 - val (pt, c) = Ctree.cappend_atomic pt p l (TermC.str2term f) (Tactic.Tac id) (TermC.str2term f', []) Ctree.Complete
10.88 + val ctxt = Ctree.get_ctxt pt pos
10.89 + val (pt, c) = Ctree.cappend_atomic pt p l
10.90 + (TermC.parse ctxt f) (Tactic.Tac id) (TermC.parse ctxt f', []) Ctree.Complete
10.91 in
10.92 ((p,Pos.Res), c, Test_Out.FormKF f', pt)
10.93 end
11.1 --- a/src/Tools/isac/Knowledge/Diff.thy Sun Oct 09 09:01:29 2022 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed Oct 19 10:43:04 2022 +0200
11.3 @@ -244,7 +244,7 @@
11.4 (** CAS-commands **)
11.5
11.6 (*.handle cas-input like "Diff (a * x^3 + b, x)".*)
11.7 -(* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)");
11.8 +(* val (t, pairl) = strip_comb (TermC.parse_test @{context} "Diff (a * x^3 + b, x)");
11.9 val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;
11.10 *)
11.11 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =
11.12 @@ -390,7 +390,7 @@
11.13 ML \<open>
11.14
11.15 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
11.16 -(* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)");
11.17 +(* val (t, pairl) = strip_comb (TermC.parse_test @{context} "Differentiate (A = s * (a - s), s)");
11.18 val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;
11.19 *)
11.20 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =
12.1 --- a/src/Tools/isac/Knowledge/Root.thy Sun Oct 09 09:01:29 2022 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Oct 19 10:43:04 2022 +0200
12.3 @@ -69,7 +69,7 @@
12.4 | NONE => NONE)
12.5 | _ => NONE);
12.6
12.7 -(*val (thmid, op_, t as Const(op0,t0) $ arg) = ("", "", str2term "sqrt 0");
12.8 +(*val (thmid, op_, t as Const(op0,t0) $ arg) = ("", "", TermC.parse_test @{context} "sqrt 0");
12.9 > eval_sqrt thmid op_ t thy;
12.10 > val Free (n1,t1) = arg;
12.11 > val SOME ni = int_of_str n1;
13.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Sun Oct 09 09:01:29 2022 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Wed Oct 19 10:43:04 2022 +0200
13.3 @@ -43,7 +43,7 @@
13.4
13.5 (*.function for handling the cas-input "Simplify (2*a + 3*a)":
13.6 make a model which is already in ctree-internal format.*)
13.7 -(* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
13.8 +(* val (h,argl) = strip_comb (TermC.parse_test @{context} "Simplify (2*a + 3*a)");
13.9 val (h,argl) = strip_comb ((Thm.term_of o the o (parse (Thy_Info_get_theory "Simplify")))
13.10 "Simplify (2*a + 3*a)");
13.11 *)
14.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Sun Oct 09 09:01:29 2022 +0200
14.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Oct 19 10:43:04 2022 +0200
14.3 @@ -22,6 +22,9 @@
14.4 datatype ppobj = PblObj of specify_data | PrfObj of solve_data
14.5 datatype ctree = EmptyPtree | Nd of ppobj * ctree list
14.6
14.7 + val rep_solve_data: ppobj -> solve_data
14.8 + val rep_specify_data: ppobj -> specify_data
14.9 +
14.10 (** basic functions **)
14.11 val e_ctree : ctree (* TODO: replace by EmptyPtree*)
14.12 val existpt' : Pos.pos' -> ctree -> bool
14.13 @@ -226,6 +229,11 @@
14.14 type state = ctree * pos'
14.15 val e_state = (EmptyPtree , e_pos')
14.16
14.17 +fun rep_solve_data (PrfObj solve_data) = solve_data
14.18 + | rep_solve_data _ = raise ERROR "rep_solve_data ONLY for solve_data"
14.19 +fun rep_specify_data (PblObj specify_data) = specify_data
14.20 + | rep_specify_data _ = raise ERROR "rep_solve_data ONLY for solve_data"
14.21 +
14.22
14.23 (*** minimal set of functions on Ctree* **)
14.24
15.1 --- a/src/Tools/isac/MathEngine/step.sml Sun Oct 09 09:01:29 2022 +0200
15.2 +++ b/src/Tools/isac/MathEngine/step.sml Wed Oct 19 10:43:04 2022 +0200
15.3 @@ -16,6 +16,7 @@
15.4
15.5 val inconsistent: Subst.input option * ThmC.T -> term -> Istate_Def.T * Proof.context ->
15.6 Pos.pos' -> Ctree.ctree -> Calc.T
15.7 +
15.8 \<^isac_test>\<open>
15.9 val specify_do_next: Calc.T -> string * Calc.state_post
15.10 val switch_specify_solve: Pos.pos_ -> Calc.T -> string * Calc.state_post
16.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Sun Oct 09 09:01:29 2022 +0200
16.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Wed Oct 19 10:43:04 2022 +0200
16.3 @@ -262,18 +262,18 @@
16.4 (*evaluate identity
16.5 > reflI;
16.6 val it = "(?t = ?t) = True"
16.7 -> val t = str2term "x = 0";
16.8 +> val t = TermC.parse_test @{context} "x = 0";
16.9 > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
16.10
16.11 -> val t = str2term "1 = 0";
16.12 +> val t = TermC.parse_test @{context} "1 = 0";
16.13 > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
16.14 ----------- thus needs Rule.Eval !
16.15 -> val t = str2term "0 = 0";
16.16 +> val t = TermC.parse_test @{context} "0 = 0";
16.17 > val SOME (t',_) = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
16.18 > UnparseC.term t';
16.19 val it = \<^const_name>\<open>True\<close>
16.20
16.21 -val t = str2term "Not (x = 0)";
16.22 +val t = TermC.parse_test @{context} "Not (x = 0)";
16.23 atomt t; UnparseC.term t;
16.24 *** -------------
16.25 *** Const ( Not)
16.26 @@ -298,17 +298,17 @@
16.27 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
16.28 | eval_ident _ _ _ _ = NONE;
16.29 (* TODO
16.30 -> val t = str2term "x =!= 0";
16.31 +> val t = TermC.parse_test @{context} "x =!= 0";
16.32 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
16.33 > UnparseC.term t';
16.34 val str = "ident_(x)_(0)" : string
16.35 val it = "(x =!= 0) = False" : string
16.36 -> val t = str2term "1 =!= 0";
16.37 +> val t = TermC.parse_test @{context} "1 =!= 0";
16.38 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
16.39 > UnparseC.term t';
16.40 val str = "ident_(1)_(0)" : string
16.41 val it = "(1 =!= 0) = False" : string
16.42 -> val t = str2term "0 =!= 0";
16.43 +> val t = TermC.parse_test @{context} "0 =!= 0";
16.44 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
16.45 > UnparseC.term t';
16.46 val str = "ident_(0)_(0)" : string
17.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Sun Oct 09 09:01:29 2022 +0200
17.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Oct 19 10:43:04 2022 +0200
17.3 @@ -63,7 +63,11 @@
17.4 val get_first_argument : term -> term option (*TODO rename get_first_argument*)
17.5 val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option
17.6 val is: term -> bool
17.7 -end
17.8 +
17.9 + val Substitute_adapt_to_type: theory -> term -> Subst.as_string_eqs
17.10 +(**)val Rewrite_Inst_adapt_to_type: theory -> term -> TermC.as_string list(**)
17.11 +(**)val Take_adapt_to_type: Proof.context -> TermC.as_string -> term(**)
17.12 +end
17.13 \<close> ML \<open>
17.14 (**)
17.15 structure Prog_Tac(**): PROGAM_TACTIC(**) =
17.16 @@ -208,9 +212,36 @@
17.17 SubProblem, Substitute, Take, Check_elementwise, Assumptions]
17.18
17.19 fun is t = TermC.contains_Const_typeless all_Consts t
17.20 -(**)end(**)
17.21 +
17.22 +
17.23 +(** adapt_to_type arguments of specific tactics **)
17.24 +(*
17.25 + Programs are stored as terms typed by the theory they are defined in.
17.26 + Specific Prog_Tac take substitutions as arguments; these substitutions have
17.27 + the variables to be substituted typed with the program;
17.28 + these variables need to be adapt_to_type from the user-context in order to conform
17.29 + with the terms input by the user.
17.30 +*)
17.31 +fun Substitute_adapt_to_type thy isasub =
17.32 + isasub
17.33 + |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)
17.34 + |> TermC.isalist2list
17.35 + |> Subst.eqs_to_input;
17.36 +
17.37 +fun Rewrite_Inst_adapt_to_type thy sub =
17.38 + sub
17.39 +(*|> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)*)
17.40 + |> Subst.program_to_input
17.41 +
17.42 +(*eliminated ERROR: c_2 = (0 :: 'a)*)
17.43 +fun Take_adapt_to_type ctxt arg = arg
17.44 + |> TermC.parse ctxt
17.45 + |> Model_Pattern.adapt_term_to_type ctxt
17.46 +
17.47 +(**)end(*struct*)
17.48 \<close> ML \<open>
17.49 \<close>
17.50 +
17.51 subsection \<open>TODO\<close>
17.52 ML \<open>
17.53 \<close> ML \<open>
18.1 --- a/src/Tools/isac/Specify/p-spec.sml Sun Oct 09 09:01:29 2022 +0200
18.2 +++ b/src/Tools/isac/Specify/p-spec.sml Wed Oct 19 10:43:04 2022 +0200
18.3 @@ -221,7 +221,7 @@
18.4 => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
18.5 | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"
18.6 val ctxt = Proof_Context.init_global (ThyC.get_theory sdI)
18.7 - in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.str2term hdf))
18.8 + in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.parse ctxt hdf))
18.9 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
18.10 let val (pos_, pits, mits) =
18.11 if dI <> sdI
19.1 --- a/src/Tools/isac/Test_Code/test-code.sml Sun Oct 09 09:01:29 2022 +0200
19.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Wed Oct 19 10:43:04 2022 +0200
19.3 @@ -86,7 +86,7 @@
19.4 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next"
19.5 | _ => raise ERROR "me: uncovered case Step.do_next")
19.6 val tac =
19.7 - case ts of
19.8 + case ts of
19.9 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
19.10 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
19.11 in
20.1 --- a/test/Tools/isac/BaseDefinitions/substitution.sml Sun Oct 09 09:01:29 2022 +0200
20.2 +++ b/test/Tools/isac/BaseDefinitions/substitution.sml Wed Oct 19 10:43:04 2022 +0200
20.3 @@ -83,10 +83,9 @@
20.4 "-------- fun input_to_terms -------------------------------------------------";
20.5 "-------- fun input_to_terms -------------------------------------------------";
20.6 "-------- fun input_to_terms -------------------------------------------------";
20.7 -Subst.input_to_terms: Subst.input -> term list;
20.8 val input = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(aaa, bbb + 2)"];
20.9
20.10 -case Subst.input_to_terms input of
20.11 +case Subst.input_to_terms @{context} input of
20.12 [Const (\<^const_name>\<open>Pair\<close>, _) $
20.13 (Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Char\<close>, _) $
20.14 Const (\<^const_name>\<open>False\<close>, _) $ _ $ _ $ _ $ _ $ _ $ _ $ _) $ _) $
21.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Sun Oct 09 09:01:29 2022 +0200
21.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Oct 19 10:43:04 2022 +0200
21.3 @@ -24,13 +24,103 @@
21.4 CalcTreeTEST
21.5 [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
21.6 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
21.7 -val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
21.8 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow> Add_Given "functionTerm (x \<up> 2 + 1)"*)
21.9 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.12 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.13 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.14 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.15 +
21.16 +val (p''',_,f,nxt''',_,pt''') = me nxt p c pt; (*nxt'''= Specify_Method ["diff", "integration"]*)
21.17 +(*/------------------- step into me Specify_Method ["diff", "integration"] -----------------\*)
21.18 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt''');
21.19 + val (pt, p) =
21.20 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
21.21 + case Step.by_tactic tac (pt, p) of
21.22 + ("ok", (_, _, ptp)) => ptp
21.23 +
21.24 +val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) = (*case*)
21.25 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
21.26 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
21.27 + = (p, ((pt, Pos.e_pos'), []));
21.28 + (*if*) Pos.on_calc_end ip (*else*);
21.29 + val (_, probl_id, _) = Calc.references (pt, p);
21.30 +val _ =
21.31 + (*case*) tacis (*of*);
21.32 + (*if*) probl_id = Problem.id_empty (*else*);
21.33 +
21.34 +val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) =
21.35 + Step.switch_specify_solve p_ (pt, ip);
21.36 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
21.37 + (*if*) Pos.on_specification ([], state_pos) (*then*);
21.38 +
21.39 + Step.specify_do_next (pt, input_pos);
21.40 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
21.41 + val (_, (p_', tac)) = Specify.find_next_step ptp
21.42 + val ist_ctxt = Ctree.get_loc pt (p, p_)
21.43 +val Tactic.Apply_Method mI =
21.44 + (*case*) tac (*of*);
21.45 +
21.46 +val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) =
21.47 + LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
21.48 + ist_ctxt (pt, (p, p_'));
21.49 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _)))
21.50 + = ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)),
21.51 + ist_ctxt, (pt, (p, p_')));
21.52 + val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
21.53 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
21.54 + | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
21.55 + val {ppc, ...} = MethodC.from_store ctxt mI;
21.56 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
21.57 + val srls = LItool.get_simplifier (pt, pos)
21.58 + val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
21.59 + (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
21.60 + | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate"
21.61 + val ini = LItool.implicit_take prog env;
21.62 + val pos = start_new_level pos
21.63 +val NONE =
21.64 + (*case*) ini (*of*);
21.65 +
21.66 +val Next_Step (iii, ccc, ttt) = (*case*)
21.67 + LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt (*of*);
21.68 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
21.69 + = (prog, (pt, (lev_dn p, Res)), is, ctxt);
21.70 +
21.71 + (*case*)
21.72 + scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
21.73 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
21.74 + = ((prog, (ptp, ctxt)), (Pstate ist));
21.75 + (*if*) path = [] (*then*);
21.76 +
21.77 +val Accept_Tac (ttt, sss, ccc) =
21.78 + scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
21.79 +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))
21.80 + = (cc, (trans_scan_dn ist), (Program.body_of prog));
21.81 +
21.82 +val Accept_Tac (ttt, sss, ccc) = (*case*)
21.83 + scan_dn cc (ist |> path_down [L, R]) e (*of*);
21.84 +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
21.85 + = (cc, (ist |> path_down [L, R]), e);
21.86 + (*if*) Tactical.contained_in t (*else*);
21.87 +val (Program.Tac prog_tac, form_arg) =
21.88 + (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
21.89 +
21.90 +val Accept_Tac (ttt, sss, ccc) =
21.91 + check_tac cc ist (prog_tac, form_arg);
21.92 +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
21.93 + = (cc, ist, (prog_tac, form_arg));
21.94 + val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
21.95 +val _ =
21.96 + (*case*) m (*of*);
21.97 +
21.98 + (*case*)
21.99 +Solve_Step.check m (pt, p) (*of*);
21.100 +"~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos as (p_, p))) = (m, (pt, p));
21.101 +
21.102 +(*+*)val ([0], Res) = pos; (*<<<-------------------------*)
21.103 +(*-------------------- stop step into me Specify_Method ["diff", "integration"] -------------*)
21.104 +(*\------------------- step into me Specify_Method ["diff", "integration"] -----------------/*)
21.105 +
21.106 +val (p,_,f,nxt,_,pt) = me nxt''' p''' c pt''';
21.107 case nxt of (Apply_Method ["diff", "integration"]) => ()
21.108 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
21.109 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
22.1 --- a/test/Tools/isac/Knowledge/algein.sml Sun Oct 09 09:01:29 2022 +0200
22.2 +++ b/test/Tools/isac/Knowledge/algein.sml Wed Oct 19 10:43:04 2022 +0200
22.3 @@ -107,7 +107,9 @@
22.4 UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)
22.5
22.6 val sube = ["?a1 = (3::real)"];
22.7 -val subte = Subst.input_to_terms sube;
22.8 +(*----------------vvvvvvvvvvvvvv ERROR Unbound schematic variable: ?a1
22.9 + --------------- review together with development of Widerspruch 3 = 77* )
22.10 +val subte = Subst.input_to_terms @{context} sube;
22.11 UnparseC.terms_short subte = "[?a1 = 3]"; (* = true*)
22.12 val subst = Subst.T_from_string_eqs thy sube;
22.13 foldl and_ (true, map TermC.contains_Var subte);
22.14 @@ -119,4 +121,4 @@
22.15 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
22.16 val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';
22.17 *)
22.18 -
22.19 +( *----------------^^^^^^^^^^^^^^ ERROR Unbound schematic variable: ?a1*)
23.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Sun Oct 09 09:01:29 2022 +0200
23.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Wed Oct 19 10:43:04 2022 +0200
23.3 @@ -3,29 +3,27 @@
23.4 (c) due to copyright terms
23.5 *)
23.6
23.7 -"-----------------------------------------------------------------";
23.8 -"table of contents -----------------------------------------------";
23.9 -"-----------------------------------------------------------------";
23.10 -"----------- occur_exactly_in ------------------------------------";
23.11 -"----------- problems --------------------------------------------";
23.12 -"----------- rewrite-order ord_simplify_System -------------------";
23.13 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
23.14 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
23.15 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
23.16 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
23.17 -"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
23.18 -"----------- refine [linear,system]-------------------------------";
23.19 -"----------- refine [2x2,linear,system] search error--------------";
23.20 -(*^^^--- eqsystem-1.sml #####################################################################*)
23.21 -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
23.22 -(*^^^--- eqsystem-1a.sml #####################################################################
23.23 - vvv--- eqsystem-2.sml #####################################################################*)
23.24 -"----------- me [linear,system] ..normalise..top_down_sub..-------";
23.25 -"----------- all systems from Biegelinie -------------------------";
23.26 -"----------- 4x4 systems from Biegelinie -------------------------";
23.27 -"-----------------------------------------------------------------";
23.28 -"-----------------------------------------------------------------";
23.29 -"-----------------------------------------------------------------";
23.30 +"-----------------------------------------------------------------------------------------------";
23.31 +"table of contents -----------------------------------------------------------------------------";
23.32 +"-----------------------------------------------------------------------------------------------";
23.33 +"----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";
23.34 +"----------- problems -----------------------------------------------------------equsystem-1.sml";
23.35 +"----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";
23.36 +"----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";
23.37 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";
23.38 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";
23.39 +"----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";
23.40 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";
23.41 +"----------- refine [linear,system]----------------------------------------------equsystem-1.sml";
23.42 +"----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";
23.43 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";
23.44 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
23.45 +"----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";
23.46 +"----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";
23.47 +"----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";
23.48 +"-----------------------------------------------------------------------------------------------";
23.49 +"-----------------------------------------------------------------------------------------------";
23.50 +"-----------------------------------------------------------------------------------------------";
23.51
23.52 val thy = @{theory "EqSystem"};
23.53 val ctxt = Proof_Context.init_global thy;
23.54 @@ -176,6 +174,7 @@
23.55 if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"
23.56 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
23.57
23.58 +
23.59 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
23.60 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
23.61 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
23.62 @@ -285,6 +284,8 @@
23.63 \ c + (c_2 + (c_3 + c_4)) = 0]"
23.64 then () else error "eqsystem.sml rewrite in 4x4 order_system";
23.65
23.66 +
23.67 +
23.68 "----------- refine [linear,system]-------------------------------";
23.69 "----------- refine [linear,system]-------------------------------";
23.70 "----------- refine [linear,system]-------------------------------";
23.71 @@ -423,6 +424,8 @@
23.72 val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
23.73 ============ inhibit exn WN120314 ==============================================*)
23.74
23.75 +
23.76 +
23.77 "----------- Refine.refine [2x2,linear,system] search error--------------";
23.78 "----------- Refine.refine [2x2,linear,system] search error--------------";
23.79 "----------- Refine.refine [2x2,linear,system] search error--------------";
23.80 @@ -512,11 +515,12 @@
23.81 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
23.82 *)
23.83
23.84 +
23.85 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
23.86 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
23.87 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
23.88 -val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
23.89 - \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
23.90 +val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
23.91 + "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
23.92 "solveForVars [c, c_2]", "solution LL"];
23.93 val (dI',pI',mI') =
23.94 ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
23.95 @@ -532,7 +536,7 @@
23.96
23.97 val (p,_,f,nxt,_,pt) = me nxt p c pt;
23.98 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
23.99 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*);
23.100 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
23.101 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
23.102 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
23.103 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
23.104 @@ -549,13 +553,6 @@
23.105 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
23.106
23.107 val (p,_,f,nxt,_,pt) = me nxt p c pt;
23.108 -val PblObj {probl,...} = get_obj I pt [5];
23.109 - (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;
23.110 -(*[
23.111 -(1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
23.112 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
23.113 -(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
23.114 -*)
23.115 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
23.116 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
23.117 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
23.118 @@ -569,8 +566,33 @@
23.119 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
23.120 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
23.121 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
23.122 +(* final test ... ----------------------------------------------------------------------------*)
23.123 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
23.124 else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
23.125 +
23.126 case nxt of
23.127 (End_Proof') => ()
23.128 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
23.129 +
23.130 +Test_Tool.show_pt pt (*[
23.131 +(([], Frm), solveSystem
23.132 + [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2],
23.133 + [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]]
23.134 + [[c], [c_2]]),
23.135 +(([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
23.136 + 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]),
23.137 +(([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]),
23.138 +(([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]),
23.139 +(([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]),
23.140 +(([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]),
23.141 +(([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]),
23.142 +(([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2),
23.143 +(([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2),
23.144 +(([5, 2], Res), L * c = q_0 * L \<up> 2 / 2),
23.145 +(([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L),
23.146 +(([5, 4], Res), c = L * q_0 / 2),
23.147 +(([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]),
23.148 +(([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]),
23.149 +(([5], Res), [c = L * q_0 / 2, c_2 = 0]),
23.150 +(([], Res), [c = L * q_0 / 2, c_2 = 0])]
23.151 +*)
24.1 --- a/test/Tools/isac/Knowledge/eqsystem-1a.sml Sun Oct 09 09:01:29 2022 +0200
24.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1a.sml Wed Oct 19 10:43:04 2022 +0200
24.3 @@ -2,34 +2,32 @@
24.4 author: Walther Neuper 050826,
24.5 *)
24.6
24.7 -"-----------------------------------------------------------------";
24.8 -"table of contents -----------------------------------------------";
24.9 -"-----------------------------------------------------------------";
24.10 -"----------- occur_exactly_in ------------------------------------";
24.11 -"----------- problems --------------------------------------------";
24.12 -"----------- rewrite-order ord_simplify_System -------------------";
24.13 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
24.14 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
24.15 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
24.16 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
24.17 -"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
24.18 -"----------- refine [linear,system]-------------------------------";
24.19 -"----------- refine [2x2,linear,system] search error--------------";
24.20 -(*^^^--- eqsystem-1.sml #####################################################################*)
24.21 -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
24.22 -(*^^^--- eqsystem-1a.sml #####################################################################
24.23 - vvv--- eqsystem-2.sml #####################################################################*)
24.24 -"----------- me [linear,system] ..normalise..top_down_sub..-------";
24.25 -"----------- all systems from Biegelinie -------------------------";
24.26 -"----------- 4x4 systems from Biegelinie -------------------------";
24.27 -"-----------------------------------------------------------------";
24.28 -"-----------------------------------------------------------------";
24.29 -"-----------------------------------------------------------------";
24.30 +"-----------------------------------------------------------------------------------------------";
24.31 +"table of contents -----------------------------------------------------------------------------";
24.32 +"-----------------------------------------------------------------------------------------------";
24.33 +"----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";
24.34 +"----------- problems -----------------------------------------------------------equsystem-1.sml";
24.35 +"----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";
24.36 +"----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";
24.37 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";
24.38 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";
24.39 +"----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";
24.40 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";
24.41 +"----------- refine [linear,system]----------------------------------------------equsystem-1.sml";
24.42 +"----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";
24.43 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";
24.44 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
24.45 +"----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";
24.46 +"----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";
24.47 +"----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";
24.48 +"-----------------------------------------------------------------------------------------------";
24.49 +"-----------------------------------------------------------------------------------------------";
24.50 +"-----------------------------------------------------------------------------------------------";
24.51
24.52
24.53 -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
24.54 -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
24.55 -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
24.56 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
24.57 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
24.58 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
24.59 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
24.60 \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
24.61 "solveForVars [c, c_2]", "solution LL"];
25.1 --- a/test/Tools/isac/Knowledge/eqsystem-2.sml Sun Oct 09 09:01:29 2022 +0200
25.2 +++ b/test/Tools/isac/Knowledge/eqsystem-2.sml Wed Oct 19 10:43:04 2022 +0200
25.3 @@ -2,30 +2,27 @@
25.4 author: Walther Neuper 050826,
25.5 (c) due to copyright terms
25.6 *)
25.7 -
25.8 -"-----------------------------------------------------------------";
25.9 -"table of contents -----------------------------------------------";
25.10 -"-----------------------------------------------------------------";
25.11 -"----------- occur_exactly_in ------------------------------------";
25.12 -"----------- problems --------------------------------------------";
25.13 -"----------- rewrite-order ord_simplify_System -------------------";
25.14 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
25.15 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
25.16 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
25.17 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
25.18 -"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
25.19 -"----------- refine [linear,system]-------------------------------";
25.20 -"----------- refine [2x2,linear,system] search error--------------";
25.21 -(*^^^--- eqsystem-1.sml #####################################################################*)
25.22 -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
25.23 -(*^^^--- eqsystem-1a.sml #####################################################################
25.24 - vvv--- eqsystem-2.sml #####################################################################*)
25.25 -"----------- me [linear,system] ..normalise..top_down_sub..-------";
25.26 -"----------- all systems from Biegelinie -------------------------";
25.27 -"----------- 4x4 systems from Biegelinie -------------------------";
25.28 -"-----------------------------------------------------------------";
25.29 -"-----------------------------------------------------------------";
25.30 -"-----------------------------------------------------------------";
25.31 +"-----------------------------------------------------------------------------------------------";
25.32 +"table of contents -----------------------------------------------------------------------------";
25.33 +"-----------------------------------------------------------------------------------------------";
25.34 +"----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";
25.35 +"----------- problems -----------------------------------------------------------equsystem-1.sml";
25.36 +"----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";
25.37 +"----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";
25.38 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";
25.39 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";
25.40 +"----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";
25.41 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";
25.42 +"----------- refine [linear,system]----------------------------------------------equsystem-1.sml";
25.43 +"----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";
25.44 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";
25.45 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
25.46 +"----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";
25.47 +"----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";
25.48 +"----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";
25.49 +"-----------------------------------------------------------------------------------------------";
25.50 +"-----------------------------------------------------------------------------------------------";
25.51 +"-----------------------------------------------------------------------------------------------";
25.52
25.53 val thy = @{theory "EqSystem"};
25.54 val ctxt = Proof_Context.init_global thy;
26.1 --- a/test/Tools/isac/Test_Isac.thy Sun Oct 09 09:01:29 2022 +0200
26.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Oct 19 10:43:04 2022 +0200
26.3 @@ -140,10 +140,11 @@
26.4 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
26.5 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
26.6 "xx"
26.7 -^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**)
26.8 -\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
26.9 -\<close> ML \<open>
26.10 -\<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
26.11 +^ "xxx" (*+*) (*+++*) (* keep for continuation*) (*isa*) (*isa2*) (**)
26.12 +\<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
26.13 + (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
26.14 +(*\\------------------ adhoc inserted n ----------------------------------------------------//*)
26.15 +\<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
26.16 \<close>
26.17 ML \<open>
26.18 \<close> ML \<open>
27.1 --- a/test/Tools/isac/Test_Isac_Short.thy Sun Oct 09 09:01:29 2022 +0200
27.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Oct 19 10:43:04 2022 +0200
27.3 @@ -142,9 +142,10 @@
27.4 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
27.5 "xx"
27.6 ^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**)
27.7 -\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
27.8 -\<close> ML \<open>
27.9 -\<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
27.10 +\<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
27.11 + (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
27.12 +(*\\------------------ adhoc inserted n ----------------------------------------------------//*)
27.13 +\<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
27.14 \<close>
27.15 ML \<open>
27.16 \<close> ML \<open>
27.17 @@ -299,7 +300,7 @@
27.18 ML_file "Knowledge/eqsystem-1a.sml"
27.19 ML_file "Knowledge/eqsystem-2.sml"
27.20 ML_file "Knowledge/test.sml"
27.21 - ML_file "Knowledge/polyminus.sml"
27.22 + ML_file "Knowledge/polyminus.sml"
27.23 ML_file "Knowledge/vect.sml"
27.24 ML_file "Knowledge/diff-app.sml" (* postponed to dev. specification | TP-prog. *)
27.25 ML_file "Knowledge/biegelinie-1.sml"
28.1 --- a/test/Tools/isac/Test_Some.thy Sun Oct 09 09:01:29 2022 +0200
28.2 +++ b/test/Tools/isac/Test_Some.thy Wed Oct 19 10:43:04 2022 +0200
28.3 @@ -57,30 +57,31 @@
28.4 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
28.5 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
28.6 "xx"
28.7 -^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**)
28.8 -\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
28.9 -\<close> ML \<open>
28.10 -\<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
28.11 -\<close> ML \<open> (*//---------------- adhoc copied up -----------------------------------------------\\*)
28.12 -\<close> ML \<open>
28.13 -\<close> ML \<open> (*\\---------------- adhoc copied up -----------------------------------------------//*)
28.14 -(*/------------------- step into XXXXX -----------------------------------------------------\*)
28.15 -(*-------------------- stop step into XXXXX -------------------------------------------------*)
28.16 -(*\------------------- step into XXXXX -----------------------------------------------------/*)
28.17 -(*-------------------- contiue step into XXXXX ----------------------------------------------*)
28.18 -(*/------------------- check entry to XXXXX ------------------------------------------------\*)
28.19 -(*\------------------- check entry to XXXXX ------------------------------------------------/*)
28.20 -(*/------------------- check within XXXXX --------------------------------------------------\*)
28.21 -(*\------------------- check within XXXXX --------------------------------------------------/*)
28.22 -(*/------------------- check result of XXXXX -----------------------------------------------\*)
28.23 -(*\------------------- check result of XXXXX -----------------------------------------------/*)
28.24 -(* final test ...*)
28.25 -(*/------------------- build new fun XXXXX -------------------------------------------------\*)
28.26 -(*\------------------- build new fun XXXXX -------------------------------------------------/*)
28.27 -(**** chapter ############################################################################ ****)
28.28 -(*** section ============================================================================== ***)
28.29 -(** subsection ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ **)
28.30 -(* subsubsection ............................................................................ *)
28.31 +^ "xxx" (*+*) (*+++*) (* keep for continuation*) (*isa*) (*isa2*) (**)
28.32 +\<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
28.33 + (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
28.34 +(*\\------------------ adhoc inserted n ----------------------------------------------------//*)
28.35 +\<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
28.36 +
28.37 +\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
28.38 +(*//------------------ step into XXXXX -----------------------------------------------------\\*)
28.39 +(*-------------------- stop step into XXXXX --------------------------------------------------*)
28.40 +\<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)
28.41 +(*\\------------------ step into XXXXX -----------------------------------------------------//*)
28.42 +\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
28.43 +
28.44 +(*/------------------- check entry to XXXXX -------------------------------------------------\*)
28.45 +(*\------------------- check entry to XXXXX -------------------------------------------------/*)
28.46 +(*/------------------- check within XXXXX ---------------------------------------------------\*)
28.47 +(*\------------------- check within XXXXX ---------------------------------------------------/*)
28.48 +(*/------------------- check result of XXXXX ------------------------------------------------\*)
28.49 +(*\------------------- check result of XXXXX ------------------------------------------------/*)
28.50 +(* final test ... ----------------------------------------------------------------------------*)
28.51 +
28.52 +\<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)
28.53 +(*//------------------ build new fun XXXXX -------------------------------------------------\\*)
28.54 +(*\\------------------ build new fun XXXXX -------------------------------------------------//*)
28.55 +\<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)
28.56 \<close> ML \<open>
28.57 \<close>
28.58 ML \<open>
28.59 @@ -108,10 +109,476 @@
28.60 \<close> ML \<open>
28.61 \<close>
28.62
28.63 -section \<open>===================================================================================\<close>
28.64 +section \<open>========= test/../Knowlegde/equsystem-1a.sml ======================================\<close>
28.65 ML \<open>
28.66 \<close> ML \<open>
28.67 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
28.68 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
28.69 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
28.70 +val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
28.71 + \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
28.72 + "solveForVars [c, c_2]", "solution LL"];
28.73 +val (dI',pI',mI') =
28.74 + ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
28.75 + ["EqSystem", "normalise", "2x2"]);
28.76 +val p = e_pos'; val c = [];
28.77 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
28.78 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
28.79 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
28.80 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
28.81 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
28.82 +case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
28.83 + | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
28.84 +
28.85 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
28.86 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
28.87 +
28.88 +(*+*)if f2str f =
28.89 + "[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n" ^
28.90 + " 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]" then () else error "";
28.91 +(*+*)(Ctree.get_istate_LI pt p |> Istate.string_of) =
28.92 + "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)";
28.93 +
28.94 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
28.95 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
28.96 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
28.97 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
28.98 +
28.99 +(*+isa==isa2*)val "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = f2str f;
28.100 + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\"], [R, L, R, L, R, R, R, L, R, R], srls_normalise_2x2, SOME e_s, \n[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2], ORundef, true, false)" =
28.101 +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);
28.102 +
28.103 +case nxt of
28.104 + (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
28.105 + | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
28.106 +
28.107 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
28.108 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
28.109 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
28.110 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
28.111 +case nxt of
28.112 + (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
28.113 + | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
28.114 +
28.115 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
28.116 +
28.117 + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
28.118 +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);
28.119 +
28.120 +val (p''',_,f,nxt''',_,pt''') = me nxt p c pt;f2str f;
28.121 +(*/------------------- step into me Apply_Method -------------------------------------------\*)
28.122 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
28.123 \<close> ML \<open>
28.124 + val (pt'''', p'''') = (* keep for continuation*)
28.125 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
28.126 +
28.127 + case Step.by_tactic tac (pt, p) of
28.128 + ("ok", (_, _, ptp)) => ptp;
28.129 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
28.130 +
28.131 +(*+isa==isa2*)val ([5], Met) = p;
28.132 +(*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt (fst p);
28.133 + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
28.134 +(*+isa==isa2*)is1 |> Istate.string_of;
28.135 + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
28.136 +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);
28.137 +
28.138 + (*case*)
28.139 + Step.check tac (pt, p) (*of*);
28.140 +"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p) );
28.141 +
28.142 +(*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
28.143 +(*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of);
28.144 +
28.145 + (*if*) Tactic.for_specify tac (*else*);
28.146 +val Applicable.Yes xxx =
28.147 +
28.148 +Solve_Step.check tac (ctree, pos);
28.149 +
28.150 +(*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
28.151 +(*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of);
28.152 +
28.153 +"~~~~~ from Step.check to Step.by_tactic return val:"; val (Applicable.Yes tac') = (Applicable.Yes xxx);
28.154 + (*if*) Tactic.for_specify' tac' (*else*);
28.155 +
28.156 +Step_Solve.by_tactic tac' ptp;;
28.157 +"~~~~~ fun by_tactic , args:"; val ((tac as Tactic.Apply_Method' _), (ptp as (pt, p)))
28.158 + = (tac', ptp);
28.159 +
28.160 +(*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
28.161 +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);
28.162 +
28.163 + LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;
28.164 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _)))
28.165 + = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);
28.166 + val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
28.167 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
28.168 + val {ppc, ...} = MethodC.from_store ctxt mI;
28.169 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
28.170 + val srls = LItool.get_simplifier (pt, pos)
28.171 + val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
28.172 + (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
28.173 +
28.174 +(*+*)val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)" =
28.175 +(*+isa==isa2*)is |> Istate.string_of
28.176 +
28.177 + val ini = LItool.implicit_take prog env;
28.178 + val pos = start_new_level pos
28.179 +val NONE =
28.180 + (*case*) ini (*of*);
28.181 + val (tac''', ist''', ctxt''') =
28.182 + case LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt of
28.183 + Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
28.184 +
28.185 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
28.186 +(*+isa==isa2*)ist''' |> Istate.string_of;
28.187 +
28.188 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
28.189 + = (prog ,(pt, (lev_dn p, Res)), is, ctxt);
28.190 +val Accept_Tac
28.191 + (Take' ttt, iii, _) =
28.192 + (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
28.193 +
28.194 +(*+isa==isa2*)val "c_2 = 0" = (ttt |> UnparseC.term);
28.195 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
28.196 +(*+isa==isa2*)(Pstate iii |> Istate.string_of);
28.197 +
28.198 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
28.199 + = ((prog, (ptp, ctxt)), (Pstate ist));
28.200 + (*if*) path = [] (*then*);
28.201 +
28.202 + scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
28.203 +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))
28.204 + = (cc, (trans_scan_dn ist), (Program.body_of prog));
28.205 +
28.206 + (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
28.207 +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
28.208 + = (cc ,(ist |> path_down [L, R]), e);
28.209 +
28.210 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" =
28.211 +(*+isa==isa2*)(Pstate ist |> Istate.string_of);
28.212 +
28.213 + (*if*) Tactical.contained_in t (*else*);
28.214 +
28.215 + (*case*)
28.216 + LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
28.217 +"~~~~~ fun check_leaf , args:"; val (call, ctxt, srls, (E, (a, v)), t)
28.218 + = ("next ", ctxt, eval, (get_subst ist), t);
28.219 +
28.220 + (*case*)
28.221 + Prog_Tac.eval_leaf E a v t (*of*);
28.222 +"~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)))
28.223 + = (E, a, v, t);
28.224 +
28.225 +val return =
28.226 + (Program.Tac (subst_atomic E t), NONE:term option);
28.227 +"~~~~~ from fun eval_leaf \<longrightarrow>fun check_leaf , return:"; val (Program.Tac stac, a') = return;
28.228 + val stac' = Rewrite.eval_prog_expr ctxt srls
28.229 + (subst_atomic (Env.update_opt E (a, v)) stac)
28.230 +
28.231 +val return =
28.232 + (Program.Tac stac', a');
28.233 +"~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val (Program.Tac prog_tac, form_arg) = return;
28.234 +
28.235 + check_tac cc ist (prog_tac, form_arg);
28.236 +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
28.237 + = (cc, ist, (prog_tac, form_arg));
28.238 + val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
28.239 +val _ =
28.240 + (*case*) m (*of*); (*tac as string/input*)
28.241 +
28.242 + (*case*)
28.243 +Solve_Step.check m (pt, p) (*of*);
28.244 +"~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos)) = (m, (pt, p));
28.245 +
28.246 +val return =
28.247 + check_tac cc ist (prog_tac, form_arg)
28.248 +
28.249 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" =
28.250 +(*+isa==isa2*)(Pstate ist |> Istate.string_of);
28.251 +
28.252 +"~~~~~ from fun scan_dn \<longrightarrow>fun scan_to_tactic \<longrightarrow>fun find_next_step , return:";
28.253 + val (Accept_Tac (tac, ist, ctxt)) = return;
28.254 +
28.255 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
28.256 +(*+isa==isa2*)(Pstate ist |> Istate.string_of)
28.257 +
28.258 +val return =
28.259 + Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac);
28.260 +"~~~~~ from fun find_next_step \<longrightarrow>fun by_tactic , return:"; val Next_Step (ist, ctxt, tac) = return;
28.261 + val (tac', ist', ctxt') = (tac, ist, ctxt)
28.262 +val Tactic.Take' t =
28.263 + (*case*) tac' (*of*);
28.264 + val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt');
28.265 +
28.266 +(*+isa==isa2*)pos; (*from check_tac*)
28.267 +(*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt [5];
28.268 + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =
28.269 +(*+isa==isa2*)is1 |> Istate.string_of;
28.270 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
28.271 +(*+isa==isa2*)(ist' |> Istate.string_of)
28.272 +(*-------------------- stop step into me Apply_Method ----------------------------------------*)
28.273 +(*+isa==isa2*)val "c_2 = 0" = f2str f;
28.274 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =
28.275 +(*+isa==isa2*)(Ctree.get_istate_LI pt''' p''' |> Istate.string_of)
28.276 +(*\\------------------- step into me Apply_Method ------------------------------------------//*)
28.277 +
28.278 +\<close> ML \<open>
28.279 +val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' c pt''';f2str f;
28.280 +\<close> ML \<open>
28.281 +(*+isa==isa2*)val ([5, 1], Frm) = p'''';
28.282 +(*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f2str f;
28.283 +(*+isa<>isa2*)val (**)Check_Postcond ["triangular", "2x2", "LINEAR", "system"](** )
28.284 + Substitute ["c_2 = 0"]( **) = nxt'''';
28.285 +(*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt'''' (fst p'''');
28.286 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
28.287 +(*+isa==isa2*)is1 |> Istate.string_of;
28.288 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
28.289 +(*+isa==isa2*)Ctree.get_istate_LI pt'''' p'''' |> Istate.string_of;
28.290 +\<close> ML \<open> (*//----------- step into me Take ---------------------------------------------------\\*)
28.291 +(*//------------------ step into me Take ---------------------------------------------------\\*)
28.292 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt''');
28.293 +\<close> ML \<open>
28.294 + val (pt, p) = (* keep for continuation*)
28.295 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
28.296 +
28.297 + case Step.by_tactic tac (pt, p) of
28.298 + ("ok", (_, _, ptp)) => ptp;
28.299 +\<close> ML \<open>
28.300 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
28.301 +(*isa==isa2*)Ctree.get_istate_LI pt p |> Istate.string_of;
28.302 +\<close> ML \<open>
28.303 + (*case*)
28.304 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
28.305 +\<close> ML \<open>
28.306 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
28.307 +\<close> ML \<open>
28.308 + (*if*) Pos.on_calc_end ip (*else*);
28.309 +\<close> ML \<open>
28.310 + val (_, probl_id, _) = Calc.references (pt, p);
28.311 +\<close> ML \<open>
28.312 +val _ =
28.313 + (*case*) tacis (*of*);
28.314 +\<close> ML \<open>
28.315 + (*if*) probl_id = Problem.id_empty (*else*);
28.316 +\<close> ML \<open>
28.317 + switch_specify_solve p_ (pt, ip);
28.318 +\<close> ML \<open>
28.319 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
28.320 +\<close> ML \<open>
28.321 + (*if*) Pos.on_specification ([], state_pos) (*else*);
28.322 +\<close> ML \<open>
28.323 + LI.do_next (pt, input_pos);
28.324 +\<close> ML \<open>
28.325 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
28.326 +\<close> ML \<open>
28.327 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
28.328 +\<close> ML \<open>
28.329 + val thy' = get_obj g_domID pt (par_pblobj pt p);
28.330 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
28.331 +\<close> ML \<open>
28.332 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
28.333 +(*+isa==isa2*)ist |> Istate.string_of;
28.334 +\<close> ML \<open>
28.335 + (*case*)
28.336 + LI.find_next_step sc (pt, pos) ist ctxt (*of*);
28.337 +\<close> ML \<open>
28.338 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
28.339 + = (sc, (pt, pos), ist, ctxt);
28.340 +\<close> ML \<open>
28.341 + (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
28.342 +\<close> ML \<open>
28.343 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
28.344 + = ((prog, (ptp, ctxt)), (Pstate ist));
28.345 +\<close> ML \<open>
28.346 + (*if*) path = [] (*else*);
28.347 +\<close> ML \<open>
28.348 + go_scan_up (prog, cc) (trans_scan_up ist);
28.349 +\<close> ML \<open>
28.350 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
28.351 + = ((prog, cc), (trans_scan_up ist));
28.352 +\<close> ML \<open>
28.353 + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, false)" =
28.354 +(*+isa==isa2*)Pstate ist |> Istate.string_of;
28.355 +(*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = act_arg |> UnparseC.term;
28.356 +\<close> ML \<open>
28.357 + (*if*) path = [R] (*root of the program body*) (*else*);
28.358 +\<close> ML \<open>
28.359 + scan_up pcc (ist |> path_up) (go_up path sc);
28.360 +\<close> ML \<open>
28.361 +"~~~~~ and scan_up , args:"; val ((pcc as (sc, cc)), ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))
28.362 + = (pcc, (ist |> path_up), (go_up path sc));
28.363 +\<close> ML \<open>
28.364 + val (i, body) = check_Let_up ist sc
28.365 +\<close> ML \<open>
28.366 + (*case*) scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
28.367 +\<close> ML \<open>
28.368 +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))
28.369 + = (cc, (ist |> path_up_down [R, D] |> upd_env i), body);
28.370 +\<close> ML \<open>
28.371 +val goback =
28.372 + (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
28.373 +\<close> ML \<open>
28.374 +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ e1 $ e2 $ a))
28.375 + = (cc, (ist |> path_down [L, R]), e);
28.376 +\<close> ML \<open>
28.377 + (*case*) scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
28.378 +\<close> ML \<open>
28.379 +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
28.380 + = (cc, (ist |> path_down_form ([L, L, R], a)), e1);
28.381 +\<close> ML \<open>
28.382 + (*if*) Tactical.contained_in t (*else*);
28.383 +\<close> ML \<open>
28.384 + (*case*)
28.385 + LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
28.386 +\<close> ML \<open>
28.387 +"~~~~~ fun check_leaf , args:"; val (call, ctxt, srls, (E, (a, v)), t)
28.388 + = ("next ", ctxt, eval, (get_subst ist), t);
28.389 +\<close> ML \<open>
28.390 +val (Program.Tac stac, a') =
28.391 + (*case*) Prog_Tac.eval_leaf E a v t (*of*);
28.392 +\<close> ML \<open>
28.393 + val stac' = Rewrite.eval_prog_expr ctxt srls
28.394 + (subst_atomic (Env.update_opt E (a, v)) stac)
28.395 +\<close> ML \<open>
28.396 +(*+*)val "Substitute [c_2 = 0] (L * c + c_2 = q_0 * L \<up> 2 / 2)" = stac' |> UnparseC.term;
28.397 +\<close> ML \<open>
28.398 +val return =
28.399 + (Program.Tac stac', a')
28.400 +\<close> ML \<open>
28.401 +"~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val ((Program.Tac prog_tac, form_arg))
28.402 + = (return);
28.403 +\<close> ML \<open>
28.404 + check_tac cc ist (prog_tac, form_arg);
28.405 +\<close> ML \<open>
28.406 +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
28.407 + = (cc, ist, (prog_tac, form_arg));
28.408 +\<close> ML \<open>
28.409 + val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
28.410 +\<close> ML \<open>
28.411 +val _ =
28.412 + (*case*) m (*of*);
28.413 +\<close> ML \<open>
28.414 + (*case*)
28.415 +Solve_Step.check m (pt, p) (*of*);
28.416 +\<close> ML \<open>
28.417 +"~~~~~ fun check , args:"; val ((Tactic.Substitute sube), (cs as (pt, pos as (p, _))))
28.418 + = (m, (pt, p));
28.419 +\<close> ML \<open>
28.420 + val pp = Ctree.par_pblobj pt p
28.421 + val ctxt = Ctree.get_loc pt pos |> snd
28.422 + val thy = Proof_Context.theory_of ctxt
28.423 + val f = Calc.current_formula cs;
28.424 + val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp)
28.425 + val subte = Subst.input_to_terms ctxt sube (*?TODO: input requires parse _: _ -> _ option?*)
28.426 + val ro = get_rew_ord ctxt rew_ord'
28.427 +\<close> ML \<open>
28.428 + (*if*) foldl and_ (true, map TermC.contains_Var subte) (*else*);
28.429 +\<close> ML \<open>
28.430 +(*+isa==isa2*)sube : TermC.as_string list
28.431 +\<close> ML \<open>
28.432 +(*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f |> UnparseC.term
28.433 +\<close> ML \<open>
28.434 +(*+isa<>isa2*)val (** )["c_2 = (0::'a)"]( **)["c_2 = 0"](**) = subte |> map UnparseC.term
28.435 +\<close> ML \<open>
28.436 +val SOME ttt =
28.437 + (*case*) Rewrite.rewrite_terms_ ctxt ro erls subte f (*of*);
28.438 +\<close> ML \<open>
28.439 +\<close> ML \<open> (*//----------- build new fun Subst.input_to_terms ----------------------------------\\*)
28.440 +(*//------------------ build new fun XXXXX -------------------------------------------------\\*)
28.441 +\<close> ML \<open>
28.442 +fun input_to_terms ctxt strs = map (TermC.parse ctxt) strs;
28.443 +\<close> ML \<open>
28.444 +input_to_terms: Proof.context -> Subst.input -> Subst.as_eqs
28.445 +\<close> ML \<open>
28.446 +(* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type*)
28.447 +fun input_to_terms ctxt strs = strs
28.448 + |> map (TermC.parse ctxt)
28.449 + |> map (Model_Pattern.adapt_term_to_type ctxt)
28.450 +\<close> ML \<open>
28.451 +\<close> ML \<open>
28.452 +\<close> ML \<open>
28.453 +\<close> ML \<open>
28.454 +(*\\------------------ build new fun XXXXX -------------------------------------------------//*)
28.455 +\<close> ML \<open> (*\\----------- build new fun Subst.input_to_terms ----------------------------------//*)
28.456 +\<close> ML \<open>
28.457 +\<close> ML \<open>
28.458 +\<close> ML \<open>
28.459 +\<close> ML \<open>
28.460 +\<close> ML \<open>
28.461 +\<close> ML \<open>
28.462 +\<close> ML \<open>
28.463 +\<close> ML \<open>
28.464 +\<close> text \<open>
28.465 +"~~~~~ from fun scan_dn \<longrightarrow>fun scan_up , return:"; val (Accept_Tac ict) = (goback);
28.466 +\<close> text \<open>
28.467 +"~~~~~ from fun scan_up \<longrightarrow>fun go_scan_up" ^
28.468 + " \<longrightarrow>fun scan_to_tactic \<longrightarrow>fun find_next_step , return:"; val (Accept_Tac (tac, ist, ctxt))
28.469 + = (Accept_Tac ict);
28.470 +\<close> ML \<open>
28.471 +\<close> ML \<open>
28.472 +\<close> ML \<open>
28.473 +\<close> ML \<open>
28.474 +\<close> ML \<open>
28.475 +\<close> ML \<open>
28.476 +\<close> ML \<open>
28.477 +\<close> ML \<open>
28.478 +(*-------------------- stop step into me Take ------------------------------------------------*)
28.479 +\<close> ML \<open> (*------------- stop step into me Take ------------------------------------------------*)
28.480 +(*\\------------------ step into me Take ---------------------------------------------------//*)
28.481 +\<close> ML \<open> (*\\----------- step into me Take ---------------------------------------------------//*)
28.482 +\<close> ML \<open>
28.483 +val (p,_,f,nxt,_,pt) = me nxt'''' p'''' c pt'''';f2str f;
28.484 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
28.485 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
28.486 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
28.487 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
28.488 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
28.489 +\<close> ML \<open>
28.490 +(*+*)val (**)"L * c + c_2 = q_0 * L \<up> 2 / 2"(** )
28.491 + "[c = L * q_0 / 2, c_2 = 0]"( **) = f2str f;
28.492 +\<close> ML \<open>
28.493 + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =
28.494 +(*val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\", \"\n(e_2, c = L * q_0 / 2)\", \"\n(e__s, [c_2 = 0, c = L * q_0 / 2])\"], [R, R, D, R, D, R, D, R, D, R, D, L, R], srls_top_down_2x2, SOME e__s, \n[c = L * q_0 / 2, c_2 = 0], ORundef, true, true)" =*)
28.495 +(*+*)(Ctree.get_istate_LI pt p |> Istate.string_of)
28.496 +\<close> text \<open>
28.497 +case nxt of
28.498 + (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
28.499 + | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
28.500 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
28.501 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
28.502 +
28.503 +(* final test ... ----------------------------------------------------------------------------*)
28.504 +if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
28.505 +else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
28.506 +
28.507 +case nxt of
28.508 + (End_Proof') => ()
28.509 + | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
28.510 +\<close> ML \<open>
28.511 +Test_Tool.show_pt pt (*[
28.512 +(([], Frm), solveSystem
28.513 + [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2],
28.514 + [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]]
28.515 + [[c], [c_2]]),
28.516 +(([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
28.517 + 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]),
28.518 +(([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]),
28.519 +(([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]),
28.520 +(([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]),
28.521 +(([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]),
28.522 +(([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]),
28.523 +(([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2),
28.524 +
28.525 +(([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2),
28.526 +(([5, 2], Res), L * c = q_0 * L \<up> 2 / 2),
28.527 +(([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L),
28.528 +(([5, 4], Res), c = L * q_0 / 2),
28.529 +(([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]),
28.530 +(([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]),
28.531 +(([5], Res), [c = L * q_0 / 2, c_2 = 0]),
28.532 +(([], Res), [c = L * q_0 / 2, c_2 = 0])]
28.533 +*)
28.534 \<close> ML \<open>
28.535 \<close>
28.536
28.537 @@ -125,10 +592,26 @@
28.538 section \<open>code for copy & paste ===============================================================\<close>
28.539 ML \<open>
28.540 "~~~~~ fun xxx , args:"; val () = ();
28.541 -"~~~~~ and xxx , args:"; val () = ();
28.542 -"~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));
28.543 +"~~~~~ and xxx , args:"; val () = ();
28.544 +"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
28.545 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
28.546 "xx"
28.547 -^ "xxx" (*+*)
28.548 +^ "xxx" (*+*) (*+++*) (* keep for continuation*) (*+isa<>isa2*) (**)
28.549 +\<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
28.550 + (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
28.551 +(*\\------------------ adhoc inserted n ----------------------------------------------------//*)
28.552 +\<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
28.553 +
28.554 +\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
28.555 +(*//------------------ step into XXXXX -----------------------------------------------------\\*)
28.556 +(*-------------------- stop step into XXXXX --------------------------------------------------*)
28.557 +\<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)
28.558 +(*\\------------------ step into XXXXX -----------------------------------------------------//*)
28.559 +\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
28.560 +
28.561 +\<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)
28.562 +(*//------------------ build new fun XXXXX -------------------------------------------------\\*)
28.563 +(*\\------------------ build new fun XXXXX -------------------------------------------------//*)
28.564 +\<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)
28.565 \<close>
28.566 end