281 "0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + (c_2::real)]", |
281 "0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + (c_2::real)]", |
282 "solveForVars [c, c_2]", "solution LL"]; |
282 "solveForVars [c, c_2]", "solution LL"]; |
283 |
283 |
284 (*WN120313 in "solution L" above "refine fmz ["LINEAR","system"]" caused an error...*) |
284 (*WN120313 in "solution L" above "refine fmz ["LINEAR","system"]" caused an error...*) |
285 "~~~~~ fun refine, args:"; val ((fmz:fmz_), (pblID:pblID)) = (fmz, ["LINEAR","system"]); |
285 "~~~~~ fun refine, args:"; val ((fmz:fmz_), (pblID:pblID)) = (fmz, ["LINEAR","system"]); |
286 "~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Store.Ptyp (pI, [py], [])): pbt Store.ptyp)) = |
286 "~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Store.Node (pI, [py], [])): pbt Store.node)) = |
287 ((rev o tl) pblID, fmz, [(*match list*)], |
287 ((rev o tl) pblID, fmz, [(*match list*)], |
288 ((Store.Ptyp ("LINEAR", [get_pbt ["LINEAR","system"]], [])): pbt Store.ptyp)); |
288 ((Store.Node ("LINEAR", [get_pbt ["LINEAR","system"]], [])): pbt Store.node)); |
289 val {thy, ppc, where_, prls, ...} = py ; |
289 val {thy, ppc, where_, prls, ...} = py ; |
290 "~~~~~ fun prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc); |
290 "~~~~~ fun prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc); |
291 val ctxt = Proof_Context.init_global thy; |
291 val ctxt = Proof_Context.init_global thy; |
292 "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt); |
292 "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt); |
293 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of |
293 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of |
425 val matches = refine fmz ["2x2", "LINEAR","system"]; |
425 val matches = refine fmz ["2x2", "LINEAR","system"]; |
426 trace_rewrite:=false; |
426 trace_rewrite:=false; |
427 (*default_print_depth 11;*) matches; (*default_print_depth 3;*) |
427 (*default_print_depth 11;*) matches; (*default_print_depth 3;*) |
428 (*brought: 'False "length_ es_ = 2"'*) |
428 (*brought: 'False "length_ es_ = 2"'*) |
429 |
429 |
430 (*-----fun refin' (pblRD:pblRD) fmz pbls ((Store.Ptyp (pI,[py],[])):pbt Store.ptyp) = |
430 (*-----fun refin' (pblRD:pblRD) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) = |
431 (* val ((pblRD:pblRD), fmz, pbls, ((Store.Ptyp (pI,[py],[])):pbt Store.ptyp)) = |
431 (* val ((pblRD:pblRD), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) = |
432 (rev ["LINEAR","system"], fmz, [(*match list*)], |
432 (rev ["LINEAR","system"], fmz, [(*match list*)], |
433 ((Store.Ptyp ("2x2",[get_pbt ["2x2","LINEAR","system"]],[])):pbt Store.ptyp)); |
433 ((Store.Node ("2x2",[get_pbt ["2x2","LINEAR","system"]],[])):pbt Store.store)); |
434 *) |
434 *) |
435 > show_types:=true; UnparseC.term (hd where_); show_types:=false; |
435 > show_types:=true; UnparseC.term (hd where_); show_types:=false; |
436 val it = "length_ (es_::real list) = (2::real)" : string |
436 val it = "length_ (es_::real list) = (2::real)" : string |
437 |
437 |
438 =========================================================================\ |
438 =========================================================================\ |