wneuper/isa: comparison src/Tools/isac/Knowledge/Integrate.thy

equal deleted inserted replaced

-:b7071d1dd263
+:007ef64dbb08
 (*.rulesets for integration.*)
 val integration_rules =
 Rule_Def.Repeat {id="integration_rules", preconds = [],
 rew_ord = ("termlessI",termlessI),
-erls = Rule_Def.Repeat {id="conditions_in_integration_rules",
+asm_rls = Rule_Def.Repeat {id="conditions_in_integration_rules",
 	  preconds = [],
 	  rew_ord = ("termlessI",termlessI),
-	  erls = Rule_Set.Empty,
+	  asm_rls = Rule_Set.Empty,
-	  srls = Rule_Set.Empty, calc = [], errpatts = [],
+	  prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
 	  rules = [(*for rewriting conditions in Thm's*)
 		   \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "#occurs_in_"),
 		   \<^rule_thm>\<open>not_true\<close>,
 		   \<^rule_thm>\<open>not_false\<close>],
-	  scr = Rule.Empty_Prog},
+	  program = Rule.Empty_Prog},
-srls = Rule_Set.Empty, calc = [], errpatts = [],
+prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
 rules = [
 	  \<^rule_thm>\<open>integral_const\<close>,
 	  \<^rule_thm>\<open>integral_var\<close>,
 	  \<^rule_thm>\<open>integral_add\<close>,
 	  \<^rule_thm>\<open>integral_mult\<close>,
 	  \<^rule_thm>\<open>integral_pow\<close>,
 	  \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")(*for n+1*)],
-scr = Rule.Empty_Prog};
+program = Rule.Empty_Prog};
 \<close>
 ML \<open>
 val add_new_c =
 Rule_Set.Sequence {id="add_new_c", preconds = [],
 rew_ord = ("termlessI",termlessI),
-erls = Rule_Def.Repeat {id="conditions_in_add_new_c",
+asm_rls = Rule_Def.Repeat {id="conditions_in_add_new_c",
-preconds = [], rew_ord = ("termlessI",termlessI), erls = Rule_Set.Empty,
+preconds = [], rew_ord = ("termlessI",termlessI), asm_rls = Rule_Set.Empty,
-srls = Rule_Set.Empty, calc = [], errpatts = [],
+prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
 rules = [
 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches""),
 	    \<^rule_eval>\<open>Integrate.is_f_x\<close> (eval_is_f_x "is_f_x_"),
 	    \<^rule_thm>\<open>not_true\<close>,
 	    \<^rule_thm>\<open>not_false\<close>],
-scr = Rule.Empty_Prog},
+program = Rule.Empty_Prog},
-srls = Rule_Set.Empty, calc = [], errpatts = [],
+prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
 rules = [ (*\<^rule_thm>\<open>call_for_new_c\<close>,*)
 Rule.Cal1 ("Integrate.add_new_c", eval_add_new_c "new_c_")],
-scr = Rule.Empty_Prog};
+program = Rule.Empty_Prog};
 \<close>
 ML \<open>
 (*.rulesets for simplifying Integrals.*)
 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
 val norm_Rational_rls_noadd_fractions =
 Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [],
 rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
-erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
+asm_rls = norm_rat_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
 rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
 	  Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
 		(Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [],
 		   rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
-		   erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
+		   asm_rls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
 				 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
-			 srls = Rule_Set.Empty, calc = [], errpatts = [],
+			 prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
 		   rules = [
 \<^rule_thm>\<open>rat_mult\<close>, (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
 	       \<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
 	       \<^rule_thm>\<open>rat_mult_poly_r\<close>, (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
 	       \<^rule_thm>\<open>divide_divide_eq_right\<close>, (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
 	       \<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
 	       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
 	       \<^rule_thm>\<open>rat_power\<close>], (*"(?a / ?b)  \<up>  ?n = ?a  \<up>  ?n / ?b  \<up>  ?n"*)
-scr = Rule.Empty_Prog}),
+program = Rule.Empty_Prog}),
 		Rule.Rls_ make_rat_poly_with_parentheses,
 		Rule.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
 		Rule.Rls_ rat_reduce_1],
