858 fconv_rule (rewr_conv @{lemma "(x + a == y) == (x == y - (a::real))" |
858 fconv_rule (rewr_conv @{lemma "(x + a == y) == (x == y - (a::real))" |
859 by (atomize (full)) (simp add: field_simps)}) |
859 by (atomize (full)) (simp add: field_simps)}) |
860 fun substitutable_monomial fvs tm = |
860 fun substitutable_monomial fvs tm = |
861 (case Thm.term_of tm of |
861 (case Thm.term_of tm of |
862 Free (_, \<^typ>\<open>real\<close>) => |
862 Free (_, \<^typ>\<open>real\<close>) => |
863 if not (member (op aconvc) fvs tm) then (@1, tm) |
863 if not (Cterms.defined fvs tm) then (@1, tm) |
864 else raise Failure "substitutable_monomial" |
864 else raise Failure "substitutable_monomial" |
865 | \<^term>\<open>(*) :: real \<Rightarrow> _\<close> $ _ $ (Free _) => |
865 | \<^term>\<open>(*) :: real \<Rightarrow> _\<close> $ _ $ (Free _) => |
866 if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso |
866 if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso |
867 not (member (op aconvc) fvs (Thm.dest_arg tm)) |
867 not (Cterms.defined fvs (Thm.dest_arg tm)) |
868 then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm) |
868 then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm) |
869 else raise Failure "substitutable_monomial" |
869 else raise Failure "substitutable_monomial" |
870 | \<^term>\<open>(+) :: real \<Rightarrow> _\<close>$_$_ => |
870 | \<^term>\<open>(+) :: real \<Rightarrow> _\<close>$_$_ => |
871 (substitutable_monomial (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg tm))) |
871 (substitutable_monomial (fvs |> Cterms.fold Cterms.add (Misc_Legacy.cterm_frees (Thm.dest_arg tm))) |
872 (Thm.dest_arg1 tm) |
872 (Thm.dest_arg1 tm) |
873 handle Failure _ => |
873 handle Failure _ => |
874 substitutable_monomial (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg1 tm))) |
874 substitutable_monomial (fvs |> Cterms.fold Cterms.add (Misc_Legacy.cterm_frees (Thm.dest_arg1 tm))) |
875 (Thm.dest_arg tm)) |
875 (Thm.dest_arg tm)) |
876 | _ => raise Failure "substitutable_monomial") |
876 | _ => raise Failure "substitutable_monomial") |
877 |
877 |
878 fun isolate_variable v th = |
878 fun isolate_variable v th = |
879 let |
879 let |
896 (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>)) |
896 (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>)) |
897 Thm.term_ord |
897 Thm.term_ord |
898 |
898 |
899 fun make_substitution th = |
899 fun make_substitution th = |
900 let |
900 let |
901 val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th)) |
901 val (c,v) = substitutable_monomial Cterms.empty (Thm.dest_arg1(concl th)) |
902 val th1 = |
902 val th1 = |
903 Drule.arg_cong_rule |
903 Drule.arg_cong_rule |
904 (Thm.apply \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close> (RealArith.cterm_of_rat (Rat.inv c))) |
904 (Thm.apply \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close> (RealArith.cterm_of_rat (Rat.inv c))) |
905 (mk_meta_eq th) |
905 (mk_meta_eq th) |
906 val th2 = fconv_rule (binop_conv (real_poly_mul_conv ctxt)) th1 |
906 val th2 = fconv_rule (binop_conv (real_poly_mul_conv ctxt)) th1 |