Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/eqsystem-1.sml
changeset 60565 f92963a33fe3
parent 60559 aba19e46dd84
child 60567 bb3140a02f3d
equal deleted inserted replaced
60564:90ea835c07b3 60565:f92963a33fe3 
    31 val ctxt = Proof_Context.init_global thy;
 
    31 val ctxt = Proof_Context.init_global thy;
 
    32 
    32 
    33 "----------- occur_exactly_in ------------------------------------";
 
    33 "----------- occur_exactly_in ------------------------------------";
 
    34 "----------- occur_exactly_in ------------------------------------";
 
    34 "----------- occur_exactly_in ------------------------------------";
 
    35 "----------- occur_exactly_in ------------------------------------";
 
    35 "----------- occur_exactly_in ------------------------------------";
 
    36 val all = [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"];
 
    36 val all = [TermC.parse_test @{context}"c", TermC.parse_test @{context}"c_2", TermC.parse_test @{context}"c_3"];
 
    37 val t = TermC.str2term"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
 
    37 val t = TermC.parse_test @{context}"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
 
    38 
    38 
    39 if occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2"] all t
 
    39 if occur_exactly_in [TermC.parse_test @{context}"c", TermC.parse_test @{context}"c_2"] all t
 
    40 then () else error "eqsystem.sml occur_exactly_in 1";
 
    40 then () else error "eqsystem.sml occur_exactly_in 1";
 
    41 
    41 
    42 if not (occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"] all t)
 
    42 if not (occur_exactly_in [TermC.parse_test @{context}"c", TermC.parse_test @{context}"c_2", TermC.parse_test @{context}"c_3"] all t)
 
    43 then () else error "eqsystem.sml occur_exactly_in 2";
 
    43 then () else error "eqsystem.sml occur_exactly_in 2";
 
    44 
    44 
    45 if not (occur_exactly_in [TermC.str2term"c_2"] all t)
 
    45 if not (occur_exactly_in [TermC.parse_test @{context}"c_2"] all t)
 
    46 then () else error "eqsystem.sml occur_exactly_in 3";
 
    46 then () else error "eqsystem.sml occur_exactly_in 3";
 
    47 
    47 
    48 val t = TermC.str2term"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
 
    48 val t = TermC.parse_test @{context}"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
 
    49 eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
 
    49 eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
 
    50 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
 
    50 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
 
    51 if str = "[c, c_2] from [c, c_2,\n" ^
 
    51 if str = "[c, c_2] from [c, c_2,\n" ^
 
    52   "               c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
 
    52   "               c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
 
    53 then () else error "eval_occur_exactly_in [c, c_2]";
 
    53 then () else error "eval_occur_exactly_in [c, c_2]";
 
    54 
    54 
    55 val t = TermC.str2term ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
 
    55 val t = TermC.parse_test @{context} ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
 
    56 		  "- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
 
    56 		  "- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
 
    57 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
 
    57 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
 
    58 if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
 
    58 if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
 
    59 "            c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
 
    59 "            c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
 
    60 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
 
    60 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
 
    61 
    61 
    62 val t = TermC.str2term"[c_2] from [c,c_2,c_3] occur_exactly_in \
 
    62 val t = TermC.parse_test @{context}"[c_2] from [c,c_2,c_3] occur_exactly_in \
 
    63 		\- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
 
    63 		\- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
 
    64 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
 
    64 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
 
    65 if str = "[c_2] from [c, c_2,\n" ^
 
    65 if str = "[c_2] from [c, c_2,\n" ^
 
    66   "            c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
 
    66   "            c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
 
    67 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
 
    67 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
 
    68 
    68 
    69 val t = TermC.str2term"[] from [c,c_2,c_3] occur_exactly_in 0";
 
    69 val t = TermC.parse_test @{context}"[] from [c,c_2,c_3] occur_exactly_in 0";
 
    70 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
 
    70 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
 
    71 if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
 
    71 if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
 
    72 else error "eval_occur_exactly_in [c, c_2, c_3]";
 
    72 else error "eval_occur_exactly_in [c, c_2, c_3]";
 
    73 
    73 
    74 val t = 
    74 val t = 
    75     TermC.str2term
 
    75     TermC.parse_test @{context}
 
    76 	"[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";
 
    76 	"[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";
 
    77 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
 
    77 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
 
    78 if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
 
    78 if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
 
    79 	 \- 1 * (q_0 * L \<up> 2) / 2 = True" then ()
 
    79 	 \- 1 * (q_0 * L \<up> 2) / 2 = True" then ()
 
    80 else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
 
    80 else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
 
    81 
    81 
    82 "----------- problems --------------------------------------------";
 
    82 "----------- problems --------------------------------------------";
 
    83 "----------- problems --------------------------------------------";
 
    83 "----------- problems --------------------------------------------";
 
    84 "----------- problems --------------------------------------------";
 
    84 "----------- problems --------------------------------------------";
 
    85 val t = TermC.str2term "Length [x+y=1,y=2] = 2";
 
    85 val t = TermC.parse_test @{context} "Length [x+y=1,y=2] = 2";
 
    86 TermC.atomty t;
 
    86 TermC.atomty t;
 
    87 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty 
    87 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty 
    88 			 [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
 
    88 			 [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
 
    89 			  (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
 
    89 			  (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
 
    90 			  Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
 
    90 			  Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
 
    97 val SOME t = TermC.parseNEW ctxt "solution LL";
 
    97 val SOME t = TermC.parseNEW ctxt "solution LL";
 
    98 TermC.atomty t;
 
    98 TermC.atomty t;
 
    99 val SOME t = TermC.parseNEW ctxt "solution LL";
 
    99 val SOME t = TermC.parseNEW ctxt "solution LL";
 
   100 TermC.atomty t;
 
   100 TermC.atomty t;
 
   101 
   101 
   102 val t = TermC.str2term 
   102 val t = TermC.parse_test @{context} 
   103 "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
 
   103 "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
 
   104 TermC.atomty t;
 
   104 TermC.atomty t;
 
   105 val t = TermC.str2term ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
 
   105 val t = TermC.parse_test @{context} ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
 
   106   "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
 
   106   "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
 
   107 (*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
 
   107 (*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
 
   108         assume flawed test setup hidden by "handle _ => ..."
 
   108         assume flawed test setup hidden by "handle _ => ..."
 
   109         ERROR rewrite__set_ called with 'Erls' for '1 < 1'
 
   109         ERROR rewrite__set_ called with 'Erls' for '1 < 1'
 
   110 val SOME (t,_) = 
   110 val SOME (t,_) = 
   124 "----------- rewrite-order ord_simplify_System -------------------";
 
   124 "----------- rewrite-order ord_simplify_System -------------------";
 
   125 "----------- rewrite-order ord_simplify_System -------------------";
 
   125 "----------- rewrite-order ord_simplify_System -------------------";
 
   126 "----------- rewrite-order ord_simplify_System -------------------";
 
   126 "----------- rewrite-order ord_simplify_System -------------------";
 
   127 "M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
 
   127 "M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
 
   128 "--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
 
   128 "--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
 
   129 if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)", 
   129 if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", 
   130 				       TermC.str2term"c * x") then ()
 
   130 				       TermC.parse_test @{context}"c * x") then ()
 
   131 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
 
   131 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
 
   132 
   132 
   133 if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)", 
   133 if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", 
   134 				       TermC.str2term"c_2") then ()
 
   134 				       TermC.parse_test @{context}"c_2") then ()
 
   135 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
 
   135 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
 
   136 
   136 
   137 if ord_simplify_System false thy [] (TermC.str2term"c * x", 
   137 if ord_simplify_System false thy [] (TermC.parse_test @{context}"c * x", 
   138 				       TermC.str2term"c_2") then ()
 
   138 				       TermC.parse_test @{context}"c_2") then ()
 
   139 else error "integrate.sml, (c * x) < (c_2) not#3";
 
   139 else error "integrate.sml, (c * x) < (c_2) not#3";
 
   140 
   140 
   141 "--- mult.commute ---";
 
   141 "--- mult.commute ---";
 
   142 if ord_simplify_System false thy [] (TermC.str2term"x * c", 
   142 if ord_simplify_System false thy [] (TermC.parse_test @{context}"x * c", 
   143 				       TermC.str2term"c * x") then ()
 
   143 				       TermC.parse_test @{context}"c * x") then ()
 
   144 else error "integrate.sml, (x * c) < (c * x) not#4";
 
   144 else error "integrate.sml, (x * c) < (c * x) not#4";
 
   145 
   145 
   146 if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c", 
   146 if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", 
   147 				       TermC.str2term"- 1 * q_0 * c * (x \<up> 2 / 2)") 
   147 				       TermC.parse_test @{context}"- 1 * q_0 * c * (x \<up> 2 / 2)") 
   148 then () else error "integrate.sml, (. * .) < (. * .) not#5";
 
   148 then () else error "integrate.sml, (. * .) < (. * .) not#5";
 
   149 
   149 
   150 if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c", 
   150 if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", 
   151 				       TermC.str2term"c * - 1 * q_0 * (x \<up> 2 / 2)") 
   151 				       TermC.parse_test @{context}"c * - 1 * q_0 * (x \<up> 2 / 2)") 
   152 then () else error "integrate.sml, (. * .) < (. * .) not#6";
 
   152 then () else error "integrate.sml, (. * .) < (. * .) not#6";
 
   153 
   153 
   154 
   154 
   155 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
 
   155 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
 
   156 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
 
   156 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
 
   157 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
 
   157 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
 
   158 val t = TermC.str2term"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
 
   158 val t = TermC.parse_test @{context}"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
 
   159 	        \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
 
   159 	        \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
 
   160 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
 
   160 val bdvs = [(TermC.parse_test @{context}"bdv_1",TermC.parse_test @{context}"c"),
 
   161 	    (TermC.str2term"bdv_2",TermC.str2term"c_2")];
 
   161 	    (TermC.parse_test @{context}"bdv_2",TermC.parse_test @{context}"c_2")];
 
   162 val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
 
   162 val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
 
   163 if UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
 
   163 if UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
 
   164 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
 
   164 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
 
   165 
   165 
   166 val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
 
   166 val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
 
   180 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
 
   180 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
 
   181 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
 
   181 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
 
   182 val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
 
   182 val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
 
   183 val ctxt = Proof_Context.init_global thy;
 
   183 val ctxt = Proof_Context.init_global thy;
 
   184 val t = 
   184 val t = 
   185     TermC.str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 +         \
 
   185     TermC.parse_test @{context}"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 +         \
 
   186 	    \                                     - 1 * q_0 / 24 * 0 \<up> 4),\
 
   186 	    \                                     - 1 * q_0 / 24 * 0 \<up> 4),\
 
   187 	    \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 +         \
 
   187 	    \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 +         \
 
   188 	    \                                     - 1 * q_0 / 24 * L \<up> 4)]";
 
   188 	    \                                     - 1 * q_0 / 24 * L \<up> 4)]";
 
   189 val SOME (t, _) = rewrite_set_ ctxt true norm_Rational t;
 
   189 val SOME (t, _) = rewrite_set_ ctxt true norm_Rational t;
 
   190 if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
 
   190 if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
 
   216 
   216 
   217 
   217 
   218 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
 
   218 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
 
   219 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
 
   219 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
 
   220 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
 
   220 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
 
   221 val e1__ = TermC.str2term "c_2 = 77";
 
   221 val e1__ = TermC.parse_test @{context} "c_2 = 77";
 
   222 val e2__ = TermC.str2term "L * c + c_2 = q_0 * L \<up> 2 / 2";
 
   222 val e2__ = TermC.parse_test @{context} "L * c + c_2 = q_0 * L \<up> 2 / 2";
 
   223 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
 
   223 val bdvs = [(TermC.parse_test @{context}"bdv_1",TermC.parse_test @{context}"c"),
 
   224 	    (TermC.str2term"bdv_2",TermC.str2term"c_2")];
 
   224 	    (TermC.parse_test @{context}"bdv_2",TermC.parse_test @{context}"c_2")];
 
   225 val SOME (e2__,_) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty [e1__] e2__;
 
   225 val SOME (e2__,_) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty [e1__] e2__;
 
   226 if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
 
   226 if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
 
   227 else error "eqsystem.sml top_down_substitution,2x2] subst";
 
   227 else error "eqsystem.sml top_down_substitution,2x2] subst";
 
   228 
   228 
   229 val SOME (e2__,_) = 
   229 val SOME (e2__,_) = 
   233 
   233 
   234 val SOME (e2__,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs e2__;
 
   234 val SOME (e2__,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs e2__;
 
   235 if UnparseC.term e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
 
   235 if UnparseC.term e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
 
   236 else error "eqsystem.sml top_down_substitution,2x2] isolate";
 
   236 else error "eqsystem.sml top_down_substitution,2x2] isolate";
 
   237 
   237 
   238 val t = TermC.str2term "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
 
   238 val t = TermC.parse_test @{context} "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
 
   239 val SOME (t,_) = rewrite_set_ ctxt true order_system t;
 
   239 val SOME (t,_) = rewrite_set_ ctxt true order_system t;
 
   240 if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
 
   240 if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
 
   241 else error "eqsystem.sml top_down_substitution,2x2] order_system";
 
   241 else error "eqsystem.sml top_down_substitution,2x2] order_system";
 
   242 
   242 
   243 if not (ord_simplify_System
 
   243 if not (ord_simplify_System
 
   244 	    false thy [] 
   244 	    false thy [] 
   245 	    (TermC.str2term"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]", 
   245 	    (TermC.parse_test @{context}"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]", 
   246 	     TermC.str2term"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]")) 
   246 	     TermC.parse_test @{context}"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]")) 
   247 then () else error "eqsystem.sml, order_result rew_ord";
 
   247 then () else error "eqsystem.sml, order_result rew_ord";
 
   248 
   248 
   249 
   249 
   250 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
 
   250 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
 
   251 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
 
   251 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
 
   252 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
 
   252 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
 
   253 (*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
 
   253 (*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
 
   254 val t = TermC.str2term (
 
   254 val t = TermC.parse_test @{context} (
 
   255   "[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^ 
   255   "[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^ 
   256   "(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^ 
   256   "(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^ 
   257   "c + c_2 + c_3 + c_4 = 0, " ^ 
   257   "c + c_2 + c_3 + c_4 = 0, " ^ 
   258   "c_2 + c_3 + c_4 = 0]");
 
   258   "c_2 + c_3 + c_4 = 0]");
 
   259 val bdvs = [(TermC.str2term"bdv_1::real",TermC.str2term"c::real"),
 
   259 val bdvs = [(TermC.parse_test @{context}"bdv_1::real",TermC.parse_test @{context}"c::real"),
 
   260 	    (TermC.str2term"bdv_2::real",TermC.str2term"c_2::real"),
 
   260 	    (TermC.parse_test @{context}"bdv_2::real",TermC.parse_test @{context}"c_2::real"),
 
   261 	    (TermC.str2term"bdv_3::real",TermC.str2term"c_3::real"),
 
   261 	    (TermC.parse_test @{context}"bdv_3::real",TermC.parse_test @{context}"c_3::real"),
 
   262 	    (TermC.str2term"bdv_4::real",TermC.str2term"c_4::real")];
 
   262 	    (TermC.parse_test @{context}"bdv_4::real",TermC.parse_test @{context}"c_4::real")];
 
   263 val SOME (t, _) = 
   263 val SOME (t, _) = 
   264     rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
 
   264     rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
 
   265 if UnparseC.term t = "[0 = c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4),\n c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
 
   265 if UnparseC.term t = "[0 = c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4),\n c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
 
   266 then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
 
   266 then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
 
   267 
   267 
   365 	  "solveForVars [c, c_2]", "solution LL"];
 
   365 	  "solveForVars [c, c_2]", "solution LL"];
 
   366 val matches = Refine.refine_PIDE @{context} fmz ["triangular", "2x2", "LINEAR", "system"];
 
   366 val matches = Refine.refine_PIDE @{context} fmz ["triangular", "2x2", "LINEAR", "system"];
 
   367 (*... resulted in 
   367 (*... resulted in 
   368    False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n    
   368    False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n    
   369           [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
 
   369           [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
 
   370 val t = TermC.str2term ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^   
   370 val t = TermC.parse_test @{context} ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^   
   371 		  "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");
 
   371 		  "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");
 
   372 
   372 
   373 val SOME (t', _) = rewrite_set_ ctxt false prls_triangular t;
 
   373 val SOME (t', _) = rewrite_set_ ctxt false prls_triangular t;
 
   374 (*found:...
 
   374 (*found:...
 
   375 ##  try thm: NTH_CONS
 
   375 ##  try thm: NTH_CONS
wneuper/isa