1.1 --- a/src/sml/IsacKnowledge/Atools.ML Fri Sep 08 20:33:59 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/Atools.ML Thu Sep 14 09:27:48 2006 +0200
1.3 @@ -58,7 +58,27 @@
1.4 else Some ((term2str p) ^ " = False",
1.5 Trueprop $ (mk_equality (p, HOLogic.false_const))))
1.6 | eval_occurs_in _ _ _ _ = None;
1.7 -
1.8 +
1.9 +(*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
1.10 +fun some_occur_in vs t =
1.11 + let fun occurs_in' a b = occurs_in b a
1.12 + in foldl or_ (false, map (occurs_in' t) vs) end;
1.13 +
1.14 +(*("some_occur_in", ("Atools.some'_occur'_in",
1.15 + eval_some_occur_in "#eval_some_occur_in_"))*)
1.16 +fun eval_some_occur_in _ "Atools.some'_occur'_in"
1.17 + (p as (Const ("Atools.some'_occur'_in",_)
1.18 + $ vs $ t)) _ =
1.19 + if some_occur_in (isalist2list vs) t
1.20 + then Some ((term2str p) ^ " = True",
1.21 + Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.22 + else Some ((term2str p) ^ " = False",
1.23 + Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.24 + | eval_some_occur_in _ _ _ _ = None;
1.25 +
1.26 +
1.27 +
1.28 +
1.29 (*evaluate 'is_atom'*)
1.30 (*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)
1.31 fun eval_is_atom (thmid:string) "Atools.is'_atom"
1.32 @@ -517,6 +537,8 @@
1.33
1.34 calclist':= overwritel (!calclist',
1.35 [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
1.36 + ("some_occur_in",
1.37 + ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
1.38 ("is_atom" ,("Atools.is'_atom",eval_is_atom "#is_atom_")),
1.39 ("is_even" ,("Atools.is'_even",eval_is_even "#is_even_")),
1.40 ("is_const" ,("Atools.is'_const",eval_const "#is_const_")),
2.1 --- a/src/sml/IsacKnowledge/Atools.thy Fri Sep 08 20:33:59 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/Atools.thy Thu Sep 14 09:27:48 2006 +0200
2.3 @@ -18,7 +18,8 @@
2.4 Arbfix, Undef :: real
2.5 dummy :: real
2.6
2.7 - occurs'_in :: "[real, real] => bool" ("_ occurs'_in _")
2.8 + some'_occur'_in :: "[real list, real] => bool" ("some'_of _ occur'_in _")
2.9 + occurs'_in :: "[real , real] => bool" ("_ occurs'_in _")
2.10
2.11 "pow" :: [real, real] => real (infixr "^^^" 80)
2.12 (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
3.1 --- a/src/sml/IsacKnowledge/EqSystem.ML Fri Sep 08 20:33:59 2006 +0200
3.2 +++ b/src/sml/IsacKnowledge/EqSystem.ML Thu Sep 14 09:27:48 2006 +0200
3.3 @@ -18,7 +18,7 @@
3.4 (*certain variables of a given list occur _all_ in a term
3.5 args: all: ..variables, which are under consideration (eg. the bound vars)
3.6 vs: variables which must be in t,
3.7 - an none of the others in all must be in t
3.8 + and none of the others in all must be in t
3.9 t: the term under consideration
3.10 *)
3.11 fun occur_exactly_in vs all t =
3.12 @@ -207,7 +207,7 @@
3.13 *1* ord_simplify_System instead of termlessI
3.14 *2* no add_fractions_p (= common_nominator_p_rls !)
3.15 *3* discard_parentheses only for (.*(.*.))
3.16 - analoguous to simplif_Integral .*)
3.17 + analoguous to simplify_Integral .*)
3.18 val simplify_System_parenthesized =
3.19 Seq {id = "simplify_System_parenthesized", preconds = []:term list,
3.20 rew_ord = ("dummy_ord", dummy_ord),
3.21 @@ -278,11 +278,7 @@
3.22 srls = Erls, calc = [],
3.23 rules = [Thm ("commute_0_equality",
3.24 num_str commute_0_equality),
3.25 - Thm ("separate_bdvs_add", num_str separate_bdvs_add),
3.26 Thm ("separate_bdvs_add1", num_str separate_bdvs_add1),
3.27 - Thm ("separate_bdvs_add2", num_str separate_bdvs_add2),
3.28 - Thm ("separate_bdvs_add3", num_str separate_bdvs_add3),
3.29 - Thm ("separate_bdvs_add4", num_str separate_bdvs_add4),
3.30 (*GOON*)
3.31 Thm ("separate_bdvs_mult", num_str separate_bdvs_mult)(*,
3.32 Thm ("", num_str ),
3.33 @@ -489,7 +485,7 @@
3.34 ("#Find" ,["solution ss___"])
3.35 ],
3.36 {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
3.37 - srls = append_rls "srls_normalize_2x2" e_rls
3.38 + srls = append_rls "srls_top_down_2x2" e_rls
3.39 [Thm ("hd_thm",num_str hd_thm),
3.40 Thm ("tl_Cons",num_str tl_Cons),
3.41 Thm ("tl_Nil",num_str tl_Nil)
3.42 @@ -589,7 +585,6 @@
3.43 Thm ("tl_Nil",num_str tl_Nil)
3.44 ],
3.45 prls = Erls, crls = Erls, nrls = Erls},
3.46 -(*@@@@@@ TODO, vvv just copied from 2x2 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
3.47 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
3.48 \ (let es__ = \
3.49 \ ((Try (Rewrite_Set norm_Rational False)) @@ \
3.50 @@ -601,7 +596,7 @@
3.51 \ isolate_bdvs_4x4 False)) @@ \
3.52 \ (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), \
3.53 \ (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] \
3.54 -\ simplify_System_parenthesized False)) @@ \
3.55 +\ simplify_System False)) @@ \
3.56 \ (Try (Rewrite_Set order_system False))) es_ \
3.57 \ in (SubProblem (EqSystem_,[linear,system],[no_met]) \
3.58 \ [bool_list_ es__, real_list_ vs_]))"
4.1 --- a/src/sml/IsacKnowledge/EqSystem.thy Fri Sep 08 20:33:59 2006 +0200
4.2 +++ b/src/sml/IsacKnowledge/EqSystem.thy Thu Sep 14 09:27:48 2006 +0200
4.3 @@ -43,17 +43,16 @@
4.4 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
4.5 \ ==> (a + b = c) = (b = c + -1*a)"
4.6 separate_bdvs_add1
4.7 - "[| [bdv_1] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
4.8 - \ ==> (a + b = c) = (b = c + -1*a)"
4.9 - separate_bdvs_add2
4.10 - "[| [bdv_2] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
4.11 - \ ==> (a + b = c) = (b = c + -1*a)"
4.12 + "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |]\
4.13 + \ ==> (a = b + c) = (a + -1*c = b)"
4.14 +(*
4.15 separate_bdvs_add3
4.16 "[| [bdv_3] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
4.17 \ ==> (a + b = c) = (b = c + -1*a)"
4.18 separate_bdvs_add4
4.19 "[| [bdv_4] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |]\
4.20 \ ==> (a + b = c) = (b = c + -1*a)"
4.21 +*)
4.22
4.23 separate_bdvs_mult
4.24 "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |]\
5.1 --- a/src/smltest/IsacKnowledge/atools.sml Fri Sep 08 20:33:59 2006 +0200
5.2 +++ b/src/smltest/IsacKnowledge/atools.sml Thu Sep 14 09:27:48 2006 +0200
5.3 @@ -31,6 +31,23 @@
5.4 if (term2s t') = "x occurs_in x = True" then ()
5.5 else raise error "atools.sml: x occurs_in x = True ???";
5.6
5.7 +"------- some_occur_in";
5.8 +some_occur_in [str2term"c",str2term"c_2"] (str2term"a + b + c");
5.9 +val t = str2term "some_of [c, c_2, c_3, c_4] occur_in \
5.10 + \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
5.11 +val Some (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;
5.12 +if term2str t' =
5.13 + "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 =\nTrue" then ()
5.14 +else raise error "atools.sml: some_occur_in true";
5.15 +
5.16 +val t = str2term "some_of [c_3, c_4] occur_in \
5.17 + \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
5.18 +val Some (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;
5.19 +if term2str t' =
5.20 + "some_of [c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
5.21 +else raise error "atools.sml: some_occur_in false";
5.22 +
5.23 +
5.24 "----------- argument_of -----------------------------------------";
5.25 "----------- argument_of -----------------------------------------";
5.26 "----------- argument_of -----------------------------------------";
6.1 --- a/src/smltest/IsacKnowledge/eqsystem.sml Fri Sep 08 20:33:59 2006 +0200
6.2 +++ b/src/smltest/IsacKnowledge/eqsystem.sml Thu Sep 14 09:27:48 2006 +0200
6.3 @@ -959,6 +959,10 @@
6.4 "----------- all systems from Biegelinie -------------------------";
6.5 "----------- all systems from Biegelinie -------------------------";
6.6 "----------- all systems from Biegelinie -------------------------";
6.7 +val subst = [(str2term "bdv_1", str2term "c"),
6.8 + (str2term "bdv_2", str2term "c_2"),
6.9 + (str2term "bdv_3", str2term "c_3"),
6.10 + (str2term "bdv_4", str2term "c_4")];
6.11 "----- Bsp 7.27";
6.12 states:=[];
6.13 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
6.14 @@ -969,11 +973,30 @@
6.15 moveActiveRoot 1;
6.16 (*
6.17 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
6.18 -*)
6.19 -"[0 = c_4, \
6.20 +##7.27##*)
6.21 +val t = str2term"[0 = c_4, \
6.22 \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
6.23 \ 0 = c_2, \
6.24 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]";
6.25 +val Some (t',_) = rewrite_set_ thy false isolate_bdvs_4x4 t;
6.26 +term2str t';
6.27 +"[c_4 = 0,\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI) =\n 0 + -1 * (c_4 + L * c_3),\n c_2 = 0, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0]";
6.28 +
6.29 +
6.30 +"--- go through the rewrites in met_eqsys_norm_4x4";
6.31 +val t = str2term "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2";
6.32 +val None = rewrite_set_ thy false norm_Rational t;
6.33 +val Some (t,_) =
6.34 + rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
6.35 +term2str t;
6.36 +(*
6.37 +val Some (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
6.38 +term2str t;
6.39 +val Some (t,_) = rewrite_set_inst_ thy false subst simplify_System t;
6.40 +term2str t;
6.41 +val Some (t,_) = rewrite_set_ thy false order_system t;
6.42 +term2str t;
6.43 +*)
6.44
6.45 "----- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
6.46 states:=[];
6.47 @@ -998,8 +1021,8 @@
6.48 moveActiveRoot 1;
6.49 (*
6.50 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
6.51 -*)
6.52 -"[0 = c_4 + 0 / (-1 * EI), \
6.53 +##7.69##*)
6.54 +val t = str2term"[0 = c_4 + 0 / (-1 * EI), \
6.55 \ 0 = c_4 + L * c_3 + (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
6.56 \ 0 = c_3 + 0 / (-1 * EI), \
6.57 \ 0 = c_3 + (6 * L * c_2 + 3 * L ^^^ 2 * c + -1 * L ^^^ 3 * q_0) / (-6 * EI)]";
6.58 @@ -1014,8 +1037,8 @@
6.59 moveActiveRoot 1;
6.60 (*
6.61 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
6.62 -*)
6.63 -"[L * q_0 = c, \
6.64 +##7.70##*)
6.65 +val t = str2term"[L * q_0 = c, \
6.66 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
6.67 \ 0 = c_4 + 0 / (-1 * EI), \
6.68 \ 0 = c_3 + 0 / (-1 * EI)]";
6.69 @@ -1030,8 +1053,8 @@
6.70 moveActiveRoot 1;
6.71 (*
6.72 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
6.73 -*)
6.74 -"[0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, \
6.75 +##7.71##*)
6.76 +val t = str2term"[0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, \
6.77 \ 0 = c_4 + 0 / (-1 * EI), \
6.78 \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) /(-24 * EI),\
6.79 \ 0 = c_3 + 0 / (-1 * EI)]";
6.80 @@ -1060,8 +1083,8 @@
6.81 moveActiveRoot 1;
6.82 (*
6.83 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
6.84 -*)
6.85 -"[0 = c_2, \
6.86 +##7.72b##*)
6.87 +val t = str2term"[0 = c_2, \
6.88 \ 0 = (6 * c_2 + 6 * L * c + -1 * L ^^^ 2 * q_0) / 6, \
6.89 \ 0 = c_4 + 0 / (-1 * EI), \
6.90 \ 0 = c_4 + L * c_3 + (60 * L ^^^ 2 * c_2 + 20 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-120 * EI)]";