39 (*val (_, hdl, (dI, pI, mI), pors, pctxt) = *) |
39 (*val (_, hdl, (dI, pI, mI), pors, pctxt) = *) |
40 Step_Specify.initialise thy (model, refs); |
40 Step_Specify.initialise thy (model, refs); |
41 "~~~~~ fun initialise , args:"; val (thy, (fmz, (_, pI, mI))) = (thy, (model, refs)); |
41 "~~~~~ fun initialise , args:"; val (thy, (fmz, (_, pI, mI))) = (thy, (model, refs)); |
42 val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *); |
42 val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *); |
43 (*if*) mI = ["no_met"] (*else*); |
43 (*if*) mI = ["no_met"] (*else*); |
44 val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz; |
44 val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; |
45 (*+*)Problem.from_store ctxt pI: Problem.T; |
45 (*+*)Problem.from_store ctxt pI: Problem.T; |
46 (*+*)(Problem.from_store ctxt pI |> #model): Model_Pattern.T; |
46 (*+*)(Problem.from_store ctxt pI |> #model): Model_Pattern.T; |
47 |
47 |
48 (*+*)val o_model = (Problem.from_store ctxt pI |> #model |> |
48 (*+*)val (o_model, ctxt) = (Problem.from_store ctxt pI |> #model |> |
49 O_Model.init thy fmz); |
49 O_Model.init thy fmz); |
50 "~~~~~ fun init , args:"; val (fmz, thy, pbt) = (fmz, thy, Problem.from_store ctxt pI |> #model); |
50 "~~~~~ fun init , args:"; val (fmz, thy, pbt) = (fmz, thy, Problem.from_store ctxt pI |> #model); |
51 val ori = (map (fn str => str |
51 val ori = (map (fn str => str |
52 |> TermC.parseNEW'' thy |
52 |> TermC.parseNEW'' thy |
53 |> Input_Descript.split |
53 |> Input_Descript.split |
176 "interval {x::real. 0 <= x & x <= 2*r}", |
176 "interval {x::real. 0 <= x & x <= 2*r}", |
177 "interval {x::real. 0 <= x & x <= pi}", |
177 "interval {x::real. 0 <= x & x <= pi}", |
178 "errorBound (eps=(0::real))"] |
178 "errorBound (eps=(0::real))"] |
179 val pbt as {model = model,...} = |
179 val pbt as {model = model,...} = |
180 Problem.from_store @{context} ["maximum_of", "function"]; |
180 Problem.from_store @{context} ["maximum_of", "function"]; |
181 val o_model = O_Model.init @{theory} formalise model; |
181 val (o_model, ctxt) = O_Model.init @{theory} formalise model; |
182 |
182 |
183 case o_model of |
183 case o_model of |
184 [ |
184 [ |
185 (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]), |
185 (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]), |
186 (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]), |
186 (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]), |