1.1 --- a/src/Tools/isac/Build_Isac.thy Wed Jul 31 09:46:50 2019 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Fri Aug 09 14:04:13 2019 +0200
1.3 @@ -19,6 +19,7 @@
1.4 theory ListC
1.5 imports "~~/src/Tools/isac/KEStore"
1.6 ML_file "~~/src/Tools/isac/ProgLang/termC.sml"
1.7 + ML_file "~~/src/Tools/isac/ProgLang/contextC.sml"
1.8 ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
1.9 ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
1.10 theory Tools imports ListC begin
2.1 --- a/src/Tools/isac/Interpret/appl.sml Wed Jul 31 09:46:50 2019 +0200
2.2 +++ b/src/Tools/isac/Interpret/appl.sml Fri Aug 09 14:04:13 2019 +0200
2.3 @@ -225,7 +225,7 @@
2.4 val {where_, ...} = Specify.get_pbt pI
2.5 val pres = map (Model.mk_env probl |> subst_atomic) where_
2.6 val ctxt = if is_e_ctxt ctxt
2.7 - then Celem.assoc_thy dI |> Proof_Context.init_global |> Stool.insert_assumptions pres
2.8 + then Celem.assoc_thy dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
2.9 else ctxt
2.10 (*TODO.WN110416 here do evalprecond according to fun check_preconds'
2.11 and then decide on Chead.Notappl/Appl accordingly once more.
3.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed Jul 31 09:46:50 2019 +0200
3.2 +++ b/src/Tools/isac/Interpret/calchead.sml Fri Aug 09 14:04:13 2019 +0200
3.3 @@ -1307,7 +1307,7 @@
3.4 val {ppc, ...} = Specify.get_met mI
3.5 val (_, vals) = oris2fmz_vals pors
3.6 val ctxt = dI |> Rule.Thy_Info_get_theory |> Proof_Context.init_global
3.7 - |> Stool.declare_constraints' vals
3.8 + |> ContextC.declare_constraints' vals
3.9 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors)
3.10 val pt = update_metppc pt p (map (ori2Coritm ppc) pors) (*WN110716 = _pblppc ?!?*)
3.11 val pt = update_spec pt p (dI, pI, mI)
4.1 --- a/src/Tools/isac/Interpret/ctree-basic.sml Wed Jul 31 09:46:50 2019 +0200
4.2 +++ b/src/Tools/isac/Interpret/ctree-basic.sml Fri Aug 09 14:04:13 2019 +0200
4.3 @@ -548,7 +548,7 @@
4.4 then get_loc pt pos |> #2 (*for script interpretation rely on fun get_loc*)
4.5 else get_obj g_ctxt pt p (*for specify phase take ctx from PblObj*)
4.6
4.7 -fun get_assumptions_ pt p = get_ctxt pt p |> Stool.get_assumptions;
4.8 +fun get_assumptions_ pt p = get_ctxt pt p |> ContextC.get_assumptions;
4.9
4.10 fun get_somespec' (dI, pI, mI) (dI', pI', mI') =
4.11 let
5.1 --- a/src/Tools/isac/Interpret/generate.sml Wed Jul 31 09:46:50 2019 +0200
5.2 +++ b/src/Tools/isac/Interpret/generate.sml Fri Aug 09 14:04:13 2019 +0200
5.3 @@ -269,7 +269,7 @@
5.4 end
5.5 | generate1 _ (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (p, _) pt =
5.6 let
5.7 - val (pt, c) = cappend_atomic pt p (is, Stool.insert_assumptions asm ctxt) f
5.8 + val (pt, c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
5.9 (Tactic.Rewrite_Inst (Selem.subst2subs subs', thm')) (f',asm) Complete;
5.10 val pt = update_branch pt p TransitiveB
5.11 in
5.12 @@ -277,7 +277,7 @@
5.13 end
5.14 | generate1 _ (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (p, _) pt =
5.15 let
5.16 - val (pt, c) = cappend_atomic pt p (is, Stool.insert_assumptions asm ctxt) f
5.17 + val (pt, c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
5.18 (Tactic.Rewrite thm') (f', asm) Complete
5.19 val pt = update_branch pt p TransitiveB
5.20 in
5.21 @@ -286,7 +286,7 @@
5.22 | generate1 thy (Tactic.Rewrite_Asm' all) l p pt = generate1 thy (Tactic.Rewrite' all) l p pt
5.23 | generate1 _ (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (p, _) pt =
5.24 let
5.25 - val (pt, c) = cappend_atomic pt p (is, Stool.insert_assumptions asm ctxt) f
5.26 + val (pt, c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
5.27 (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs', Rule.id_rls rls')) (f', asm) Complete
5.28 val pt = update_branch pt p TransitiveB
5.29 in
5.30 @@ -294,7 +294,7 @@
5.31 end
5.32 | generate1 thy (Tactic.Detail_Set_Inst' (_, _, subs, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
5.33 let
5.34 - val ctxt' = Stool.insert_assumptions asm ctxt
5.35 + val ctxt' = ContextC.insert_assumptions asm ctxt
5.36 val (pt, _) = cappend_form pt p (is, ctxt') f
5.37 val pt = update_branch pt p TransitiveB
5.38 val is = init_istate (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs, Rule.id_rls rls)) f
5.39 @@ -305,7 +305,7 @@
5.40 end
5.41 | generate1 _ (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (p, _) pt =
5.42 let
5.43 - val (pt, c) = cappend_atomic pt p (is, Stool.insert_assumptions asm ctxt) f
5.44 + val (pt, c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
5.45 (Tactic.Rewrite_Set (Rule.id_rls rls')) (f',asm) Complete
5.46 val pt = update_branch pt p TransitiveB
5.47 in
5.48 @@ -313,7 +313,7 @@
5.49 end
5.50 | generate1 thy (Tactic.Detail_Set' (_, _, rls, f, (_, asm))) (is, ctxt) (p, _) pt =
5.51 let
5.52 - val ctxt' = Stool.insert_assumptions asm ctxt
5.53 + val ctxt' = ContextC.insert_assumptions asm ctxt
5.54 val (pt, _) = cappend_form pt p (is, ctxt') f
5.55 val pt = update_branch pt p TransitiveB
5.56 val is = init_istate (Tactic.Rewrite_Set (Rule.id_rls rls)) f
5.57 @@ -373,9 +373,9 @@
5.58 val f = get_curr_formula (pt, pos)
5.59 val pos' as (p', _) = (lev_on p, Res)
5.60 val (pt, _) = case subs_opt of
5.61 - NONE => cappend_atomic pt p' (is, Stool.insert_assumptions [] ctxt) f
5.62 + NONE => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f
5.63 (Tactic.Rewrite thm') (f', []) Inconsistent
5.64 - | SOME subs => cappend_atomic pt p' (is, Stool.insert_assumptions [] ctxt) f
5.65 + | SOME subs => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f
5.66 (Tactic.Rewrite_Inst (subs, thm')) (f', []) Inconsistent
5.67 val pt = update_branch pt p' TransitiveB
5.68 in (pt, pos') end
6.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Jul 31 09:46:50 2019 +0200
6.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Fri Aug 09 14:04:13 2019 +0200
6.3 @@ -687,7 +687,7 @@
6.4 val (E, l, a, b, ctxt') = case get_loc pt (pp, Frm) of
6.5 (Istate.ScrState (E,l,a,_,_,b), ctxt') => (E, l, a, b, ctxt')
6.6 | _ => error "begin_end_prog Check_Postcond' script of parpbl: uncovered case get_loc"
6.7 - val ctxt'' = Stool.from_subpbl_to_caller ctxt scval ctxt'
6.8 + val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt'
6.9 val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))
6.10 val is = Istate.ScrState (E,l,a,scval,scsaf,b)
6.11 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
7.1 --- a/src/Tools/isac/Interpret/model.sml Wed Jul 31 09:46:50 2019 +0200
7.2 +++ b/src/Tools/isac/Interpret/model.sml Fri Aug 09 14:04:13 2019 +0200
7.3 @@ -45,8 +45,6 @@
7.4 val mk_env : itm list -> (term * term) list (* close to Chead.all_dsc_in, Chead.is_error, etc *)
7.5 val max_vt : itm list -> int
7.6
7.7 - val dest_list' : term -> term list
7.8 -
7.9 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.10 type penv
7.11 val penv2str_ : Proof.context -> penv -> string (* NONE *)
7.12 @@ -124,9 +122,6 @@
7.13 fun is_var (Free _) = true
7.14 | is_var _ = false;
7.15
7.16 -(* this may decompose an object-language isa-list;
7.17 - use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*)
7.18 -fun dest_list' t = if TermC.is_list t then TermC.isalist2list t else [t];
7.19 (* special handling for lists. ?WN:14.5.03 ??!? *)
7.20 fun dest_list (d, ts) =
7.21 let fun dest t =
7.22 @@ -172,13 +167,13 @@
7.23 then if LTool.is_list_dsc d andalso TermC.is_list arg andalso LTool.is_unl d |> not
7.24 then (d, take_apart arg)
7.25 else (d, [arg])
7.26 - else (Rule.e_term, dest_list' t)
7.27 + else (Rule.e_term, TermC.dest_list' t)
7.28 | split_dts t =
7.29 let val t' as (h, _) = strip_comb t;
7.30 in
7.31 if LTool.is_dsc h
7.32 then (h, dest_list t')
7.33 - else (Rule.e_term, dest_list' t)
7.34 + else (Rule.e_term, TermC.dest_list' t)
7.35 end;
7.36 (* version returning ts only *)
7.37 fun split_dts' (d, arg) =
7.38 @@ -190,7 +185,7 @@
7.39 else (take_apart arg) (* [a,b] --> SML[ [a], [b] ]SML *)
7.40 else ([arg]) (* a variable or metavariable for a list *)
7.41 else ([arg])
7.42 - else (dest_list' arg)
7.43 + else (TermC.dest_list' arg)
7.44 (* WN170204: Warning "redundant"
7.45 | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
7.46 let val (h,argl) = strip_comb t
8.1 --- a/src/Tools/isac/Interpret/mstools.sml Wed Jul 31 09:46:50 2019 +0200
8.2 +++ b/src/Tools/isac/Interpret/mstools.sml Fri Aug 09 14:04:13 2019 +0200
8.3 @@ -12,12 +12,6 @@
8.4 val check_preconds : 'a -> Rule.rls -> term list -> Model.itm list -> (bool * term) list
8.5 val check_preconds' : Rule.rls -> term list -> Model.itm list -> 'a -> (bool * term) list
8.6
8.7 - val get_assumptions : Proof.context -> term list
8.8 - val insert_assumptions : term list -> Proof.context -> Proof.context
8.9 - val declare_constraints : string -> Proof.context -> Proof.context
8.10 - val declare_constraints' : term list -> Proof.context -> Proof.context
8.11 - val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context
8.12 -
8.13 datatype match_ = Match_ of Celem.pblID * (Model.itm list * (bool * term) list) | NoMatch_
8.14 val refined_ : match_ list -> match_ option
8.15 datatype match = Matches of Celem.pblID * Model.item Model.ppc | NoMatch of Celem.pblID * Model.item Model.ppc
8.16 @@ -27,7 +21,7 @@
8.17 val pres2str : (bool * term) list -> string
8.18 val refined : match list -> Celem.pblID
8.19 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.20 - val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context
8.21 + (*NONE*)
8.22 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.23
8.24 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
8.25 @@ -95,43 +89,6 @@
8.26 in map (evalprecond prls) pres' end;
8.27 fun check_preconds _(*thy*) prls pres pbl = check_preconds' prls pres pbl (Model.max_vt pbl);
8.28
8.29 -fun declare_constraints' ts ctxt = fold Variable.declare_constraints (flat (map TermC.vars ts)) ctxt;
8.30 -(*WN110613 fun declare_constraints' shall replace fun declare_constraints*)
8.31 -fun declare_constraints t ctxt =
8.32 - let
8.33 - fun get_vars ((v, T) :: vs) = (case raw_explode v |> Library.read_int of
8.34 - (_, _ :: _) => (Free (v, T) :: get_vars vs)
8.35 - | (_, [] ) => get_vars vs) (*filter out nums as long as we have Free ("123",_)*)
8.36 - | get_vars [] = [];
8.37 - val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
8.38 - in fold Variable.declare_constraints ts ctxt end;
8.39 -
8.40 -structure Context_Data = Proof_Data (type T = term list fun init _ = []);
8.41 -fun get_assumptions ctxt = Context_Data.get ctxt
8.42 -fun insert_assumptions asms = Context_Data.map (fn xs => distinct (asms @ xs))
8.43 -
8.44 -(* transfer assumptions from one to another ctxt.
8.45 - does NOT respect scope: in a calculation identifiers are unique.
8.46 - but environments are scoped as usual in Luacs-interpretation.
8.47 - WN110520 redo (1) take declare_constraints (2) with combinators*)
8.48 -fun transfer_asms_from_to from_ctxt to_ctxt =
8.49 - let
8.50 - val to_vars = get_assumptions to_ctxt |> map TermC.vars |> flat
8.51 - fun transfer [] to_ctxt = to_ctxt
8.52 - | transfer (from_asm :: fas) to_ctxt =
8.53 - if inter op = (TermC.vars from_asm) to_vars = []
8.54 - then transfer fas to_ctxt
8.55 - else transfer fas (insert_assumptions [from_asm] to_ctxt)
8.56 - in transfer (get_assumptions from_ctxt) to_ctxt end
8.57 -
8.58 -(* exported from a subproblem to the context of the calling method:
8.59 - # 'scrval': the result of script interpretation and
8.60 - # those assumptions in the subproblem wich contain a variable known
8.61 - in the calling method. *)
8.62 -fun from_subpbl_to_caller sub_ctxt scrval caller_ctxt =
8.63 - let
8.64 - val caller_ctxt = (scrval |> Model.dest_list' |> insert_assumptions) caller_ctxt
8.65 - in transfer_asms_from_to sub_ctxt caller_ctxt end;
8.66
8.67 fun common_subthy (thy1, thy2) =
8.68 if Context.subthy (thy1, thy2) then thy2
9.1 --- a/src/Tools/isac/Interpret/ptyps.sml Wed Jul 31 09:46:50 2019 +0200
9.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Fri Aug 09 14:04:13 2019 +0200
9.3 @@ -226,7 +226,7 @@
9.4 fun prep_ori [] _ _ = ([], Selem.e_ctxt)
9.5 | prep_ori fmz thy pbt =
9.6 let
9.7 - val ctxt = Proof_Context.init_global thy |> fold Stool.declare_constraints fmz;
9.8 + val ctxt = Proof_Context.init_global thy |> fold ContextC.declare_constraints fmz;
9.9 val ori = map (add_field thy pbt o Model.split_dts o the o TermC.parseNEW ctxt) fmz |> add_variants;
9.10 val maxv = map fst ori |> max;
9.11 val maxv = if maxv = 0 then 1 else maxv;
10.1 --- a/src/Tools/isac/Interpret/script.sml Wed Jul 31 09:46:50 2019 +0200
10.2 +++ b/src/Tools/isac/Interpret/script.sml Fri Aug 09 14:04:13 2019 +0200
10.3 @@ -233,7 +233,7 @@
10.4 val {cas,ppc,thy,...} = Specify.get_pbt pI
10.5 val dI = Rule.theory2theory' thy (*.take dI from _refined_ pbl.*)
10.6 val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt));
10.7 - val ctxt = dI |> Rule.Thy_Info_get_theory |> Proof_Context.init_global |> Stool.declare_constraints' vals
10.8 + val ctxt = dI |> Rule.Thy_Info_get_theory |> Proof_Context.init_global |> ContextC.declare_constraints' vals
10.9 val hdl =
10.10 case cas of
10.11 NONE => LTool.pblterm dI pI
10.12 @@ -392,7 +392,7 @@
10.13 val {cas, ppc, thy, ...} = Specify.get_pbt pI
10.14 val dI = Rule.theory2theory' thy (*take dI from _refined_ pbl*)
10.15 val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt))
10.16 - val ctxt = dI |> Rule.Thy_Info_get_theory |> Proof_Context.init_global |> Stool.declare_constraints' vals
10.17 + val ctxt = dI |> Rule.Thy_Info_get_theory |> Proof_Context.init_global |> ContextC.declare_constraints' vals
10.18 val hdl =
10.19 case cas of
10.20 NONE => LTool.pblterm dI pI
10.21 @@ -582,10 +582,10 @@
10.22 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
10.23 val env = relate_args [] formals actuals;
10.24 val _ = trace_istate env;
10.25 - val ctxt = Proof_Context.init_global thy |> Stool.declare_constraints' actuals
10.26 + val ctxt = Proof_Context.init_global thy |> ContextC.declare_constraints' actuals
10.27 val {pre, prls, ...} = Specify.get_met metID;
10.28 val pres = Stool.check_preconds thy prls pre itms |> map snd;
10.29 - val ctxt = ctxt |> Stool.insert_assumptions pres;
10.30 + val ctxt = ctxt |> ContextC.insert_assumptions pres;
10.31 in (Istate.ScrState (env, [], NONE, Rule.e_term, Istate.Safe, true), ctxt, scr) end;
10.32 end (*local*)
10.33
11.1 --- a/src/Tools/isac/Interpret/solve.sml Wed Jul 31 09:46:50 2019 +0200
11.2 +++ b/src/Tools/isac/Interpret/solve.sml Fri Aug 09 14:04:13 2019 +0200
11.3 @@ -137,7 +137,7 @@
11.4 in
11.5 case LucinNEW.locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' of
11.6 LucinNEW.Safe_Step (cstate, istate, ctxt, tac) =>
11.7 - ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))], [(*ctree NOT cut*)], cstate))
11.8 + ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))], [(*ctree NOT cut?*)], cstate))
11.9 | _ => (* NotLocatable *)
11.10 let val (p, ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac") m (p, Frm) pt;
11.11 in
11.12 @@ -185,7 +185,7 @@
11.13 val (E, l, a, b, ctxt') = case get_loc pt (pp, Frm) of
11.14 (Istate.ScrState (E, l, a, _, _, b), ctxt') => (E, l, a, b, ctxt')
11.15 | _ => error "solve Check_Postcond resume script of parpbl: uncovered case get_loc"
11.16 - val ctxt'' = Stool.from_subpbl_to_caller ctxt scval ctxt'
11.17 + val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt'
11.18 val ((p, p_), ps, _, pt) = Generate.generate1 thy (Tactic.Check_Postcond' (pI, (scval, asm)))
11.19 (Istate.ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
11.20 in ("ok", ([(Tactic.Check_Postcond pI, Tactic.Check_Postcond'(pI, (scval, asm)),
12.1 --- a/src/Tools/isac/ProgLang/ListC.thy Wed Jul 31 09:46:50 2019 +0200
12.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Fri Aug 09 14:04:13 2019 +0200
12.3 @@ -8,6 +8,7 @@
12.4 begin
12.5
12.6 ML_file "~~/src/Tools/isac/ProgLang/termC.sml"
12.7 +ML_file "~~/src/Tools/isac/ProgLang/contextC.sml"
12.8 ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
12.9 ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
12.10 ML \<open>
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/Tools/isac/ProgLang/contextC.sml Fri Aug 09 14:04:13 2019 +0200
13.3 @@ -0,0 +1,218 @@
13.4 +(* Title: ../contextC.sml
13.5 + Author: Walther Neuper, Mathias Lehnfeld
13.6 + (c) due to copyright terms
13.7 +*)
13.8 +(* Extension to Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *)
13.9 +signature CONTEXT_C =
13.10 +sig
13.11 + val declare_constraints : string -> Proof.context -> Proof.context
13.12 + val declare_constraints' : term list -> Proof.context -> Proof.context
13.13 + val get_assumptions : Proof.context -> term list
13.14 + val insert_assumptions : term list -> Proof.context -> Proof.context
13.15 + val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context
13.16 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
13.17 + (*NONE*)
13.18 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
13.19 + val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context
13.20 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
13.21 +end
13.22 +
13.23 +(* survey on handling contexts:
13.24 +-------------------------------
13.25 + theory is required for Pattern.match (and thus for Tactic.Rewrite* ), while
13.26 + ctxt is required for parsing and for managing pre-conditions and assumptions.
13.27 + * model-specify-phase:
13.28 + * Tactic.Model_Problem does declare_constraints for parsing (in Tactic.Add_Given, etc)
13.29 + ("insert_assumptions pres" has to wait for completing Tactic.Add_Given, etc)
13.30 + (Tactic.Refine_Problem uses theory NOT ctxt due to Pattern.match)
13.31 + *
13.32 + *
13.33 + * solve-phase by Lucas-Interpretation:
13.34 + * locate_input_tactic:
13.35 + * Tactic.Apply_Method
13.36 + * initialises ctxt (declare_constraints' + insert_assumptions pres) by init_scrstate
13.37 + * in solve for root problem
13.38 + * in begin_end_prog for subproblem
13.39 + * Tactic.Rewrite* create assumptions; respective insert_assumptions is done by associate
13.40 + * associate..Subproblem' returns ctxt ONLY with declare_constraints',
13.41 + with insert_assumptions wait for Tactic.Apply_Method
13.42 + * storing ctxt is done after return form locate_input_tactic
13.43 + * determine_next_tactic:
13.44 + * TODO initialises ctxt by TODO
13.45 + * Tactic.Rewrite* create assumptions; respective insert_assumptions TODO
13.46 + *
13.47 + *
13.48 + *
13.49 + * locate_input_formula: follows sig. of determine_next_tactic
13.50 + * changing from one method to another (in determine_next_tactic only):
13.51 + * from method to sub-program: just add new preconditions of the guard
13.52 + * locate_input_tactic: init_scrstate by begin_end_prog
13.53 + * determine_next_tactic:
13.54 + * from_subpbl_to_caller
13.55 + * finishing a method:
13.56 + * Tactic.Check_Postcond' uses ctxt for proving the post-condition (not yet implemented)
13.57 + *
13.58 + *
13.59 + *
13.60 + *
13.61 +================================================================================================
13.62 +call hierarchy
13.63 +================================================================================================
13.64 +
13.65 + locatetac
13.66 + applicable_in (p, p_) pt (Tactic.Apply_Method pres
13.67 + insert_assumptions
13.68 +
13.69 + context_thy
13.70 + applicable_in (p, p_) pt (Tactic.Apply_Method pres
13.71 + insert_assumptions
13.72 +
13.73 +
13.74 +
13.75 +
13.76 +
13.77 +
13.78 + generate1 _ (Tactic.Rewrite***
13.79 + insert_assumptions
13.80 +
13.81 +
13.82 +
13.83 +
13.84 +
13.85 +------------------------------------------------------------------------------------------------
13.86 +solve phase before LI
13.87 +------------------------------------------------------------------------------------------------
13.88 +autocalc
13.89 + all_modspec
13.90 + declare_constraints'
13.91 + complete_solve
13.92 + all_modspec
13.93 + declare_constraints'
13.94 +
13.95 +all_solve
13.96 + begin_end_prog (Tactic.Apply_Method'
13.97 + init_scrstate
13.98 + declare_constraints'
13.99 + insert_assumptions
13.100 +
13.101 +nxt_specify_
13.102 + begin_end_prog (Tactic.Apply_Method'
13.103 + init_scrstate
13.104 + declare_constraints'
13.105 + insert_assumptions
13.106 +------------------------------------------------------------------------------------------------
13.107 +LI
13.108 +------------------------------------------------------------------------------------------------
13.109 +solve ("Apply_Method" root-program
13.110 + init_scrstate
13.111 + declare_constraints'
13.112 + insert_assumptions
13.113 + locate_input_tactic
13.114 + execute_progr_2
13.115 + assy ..leaf sub-program
13.116 + associate
13.117 + declare_constraints'
13.118 + applicable_in .. Tactic.Apply_Method pres
13.119 + insert_assumptions
13.120 + ? generate1 (look in test with "from ... to..))
13.121 +
13.122 +determine_next_tactic
13.123 + execute_progr_1
13.124 + appy ..leaf
13.125 + stac2tac_
13.126 + declare_constraints'
13.127 + applicable_in (p, p_) pt (Tactic.Apply_Method pres
13.128 + insert_assumptions
13.129 + ? generate1 (look in test with "from ... to..))
13.130 +
13.131 +locate_input_formula uses determine_next_tactic
13.132 + compare_step
13.133 + all_modspec
13.134 + declare_constraints'
13.135 + begin_end_prog (Tactic.Apply_Method'
13.136 + init_scrstate
13.137 + declare_constraints'
13.138 + insert_assumptions
13.139 +------------------------------------------------------------------------------------------------
13.140 +specification phase
13.141 +------------------------------------------------------------------------------------------------
13.142 + loc_specify_
13.143 + specify (Tactic.Init_Proof'
13.144 + prep_ori
13.145 + declare_constraints
13.146 +
13.147 + CalcTree
13.148 + nxt_specify_init_calc
13.149 + prep_ori
13.150 + declare_constraints
13.151 +
13.152 + modifyCalcHead
13.153 + input_icalhd
13.154 + prep_ori
13.155 + declare_constraints
13.156 +
13.157 + refine
13.158 + refin'
13.159 + prep_ori
13.160 + declare_constraints
13.161 +------------------------------------------------------------------------------------------------
13.162 +unused ?!
13.163 +------------------------------------------------------------------------------------------------
13.164 + ??
13.165 + match_pbl
13.166 + prep_ori
13.167 + declare_constraints
13.168 + ??
13.169 + from_pblobj'
13.170 + init_scrstate
13.171 + declare_constraints'
13.172 + insert_assumptions
13.173 + ??
13.174 + tac2tac_
13.175 + applicable_in (p, p_) pt (Tactic.Apply_Method pres
13.176 + insert_assumptions
13.177 +
13.178 +*)
13.179 +
13.180 +structure ContextC(**) : CONTEXT_C(**) =
13.181 +struct
13.182 +
13.183 +fun declare_constraints' ts ctxt = fold Variable.declare_constraints (flat (map TermC.vars ts)) ctxt;
13.184 +(*WN110613 fun declare_constraints' shall replace fun declare_constraints*)
13.185 +fun declare_constraints t ctxt =
13.186 + let
13.187 + fun get_vars ((v, T) :: vs) = (case raw_explode v |> Library.read_int of
13.188 + (_, _ :: _) => (Free (v, T) :: get_vars vs)
13.189 + | (_, [] ) => get_vars vs) (*filter out nums as long as we have Free ("123",_)*)
13.190 + | get_vars [] = [];
13.191 + val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
13.192 + in fold Variable.declare_constraints ts ctxt end;
13.193 +
13.194 +structure Context_Data = Proof_Data (type T = term list fun init _ = []);
13.195 +fun get_assumptions ctxt = Context_Data.get ctxt
13.196 +fun insert_assumptions asms = Context_Data.map (fn xs => distinct (asms @ xs))
13.197 +
13.198 +(* transfer assumptions from one to another ctxt.
13.199 + does NOT respect scope: in a calculation identifiers are unique.
13.200 + but environments are scoped as usual in Luacs-interpretation.
13.201 + WN110520 redo (1) take declare_constraints (2) with combinators*)
13.202 +fun transfer_asms_from_to from_ctxt to_ctxt =
13.203 + let
13.204 + val to_vars = get_assumptions to_ctxt |> map TermC.vars |> flat
13.205 + fun transfer [] to_ctxt = to_ctxt
13.206 + | transfer (from_asm :: fas) to_ctxt =
13.207 + if inter op = (TermC.vars from_asm) to_vars = []
13.208 + then transfer fas to_ctxt
13.209 + else transfer fas (insert_assumptions [from_asm] to_ctxt)
13.210 + in transfer (get_assumptions from_ctxt) to_ctxt end
13.211 +
13.212 +(* exported from a subproblem to the context of the calling method:
13.213 + # 'scrval': the result of script interpretation and
13.214 + # those assumptions in the subproblem wich contain a variable known
13.215 + in the calling method. *)
13.216 +fun from_subpbl_to_caller sub_ctxt scrval caller_ctxt =
13.217 + let
13.218 + val caller_ctxt = (scrval |> TermC.dest_list' |> insert_assumptions) caller_ctxt
13.219 + in transfer_asms_from_to sub_ctxt caller_ctxt end;
13.220 +
13.221 +end
14.1 --- a/src/Tools/isac/ProgLang/termC.sml Wed Jul 31 09:46:50 2019 +0200
14.2 +++ b/src/Tools/isac/ProgLang/termC.sml Fri Aug 09 14:04:13 2019 +0200
14.3 @@ -4,7 +4,8 @@
14.4 *)
14.5 infix contains_one_of
14.6
14.7 -signature TERMC =
14.8 +(* TERM_C extends Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *)
14.9 +signature TERM_C =
14.10 sig
14.11 val contains_Var: term -> bool
14.12 val dest_binop_typ: typ -> typ * typ * typ
14.13 @@ -71,6 +72,7 @@
14.14 val var2free: term -> term
14.15 val vars: term -> term list
14.16 val vars_of : term -> term list (* probably should replace "fun vars" *)
14.17 + val dest_list' : term -> term list
14.18
14.19 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
14.20 val scala_of_term: term -> string
14.21 @@ -88,7 +90,7 @@
14.22 end
14.23
14.24 (**)
14.25 -structure TermC(**): TERMC(**) =
14.26 +structure TermC(**): TERM_C(**) =
14.27 struct
14.28 (**)
14.29
14.30 @@ -546,4 +548,8 @@
14.31 val var_ids = t |> ids2str |> subtract op = poly_consts |> map strip_thy |> sort string_ord
14.32 in (map (var_for [] t) var_ids) |> flat |> distinct end
14.33
14.34 +(* this may decompose an object-language isa-list;
14.35 + use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*)
14.36 +fun dest_list' t = if is_list t then isalist2list t else [t];
14.37 +
14.38 end
14.39 \ No newline at end of file
15.1 --- a/src/Tools/isac/TODO.thy Wed Jul 31 09:46:50 2019 +0200
15.2 +++ b/src/Tools/isac/TODO.thy Fri Aug 09 14:04:13 2019 +0200
15.3 @@ -16,7 +16,27 @@
15.4 \item xxx
15.5 \item introduce simple type names to LUCAS_INTERPRETER <-?-> readable paper
15.6 \item check in states: length ?? > 1 with tracing these cases
15.7 + \item rename ScrState --> Program_State
15.8 + \item locate_input_tactic arg: type istate ((ScrState is))
15.9 + result: type scrstate ((is)) ... unify + readable paper!
15.10 + rename ? ^^^^^^^^ prog_state, pstate
15.11 + \item script: rename AssWeak --> Ass_Weak
15.12 + \item script.associate: remove ctxt from Subproblem' -- analogous Rewrite'...
15.13 + \item lucas-intrpreter.assy: Generate.generate1 (Celem.assoc_thy "Isac")
15.14 + \item lucas-intrpreter.locate_input_tactic: execute_progr_2 srls tac cstate (progr, Rule.e_rls)
15.15 + ^^^^^^^^^^
15.16 + \item Lucin.associate: ctree -> Proof.context -> Tactic.T -> term -> Lucin.ass
15.17 + -----> : ctree -> Proof.context -> (Tactic.T * term) -> Lucin.ass
15.18 + \item ?delete Check_Postcond' in begin_end_prog (already done in solve?)
15.19 + in case both are needed, unify !
15.20 + \item rm ctxt from Subproblem' (is separated in associate!))
15.21 \item xxx
15.22 + \item comoplete mstools.sml (* survey on handling contexts:
15.23 + \item collect ctxt to structure ContextC + address all uses of insert_assumptions here
15.24 + \item xxx
15.25 + \item dest_spec (Const ("Product_Type.Pair", _) $ d $ (Const ("Product_Type.Pair", _) FORALL occur.
15.26 + \item xxx
15.27 + \item check Tactic.Subproblem': are 2 terms required?
15.28 \item xxx
15.29 \item xxx
15.30 \end{itemize}
15.31 @@ -24,6 +44,10 @@
15.32 subsection \<open>Postponed from current changeset\<close>
15.33 text \<open>
15.34 \begin{itemize}
15.35 + \item xxx
15.36 + \item rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl
15.37 + \item xxx
15.38 + \item xxx
15.39 \item language definition: use (f #> g) x = x |> f |> g instead of @
15.40 see implementation.pdf p.16
15.41 \item xxx
15.42 @@ -32,9 +56,19 @@
15.43 \begin{itemize}
15.44 \item 1. check if Ctree.state can be updated OUTSIDE determine_next_step
15.45 \item 2. fun locate_input_tactic: pull generate1 out (because it stores ctxt also in cstate)
15.46 - \item xxx
15.47 + \item
15.48 \item xxx
15.49 \end{itemize}
15.50 + \item concentracte "insert_assumptions" in "associate" ?for determine_next_tactic ?where?
15.51 + \begin{itemize}
15.52 + \item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)
15.53 + \item shift from "applicable_in..Apply_Method" to ? ? ? (is ONLY use-case in appl.sml))
15.54 + \item ?"insert_assumptions" necessary in "init_scrstate" ?+++? in "applicable_in" ?+++? "associate"
15.55 + \item xxx
15.56 + \item xxx
15.57 + \item DO DELETIONS AFTER analogous concentrations in determine_next_tactic
15.58 + \end{itemize}
15.59 + \item xxx
15.60 \item xxx
15.61 \item xxx
15.62 \item inform: TermC.parse (Celem.assoc_thy "Isac") istr --> parseNEW context istr
15.63 @@ -51,6 +85,9 @@
15.64 \item Diff.thy: differentiateX --> differentiate after removal of script-constant
15.65 \item Test.thy: met_test_sqrt2: deleted?!
15.66 \item xxx
15.67 + \item drop "init_form" and use "Take" in programs (start with latter!)
15.68 + \item Applicable.applicable_in --> Applicable.tactic_at
15.69 + \item Const ("Script.SubProblem", _) --> Const ("Program.SubProblem", _):rename! separate?
15.70 \item xxx
15.71 \item xxx
15.72 \end{itemize}
15.73 @@ -162,10 +199,17 @@
15.74 subsection \<open>replace theory/thy by context/ctxt\<close>
15.75 text \<open>
15.76 \begin{itemize}
15.77 + \item cleaup the many conversions string -- theory
15.78 + \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?
15.79 \item 1. Rewrite.eval_true_, then
15.80 Lucin.handle_leaf, Rewrite.eval_listexpr_, Generate.generate1, Lucin.stac2tac.
15.81 + \item fun associate
15.82 + let val thy = Celem.assoc_thy "Isac";(*TODO*)
15.83 \item xxx
15.84 \item xxx
15.85 + \item xxx
15.86 + \item !!! Tactic.Refine_Problem uses Pattern.match, which takes a theory, NOT a ctxt
15.87 + but there is Proof_Context.theory_of !!!
15.88 \end{itemize}
15.89 \<close>
15.90 subsection \<open>Rfuns, Begin_/End_Detail', Rrls\<close>
16.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Wed Jul 31 09:46:50 2019 +0200
16.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Fri Aug 09 14:04:13 2019 +0200
16.3 @@ -104,7 +104,7 @@
16.4 ML \<open>
16.5 "artifically inject assumptions";
16.6 val (SOME (iform, cform), SOME (ires, cres)) = Ctree.get_obj Ctree.g_loc pt (fst p);
16.7 - val ctxt = Stool.insert_assumptions [TermC.str2term "x < sub_asm_out",
16.8 + val ctxt = ContextC.insert_assumptions [TermC.str2term "x < sub_asm_out",
16.9 TermC.str2term "a < sub_asm_local"] cres;
16.10 val pt = Ctree.update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
16.11 \<close>
17.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Jul 31 09:46:50 2019 +0200
17.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri Aug 09 14:04:13 2019 +0200
17.3 @@ -126,7 +126,7 @@
17.4 Isabelle can handle best.\<close>
17.5 ML \<open>
17.6 val ctxt = Proof_Context.init_global @{theory};
17.7 - val ctxt = Stool.declare_constraints' [@{term "z::real"}] ctxt;
17.8 + val ctxt = ContextC.declare_constraints' [@{term "z::real"}] ctxt;
17.9
17.10 val SOME fun1 =
17.11 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
18.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Wed Jul 31 09:46:50 2019 +0200
18.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Fri Aug 09 14:04:13 2019 +0200
18.3 @@ -54,7 +54,7 @@
18.4 | _ => error ""
18.5
18.6 "~~~~~ fun prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, yyy);
18.7 - val ctxt = Proof_Context.init_global thy |> fold Stool.declare_constraints fmz;
18.8 + val ctxt = Proof_Context.init_global thy |> fold ContextC.declare_constraints fmz;
18.9 (*ADD check*)
18.10 case TermC.parseNEW ctxt "equality (x+1=(2::real))" of
18.11 SOME (Const ("Descript.equality", _) (* <<< ---------------- this needs to be recognised *) $
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/test/Tools/isac/ProgLang/contextC.sml Fri Aug 09 14:04:13 2019 +0200
19.3 @@ -0,0 +1,18 @@
19.4 +(* Title: "ProgLang/contextC.sml"
19.5 + Author: Walther Neuper
19.6 + (c) due to copyright terms
19.7 +*)
19.8 +
19.9 +"-----------------------------------------------------------------------------------------------";
19.10 +"table of contents -----------------------------------------------------------------------------";
19.11 +"-----------------------------------------------------------------------------------------------";
19.12 +"----------- check all handling of context -----------------------------------------------------";
19.13 +"-----------------------------------------------------------------------------------------------";
19.14 +"-----------------------------------------------------------------------------------------------";
19.15 +"-----------------------------------------------------------------------------------------------";
19.16 +
19.17 +
19.18 +"----------- check all handling of context -----------------------------------------------------";
19.19 +"----------- check all handling of context -----------------------------------------------------";
19.20 +"----------- check all handling of context -----------------------------------------------------";
19.21 +(* waits in Test_Some.thy for checking further updates to context handling *)
19.22 \ No newline at end of file
20.1 --- a/test/Tools/isac/Test_Isac.thy Wed Jul 31 09:46:50 2019 +0200
20.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Aug 09 14:04:13 2019 +0200
20.3 @@ -105,7 +105,8 @@
20.4 open Applicable; mk_set;
20.5 open Solve; (* NONE *)
20.6 open Selem; e_fmz;
20.7 - open Stool; transfer_asms_from_to;
20.8 + open Stool; (* NONE *)
20.9 + open ContextC; transfer_asms_from_to;
20.10 open Tactic; (* NONE *)
20.11 open Model; (* NONE *)
20.12 open LTool; rule2stac;
20.13 @@ -147,6 +148,7 @@
20.14 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
20.15 ML_file "kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
20.16 ML_file "ProgLang/termC.sml"
20.17 + ML_file "ProgLang/contextC.sml"
20.18 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
20.19 ML_file "ProgLang/rewrite.sml"
20.20 ML_file "ProgLang/listC.sml"
21.1 --- a/test/Tools/isac/Test_Isac_Short.thy Wed Jul 31 09:46:50 2019 +0200
21.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Fri Aug 09 14:04:13 2019 +0200
21.3 @@ -105,7 +105,8 @@
21.4 open Applicable; mk_set;
21.5 open Solve; (* NONE *)
21.6 open Selem; e_fmz;
21.7 - open Stool; transfer_asms_from_to;
21.8 + open Stool; (* NONE *)
21.9 + open ContextC; transfer_asms_from_to;
21.10 open Tactic; (* NONE *)
21.11 open Model; (* NONE *)
21.12 open LTool; rule2stac;
21.13 @@ -147,6 +148,7 @@
21.14 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
21.15 ML_file "kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
21.16 ML_file "ProgLang/termC.sml"
21.17 + ML_file "ProgLang/contextC.sml"
21.18 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
21.19 ML_file "ProgLang/rewrite.sml"
21.20 ML_file "ProgLang/listC.sml"
22.1 --- a/test/Tools/isac/Test_Some.thy Wed Jul 31 09:46:50 2019 +0200
22.2 +++ b/test/Tools/isac/Test_Some.thy Fri Aug 09 14:04:13 2019 +0200
22.3 @@ -17,7 +17,8 @@
22.4 open Applicable; mk_set;
22.5 open Solve; (* NONE *)
22.6 open Selem; e_fmz;
22.7 - open Stool; transfer_asms_from_to;
22.8 + open Stool; (* NONE *)
22.9 + open ContextC; transfer_asms_from_to;
22.10 open Tactic; (* NONE *)
22.11 open Model; (* NONE *)
22.12 open LTool; rule2stac;
22.13 @@ -68,10 +69,113 @@
22.14 "~~~~~ fun xxx , args:"; val () = ();
22.15 \<close>
22.16
22.17 -section \<open>===================================================================================\<close>
22.18 +section \<open>===========--- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x"===============\<close>
22.19 ML \<open>
22.20 "~~~~~ fun xxx , args:"; val () = ();
22.21 \<close> ML \<open>
22.22 +"----------- check all handling of context -----------------------------------------------------";
22.23 +"----------- check all handling of context -----------------------------------------------------";
22.24 +"----------- check all handling of context -----------------------------------------------------";
22.25 +(*ER-7*) (*Schalk I s.87 Bsp 55b*)
22.26 +(* peculiarity of this example:
22.27 + show_pt_tac pt;
22.28 +
22.29 +. . . . . . . . . . ("RatEq",["univariate","equation"],["no_met"]);
22.30 +([], Frm), solve (x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x, x)
22.31 + asm ^^^^^ "x \<noteq> 0"
22.32 +. . . . . . . . . . Subproblem (PolyEq, ["normalise","polynomial","univariate","equation"]),
22.33 +([4], Pbl), solve ((3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3), x)
22.34 +. . . . . . . . . . Subproblem (PolyEq, ["bdv_only","degree_2","polynomial","univariate","equation"]),
22.35 +([4,4], Pbl), solve (-6 * x + 5 * x ^^^ 2 = 0, x)
22.36 +([4,4,5], Res), [x = 0, x = 6 / 5]
22.37 +. . . . . . . . . . Check_Postcond ["bdv_only","degree_2","polynomial","univariate","equation"],
22.38 +([4,4], Res), [x = 0, x = 6 / 5]
22.39 +. . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"],
22.40 + ^^^^^ from_subpbl_to_caller must drop "x = 0" due to asm "x \<noteq> 0"
22.41 +([5], Res), [x = 0, x = 6 / 5]
22.42 +. . . . . . . . . . Check_Postcond ["rational","univariate","equation"],
22.43 +([], Res), [x = 6 / 5]
22.44 +*)
22.45 +val fmz = ["equality (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)",
22.46 + "solveFor x","solutions L"];
22.47 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
22.48 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
22.49 +(*---------solve (x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x, x)*)
22.50 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.51 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.52 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.53 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["RatEq", "solve_rat_equation"]*)
22.54 +\<close> ML \<open>
22.55 +if p = ([], Met) andalso fst nxt = "Apply_Method" andalso
22.56 +terms2str (get_assumptions_ pt p) = "[]"
22.57 +then () else error "BEFORE 1 changed";
22.58 +\<close> ML \<open>
22.59 +(*//--1 begin step into relevant call -------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^---\\
22.60 + 1 relevant for init_scrstate in root-pbl*)
22.61 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.62 +(*\\--1 end step into relevant call ----------------------------------------------------------//*)
22.63 +\<close> ML \<open>
22.64 +if p = ([1], Frm) andalso fst nxt = "Rewrite_Set" andalso
22.65 +terms2str (get_assumptions_ pt p) = "[\"x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x\"]"
22.66 +then () else error "AFTER 1 changed";
22.67 +\<close> ML \<open>
22.68 +(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "norm_Rational"*)
22.69 +(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "RatEq_eliminate"*)
22.70 +\<close> ML \<open>
22.71 +if p = ([2], Res) andalso fst nxt = "Rewrite_Set" andalso
22.72 +terms2str (get_assumptions_ pt p) = "[\"9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0\",\"x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x\"]"
22.73 +then () else error "BEFORE 2 changed";
22.74 +\<close> ML \<open>
22.75 +(*//--2 begin step into relevant call -------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^---\\
22.76 + 2 relevant for preconds like "x \<noteq> 0" *)
22.77 +(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]*)
22.78 +(*---------solve ((3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3), x)*)
22.79 +(*\\--2 end step into relevant call ----------------------------------------------------------//*)
22.80 +\<close> ML \<open>
22.81 +if p = ([3], Res) andalso fst nxt = "Subproblem" andalso
22.82 +terms2str (get_assumptions_ pt p) = "[\"9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0\",\"x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x\"]"
22.83 +then () else error "AFTER 2 changed";
22.84 +\<close> ML \<open>
22.85 +(*[4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.86 +(*[4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)
22.87 +(*[4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)
22.88 +(*[4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["PolyEq", "normalise_poly"]*)
22.89 +(*[4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)")*)
22.90 +(*[4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.91 +(*[4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*)
22.92 +(*---------solve (-6 * x + 5 * x ^^^ 2 = 0, x)*)
22.93 +(*4, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)
22.94 +(*4, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)
22.95 +(*4, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)
22.96 +(*4, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.97 +(*4, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"]*)
22.98 +(*[4, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_bdv_only_simplify")*)
22.99 +(*[4, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set_Inst (["(''bdv'', x)"], "d1_polyeq_simplify")*)
22.100 +(*[4, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "polyeq_simplify"*)
22.101 +(*[4, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Or_to_List*)
22.102 +(*[4, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_elementwise "Assumptions"*)
22.103 +(*[4, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*)
22.104 +\<close> ML \<open>
22.105 +if p = ([4, 4, 5], Res) andalso fst nxt = "Check_Postcond" andalso
22.106 +terms2str (get_assumptions_ pt p) = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\"]"
22.107 +then () else error "BEFORE 8 changed";
22.108 +\<close> ML \<open>
22.109 +(*//--9 begin step into relevant call ----------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^---\\
22.110 + 9 relevant for dropping "x = 0" due to asm "x \<noteq> 0"*)
22.111 +(*[4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
22.112 +(*\\--9 end step into relevant call ----------------------------------------------------------//*)
22.113 +\<close> ML \<open>
22.114 +if p = ([4, 4], Res) andalso fst nxt = "Check_Postcond" andalso
22.115 +terms2str (get_assumptions_ pt p) = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"x = 0\",\"x = 6 / 5\",\"\<not> matches (?a = 0)\n ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x\"]"
22.116 +then () else error "AFTER 8 changed";
22.117 +\<close> ML \<open>
22.118 +(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_elementwise "Assumptions"*)
22.119 +(*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_Postcond ["rational", "univariate", "equation"]*)
22.120 +(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*End_Proof'*)
22.121 +\<close> ML \<open>
22.122 +if p = ([], Res) andalso f2str f = "[]" (*..must change*)andalso fst nxt = "End_Proof'" andalso
22.123 +terms2str (get_assumptions_ pt p) = "[\"\<not> matches (?a = 0)\n ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x\",\"x = 6 / 5\",\"x = 0\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\",\"9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0\",\"x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x\"]"
22.124 +then () else error "ERROR CHANGED: rateq.sml: diff.behav. in I s.87 Bsp 55b [x = 6 / 5], End_Proof'";
22.125 \<close> ML \<open>
22.126 \<close> ML \<open>
22.127 "~~~~~ fun xxx , args:"; val () = ();