1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Apr 09 12:03:14 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Thu Apr 09 17:13:17 2020 +0200
1.3 @@ -43,9 +43,9 @@
1.4 fun eval_is_ratpolyexp (thmid:string) _
1.5 (t as (Const("Rational.is'_ratpolyexp", _) $ arg)) thy =
1.6 if is_ratpolyexp arg
1.7 - then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
1.8 + then SOME (TermC.mk_thmid thmid (UnparseC.term_to_string''' thy arg) "",
1.9 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.10 - else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
1.11 + else SOME (TermC.mk_thmid thmid (UnparseC.term_to_string''' thy arg) "",
1.12 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.13 | eval_is_ratpolyexp _ _ _ _ = NONE;
1.14
1.15 @@ -54,7 +54,7 @@
1.16 (t as Const ("Rational.get_denominator", _) $
1.17 (Const ("Rings.divide_class.divide", _) $ _(*num*) $
1.18 denom)) thy =
1.19 - SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy denom) "",
1.20 + SOME (TermC.mk_thmid thmid (UnparseC.term_to_string''' thy denom) "",
1.21 HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
1.22 | eval_get_denominator _ _ _ _ = NONE;
1.23
1.24 @@ -63,7 +63,7 @@
1.25 (t as Const ("Rational.get_numerator", _) $
1.26 (Const ("Rings.divide_class.divide", _) $num
1.27 $denom )) thy =
1.28 - SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy num) "",
1.29 + SOME (TermC.mk_thmid thmid (UnparseC.term_to_string''' thy num) "",
1.30 HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
1.31 | eval_get_numerator _ _ _ _ = NONE;
1.32 \<close>
1.33 @@ -132,7 +132,7 @@
1.34 | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
1.35 let val (c', es') = monom_of_term vs (c, es) m1
1.36 in monom_of_term vs (c', es') m2 end
1.37 - | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ Rule.term2str t)
1.38 + | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term2str t)
1.39
1.40 fun monoms_of_term vs (t as Const _) =
1.41 [monom_of_term vs (1, replicate (length vs) 0) t]
1.42 @@ -144,7 +144,7 @@
1.43 [monom_of_term vs (1, replicate (length vs) 0) t]
1.44 | monoms_of_term vs (Const ("Groups.plus_class.plus", _) $ ms1 $ ms2) =
1.45 (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)
1.46 - | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ Rule.term2str t)
1.47 + | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term2str t)
1.48
1.49 (* convert a term to the internal representation of a multivariate polynomial;
1.50 the conversion is quite liberal, see test --- fun poly_of_term ---:
1.51 @@ -355,7 +355,6 @@
1.52 | _ => NONE : (term * term list) option
1.53 end
1.54 end
1.55 -
1.56 \<close>
1.57
1.58 subsubsection \<open>Addition of at least one fraction within a sum\<close>
1.59 @@ -452,9 +451,9 @@
1.60 fun eval_is_expanded (thmid:string) _
1.61 (t as (Const("Rational.is'_expanded", _) $ arg)) thy =
1.62 if is_expanded arg
1.63 - then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
1.64 + then SOME (TermC.mk_thmid thmid (UnparseC.term_to_string''' thy arg) "",
1.65 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.66 - else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
1.67 + else SOME (TermC.mk_thmid thmid (UnparseC.term_to_string''' thy arg) "",
1.68 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.69 | eval_is_expanded _ _ _ _ = NONE;
1.70 \<close>
1.71 @@ -486,15 +485,15 @@
1.72 in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;
1.73
1.74 fun locate_rule thy eval_rls ro [rs] t r =
1.75 - if member op = ((map (Celem.id_of_thm)) rs) (Celem.id_of_thm r)
1.76 + if member op = ((map (ThmC.id_of_thm)) rs) (ThmC.id_of_thm r)
1.77 then
1.78 - let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Celem.thm_of_thm r) t;
1.79 + let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC.thm_of_thm r) t;
1.80 in
1.81 case ropt of SOME ta => [(r, ta)]
1.82 | NONE => ((*tracing
1.83 - ("### locate_rule: rewrite " ^ Celem.id_of_thm r ^ " " ^ Rule.term2str t ^ " = NONE");*) [])
1.84 + ("### locate_rule: rewrite " ^ ThmC.id_of_thm r ^ " " ^ UnparseC.term2str t ^ " = NONE");*) [])
1.85 end
1.86 - else ((*tracing ("### locate_rule: " ^ Celem.id_of_thm r ^ " not mem rrls");*) [])
1.87 + else ((*tracing ("### locate_rule: " ^ ThmC.id_of_thm r ^ " not mem rrls");*) [])
1.88 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
1.89
1.90 fun next_rule thy eval_rls ro [rs] t =
1.91 @@ -506,7 +505,7 @@
1.92 fun attach_form (_: Rule.rule list list) (_: term) (_: term) =
1.93 [(*TODO*)]: ( Rule.rule * (term * term list)) list;
1.94
1.95 -in
1.96 +(**)in(**)
1.97
1.98 val cancel_p =
1.99 Rule_Set.Rrls {id = "cancel_p", prepat = [],
1.100 @@ -524,12 +523,12 @@
1.101 locate_rule = locate_rule thy Atools_erls ro,
1.102 next_rule = next_rule thy Atools_erls ro,
1.103 attach_form = attach_form}}
1.104 -end; (* local cancel_p *)
1.105 +(**)end(* local cancel_p *)
1.106 \<close>
1.107
1.108 subsection \<open>Embed addition into rewriting\<close>
1.109 ML \<open>
1.110 -(** )local ( * add_fractions_p *)
1.111 +(**)local (* add_fractions_p *)
1.112
1.113 (*val {rules = rules, rew_ord = (_, ro), ...} = Rule_Set.rep (assoc_rls "make_polynomial");*)
1.114 val {rules, rew_ord=(_,ro),...} = Rule_Set.rep (assoc_rls' @{theory} "rev_rew_p");
1.115 @@ -546,18 +545,17 @@
1.116 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs;
1.117 in (t, t'', [rs(*here only _ONE_*)], der) end;
1.118
1.119 -\<close> ML \<open>
1.120 fun locate_rule thy eval_rls ro [rs] t r =
1.121 - if member op = ((map (Celem.id_of_thm)) rs) (Celem.id_of_thm r)
1.122 + if member op = ((map (ThmC.id_of_thm)) rs) (ThmC.id_of_thm r)
1.123 then
1.124 - let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Celem.thm_of_thm r) t;
1.125 + let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC.thm_of_thm r) t;
1.126 in
1.127 case ropt of
1.128 SOME ta => [(r, ta)]
1.129 | NONE =>
1.130 - ((*tracing ("### locate_rule: rewrite " ^ Celem.id_of_thm r ^ " " ^ Rule.term2str t ^ " = NONE");*)
1.131 + ((*tracing ("### locate_rule: rewrite " ^ ThmC.id_of_thm r ^ " " ^ UnparseC.term2str t ^ " = NONE");*)
1.132 []) end
1.133 - else ((*tracing ("### locate_rule: " ^ Celem.id_of_thm r ^ " not mem rrls");*) [])
1.134 + else ((*tracing ("### locate_rule: " ^ ThmC.id_of_thm r ^ " not mem rrls");*) [])
1.135 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
1.136
1.137 fun next_rule thy eval_rls ro [rs] t =
1.138 @@ -575,7 +573,7 @@
1.139 val prepat = [([@{term True}], pat0),
1.140 ([@{term True}], pat1),
1.141 ([@{term True}], pat2)];
1.142 -(** )in( **)
1.143 +(**)in(**)
1.144
1.145 val add_fractions_p =
1.146 Rule_Set.Rrls {id = "add_fractions_p", prepat=prepat,
1.147 @@ -591,7 +589,7 @@
1.148 locate_rule = locate_rule thy Atools_erls ro,
1.149 next_rule = next_rule thy Atools_erls ro,
1.150 attach_form = attach_form}}
1.151 -(** )end; ( *local add_fractions_p *)
1.152 +(**)end(*local add_fractions_p *)
1.153 \<close>
1.154
1.155 subsection \<open>Cancelling and adding all occurrences in a term /////////////////////////////\<close>