461 (*\------------------- check within item_to_add --------------------------------------------/*) |
461 (*\------------------- check within item_to_add --------------------------------------------/*) |
462 |
462 |
463 (*if*) icl = [] (*else*); |
463 (*if*) icl = [] (*else*); |
464 val SOME ori =(*case*) find_first (test_subset (hd icl)) vors (*of*); |
464 val SOME ori =(*case*) find_first (test_subset (hd icl)) vors (*of*); |
465 |
465 |
466 (*+*)val (5, [1], "#Given", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]) = ori |
466 (*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) = ori |
467 (*+*)val SOME ("#Given", "FunktionsVariable x") = |
467 (*+*)val SOME ("#Given", "FunktionsVariable x") = |
468 |
468 |
469 SOME |
469 SOME |
470 (I_Model.geti_ct thy ori (hd icl)) (*return from item_to_add*); |
470 (I_Model.geti_ct thy ori (hd icl)) (*return from item_to_add*); |
471 "~~~~~ ~~ fun geti_ct , args:"; val (thy, (_, _, _, d, ts), (_, _, _, fd, itm_)) = (thy, ori, (hd icl)); |
471 "~~~~~ ~~ fun geti_ct , args:"; val (thy, (_, _, _, d, ts), (_, _, _, fd, itm_)) = (thy, ori, (hd icl)); |
495 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos); |
495 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos); |
496 (*if*) p_ = Pos.Met (*then*); |
496 (*if*) p_ = Pos.Met (*then*); |
497 val (i_model, m_patt) = (met, |
497 val (i_model, m_patt) = (met, |
498 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc) |
498 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc) |
499 |
499 |
500 val Add (5, [1], true, "#Given", Cor ((Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) = |
500 val Add (5, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) = |
501 (*case*) |
501 (*case*) |
502 I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*); |
502 I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*); |
503 "~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) = |
503 "~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) = |
504 (ctxt, m_field, oris, i_model, m_patt, ct); |
504 (ctxt, m_field, oris, i_model, m_patt, ct); |
505 (*.NEW*) val SOME (t as (descriptor $ _)) = (*case*) TermC.parseNEW ctxt str (*of*); |
505 (*.NEW*) val SOME (t as (descriptor $ _)) = (*case*) TermC.parseNEW ctxt str (*of*); |
506 (*.NEW*) val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*); |
506 (*.NEW*) val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*); |
507 |
507 |
508 val ("", (5, [1], "#Given", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), [Free ("x", _)]) = |
508 val ("", (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), [Free ("x", _)]) = |
509 (*case*) |
509 (*case*) |
510 O_Model.is_known ctxt m_field o_model t (*of*); |
510 O_Model.is_known ctxt m_field o_model t (*of*); |
511 "~~~~~ ~~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t); |
511 "~~~~~ ~~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t); |
512 val ots = ((distinct op =) o flat o (map #5)) ori |
512 val ots = ((distinct op =) o flat o (map #5)) ori |
513 val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots |
513 val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots |
522 (ctxt, sel, (d, ts), ori); |
522 (ctxt, sel, (d, ts), ori); |
523 |
523 |
524 (*/------------------- check within seek_oridts --------------------------------------------\*) |
524 (*/------------------- check within seek_oridts --------------------------------------------\*) |
525 (*+*)val Add_Given "FunktionsVariable x" = tac; |
525 (*+*)val Add_Given "FunktionsVariable x" = tac; |
526 (*+*)m_field = "#Given"; |
526 (*+*)m_field = "#Given"; |
527 (*+*)val Const ("Biegelinie.FunktionsVariable", _) = descript; |
527 (*+*)val Const (\<^const_name>\<open>FunktionsVariable\<close>, _) = descript; |
528 (*+*)val [Free ("x", _)] = vals; |
528 (*+*)val [Free ("x", _)] = vals; |
529 (*+*)O_Model.to_string ori = "[\n" ^ |
529 (*+*)O_Model.to_string ori = "[\n" ^ |
530 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^ |
530 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^ |
531 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^ |
531 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^ |
532 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^ |
532 "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^ |
533 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^ |
533 "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^ |
534 "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^ |
534 "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^ |
535 "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^ |
535 "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^ |
536 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"; |
536 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"; |
537 (*+*)val (id, vat, m_field', descript', vals') = nth 5 ori |
537 (*+*)val (id, vat, m_field', descript', vals') = nth 5 ori |
538 (*+*)val (5, [1], "#Given", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]) = |
538 (*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) = |
539 (id, vat, m_field', descript', vals') |
539 (id, vat, m_field', descript', vals') |
540 (*\------------------- check within seek_oridts --------------------------------------------/*) |
540 (*\------------------- check within seek_oridts --------------------------------------------/*) |
541 (*-------------------- stop step into whole me ----------------------------------------------*) |
541 (*-------------------- stop step into whole me ----------------------------------------------*) |
542 (*\------------------- step into whole me \<rightarrow>Specify_Method |||||||||||||||||||||||||||||||||/*) |
542 (*\------------------- step into whole me \<rightarrow>Specify_Method |||||||||||||||||||||||||||||||||/*) |
543 |
543 |
778 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos); |
778 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos); |
779 (*if*) p_ = Pos.Met (*then*); |
779 (*if*) p_ = Pos.Met (*then*); |
780 val (i_model, m_patt) = (met, |
780 val (i_model, m_patt) = (met, |
781 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc) |
781 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc) |
782 |
782 |
783 val Add (4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", _), [Free ("y", _)]), (Free ("id_fun", _), [Free ("y", _)]))) = |
783 val Add (4, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]), (Free ("id_fun", _), [Free ("y", _)]))) = |
784 (*case*) |
784 (*case*) |
785 check_single ctxt m_field oris i_model m_patt ct (*of*); |
785 check_single ctxt m_field oris i_model m_patt ct (*of*); |
786 |
786 |
787 (*/------------------- check for entry to check_single -------------------------------------\*) |
787 (*/------------------- check for entry to check_single -------------------------------------\*) |
788 (*+*)if O_Model.to_string oris = "[\n" ^ |
788 (*+*)if O_Model.to_string oris = "[\n" ^ |
803 |
803 |
804 "~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) = |
804 "~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) = |
805 (ctxt, sel, oris, met, ((#ppc o MethodC.from_store) cmI), ct); |
805 (ctxt, sel, oris, met, ((#ppc o MethodC.from_store) cmI), ct); |
806 val SOME t = (*case*) TermC.parseNEW ctxt str (*of*); |
806 val SOME t = (*case*) TermC.parseNEW ctxt str (*of*); |
807 |
807 |
808 (*+*)val Const ("Biegelinie.Biegelinie", _) $ Free ("y", _) = t; |
808 (*+*)val Const (\<^const_name>\<open>Biegelinie\<close>, _) $ Free ("y", _) = t; |
809 |
809 |
810 (*("seek_oridts: input ('Biegelinie y') not found in oris (typed)", (0, [], "#Given", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]), [])*) |
810 (*("seek_oridts: input ('Biegelinie y') not found in oris (typed)", (0, [], "#Given", Const (\<^const_name>\<open>Biegelinie\<close>, "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]), [])*) |
811 (*case*) |
811 (*case*) |
812 is_known ctxt m_field o_model t (*of*); |
812 is_known ctxt m_field o_model t (*of*); |
813 "~~~~~ ~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t); |
813 "~~~~~ ~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t); |
814 val ots = ((distinct op =) o flat o (map #5)) ori |
814 val ots = ((distinct op =) o flat o (map #5)) ori |
815 val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots |
815 val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots |