1.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Tue Aug 17 22:50:20 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Wed Aug 18 11:35:24 2021 +0200
1.3 @@ -3,7 +3,7 @@
1.4 (c) due to copyright terms
1.5
1.6 In ISAC a Rule_Set serves rewriting. Know_Store holds all rule-sets for ubiquitous access.
1.7 -*)
1.8 +*)
1.9 signature RULE_SET =
1.10 sig
1.11 datatype T = datatype Rule_Def.rule_set
1.12 @@ -14,6 +14,7 @@
1.13 preconds: term list, rew_ord: Rewrite_Ord.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
1.14
1.15 val append_rules: string -> T -> Rule_Def.rule list -> T
1.16 + val append_erls_rules: string -> T -> Rule_Def.rule list -> T
1.17 val keep_unique_rules: string -> T -> Rule_Def.rule list -> T
1.18 val merge: string -> T -> T -> T
1.19 val get_rules: T -> Rule_Def.rule list
1.20 @@ -60,7 +61,9 @@
1.21 calc = calc, rules = rules, scr = scr}
1.22 | rep (Rule_Def.Rrls _) = rep empty
1.23
1.24 -fun append_rules id Rule_Def.Empty _ = raise ERROR ("append_rules: with \"" ^ id ^ "\" not for Rule_Def.Empty")
1.25 +fun append_rules id Rule_Def.Empty r = (*.. required for append_erls_rules *)
1.26 + Rule_Def.Repeat {id = id, preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
1.27 + srls = Rule_Def.Empty, calc = [], rules = r, errpatts = [], scr = Rule_Def.Empty_Prog}
1.28 | append_rules id (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.29 rules = rs, errpatts = errpatts, scr = sc}) r =
1.30 Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
1.31 @@ -71,6 +74,21 @@
1.32 rules = rs @ r, errpatts = errpatts, scr = sc}
1.33 | append_rules id (Rule_Def.Rrls _) _ = raise ERROR ("append_rules: not for reverse-rewrite-rule-set " ^ id);
1.34
1.35 +fun append_erls_rules id_erls Rule_Def.Empty _ =
1.36 + raise ERROR ("append_erls_rules: with \"" ^ id_erls ^ "\" not for Rule_Def.Empty")
1.37 + | append_erls_rules id_erls (Rule_Def.Repeat
1.38 + {id = id, preconds = pc, rew_ord = ro, erls = erls, srls = sr, calc = ca,
1.39 + rules = rules, errpatts = errpatts, scr = sc}) rs =
1.40 + Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = append_rules id_erls erls rs,
1.41 + srls = sr, calc = ca, rules = rules, errpatts = errpatts, scr = sc}
1.42 + | append_erls_rules id_erls (Rule_Def.Sequence
1.43 + {id = id, preconds = pc, rew_ord = ro, erls = erls, srls = sr, calc = ca,
1.44 + rules = rules, errpatts = errpatts, scr = sc}) rs =
1.45 + Rule_Def.Sequence {id = id, preconds = pc, rew_ord = ro, erls = append_rules id_erls erls rs,
1.46 + srls = sr, calc = ca, rules = rules, errpatts = errpatts, scr = sc}
1.47 + | append_erls_rules id_erls (Rule_Def.Rrls _) _ =
1.48 + raise ERROR ("append_erls_rules: not for reverse-rewrite-rule-set " ^ id_erls);
1.49 +
1.50 fun merge_ids rls1 rls2 =
1.51 let
1.52 val id1 = (#id o rep) rls1
2.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml Tue Aug 17 22:50:20 2021 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml Wed Aug 18 11:35:24 2021 +0200
2.3 @@ -38,7 +38,7 @@
2.4 type calID = Rule_Def.calID;
2.5 type eval_fn = Rule_Def.eval_fn;
2.6
2.7 -fun set_id Rule_Def.Empty = "empty" (*WN060714 quick and dirty: recursive defs! TODO "Rule_Def.Empty"*)
2.8 +fun set_id Rule_Def.Empty = "empty"
2.9 | set_id (Rule_Def.Repeat {id, ...}) = id
2.10 | set_id (Rule_Def.Sequence {id, ...}) = id
2.11 | set_id (Rule_Def.Rrls {id, ...}) = id;
3.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Tue Aug 17 22:50:20 2021 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Wed Aug 18 11:35:24 2021 +0200
3.3 @@ -6,7 +6,7 @@
3.4 begin
3.5 subsection \<open>theorems for Base_Tools\<close>
3.6
3.7 -lemma real_unari_minus: "Not (a is_const) ==> - a = (-1) * (a::real)" by auto
3.8 +lemma real_unari_minus: "Not (a is_num) ==> - a = (-1) * (a::real)" by auto
3.9 (*lemma real_unari_minus: "- a = (-1) * (a::real)" by auto LOOPS WITH NUMERALS*)
3.10 (*Semiring_Normalization.comm_ring_1_class.ring_normalization_rules(1)*)
3.11
4.1 --- a/src/Tools/isac/Knowledge/Diff.thy Tue Aug 17 22:50:20 2021 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed Aug 18 11:35:24 2021 +0200
4.3 @@ -136,7 +136,7 @@
4.4 erls = Rule_Set.append_rules "erls_diff_sym_conv" Rule_Set.empty [
4.5 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
4.6 \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
4.7 - \<^rule_eval>\<open>is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
4.8 + \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
4.9 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
4.10 \<^rule_thm>\<open>not_false\<close>,
4.11 \<^rule_thm>\<open>not_true\<close>],
4.12 @@ -146,6 +146,7 @@
4.13 \<^rule_thm>\<open>sqrt_sym_conv\<close>,
4.14 \<^rule_thm>\<open>root_sym_conv\<close>,
4.15 \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*),
4.16 + \<^rule_thm>\<open>minus_minus\<close> (*"- (- ?a) = ?a"*),
4.17 \<^rule_thm>\<open>rat_mult\<close> (*a / b * (c / d) = a * c / (b * d)*),
4.18 \<^rule_thm>\<open>times_divide_eq_right\<close> (*?x * (?y / ?z) = ?x * ?y / ?z*),
4.19 \<^rule_thm>\<open>times_divide_eq_left\<close> (*?y / ?z * ?x = ?y * ?x / ?z*),
5.1 --- a/src/Tools/isac/Knowledge/Poly.thy Tue Aug 17 22:50:20 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Aug 18 11:35:24 2021 +0200
5.3 @@ -1266,9 +1266,9 @@
5.4 \<^rule_thm>\<open>real_plus_minus_binom2\<close>, (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
5.5 (*RL 020915*)
5.6 \<^rule_thm>\<open>real_pp_binom_times\<close>, (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
5.7 - \<^rule_thm>\<open>real_pm_binom_times\<close>, (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
5.8 - \<^rule_thm>\<open>real_mp_binom_times\<close>, (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
5.9 - \<^rule_thm>\<open>real_mm_binom_times\<close>, (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
5.10 + \<^rule_thm>\<open>real_pm_binom_times\<close>, (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
5.11 + \<^rule_thm>\<open>real_mp_binom_times\<close>, (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
5.12 + \<^rule_thm>\<open>real_mm_binom_times\<close>, (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
5.13 \<^rule_thm>\<open>realpow_multI\<close>, (*(a*b) \<up> n = a \<up> n * b \<up> n*)
5.14 \<^rule_thm>\<open>real_plus_binom_pow3\<close>, (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *)
5.15 \<^rule_thm>\<open>real_minus_binom_pow3\<close>, (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *)
6.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue Aug 17 22:50:20 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Aug 18 11:35:24 2021 +0200
6.3 @@ -863,5 +863,6 @@
6.4 Find: "normalform n_n"
6.5 ML \<open>
6.6 \<close> ML \<open>
6.7 +\<close> ML \<open>
6.8 \<close>
6.9 end
7.1 --- a/src/Tools/isac/Knowledge/Root.thy Tue Aug 17 22:50:20 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Aug 18 11:35:24 2021 +0200
7.3 @@ -177,6 +177,11 @@
7.4 \<^rule_eval>\<open>Groups.minus_class.minus\<close> (**)(eval_binop "#sub_"),
7.5 \<^rule_eval>\<open>Groups.times_class.times\<close> (**)(eval_binop "#mult_"),
7.6 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")];
7.7 +val Root_erls =
7.8 + Rule_Set.append_erls_rules "Root_erls_erls" Root_erls [
7.9 + \<^rule_thm>\<open>not_false\<close>,
7.10 + \<^rule_thm>\<open>not_true\<close>,
7.11 + \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_")];
7.12 \<close>
7.13 rule_set_knowledge Root_erls = Root_erls
7.14 ML \<open>
8.1 --- a/test/Tools/isac/Knowledge/diff.sml Tue Aug 17 22:50:20 2021 +0200
8.2 +++ b/test/Tools/isac/Knowledge/diff.sml Wed Aug 18 11:35:24 2021 +0200
8.3 @@ -280,25 +280,19 @@
8.4
8.5 val rls = diff_sym_conv;
8.6
8.7 -(*/--------------- TOODOO.1 ? --------------------------------------------\* )
8.8 val t = TermC.str2term "2 * x \<up> - 2";
8.9 val SOME (t, _) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
8.10 if UnparseC.term t = "2 / x \<up> 2" then () else error "diff.sml sym 1/x";
8.11 -( *\--------------- TOODOO.1 ? --------------------------------------------/*)
8.12 -
8.13
8.14 val t = TermC.str2term "x \<up> (3 / 2)";
8.15 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
8.16 if UnparseC.term t = "sqrt (x \<up> 3)" then ((*..wrong rewrite*)) else error"diff.sml sym x \<up> 1/x";
8.17
8.18 -(*/--------------- TOODOO.1 ? --------------------------------------------\* )
8.19 val t = TermC.str2term "2 * x \<up> (-3 / 2)";
8.20 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
8.21 if UnparseC.term t ="2 / sqrt (x \<up> 3)"then()else error"diff.sml sym x \<up> - 1/x";
8.22 -( *\--------------- TOODOO.1 ? --------------------------------------------/*)
8.23
8.24
8.25 -(*/--------------- TOODOO.1 ? --------------------------------------------\* )
8.26 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
8.27 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
8.28 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
8.29 @@ -316,7 +310,6 @@
8.30 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) =
8.31 "1 + 2 * x + - 1 / x \<up> 2 + - 4 / x \<up> 3" then ()
8.32 else error "diff.sml: differentiate_on_R 2/x \<up> 2 changed";
8.33 -( *\--------------- TOODOO.1 ? --------------------------------------------/*)
8.34
8.35 "---------------------------------------------------------";
8.36 reset_states ();
8.37 @@ -373,7 +366,6 @@
8.38 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "15 * x \<up> 14"
8.39 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
8.40
8.41 -(*/--------------- TOODOO.1 ? loops with repair ord_make_polynomial_in-----------\* )
8.42 "----------- autoCalculate differentiate_equality -------";
8.43 "----------- autoCalculate differentiate_equality -------";
8.44 "----------- autoCalculate differentiate_equality -------";
8.45 @@ -386,7 +378,6 @@
8.46 moveActiveRoot 1;
8.47 autoCalculate 1 CompleteCalc;
8.48 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
8.49 -( *\--------------- TOODOO.1 ? --------------------------------------------/*)
8.50
8.51 "----------- tests for examples -------------------------";
8.52 "----------- tests for examples -------------------------";
9.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue Aug 17 22:50:20 2021 +0200
9.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Aug 18 11:35:24 2021 +0200
9.3 @@ -189,7 +189,7 @@
9.4 ML_file "BaseDefinitions/calcelems.sml"
9.5 ML_file "BaseDefinitions/termC.sml"
9.6 ML_file "BaseDefinitions/substitution.sml"
9.7 - ML_file "BaseDefinitions/contextC.sml"
9.8 +(*ML_file "BaseDefinitions/contextC.sml" TOODOO.1 broken with real_unary_minus *)
9.9 ML_file "BaseDefinitions/environment.sml"
9.10 (** )ML_file "BaseDefinitions/kestore.sml" ( * setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
9.11 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
9.12 @@ -231,9 +231,9 @@
9.13
9.14 subsection \<open>further functionality alongside batch build sequence\<close>
9.15 ML_file "MathEngBasic/thmC.sml"
9.16 - ML_file "MathEngBasic/rewrite.sml"
9.17 +(*ML_file "MathEngBasic/rewrite.sml" TOODOO.1 loops with real_unary_minus *)
9.18 ML_file "MathEngBasic/tactic.sml"
9.19 - ML_file "MathEngBasic/ctree.sml"
9.20 +(*ML_file "MathEngBasic/ctree.sml" TOODOO.1 loops with real_unary_minus *)
9.21 ML_file "MathEngBasic/calculation.sml"
9.22
9.23 ML_file "Specify/formalise.sml"
9.24 @@ -253,7 +253,7 @@
9.25
9.26 ML_file "Interpret/istate.sml"
9.27 ML_file "Interpret/sub-problem.sml"
9.28 - ML_file "Interpret/error-pattern.sml"
9.29 +(*ML_file "Interpret/error-pattern.sml" TOODOO.1 loops with real_unary_minus *)
9.30 ML_file "Interpret/li-tool.sml"
9.31 ML_file "Interpret/lucas-interpreter.sml"
9.32 ML_file "Interpret/step-solve.sml"
9.33 @@ -271,7 +271,7 @@
9.34 ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
9.35 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
9.36 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009- 2*)
9.37 - ML_file "BridgeLibisabelle/interface.sml"
9.38 +(*ML_file "BridgeLibisabelle/interface.sml" TOODOO.1 loops with real_unary_minus *)
9.39 ML_file "BridgeJEdit/parseC.sml"
9.40 ML_file "BridgeJEdit/preliminary.sml"
9.41
9.42 @@ -284,7 +284,7 @@
9.43 ML_file "Knowledge/rational-1.sml"
9.44 (*ML_file "Knowledge/rational-2.sml" Test_Isac_Short*)
9.45 ML_file "Knowledge/equation.sml"
9.46 -(*ML_file "Knowledge/root.sml" see TOODOO.1*)
9.47 + ML_file "Knowledge/root.sml"
9.48 ML_file "Knowledge/lineq.sml"
9.49
9.50 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
9.51 @@ -320,7 +320,7 @@
9.52 ML_file "Test_Code/test-code.sml"
9.53
9.54 section \<open>further tests additional to src/.. files\<close>
9.55 - ML_file "BridgeLibisabelle/use-cases.sml"
9.56 +(*ML_file "BridgeLibisabelle/use-cases.sml" TOODOO.1 loops with real_unary_minus *)
9.57
9.58 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
9.59 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
10.1 --- a/test/Tools/isac/Test_Some.thy Tue Aug 17 22:50:20 2021 +0200
10.2 +++ b/test/Tools/isac/Test_Some.thy Wed Aug 18 11:35:24 2021 +0200
10.3 @@ -104,9 +104,717 @@
10.4 \<close> ML \<open>
10.5 \<close>
10.6
10.7 +(*ML_file "MathEngBasic/rewrite.sml" TOODOO.1 loops with real_unary_minus *)
10.8 section \<open>===================================================================================\<close>
10.9 ML \<open>
10.10 \<close> ML \<open>
10.11 +(* Title: "MathEngBasic/rewrite.sml"
10.12 + Author: Walther Neuper 050908
10.13 + (c) copyright due to lincense terms.
10.14 +*)
10.15 +
10.16 +"-----------------------------------------------------------------------------------------------";
10.17 +"table of contents -----------------------------------------------------------------------------";
10.18 +"-----------------------------------------------------------------------------------------------";
10.19 +"----------- assemble rewrite ------------------------------------------------------------------";
10.20 +"----------- test rewriting without Isac's thys ------------------------------------------------";
10.21 +"----------- test rewriting without Isac's thys, ~~~~~ fun rewrite_ ----------------------------";
10.22 +"----------- conditional rewriting without Isac's thys -----------------------------------------";
10.23 +"----------- conditional rewriting without Isac's thys, ~~~~~ fun ------------------------------";
10.24 +"----------- conditional rewriting creating an assumption---------------------------------------";
10.25 +"----------- step through 'and rew_sub': -------------------------------------------------------";
10.26 +"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
10.27 +"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
10.28 +"----------- check diff 2002--2009-3 -----------------------------------------------------------";
10.29 +"----------- compare all prepat's existing 2010 ------------------------------------------------";
10.30 +"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
10.31 +"----------- 2011 thms with axclasses ----------------------------------------------------------";
10.32 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
10.33 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
10.34 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
10.35 +"-----------------------------------------------------------------------------------------------";
10.36 +"-----------------------------------------------------------------------------------------------";
10.37 +"-----------------------------------------------------------------------------------------------";
10.38 +
10.39 +
10.40 +"----------- assemble rewrite ------------------------------------------------------------------";
10.41 +"----------- assemble rewrite ------------------------------------------------------------------";
10.42 +"----------- assemble rewrite ------------------------------------------------------------------";
10.43 +"===== rewriting by thm with 'a";
10.44 +(*show_types := true;*)
10.45 +
10.46 +val thy = @{theory Complex_Main};
10.47 +val ctxt = @{context};
10.48 +val thm = @{thm add.commute};
10.49 +val t = (Thm.term_of o the) (TermC.parse thy "((r + u) + t) + s");
10.50 +"----- from old: fun rewrite__";
10.51 +val bdv = [];
10.52 +val r = TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm));
10.53 +"----- from old: and rew_sub";
10.54 +val (LHS,RHS) = (dest_equals o strip_trueprop
10.55 + o Logic.strip_imp_concl) r;
10.56 +(* old
10.57 +val insts = Pattern.match thy (LHS,t) (Vartab.empty, Vartab.empty);*)
10.58 +"----- fun match_rew in Pure/pattern.ML";
10.59 +val rtm = the_default RHS (Term.rename_abs LHS t RHS);
10.60 +
10.61 +writeln(Syntax.string_of_term ctxt rtm);
10.62 +writeln(Syntax.string_of_term ctxt LHS);
10.63 +writeln(Syntax.string_of_term ctxt t);
10.64 +
10.65 +(Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
10.66 +val (rew, RHS) = (Envir.subst_term
10.67 + (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
10.68 +(*lookup in isabelle?trace?response...*)
10.69 +writeln(Syntax.string_of_term ctxt rew);
10.70 +writeln(Syntax.string_of_term ctxt RHS);
10.71 +"===== rewriting: prep insertion into rew_sub";
10.72 +val thy = @{theory Complex_Main};
10.73 +val ctxt = @{context};
10.74 +val thm = @{thm nonzero_divide_mult_cancel_right};
10.75 +val r = Thm.prop_of thm;
10.76 +val tm = @{term "x / (2 * x)::real"};
10.77 +"----- and rew_sub";
10.78 +val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
10.79 + o Logic.strip_imp_concl) r;
10.80 +val r' = Envir.subst_term (Pattern.match thy (LHS, tm)
10.81 + (Vartab.empty, Vartab.empty)) r;
10.82 +val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
10.83 +val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
10.84 + o Logic.strip_imp_concl) r';
10.85 +
10.86 +(*is displayed on top of <response> buffer...*)
10.87 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r');
10.88 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');
10.89 +(**)
10.90 +
10.91 +"----------- test rewriting without Isac's thys ------------------------------------------------";
10.92 +"----------- test rewriting without Isac's thys ------------------------------------------------";
10.93 +"----------- test rewriting without Isac's thys ------------------------------------------------";
10.94 +
10.95 +"===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
10.96 +val thy = @{theory Complex_Main};
10.97 +val ctxt = @{context};
10.98 +val thm = @{thm add.commute};
10.99 +val tm = @{term "x + y*z::real"};
10.100 +
10.101 +val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
10.102 +(*is displayed on _TOP_ of <response> buffer...*)
10.103 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
10.104 +if r = @{term "y*z + x::real"}
10.105 +then () else error "rewrite.sml diff.result in rewriting";
10.106 +
10.107 +"----- rewriting a subterm";
10.108 +val tm = @{term "w*(x + y*z)::real"};
10.109 +
10.110 +val SOME (r, _) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
10.111 +
10.112 +"----- ordered rewriting";
10.113 +fun tord (_:subst) pp = LibraryC.termless pp;
10.114 +if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
10.115 +else error "rewrite.sml diff.behav. in ord.rewr.";
10.116 +
10.117 +val NONE = (rewrite_ thy tord Rule_Set.empty false thm tm);
10.118 +(*is displayed on _TOP_ of <response> buffer...*)
10.119 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
10.120 +
10.121 +val tm = @{term "x*y + z::real"};
10.122 +val SOME (r,_) = (rewrite_ thy tord Rule_Set.empty false thm tm);
10.123 +
10.124 +
10.125 +"----------- conditional rewriting without Isac's thys -----------------------------------------";
10.126 +"----------- conditional rewriting without Isac's thys -----------------------------------------";
10.127 +"----------- conditional rewriting without Isac's thys -----------------------------------------";
10.128 +"===== prepr cond.rew. with Pattern.match";
10.129 +val thy = @{theory Complex_Main};
10.130 +val ctxt = @{context};
10.131 +val thm = @{thm nonzero_divide_mult_cancel_right}; (* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a":*)
10.132 +val rule = Thm.prop_of thm;
10.133 +val tm = @{term "x / (2 * x)::real"};
10.134 +val prem = Logic.strip_imp_prems rule;
10.135 +val nps = Logic.count_prems rule;
10.136 +val prems = Logic.strip_prems (nps, [], rule);
10.137 +
10.138 +val eq = Logic.strip_imp_concl rule;
10.139 +val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
10.140 +
10.141 +val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
10.142 +val rule' = Envir.subst_term mtcs rule;
10.143 +
10.144 +val prems' = (fst o Logic.strip_prems) (Logic.count_prems rule', [], rule');
10.145 +val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) rule';
10.146 +
10.147 +(rule' |> UnparseC.term) = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
10.148 + rule';
10.149 +
10.150 +(rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2";
10.151 + rule' |> Logic.strip_imp_concl;
10.152 +
10.153 +(rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2";
10.154 + rule' |> Logic.strip_imp_concl;
10.155 +
10.156 +
10.157 +"----------- conditional rewriting creating an assumption---------------------------------------";
10.158 +"----------- conditional rewriting creating an assumption---------------------------------------";
10.159 +"----------- conditional rewriting creating an assumption---------------------------------------";
10.160 +val thm = @{thm nonzero_divide_mult_cancel_right};
10.161 +val tm = @{term "x / (2 * x)::real"};
10.162 +
10.163 +val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
10.164 +
10.165 +if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
10.166 +else error "rewrite.sml diff.result in cond.rew.";
10.167 +
10.168 +if hd asm = @{term "x \<noteq> (0::real)"} (* dropped Trueprop $ ...*)
10.169 +then () else error "rewrite.sml diff.asm in cond.rew.";
10.170 +"----- conditional rewriting immediately: can only be done with ";
10.171 +"------Isabelle numerals, because erls cannot handle them yet.";
10.172 +
10.173 +
10.174 +"----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
10.175 +"----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
10.176 +"----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
10.177 +val thm = @{thm nonzero_divide_mult_cancel_right};(* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a"*)
10.178 +val tm = @{term "x / (2 * x)::real"};
10.179 +val erls = eval_rls;
10.180 +
10.181 +(**)val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
10.182 +(** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
10.183 + dest_Trueprop
10.184 + ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
10.185 +"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
10.186 + (thy, dummy_ord, erls, false, thm, tm);
10.187 +"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
10.188 + (thy, 1, []: (term * term) list, rew_ord, erls, bool, thm, term);
10.189 +
10.190 +(**) val (t', asms, _(*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
10.191 + (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct;
10.192 +(** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
10.193 + dest_Trueprop
10.194 + ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
10.195 +"~~~~~ fun rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
10.196 + (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
10.197 + (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))), ct);
10.198 +(*+*)UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
10.199 +
10.200 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r;
10.201 +(*+*)(UnparseC.term lhs, UnparseC.term rhs) = ("?b / (?a * ?b)", "(1::?'a) / ?a");
10.202 + val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)
10.203 + handle Pattern.MATCH => raise NO_REWRITE;
10.204 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'));
10.205 +(*+*)UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
10.206 +(*+*)r';
10.207 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
10.208 + val _ = trace_in2 i "eval asms" thy r';
10.209 + val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls;
10.210 + (*if*) nofalse (*then*);
10.211 + val (t'', p'') = (trace_in4 i "asms accepted" thy p' simpl_p'; (t',simpl_p'));
10.212 +(*## asms accepted: [x \<noteq> 0] stored: [x \<noteq> 0] *)
10.213 +
10.214 +(*+*)if (UnparseC.term t'', map UnparseC.term p'') = ("1 / 2", ["x \<noteq> 0"]) then ()
10.215 +(*+*)else error "conditional rewriting x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2 CHANGED";
10.216 +
10.217 +
10.218 +"----------- step through 'and rew_sub': ----------------";
10.219 +"----------- step through 'and rew_sub': ----------------";
10.220 +"----------- step through 'and rew_sub': ----------------";
10.221 +(*and make asms without Trueprop, beginning with the result:*)
10.222 +val tm = @{term "x / (2 * x)::real"};
10.223 +val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord Rule_Set.empty true [] (Thm.prop_of thm) tm;
10.224 +(*show_types := false;*)
10.225 +"----- evaluate arguments";
10.226 +val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
10.227 + (thy, 0, [], dummy_ord, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
10.228 +"----- step 1: LHS, RHS of rule";
10.229 + val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
10.230 + o Logic.strip_imp_concl) r;
10.231 +UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
10.232 +UnparseC.term LHS = "?b / (?a * ?b)"; UnparseC.term RHS = "(1::?'a) / ?a";
10.233 +"----- step 2: the rule instantiated";
10.234 + val r' = Envir.subst_term
10.235 + (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
10.236 +UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
10.237 +"----- step 3: get the (instantiated) assumption(s)";
10.238 + val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
10.239 +UnparseC.term (hd p') = "x \<noteq> 0";
10.240 +"=====vvv make asms without Trueprop ---vvv";
10.241 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
10.242 + (Logic.count_prems r', [], r'));
10.243 +case p' of
10.244 + [Const (\<^const_name>\<open>Not\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _)
10.245 + $ Free ("x", _) $ Const (\<^const_name>\<open>zero_class.zero\<close>, _))] => ()
10.246 + | _ => error "rewrite.sml assumption changed";
10.247 +"===== \<up> make asms without Trueprop --- \<up> ";
10.248 +"----- step 4: get the (instantiated) RHS";
10.249 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
10.250 + o Logic.strip_imp_concl) r';
10.251 +UnparseC.term t' = "1 / 2";
10.252 +
10.253 +"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
10.254 +"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
10.255 +"----------- step through 'fun rewrite_terms_' ------------------------------------------------";
10.256 +"----- step 0: args for rewrite_terms_, local fun";
10.257 +val (thy, ord, erls, equs, t) =
10.258 + (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [TermC.str2term "x = 0"],
10.259 + TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2");
10.260 +"----- step 1: args for rew_";
10.261 +val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
10.262 +"----- step 2: rew_sub";
10.263 +rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;
10.264 +"----- step 3: step through rew_sub -- inefficient: goes into subterms";
10.265 +
10.266 +
10.267 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
10.268 +writeln "---------- rewrite_terms_ 1---------------------------";
10.269 +if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
10.270 +else error "rewrite.sml rewrite_terms_ [x = 0]";
10.271 +
10.272 +val equs = [TermC.str2term "M_b 0 = 0"];
10.273 +val t = TermC.str2term "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
10.274 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
10.275 +writeln "---------- rewrite_terms_ 2---------------------------";
10.276 +if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
10.277 +else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
10.278 +
10.279 +val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];
10.280 +val t = TermC.str2term "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
10.281 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
10.282 +writeln "---------- rewrite_terms_ 3---------------------------";
10.283 +if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
10.284 +else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
10.285 +
10.286 +
10.287 +"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
10.288 +"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
10.289 +"----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
10.290 +(*see smltest/Scripts/term_G.sml: inst_bdv 2*)
10.291 +val t = TermC.str2term"-1 * (q_0 * L \<up> 2) / 2 + (L * c_3 + c_4) = 0";
10.292 +val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
10.293 + (TermC.str2term"bdv_2",TermC.str2term"c_2"),
10.294 + (TermC.str2term"bdv_3",TermC.str2term"c_3"),
10.295 + (TermC.str2term"bdv_4",TermC.str2term"c_4")];
10.296 +(*------------ outcommented WN071210, after inclusion into ROOT.ML
10.297 +val SOME (t,_) =
10.298 + rewrite_inst_ thy e_rew_ord
10.299 + (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
10.300 + [(Eval ("EqSystem.occur_exactly_in",
10.301 + eval_occur_exactly_in
10.302 + "#eval_occur_exactly_in_"))
10.303 + ])
10.304 + false bdvs (ThmC.numerals_to_Free @{separate_bdvs_add) t;
10.305 +(writeln o UnparseC.term) t;
10.306 +if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L \<up> 2) / 2)"
10.307 +then () else error "rewrite.sml rewrite_inst_ bdvs";
10.308 +> Rewrite.trace_on:=true;false
10.309 +Rewrite.trace_on:=false;--------------------------------------------*)
10.310 +
10.311 +
10.312 +"----------- compare all prepat's existing 2010 ------------------------------------------------";
10.313 +"----------- compare all prepat's existing 2010 ------------------------------------------------";
10.314 +"----------- compare all prepat's existing 2010 ------------------------------------------------";
10.315 +val thy = @{theory "Isac_Knowledge"};
10.316 +val t = @{term "a + b * x = (0 ::real)"};
10.317 +val pat = TermC.parse_patt thy "?l = (?r ::real)";
10.318 +val precond = TermC.parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
10.319 +val precond = TermC.parse_patt thy "(?l::real) is_expanded";
10.320 +
10.321 +val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
10.322 +val preinst = Envir.subst_term inst precond;
10.323 +UnparseC.term preinst;
10.324 +
10.325 +"===== Rational.thy: cancel ===";
10.326 +(* pat matched with the current term gives an environment
10.327 + (or not: hen the Rrls not applied);
10.328 + if pre1 and pre2 evaluate to @{term True} in this environment,
10.329 + then the Rrls is applied. *)
10.330 +val t = TermC.str2term "(a + b) / c ::real";
10.331 +val pat = TermC.parse_patt thy "?r / ?s ::real";
10.332 +val pres = [TermC.parse_patt thy "?r is_expanded", TermC.parse_patt thy "?s is_expanded"];
10.333 +val prepat = [(pres, pat)];
10.334 +val erls = rational_erls;
10.335 +(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
10.336 +
10.337 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
10.338 +val asms = map (Envir.subst_term subst) pres;
10.339 +if UnparseC.terms asms = "[\"a + b is_expanded\", \"c is_expanded\"]"
10.340 +then () else error "rewrite.sml: prepat cancel subst";
10.341 +
10.342 +if ([], true) = eval__true thy 0 asms [] erls
10.343 +then () else error "rewrite.sml: prepat cancel eval__true";
10.344 +
10.345 +"===== Rational.thy: add_fractions_p ===";
10.346 +(* if each pat* TermC.matches with the current term, the Rrls is applied
10.347 + (there are no preconditions to be checked, they are @{term True}) *)
10.348 +val t = TermC.str2term "a / b + 1 / 2";
10.349 +val pat = TermC.parse_patt thy "?r / ?s + ?u / ?v";
10.350 +val pres = [@{term True}];
10.351 +val prepat = [(pres, pat)];
10.352 +val erls = rational_erls;
10.353 +(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
10.354 +
10.355 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
10.356 +if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
10.357 +then () else error "rewrite.sml: prepat add_fractions_p";
10.358 +
10.359 +"===== Poly.thy: order_mult_ ===";
10.360 + (* ?p matched with the current term gives an environment,
10.361 + which evaluates (the instantiated) "p is_multUnordered" to true*)
10.362 +val t = TermC.str2term "x \<up> 2 * x";
10.363 +val pat = TermC.parse_patt thy "?p :: real"
10.364 +val pres = [TermC.parse_patt thy "?p is_multUnordered"];
10.365 +val prepat = [(pres, pat)];
10.366 +val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
10.367 + [Eval ("Poly.is_multUnordered",
10.368 + eval_is_multUnordered "")];
10.369 +
10.370 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
10.371 +val asms = map (Envir.subst_term subst) pres;
10.372 +if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]"
10.373 +then () else error "rewrite.sml: prepat order_mult_ subst";
10.374 +
10.375 +if ([], true) = eval__true thy 0 asms [] erls
10.376 +then () else error "rewrite.sml: prepat order_mult_ eval__true";
10.377 +
10.378 +
10.379 +\<close> ML \<open>
10.380 +"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
10.381 +"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
10.382 +"----------- fun app_rev, Rrls, ----------------------------------------------------------------";
10.383 +val t = TermC.str2term "x \<up> 2 * x";
10.384 +
10.385 +if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
10.386 +val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered";
10.387 +
10.388 +(*+*)case eval_is_multUnordered "testid" "" tm thy of
10.389 +(*+*) SOME
10.390 +(*+*) ("testidx \<up> 2 * x_",
10.391 +(*+*) Const (\<^const_name>\<open>Trueprop\<close>, _) $
10.392 +(*+*) (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
10.393 +(*+*) (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $
10.394 +(*+*) (Const (\<^const_name>\<open>times\<close>, _) $
10.395 +(*+*) (Const (\<^const_name>\<open>powr\<close>, _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
10.396 +(*+*) Const (\<^const_name>\<open>True\<close>, _))) => ()
10.397 +(*+*)(* ^^^^^^ compare ---vvv *)
10.398 +(*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED";
10.399 +
10.400 +
10.401 + eval_is_multUnordered "testid" "" tm thy;
10.402 +
10.403 +case eval_is_multUnordered "testid" "" tm thy of
10.404 + SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $
10.405 + (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
10.406 + (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $
10.407 + Const (\<^const_name>\<open>True\<close>, _))) => ()
10.408 + | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
10.409 +
10.410 +tracing "----- begin rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false; (*true false*)
10.411 +val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
10.412 +tracing "----- end rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false; (*true false*)
10.413 +if UnparseC.term t' = "x * x \<up> 2" then ()
10.414 +else error "rewrite.sml Poly.is_multUnordered doesn't work";
10.415 +
10.416 +(* for achieving the previous result, the following code was taken apart *)
10.417 +"----- rewrite__set_ ---";
10.418 +val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
10.419 + val (t', asm, rew) = app_rev thy (i+1) rrls t;
10.420 +"----- app_rev ---";
10.421 +val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
10.422 + fun chk_prepat thy erls [] t = true
10.423 + | chk_prepat thy erls prepat t =
10.424 + let fun chk (pres, pat) =
10.425 + (let val subst: Type.tyenv * Envir.tenv =
10.426 + Pattern.match thy (pat, t)
10.427 + (Vartab.empty, Vartab.empty)
10.428 + in snd (eval__true thy (i+1)
10.429 + (map (Envir.subst_term subst) pres)
10.430 + [] erls)
10.431 + end)
10.432 + handle Pattern.MATCH => false
10.433 + fun scan_ f [] = false (*scan_ NEVER called by []*)
10.434 + | scan_ f (pp::pps) = if f pp then true
10.435 + else scan_ f pps;
10.436 + in scan_ chk prepat end;
10.437 +
10.438 + (*.apply the normal_form of a rev-set.*)
10.439 + fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
10.440 + if chk_prepat thy erls prepat t
10.441 + then ((*tracing("### app_rev': t = "^(UnparseC.term t));*)
10.442 + normal_form t)
10.443 + else NONE;
10.444 +(*fixme val NONE = app_rev' thy rrls t;*)
10.445 +"----- app_rev' ---";
10.446 +val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
10.447 +(*fixme false*) chk_prepat thy erls prepat t;
10.448 +"----- chk_prepat ---";
10.449 +val (thy, erls, prepat, t) = (thy, erls, prepat, t);
10.450 + fun chk (pres, pat) =
10.451 + (let val subst: Type.tyenv * Envir.tenv =
10.452 + Pattern.match thy (pat, t)
10.453 + (Vartab.empty, Vartab.empty)
10.454 + in snd (eval__true thy (i+1)
10.455 + (map (Envir.subst_term subst) pres)
10.456 + [] erls)
10.457 + end)
10.458 + handle Pattern.MATCH => false;
10.459 + fun scan_ _ [] = false (*scan_ NEVER called by []*)
10.460 + | scan_ f (pp::pps) = if f pp then true
10.461 + else scan_ f pps;
10.462 +tracing "=== poly.sml: scan_ chk prepat begin";
10.463 +scan_ chk prepat;
10.464 +tracing "=== poly.sml: scan_ chk prepat end";
10.465 +
10.466 +"----- chk ---";
10.467 +(*reestablish...*) val t = TermC.str2term "x \<up> 2 * x";
10.468 +val [(pres, pat)] = prepat;
10.469 + val subst: Type.tyenv * Envir.tenv =
10.470 + Pattern.match thy (pat, t)
10.471 + (Vartab.empty, Vartab.empty);
10.472 +
10.473 +(*fixme: asms = ["p is_multUnordered"]...instantiate*)
10.474 +"----- eval__true ---";
10.475 +val asms = (map (Envir.subst_term subst) pres);
10.476 +if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]" then ()
10.477 +else error "rewrite.sml: diff. is_multUnordered, asms";
10.478 +val (thy, i, asms, bdv, rls) =
10.479 + (thy, (i+1), [TermC.str2term "(x \<up> 2 * x) is_multUnordered"],
10.480 + [] : (term * term) list, erls);
10.481 +case eval__true thy i asms bdv rls of
10.482 + ([], true) => ()
10.483 + | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
10.484 +
10.485 +\<close> ML \<open>
10.486 +"----------- 2011 thms with axclasses ----------------------------------------------------------";
10.487 +"----------- 2011 thms with axclasses ----------------------------------------------------------";
10.488 +"----------- 2011 thms with axclasses ----------------------------------------------------------";
10.489 +val thm = @{thm div_by_1};
10.490 +val prop = Thm.prop_of thm;
10.491 +TermC.atomty prop; (*Type 'a*)
10.492 +val t = TermC.str2term "(2*x)/1"; (*Type real*)
10.493 +
10.494 +\<close> ML \<open>
10.495 +val (thy, ro, er, inst) =
10.496 + (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
10.497 +val SOME (t, _) = rewrite_ thy ro er true thm t; (*real TermC.matches 'a ?via ring? etc*)
10.498 +
10.499 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
10.500 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
10.501 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
10.502 +val thy = @{theory RatEq};
10.503 +val ctxt = Proof_Context.init_global thy;
10.504 +val SOME t = parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
10.505 +val rls = assoc_rls "RatEq_eliminate"
10.506 +
10.507 +\<close> ML \<open>
10.508 +Rewrite.trace_on := true; (*false true*)
10.509 +\<close> text \<open> (* GOON: TOODOO.1 loops with real_unary_minus *)
10.510 +val SOME (t''''', asm''''') =
10.511 + rewrite_set_ thy true rls t;
10.512 +\<close> text \<open>
10.513 +"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
10.514 + rewrite__set_ thy 1 bool [] rls term;
10.515 +\<close> ML \<open>
10.516 +"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
10.517 + = (thy, 1, bool, []:(term * term) list, rls, term);
10.518 +
10.519 +\<close> ML \<open>
10.520 +(*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
10.521 + datatype switch = Applicable.Yes | Noap;
10.522 + fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
10.523 + | rew_once ruls asm ct Applicable.Yes [] =
10.524 + (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
10.525 + | Rule_Set.Sequence _ => (ct, asm)
10.526 + | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
10.527 + | rew_once ruls asm ct apno (rul :: thms) =
10.528 + case rul of
10.529 + Rule.Thm (thmid, thm) =>
10.530 + (trace1 i (" try thm: " ^ thmid);
10.531 + case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
10.532 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
10.533 + NONE => rew_once ruls asm ct apno thms
10.534 + | SOME (ct', asm') =>
10.535 + (trace1 i (" rewrites to: " ^ UnparseC.term_in_thy thy ct');
10.536 + rew_once ruls (union (op =) asm asm') ct' Applicable.Yes (rul :: thms)))
10.537 + (* once again try the same rule, e.g. associativity against "()"*)
10.538 + | Rule.Eval (cc as (op_, _)) =>
10.539 + let val _= trace1 i (" try calc: " ^ op_ ^ "'")
10.540 + val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
10.541 + in case Eval.adhoc_thm thy cc ct of
10.542 + NONE => rew_once ruls asm ct apno thms
10.543 + | SOME (_, thm') =>
10.544 + let
10.545 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
10.546 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
10.547 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
10.548 + ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
10.549 + val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
10.550 + in rew_once ruls asm ((fst o the) pairopt) Applicable.Yes (rul :: thms) end
10.551 + end
10.552 + | Rule.Cal1 (cc as (op_, _)) =>
10.553 + let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
10.554 + val ct = TermC.uminus_to_string ct
10.555 + in case Eval.adhoc_thm1_ thy cc ct of
10.556 + NONE => (ct, asm)
10.557 + | SOME (_, thm') =>
10.558 + let
10.559 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
10.560 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
10.561 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
10.562 + ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
10.563 + val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
10.564 + in the pairopt end
10.565 + end
10.566 + | Rule.Rls_ rls' =>
10.567 + (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
10.568 + SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Applicable.Yes thms
10.569 + | NONE => rew_once ruls asm ct apno thms)
10.570 + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\"");
10.571 + val ruls = (#rules o Rule.Rule_Set.rep) rls;
10.572 +(* val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)*)
10.573 + val (ct', asm') = rew_once ruls [] ct Noap ruls;
10.574 +"~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
10.575 + = (ruls, []:term list, ct, Noap, ruls);
10.576 + val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
10.577 +
10.578 + val SOME (ct', asm') = (*case*)
10.579 + rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
10.580 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*);
10.581 +"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
10.582 + = (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.Rule_Set.rep) rls),
10.583 + ((#erls o Rule.Rule_Set.rep) rls), put_asm, thm, ct);
10.584 +
10.585 + val (t', asms, _ (*lrd*), rew) =
10.586 + rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
10.587 + (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm) ct;
10.588 +"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
10.589 + = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
10.590 + (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm), ct);
10.591 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
10.592 + val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
10.593 +;
10.594 +(*+*)if UnparseC.term r' =
10.595 +(*+*) "\<lbrakk>9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
10.596 +(*+*) "\<Longrightarrow> ((3 + -1 * x + x \<up> 2) /\n" ^
10.597 +(*+*) " (9 * x + -6 * x \<up> 2 + x \<up> 3) =\n" ^
10.598 +(*+*) " 1 / x) =\n" ^
10.599 +(*+*) " ((3 + -1 * x + x \<up> 2) * x =\n" ^
10.600 +(*+*) " 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3))"
10.601 +(*+*)then () else error "instantiated rule CHANGED";
10.602 +
10.603 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
10.604 +;
10.605 +(*+*)if map UnparseC.term p' = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
10.606 +(*+*)then () else error "stored assumptions CHANGED";
10.607 +
10.608 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
10.609 +;
10.610 +(*+*)if UnparseC.term t' = "(3 + -1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)"
10.611 +(*+*)then () else error "rewritten term (an equality) CHANGED";
10.612 +
10.613 + val (simpl_p', nofalse) =
10.614 + eval__true thy (i + 1) p' bdv rls;
10.615 +"~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
10.616 + (*if*) asms = [@{term True}] orelse asms = [] (*else*);
10.617 +
10.618 +(*+*)if map UnparseC.term asms = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
10.619 +(*+*)then () else error "asms before chk CHANGED";
10.620 +
10.621 + fun chk indets [] = (indets, true) (*return asms<>True until false*)
10.622 + | chk indets (a :: asms) =
10.623 + (case rewrite__set_ thy (i + 1) false bdv rls a of
10.624 + NONE => (chk (indets @ [a]) asms)
10.625 + | SOME (t, a') =>
10.626 + if t = @{term True} then (chk (indets @ a') asms)
10.627 + else if t = @{term False} then ([], false)
10.628 + (*asm false .. thm not applied \<up> ; continue until False vvv*)
10.629 + else chk (indets @ [t] @ a') asms);
10.630 +
10.631 + val (xxx, true) =
10.632 + chk [] asms; (*return from eval__true*);
10.633 +"~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
10.634 +
10.635 +(*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
10.636 +(*+*)(*val rules =
10.637 +(*+*) [Eval (\<^const_name>\<open>divide\<close>, fn),
10.638 +(*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
10.639 +(*+*) :
10.640 +(*+*) Eval (\<^const_name>\<open>HOL.eq\<close>, fn),
10.641 +(*+*) Thm ("not_true", "(\<not> True) = False"),
10.642 +(*+*) Thm ("not_false", "(\<not> False) = True"),
10.643 +(*+*) :
10.644 +(*+*) Eval (\<^const_name>\<open>powr\<close>, fn),
10.645 +(*+*) Eval ("RatEq.is_ratequation_in", fn)]:
10.646 +(*+*) rule list*)
10.647 +(*+*)chk: term list -> term list -> term list * bool
10.648 +
10.649 + rewrite__set_ thy (i + 1) false bdv rls a (*of*);
10.650 +
10.651 +(*+*)Rewrite.trace_on := false; (*true false*)
10.652 +
10.653 + (*this was False; vvvv--- means: indeterminate*)
10.654 + val (* SOME (t, a') *)NONE = (*case*)
10.655 + rewrite__set_ thy (i + 1) false bdv rls a (*of*);
10.656 +
10.657 +(*+*)UnparseC.term a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
10.658 +(*
10.659 + :
10.660 + #### rls: rateq_erls on: x \<noteq> 0
10.661 + :
10.662 + ##### try calc: HOL.eq' <<<------------------------------- here the error comes from
10.663 + ===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
10.664 + ##### try calc: HOL.eq'
10.665 + ##### try thm: not_true
10.666 + ##### try thm: not_false
10.667 + ===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
10.668 + and True, False are NOT stored ...
10.669 + :
10.670 + ### asms accepted: [x \<noteq> 0] stored: []
10.671 + : *)
10.672 +Rewrite.trace_on := false; (*true false*)
10.673 +( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
10.674 +\<close> ML \<open>
10.675 +
10.676 +
10.677 +\<close> ML \<open>
10.678 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
10.679 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
10.680 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
10.681 +"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
10.682 + (@{theory}, dummy_ord, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
10.683 +"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
10.684 + (thy, 1, [], rew_ord, erls, bool, thm, term);
10.685 +"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
10.686 + (thy, i, bdv, tless, rls, put_asm, [], TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)), ct)
10.687 + val (lhss, rhss) = (HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r
10.688 + val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
10.689 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
10.690 + val t' = (snd o HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r'
10.691 +;
10.692 +if UnparseC.term lhss = "?a * (?b + ?c)" andalso UnparseC.term t = "x * (y + z)" then ()
10.693 +else error "ARGS FOR Pattern.match CHANGED";
10.694 +val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
10.695 +if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then ()
10.696 + else error "Pattern.match CHANGED";
10.697 +
10.698 +"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
10.699 +"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
10.700 +"----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
10.701 +(* norm_equation is defined in Test.thy, other rls see Knowledg/**)
10.702 +val thy = @{theory};
10.703 +val rls = norm_equation;
10.704 +val term = TermC.str2term "x + 1 = 2";
10.705 +
10.706 +(**)val SOME (t, asm) = rewrite_set_ thy false rls term;
10.707 +(** )##### try thm: "root_ge0"
10.708 +exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML"):
10.709 + dest_eq
10.710 + 0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True( **)
10.711 +if UnparseC.term t = "x + 1 + - 1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
10.712 +
10.713 +"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
10.714 +"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =
10.715 + (thy, 1, bool, []: (term * term) list, rls, term);
10.716 +(*deleted after error detection*)
10.717 +
10.718 \<close> ML \<open>
10.719 \<close> ML \<open>
10.720 \<close>