-scr = Rule.Empty_Prog};
+program = Rule.Empty_Prog};
 (*.for simplify_Integral adapted from 'norm_Rational'.*)
 val norm_Rational_noadd_fractions =
 Rule_Set.Sequence {id = "norm_Rational_noadd_fractions", preconds = [],
 rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
-erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
+asm_rls = norm_rat_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
 rules = [Rule.Rls_ discard_minus,
 		Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c    *)
 		Rule.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
 		Rule.Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
 		Rule.Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#)   *)
 		Rule.Rls_ discard_parentheses1], (* mult only                       *)
-scr = Rule.Empty_Prog};
+program = Rule.Empty_Prog};
 (*.simplify terms before and after Integration such that
 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
 common denominator as done by norm_Rational or make_ratpoly_in.
 This is a copy from 'make_ratpoly_in' with respective reduction of rules and
 		rule_thm>\<open>add_divide_distrib\<close> (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
 		];
 val simplify_Integral =
 Rule_Set.Sequence {id = "simplify_Integral", preconds = []:term list,
 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
-erls = Atools_erls, srls = Rule_Set.Empty,
+asm_rls = Atools_erls, prog_rls = Rule_Set.Empty,
 calc = [],  errpatts = [],
 rules = [
 \<^rule_thm>\<open>distrib_right\<close>, (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
 	    \<^rule_thm>\<open>add_divide_distrib\<close>, (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
 	     (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
 	    Rule.Rls_ order_add_mult_in,
 	    Rule.Rls_ discard_parentheses,
 	    (*Rule.Rls_ collect_bdv, from make_polynomial_in*)
 	    Rule.Rls_ separate_bdv2,
 	    \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
-scr = Rule.Empty_Prog};
+program = Rule.Empty_Prog};
 val integration =
 Rule_Set.Sequence {
 id="integration", preconds = [], rew_ord = ("termlessI",termlessI),
-	 erls = Rule_Def.Repeat {
+	 asm_rls = Rule_Def.Repeat {
 id="conditions_in_integration",  preconds = [], rew_ord = ("termlessI",termlessI),
-		 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
+		 asm_rls = Rule_Set.Empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
-		 rules = [], scr = Rule.Empty_Prog},
+		 rules = [], program = Rule.Empty_Prog},
-	 srls = Rule_Set.Empty, calc = [], errpatts = [],
+	 prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
 	 rules = [
 Rule.Rls_ integration_rules,
 		 Rule.Rls_ add_new_c,
 		 Rule.Rls_ simplify_Integral],
-	 scr = Rule.Empty_Prog};
+	 program = Rule.Empty_Prog};
 val prep_rls' = Auto_Prog.prep_rls @{theory};
 \<close>
 rule_set_knowledge
 integration_rules = \<open>prep_rls' integration_rules\<close> and
 t_t = Take (Integral f_f D v_v)
 in
 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
 method met_diffint : "diff/integration" =
-\<open>{rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
+\<open>{rew_ord="tless_true", rls'=Atools_erls, calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,
-	  crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
+	  crls = Atools_erls, errpats = [], rew_rls = Rule_Set.empty}\<close>
 Program: integrate.simps
 Given: "functionTerm f_f" "integrateBy v_v"
 Find: "antiDerivative F_F"
 partial_function (tailrec) intergrate_named :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'')) #>
 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
 ) t_t)"
 method met_diffint_named : "diff/integration/named" =
-\<open>{rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
+\<open>{rew_ord="tless_true", rls'=Atools_erls, calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,
-crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
+crls = Atools_erls, errpats = [], rew_rls = Rule_Set.empty}\<close>
 Program: intergrate_named.simps
 Given: "functionTerm f_f" "integrateBy v_v"
 Find: "antiDerivativeName F_F"
 ML \<open>

changeset 60586	007ef64dbb08
parent 60515	03e19793d81e
child 60587	8af797c555a8