1.1 --- a/src/sml/IsacKnowledge/EqSystem.ML	Thu Sep 14 15:29:45 2006 +0200
     1.2 +++ b/src/sml/IsacKnowledge/EqSystem.ML	Thu Sep 14 16:14:01 2006 +0200
     1.3 @@ -323,6 +323,33 @@
     1.4  		  ],
     1.5  	 scr = EmptyScr};
     1.6  
     1.7 +(*WN060914 quickly created for 4x4; 
     1.8 + more similarity to prls_triangular desirable*)
     1.9 +val prls_triangular4 = 
    1.10 +    Rls {id="prls_triangular4", preconds = [], 
    1.11 +	 rew_ord = ("e_rew_ord", e_rew_ord), 
    1.12 +	 erls = Rls {id="erls_prls_triangular4", preconds = [], 
    1.13 +		     rew_ord = ("e_rew_ord", e_rew_ord), 
    1.14 +		     erls = Erls, srls = Erls, calc = [],
    1.15 +		     rules = [(*for precond nth_Cons_ ...*)
    1.16 +			      Calc ("op <",eval_equ "#less_"),
    1.17 +			      Calc ("op +", eval_binop "#add_")
    1.18 +			      (*immediately repeated rewrite pushes
    1.19 +					    '+' into precondition !*)
    1.20 +			      ],
    1.21 +		     scr = EmptyScr}, 
    1.22 +	 srls = Erls, calc = [],
    1.23 +	 rules = [Thm ("nth_Cons_",num_str nth_Cons_),
    1.24 +		  Calc ("op +", eval_binop "#add_"),
    1.25 +		  Thm ("nth_Nil_",num_str nth_Nil_),
    1.26 +		  Thm ("tl_Cons",num_str tl_Cons),
    1.27 +		  Thm ("tl_Nil",num_str tl_Nil),
    1.28 +		  Calc ("EqSystem.occur'_exactly'_in", 
    1.29 +			eval_occur_exactly_in 
    1.30 +			    "#eval_occur_exactly_in_")
    1.31 +		  ],
    1.32 +	 scr = EmptyScr};
    1.33 +
    1.34  ruleset' := 
    1.35  overwritelthy thy 
    1.36  	      (!ruleset', 
    1.37 @@ -448,11 +475,11 @@
    1.38   (prep_pbt EqSystem.thy "pbl_equsys_lin_4x4_tri" [] e_pblID
    1.39   (["triangular", "4x4", "linear", "system"],
    1.40    [("#Given" ,["equalities es_", "solveForVars vs_"]),
    1.41 -   ("#Where" , (*accepts missing*)
    1.42 -    ["(tl (tl (tl vs_))) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))",
    1.43 -     "    (tl (tl vs_))  from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))",
    1.44 -     "        (tl vs_)   from_ vs_ occur_exactly_in (nth_ 3 (es_::bool list))",
    1.45 -     "            vs_    from_ vs_ occur_exactly_in (nth_ 4 (es_::bool list))"
    1.46 +   ("#Where" , (*accepts missing variables up to diagional form*)
    1.47 +    ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))",
    1.48 +     "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))",
    1.49 +     "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))",
    1.50 +     "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))"
    1.51       ]),
    1.52     ("#Find"  ,["solution ss___"])
    1.53    ],

     2.1 --- a/src/smltest/IsacKnowledge/eqsystem.sml	Thu Sep 14 15:29:45 2006 +0200
     2.2 +++ b/src/smltest/IsacKnowledge/eqsystem.sml	Thu Sep 14 16:14:01 2006 +0200
     2.3 @@ -729,6 +729,22 @@
     2.4  trace_rewrite:=false;
     2.5  (*WN051014------------------------------------------------------------------*)
     2.6  
     2.7 +"----- relaxed preconditions for triangular system";
     2.8 +val fmz = ["equalities [L * q_0 = c,                                       \
     2.9 +	   \            0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
    2.10 +	   \            0 = c_4 + 0 / (-1 * EI),                           \
    2.11 +	   \            0 = c_3 + 0 / (-1 * EI)]", 
    2.12 +	   "solveForVars [c, c_2, c_3, c_4]", "solution L"];
    2.13 +(*
    2.14 +val matches = refine fmz ["linear","system"];
    2.15 +val t =str2term"(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))";
    2.16 +val t =str2term"(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_))";
    2.17 +val t =str2term"(nth_ 2 (vs_)) occurs_in (nth_ 2 (es_))";
    2.18 +atomty t;
    2.19 +*)
    2.20 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
    2.21 +
    2.22 +
    2.23  
    2.24  "----------- refine [2x2,linear,system] search error--------------";
    2.25  "----------- refine [2x2,linear,system] search error--------------";
    2.26 @@ -994,7 +1010,7 @@
    2.27      rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
    2.28  term2str t = "0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)";
    2.29  "--- isolate_bdvs_4x4";
    2.30 -(*@@@@@
    2.31 +(*
    2.32  val Some (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
    2.33  term2str t;
    2.34  val Some (t,_) = rewrite_set_inst_ thy false subst simplify_System t;