1.1 --- a/src/Tools/isac/Interpret/appl.sml Mon May 09 10:43:43 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Wed May 11 07:28:13 2011 +0200
1.3 @@ -217,7 +217,7 @@
1.4
1.5
1.6 (*.applicability of a tacic wrt. a calc-state (ptree,pos').
1.7 - additionally used by next_tac in the script-interpreter for sequence-tacs.
1.8 + additionally used by next_tac in the script-interpreter for script-tacs.
1.9 tests for applicability are so expensive, that results (rewrites!)
1.10 are kept in the return-value of 'type tac_'.
1.11 .*)
2.1 --- a/src/Tools/isac/Interpret/calchead.sml Mon May 09 10:43:43 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/calchead.sml Wed May 11 07:28:13 2011 +0200
2.3 @@ -1134,38 +1134,29 @@
2.4
2.5 (*. called only if no_met is specified .*)
2.6 | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
2.7 - let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m;
2.8 - *)
2.9 - val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) =
2.10 - get_obj I pt p;
2.11 - val {prls,met,ppc,thy,where_,...} = get_pbt pIre
2.12 - (*val pbl = init_pbl ppc --- Model_Problem recognizes probl=[]*)
2.13 - (*val pt = update_pbl pt p pbl;
2.14 - val pt = update_orispec pt p
2.15 - (string_of_thy thy, pIre,
2.16 - if length met = 0 then e_metID else hd met);*)
2.17 - val (domID, metID) = (string_of_thy thy,
2.18 - if length met = 0 then e_metID else hd met)
2.19 - val ((p,_),_,_,pt) =
2.20 - generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
2.21 - (Uistate, e_ctxt) pos pt
2.22 - (*val pre = check_preconds thy prls where_ pbl
2.23 - val pb = foldl and_ (true, map fst pre)*)
2.24 - val (pbl, pre, pb) = ([], [], false)
2.25 - in ((p,Pbl), (pos,Uistate),
2.26 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
2.27 - (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
2.28 - Model_Problem, Safe, pt) end
2.29 + let
2.30 + val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) = get_obj I pt p;
2.31 + val {prls,met,ppc,thy,where_,...} = get_pbt pIre
2.32 + val (domID, metID) =
2.33 + (string_of_thy thy, if length met = 0 then e_metID else hd met)
2.34 + val ((p,_),_,_,pt) =
2.35 + generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
2.36 + (Uistate, e_ctxt) pos pt
2.37 + val (pbl, pre, pb) = ([], [], false)
2.38 + in ((p, Pbl), (pos, Uistate),
2.39 + Form' (PpcKF (0,EdUndef,(length p),Nundef,
2.40 + (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
2.41 + Model_Problem, Safe, pt)
2.42 + end
2.43
2.44 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
2.45 - let val (pos,_,_,pt) = generate1 (assoc_thy "Isac")
2.46 - (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
2.47 - in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
2.48 - Model_Problem, Safe, pt) end
2.49 + let
2.50 + val (pos,_,_,pt) = generate1 (assoc_thy "Isac")
2.51 + (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
2.52 + in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
2.53 + Model_Problem, Safe, pt)
2.54 + end
2.55
2.56 -(* val (Specify_Problem' (pI, (ok, (itms, pre)))) = nxt; val (p,_) = p;
2.57 - val (Specify_Problem' (pI, (ok, (itms, pre)))) = m; val (p,_) = p;
2.58 - *)
2.59 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
2.60 let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
2.61 meth=met, ...}) = get_obj I pt p;
2.62 @@ -1567,7 +1558,7 @@
2.63 val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;
2.64 val pI' = refine_ori' pors pI;
2.65 in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
2.66 - (hd o #met o get_pbt) pI') end
2.67 + (hd o #met o get_pbt) pI') end
2.68 else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
2.69 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
2.70 val dI = theory2theory' (maxthy thy thy');
2.71 @@ -1720,23 +1711,13 @@
2.72
2.73 (* called only once, if a Subproblem has been located in the script*)
2.74 fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_)) ptp =
2.75 -(* val (Subproblem'((_,pblID,metID),_,_,_,_),ptp) = (m', (pt,(p,p_)));
2.76 - *)
2.77 - (case metID of
2.78 - ["no_met"] =>
2.79 - (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
2.80 - | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
2.81 - (*all stored in tac_ itms ^^^^^^^^^^*)
2.82 + (case metID of
2.83 + ["no_met"] =>
2.84 + (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
2.85 + | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
2.86 + (*all stored in tac_ itms^^^^^^^^^^*)
2.87 | nxt_model_pbl tac_ _ =
2.88 - error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
2.89 -(* run subp_rooteq.sml ''
2.90 - until nxt=("Subproblem",Subproblem ("SqRoot",["univariate","equation"]))
2.91 -> val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
2.92 - (last_elem o drop_last) ets'';
2.93 -> val mst = (last_elem o drop_last) ets'';
2.94 -> nxt_model_pbl mst;
2.95 -val it = Refine_Tacitly ["univariate","equation"] : tac
2.96 -*)
2.97 + error ("nxt_model_pbl: called by tac= " ^ tac_2str tac_);
2.98
2.99 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
2.100 fun eq4 v (_,vts,_,_,_) = member op = vts v;
3.1 --- a/src/Tools/isac/Interpret/ctree.sml Mon May 09 10:43:43 2011 +0200
3.2 +++ b/src/Tools/isac/Interpret/ctree.sml Wed May 11 07:28:13 2011 +0200
3.3 @@ -529,12 +529,10 @@
3.4 type fmz = fmz_ * spec;
3.5 val e_fmz = ([],e_spec);
3.6
3.7 -(*tac_ is made from tac in applicable_in,
3.8 - and carries all data necessary for generate;*)
3.9 +(* tac_ is made from tac in applicable_in,
3.10 + and carries all data necessary for generate *)
3.11 datatype tac_ =
3.12 -(* datatype tac = *)
3.13 Init_Proof' of ((cterm' list) * spec)
3.14 - (* ori list !: code specify -> applicable*)
3.15 | Model_Problem' of pblID *
3.16 itm list * (*the 'untouched' pbl*)
3.17 itm list (*the casually completed met*)
4.1 --- a/src/Tools/isac/Interpret/mathengine.sml Mon May 09 10:43:43 2011 +0200
4.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Wed May 11 07:28:13 2011 +0200
4.3 @@ -129,32 +129,6 @@
4.4 end
4.5 end;
4.6
4.7 -(*------------------------------------------------------------------
4.8 -fun init_detail ptp = e_calcstate;(*15.8.03.MISSING-->solve.sml!?*)
4.9 -(*----------------------------------------------------from solve.sml*)
4.10 - | nxt_solv (Detail_Set'(thy', rls, t)) (pt, p) =
4.11 - let (*val rls = the (assoc(!ruleset',rls'))
4.12 - handle _ => error ("solve: '"^rls'^"' not known");*)
4.13 - val thy = assoc_thy thy';
4.14 - val (srls, sc, is) =
4.15 - case rls of
4.16 - Rrls {scr=sc as Rfuns {init_state=ii,...},...} =>
4.17 - (e_rls, sc, RrlsState (ii t))
4.18 - | Rls {srls=srls,scr=sc as Script s,...} =>
4.19 - (srls, sc, ScrState ([(one_scr_arg s,t)], [],
4.20 - NONE, e_term, Sundef, true));
4.21 - val pt = update_tac pt (fst p) (Detail_Set (id_rls rls));
4.22 - val (p,cid,_,pt) = generate1 thy (Begin_Trans' t) is p pt;
4.23 - val nx = (tac_2tac o fst3) (next_tac (thy',srls) (pt,p) sc is);
4.24 - val aopt = applicable_in p pt nx;
4.25 - in case aopt of
4.26 - Notappl s => error ("solve Detail_Set: "^s)
4.27 - (* val Appl m = aopt;
4.28 - *)
4.29 - | Appl m => solve ("discardFIXME",m) p pt end
4.30 -------------------------------------------------------------------*)
4.31 -
4.32 -
4.33 (*iterated by nxt_me; there (the resulting) ptp dropped
4.34 may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*)
4.35 fun nxt_specify_ (ptp as (pt, pos as (p,p_))) =
4.36 @@ -193,14 +167,8 @@
4.37 val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
4.38 in (pt, (complete, Met, hdf, mits, pre, spec):ocalhd) end;
4.39
4.40 -(* val ([(_, Specify_Method' (_, _, mits), _)], [],_) =
4.41 - nxt_specif (Specify_Method mI) ptp;
4.42 - *)
4.43 -
4.44 (*.specify a new problem;
4.45 WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' .*)
4.46 -(* val (pI, ptp) = (pI, (pt, ip));
4.47 - *)
4.48 fun set_problem pI (ptp: ptree * pos') =
4.49 let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
4.50 _, (pt, pos as (p,_))) = nxt_specif (Specify_Problem pI) ptp
5.1 --- a/src/Tools/isac/Interpret/ptyps.sml Mon May 09 10:43:43 2011 +0200
5.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Wed May 11 07:28:13 2011 +0200
5.3 @@ -964,45 +964,9 @@
5.4 val pre' = check_preconds' prls pre itms mvat
5.5 val pb = foldl and_ (true, map fst pre')
5.6 in if complete andalso pb then true else false end;
5.7 -(*run subp-rooteq.sml 'root-eq + subpbl: solve_linear'
5.8 - until 'val nxt = ("Model_Problem",Model_Problem ["linear","univariate"...
5.9 -> val Nd(PblObj _,[_,_,_,_,_,_,_,_,_,_,_,
5.10 - Nd(PblObj{origin=(oris,_,_),...},[])]) = pt;
5.11 -> val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"],
5.12 - (#where_ o get_pbt) ["linear","univariate","equation"]);
5.13 -> match_oris oris (pbt,pre);
5.14 -val it = true : bool
5.15 -
5.16 -
5.17 -> val (pbt,pre) =((#ppc o get_pbt) ["plain_square","univariate","equation"],
5.18 - (#where_ o get_pbt)["plain_square","univariate","equation"]);
5.19 -> match_oris oris (pbt,pre);
5.20 -val it = false : bool
5.21 -
5.22 -
5.23 - ---------------------------------------------------
5.24 - run subp-rooteq.sml 'root-eq + subpbl: solve_plain_square'
5.25 - until 'val nxt = ("Model_Problem",Model_Problem ["plain_square","univ...
5.26 -> val Nd (PblObj _, [_,_,_,_,_,_,_,Nd (PrfObj _,[]),
5.27 - Nd (PblObj {origin=(oris,_,_),...},[])]) = pt;
5.28 -> val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"],
5.29 - (#where_ o get_pbt) ["linear","univariate","equation"]);
5.30 -> match_oris oris (pbt,pre);
5.31 -val it = false : bool
5.32 -
5.33 -
5.34 -> val (pbt,pre)=((#ppc o get_pbt) ["plain_square","univariate","equation"],
5.35 - (#where_ o get_pbt) ["plain_square","univariate","equation"]);
5.36 -> match_oris oris (pbt,pre);
5.37 -val it = true : bool
5.38 -*)
5.39 -(*^^^--- doubled 20.9.01 *)
5.40 -
5.41
5.42 (*. check a problem (ie. ori list) for matching a problemtype,
5.43 returns items for output to math-experts .*)
5.44 -(* val (ppc,pre) = (#ppc py, #where_ py);
5.45 - *)
5.46 fun match_oris' thy oris (ppc,pre,prls) =
5.47 (* val (thy, oris, (ppc,pre,prls)) = (thy, oris, (ppc, where_, prls));
5.48 *)
5.49 @@ -1014,12 +978,12 @@
5.50 val pb = foldl and_ (true, map fst pre')
5.51 in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
5.52
5.53 -(*. for the user .*)
5.54 +(* for the user *)
5.55 datatype match' =
5.56 Matches' of item ppc
5.57 | NoMatch' of item ppc;
5.58
5.59 -(*. match a formalization with a problem type .*)
5.60 +(* match a formalization with a problem type *)
5.61 fun match_pbl (fmz:fmz_) ({thy=thy,where_=pre,ppc,prls=er,...}:pbt) =
5.62 let val oris = prep_ori fmz thy ppc |> #1;
5.63 val (bool, (itms, pre')) = match_oris' thy oris (ppc,pre,er);
6.1 --- a/test/Tools/isac/ADDTESTS/Ctxt.thy Mon May 09 10:43:43 2011 +0200
6.2 +++ b/test/Tools/isac/ADDTESTS/Ctxt.thy Wed May 11 07:28:13 2011 +0200
6.3 @@ -1,16 +1,17 @@
6.4 theory Ctxt imports Main begin
6.5
6.6 -lemma ctxt:
6.7 +text {*from Lars Noschinski 110415*}
6.8 +lemma ctxt1:
6.9 + assumes asm1: "a = 1" and asm2: "b = -2"
6.10 + shows "2 * a + b = (0::int)"
6.11 + apply (insert asm1 asm2)
6.12 + apply simp
6.13 +done
6.14 +
6.15 +lemma ctxt2:
6.16 assumes asm1: "a = 1"
6.17 and asm2: "b = -2"
6.18 shows "2 * a + b = (0::int)"
6.19 using asm1 asm2 by (simp)
6.20
6.21 -text {*from Lars Noschinski 110415*}
6.22 -lemma ctxt:
6.23 - assumes asm1: "a = 1" and asm2: "b = -2"
6.24 - shows "2 * a + b = (0::int)"
6.25 - apply (insert asm1 asm2)
6.26 - apply simp
6.27 -
6.28 end
7.1 --- a/test/Tools/isac/Knowledge/Rational_Test.thy Mon May 09 10:43:43 2011 +0200
7.2 +++ b/test/Tools/isac/Knowledge/Rational_Test.thy Wed May 11 07:28:13 2011 +0200
7.3 @@ -1,17 +1,24 @@
7.4 -theory Rational_Test imports Main begin
7.5 +theory Rational_Test imports Complex_Main begin
7.6
7.7 -lemma cancel:
7.8 - assumes asm1: "a = 1" and asm2: "b = -2"
7.9 - shows "(x^2 - 1) / (x - 1) = (x + (1::real))"
7.10 - apply (insert asm1 asm2)
7.11 +lemma cancel_2011:
7.12 + assumes asm1: "(x^2 - y^2) = (x + y) * (x - y)"
7.13 + and asm2: "x^2 - x*y = x * (x - y)"
7.14 + and asm3: "x - y \<noteq> 0"
7.15 + and asm4: "x \<noteq> 0"
7.16 + shows "(x^2 - y^2) / (x^2 - x*y) = (x + y) / (x::real)"
7.17 + apply (insert asm1 asm2 asm3 asm4)
7.18 apply simp
7.19 +done
7.20
7.21 -(*
7.22 -lemma ctxt:
7.23 - assumes asm1: "a = 1" and asm2: "b = -2"
7.24 - shows "2 * a + b = (0::int)"
7.25 - apply (insert asm1 asm2)
7.26 +text {* due to Rational.thy the asumptions asm1 and asm2 will be unnecessary: *}
7.27 +lemma cancel_2011ff:
7.28 + assumes asm3: "x - y \<noteq> 0"
7.29 + and asm4: "x \<noteq> 0"
7.30 + shows "(x^2 - y^2) / (x^2 - x*y) = (x + y) / (x::real)"
7.31 + apply (insert asm3 asm4)
7.32 apply simp
7.33 -*)
7.34 +sorry
7.35
7.36 -end
7.37 +ML {* @{thm nonzero_mult_divide_mult_cancel_right}*}
7.38 +
7.39 +end
7.40 \ No newline at end of file
8.1 --- a/test/Tools/isac/Test_Isac.thy Mon May 09 10:43:43 2011 +0200
8.2 +++ b/test/Tools/isac/Test_Isac.thy Wed May 11 07:28:13 2011 +0200
8.3 @@ -11,6 +11,7 @@
8.4 theory Test_Isac imports
8.5 Isac
8.6 "Knowledge/Rational_Test"
8.7 + "ADDTESTS/Ctxt"
8.8
8.9 uses
8.10 ( "library.sml")