# HG changeset patch # User wneuper # Date 1626712186 -7200 # Node ID cbad4e18e91b14da31fbe9ba82457e60ff447b33 # Parent dcb37736d573010b0216b519a458673bb94d24b7 cleanup after "eliminate ThmC.numerals_to_Free" diff -r dcb37736d573 -r cbad4e18e91b src/Tools/isac/BaseDefinitions/termC.sml --- a/src/Tools/isac/BaseDefinitions/termC.sml Mon Jul 19 17:29:35 2021 +0200 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Mon Jul 19 18:29:46 2021 +0200 @@ -90,9 +90,6 @@ val raise_type_conflicts: term list -> unit val strip_trueprop: term -> term - val numbers_to_string: term -> term - val uminus_to_string: term -> term - val var2free: term -> term val vars: term -> term list (* recognises numerals, should replace "fun vars_of" TODOO*) val vars': term list -> term list @@ -494,9 +491,6 @@ end; (** transform binary numeralsstrings **) -val numbers_to_string = ThmC_Def.num_to_Free -val uminus_to_string = ThmC_Def.uminus_to_string - fun mk_Free (s,T) = Free (s, T); fun mk_free T s = Free (s, T); @@ -542,21 +536,21 @@ (* TODO clarify parse with Test_Isac *) fun parseold thy str = (* before 2002 *) \<^try>\ - let val t = ((*typ_a2real o*) numbers_to_string) (Syntax.read_term_global thy str) + let val t = Syntax.read_term_global thy str in Thm.global_cterm_of thy t end\; fun parseN thy str = (* introduced 2002 *) \<^try>\ let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str) in Thm.global_cterm_of thy t end\; -fun parse_strict thy str = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str); +fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str); fun parse thy str = (* introduced 2010 *) \<^try>\ let val t = parse_strict thy str in Thm.global_cterm_of thy t end\; (*WN110317 parseNEW will replace parse after introduction of ctxt completed*) -fun parseNEW ctxt str = \<^try>\Syntax.read_term ctxt str |> numbers_to_string\; +fun parseNEW ctxt str = \<^try>\Syntax.read_term ctxt str\; fun parseNEW' ctxt str = case parseNEW ctxt str of SOME t => t diff -r dcb37736d573 -r cbad4e18e91b src/Tools/isac/BaseDefinitions/thmC-def.sml --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml Mon Jul 19 17:29:35 2021 +0200 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml Mon Jul 19 18:29:46 2021 +0200 @@ -16,9 +16,6 @@ (* required in ProgLang BEFORE definition in ---------------vvv *) val int_opt_of_string: string -> int option (* belongs to TermC *) - val numerals_to_Free: thm -> thm (* belongs to ThmC *) - val num_to_Free: term -> term (* belongs to TermC *) - val uminus_to_string: term -> term (* belongs to TermC *) end (**) @@ -47,51 +44,4 @@ case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE end; - -(** transform Isabelle's binary numerals to "Free (string, T)" **) - -val num_to_Free = (**)I(* Makarius 100308 *) -(** ) - let - fun dest_num t = - (case try HOLogic.dest_number t of - SOME (T, i) => SOME (Free (signed_string_of_int i, T)) - | NONE => NONE); - fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b) - | to_str (t as (u1 $ u2)) = - (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2) - | to_str t = perhaps dest_num t; - in to_str end -( **) - -val uminus_to_string = (**)I -(** ) - let - fun dest_num t = - case t of - (Const (\<^const_name>\uminus\, _) $ Free (s, T)) => - (case int_opt_of_string s of - SOME i => SOME (Free (signed_string_of_int (~1 * i), T)) - | NONE => NONE) - | _ => NONE; - fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b) - | to_str (t as (u1 $ u2)) = - (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2) - | to_str t = perhaps dest_num t; - in to_str end; -( **) - -fun numerals_to_Free thm = (**)thm -(** ) - let - val prop = Thm.plain_prop_of thm - val prop' = num_to_Free prop; - in - if prop = prop' then thm - else - Skip_Proof.make_thm (Thm.theory_of_thm thm) prop' - |> Thm.put_name_hint (Thm.get_name_hint thm) - end; -( **) - (**)end(**) diff -r dcb37736d573 -r cbad4e18e91b src/Tools/isac/Interpret/derive.sml --- a/src/Tools/isac/Interpret/derive.sml Mon Jul 19 17:29:35 2021 +0200 +++ b/src/Tools/isac/Interpret/derive.sml Mon Jul 19 18:29:46 2021 +0200 @@ -84,7 +84,7 @@ (msg_3 t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')) | Rule.Eval (c as (op_, _)) => (msg_4 op_; - case Eval.adhoc_thm thy c (TermC.uminus_to_string t) of + case Eval.adhoc_thm thy c t of NONE => rew_once lim rts t apno rs' | SOME (thmid, tm) => (let diff -r dcb37736d573 -r cbad4e18e91b src/Tools/isac/Knowledge/Diff.thy --- a/src/Tools/isac/Knowledge/Diff.thy Mon Jul 19 17:29:35 2021 +0200 +++ b/src/Tools/isac/Knowledge/Diff.thy Mon Jul 19 18:29:46 2021 +0200 @@ -156,8 +156,8 @@ Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"), Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"), Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}), - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true})], + Rule.Thm ("not_false", @{thm not_false}), + Rule.Thm ("not_true", @{thm not_true})], srls = Rule_Set.Empty, calc = [], errpatts = [], rules = [\<^rule_thm>\frac_sym_conv\, \<^rule_thm>\sqrt_sym_conv\, diff -r dcb37736d573 -r cbad4e18e91b src/Tools/isac/Knowledge/Poly.thy --- a/src/Tools/isac/Knowledge/Poly.thy Mon Jul 19 17:29:35 2021 +0200 +++ b/src/Tools/isac/Knowledge/Poly.thy Mon Jul 19 18:29:46 2021 +0200 @@ -739,8 +739,8 @@ Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"), Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"), Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}), - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}), + Rule.Thm ("not_false", @{thm not_false}), + Rule.Thm ("not_true", @{thm not_true}), Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_") ], scr = Rule.Empty_Prog @@ -753,7 +753,7 @@ rules = [\<^rule_thm>\real_diff_minus\, (*"a - b = a + -1 * b"*) - Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym})) + Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym})) (*"\(z is_const) ==> - (z::real) = -1 * z"*)], scr = Rule.Empty_Prog}; @@ -790,9 +790,9 @@ \<^rule_thm>\realpow_pow\, (*"(a \ b) \ c = a \ (b * c)"*) (**) - Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}), + Rule.Thm ("realpow_minus_even", @{thm realpow_minus_even}), (*"n is_even ==> (- r) \ n = r \ n"*) - Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd}) + Rule.Thm ("realpow_minus_odd", @{thm realpow_minus_odd}) (*"Not (n is_even) ==> (- r) \ n = -1 * r \ n"*) (**) ], scr = Rule.Empty_Prog}; @@ -803,8 +803,8 @@ erls = Rule_Set.append_rules "Rule_Set.empty-expand_poly_rat_" Rule_Set.empty [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp ""), Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"), - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}), - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}) + Rule.Thm ("not_false", @{thm not_false}), + Rule.Thm ("not_true", @{thm not_true}) ], srls = Rule_Set.Empty, calc = [], errpatts = [], @@ -832,11 +832,11 @@ \<^rule_thm>\realpow_multI_poly\, (*"[| r is_polyexp; s is_polyexp |] ==> (r * s) \ n = r \ n * s \ n"*) - Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}), + Rule.Thm ("realpow_pow", @{thm realpow_pow}), (*"(a \ b) \ c = a \ (b * c)"*) - Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}), + Rule.Thm ("realpow_minus_even", @{thm realpow_minus_even}), (*"n is_even ==> (- r) \ n = r \ n"*) - Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd}) + Rule.Thm ("realpow_minus_odd", @{thm realpow_minus_odd}) (*"\ (n is_even) ==> (- r) \ n = -1 * r \ n"*) ], scr = Rule.Empty_Prog}; @@ -962,11 +962,11 @@ rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], rules = - [Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}), + [Rule.Thm ("distrib_right" , @{thm distrib_right}), (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) \<^rule_thm>\distrib_left\, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) - (*Rule.Thm ("distrib_right1",ThmC.numerals_to_Free @{thm distrib_right}1), + (*Rule.Thm ("distrib_right1", @{thm distrib_right}1), ....... 18.3.03 undefined???*) \<^rule_thm>\real_plus_binom_pow2\, @@ -982,7 +982,7 @@ (*"- (- ?z) = ?z"*) \<^rule_thm>\real_diff_minus\, (*"a - b = a + -1 * b"*) - Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym})) + Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym})) (*"\(z is_const) ==> - (z::real) = -1 * z"*) (*\<^rule_thm>\real_minus_add_distrib\,*) @@ -1043,7 +1043,7 @@ (*"1 * z = z"*) (*\<^rule_thm>\real_mult_minus1\,14.3.03*) (*"-1 * z = - z"*) - Rule.Thm ("minus_mult_left", ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})), + Rule.Thm ("minus_mult_left", (@{thm minus_mult_left} RS @{thm sym})), (*- (?x * ?y) = "- ?x * ?y"*) (*\<^rule_thm>\real_minus_mult_cancel\, (*"- ?x * - ?y = ?x * ?y"*)---*) diff -r dcb37736d573 -r cbad4e18e91b src/Tools/isac/Knowledge/PolyEq.thy --- a/src/Tools/isac/Knowledge/PolyEq.thy Mon Jul 19 17:29:35 2021 +0200 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Mon Jul 19 18:29:46 2021 +0200 @@ -337,12 +337,12 @@ Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"), Rule.Eval ("RootEq.is_rootTerm_in", eval_is_rootTerm_in ""), Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in ""), - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}), - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}), - Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}), - Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}), - Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}), - Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false}) + Rule.Thm ("not_true", @{thm not_true}), + Rule.Thm ("not_false", @{thm not_false}), + Rule.Thm ("and_true", @{thm and_true}), + Rule.Thm ("and_false", @{thm and_false}), + Rule.Thm ("or_true", @{thm or_true}), + Rule.Thm ("or_false", @{thm or_false}) ]; val PolyEq_erls = diff -r dcb37736d573 -r cbad4e18e91b src/Tools/isac/Knowledge/Rational.thy --- a/src/Tools/isac/Knowledge/Rational.thy Mon Jul 19 17:29:35 2021 +0200 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Jul 19 18:29:46 2021 +0200 @@ -410,8 +410,8 @@ [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"), Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"), Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"), - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}), - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})], + Rule.Thm ("not_true", @{thm not_true}), + Rule.Thm ("not_false", @{thm not_false})], scr = Rule.Empty_Prog}); (* simplifies expressions with numerals; @@ -425,7 +425,7 @@ rules = [\<^rule_eval>\divide\ (Prog_Expr.eval_cancel "#divide_e"), - Rule.Thm ("minus_divide_left", ThmC.numerals_to_Free (@{thm minus_divide_left} RS @{thm sym})), + Rule.Thm ("minus_divide_left", (@{thm minus_divide_left} RS @{thm sym})), (*SYM - ?x / ?y = - (?x / ?y) may come from subst*) \<^rule_thm>\rat_add\, (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \ diff -r dcb37736d573 -r cbad4e18e91b src/Tools/isac/Knowledge/RootRat.thy --- a/src/Tools/isac/Knowledge/RootRat.thy Mon Jul 19 17:29:35 2021 +0200 +++ b/src/Tools/isac/Knowledge/RootRat.thy Mon Jul 19 18:29:46 2021 +0200 @@ -20,7 +20,7 @@ (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *) \<^rule_thm>\mult_1_left\, (* 1 * z = z *) - Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym})), + Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym})), (*"\(z is_const) ==> - (z::real) = -1 * z"*) Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_") ]; diff -r dcb37736d573 -r cbad4e18e91b src/Tools/isac/Knowledge/Test.thy --- a/src/Tools/isac/Knowledge/Test.thy Mon Jul 19 17:29:35 2021 +0200 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Jul 19 18:29:46 2021 +0200 @@ -457,7 +457,7 @@ scr = Rule.Empty_Prog }; -(*todo: replace by Rewrite("rnorm_equation_add",ThmC.numerals_to_Free @{thm rnorm_equation_add)*) +(*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*) val norm_equation = Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [], diff -r dcb37736d573 -r cbad4e18e91b src/Tools/isac/MathEngBasic/rewrite.sml --- a/src/Tools/isac/MathEngBasic/rewrite.sml Mon Jul 19 17:29:35 2021 +0200 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Mon Jul 19 18:29:46 2021 +0200 @@ -167,8 +167,7 @@ rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms))) (* once again try the same rule, e.g. associativity against "()"*) | Rule.Eval (cc as (op_, _)) => - let val _= trace_in1 i "try calc" op_; - val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*) + let val _ = trace_in1 i "try calc" op_; in case Eval.adhoc_thm thy cc ct of NONE => rew_once ruls asm ct apno thms | SOME (_, thm') => @@ -181,8 +180,7 @@ in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end end | Rule.Cal1 (cc as (op_, _)) => - let val _= trace_in1 i "try cal1" op_; - val ct = TermC.uminus_to_string ct + let val _ = trace_in1 i "try cal1" op_; in case Eval.adhoc_thm1_ thy cc ct of NONE => (ct, asm) | SOME (_, thm') => @@ -282,16 +280,14 @@ (* search ct for adjacent numerals and calculate them by operator isa_fn *) fun calculate_ thy isa_fn ct = - let val ct = TermC.uminus_to_string ct - in case Eval.adhoc_thm thy isa_fn ct of - NONE => NONE - | SOME (thmID, thm) => - (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of - SOME (rew, _) => rew - | NONE => raise ERROR "" - in SOME (rew, (thmID, thm)) end) - handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite") - end; + case Eval.adhoc_thm thy isa_fn ct of + NONE => NONE + | SOME (thmID, thm) => + (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of + SOME (rew, _) => rew + | NONE => raise ERROR "" + in SOME (rew, (thmID, thm)) end) + handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite"); fun eval_prog_expr thy srls t = let val rew = rewrite_set_ thy false srls t; diff -r dcb37736d573 -r cbad4e18e91b src/Tools/isac/MathEngBasic/thmC.sml --- a/src/Tools/isac/MathEngBasic/thmC.sml Mon Jul 19 17:29:35 2021 +0200 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Mon Jul 19 18:29:46 2021 +0200 @@ -20,8 +20,6 @@ val from_rule : Rule.rule -> T val member': id list -> Rule.rule -> bool - val numerals_to_Free: thm -> thm - val is_sym: id -> bool val thm_from_thy: theory -> ThmC_Def.id -> thm @@ -67,11 +65,6 @@ handle ERROR _ => false -(** convert Isabelle's numerals to ISAC's specific format, LEGACY **) - -val numerals_to_Free = ThmC_Def.numerals_to_Free; (* numeral \ Free ("int", T) *) - - (** handle symmetric equalities, generated by deriving input terms **) fun is_sym id = @@ -91,11 +84,11 @@ "s" :: "y" :: "m" :: "_" :: "#" :: _ => raise ERROR ("thm_from_thy not impl.for " ^ thmid) | "s" :: "y" :: "m" :: "_" :: id => - ((numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym + ((Global_Theory.get_thm thy) (implode id)) RS sym | "#" :: _ => raise ERROR ("thm_from_thy not impl.for " ^ thmid) | _ => - thmid |> Global_Theory.get_thm thy |> numerals_to_Free + thmid |> Global_Theory.get_thm thy fun dest_eq_concl thm = (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) thm of @@ -179,7 +172,7 @@ if dynamic then error ("Bad dynamic fact " ^ quote name ^ Position.here pos) else Facts.the_single (name, pos) thms; val (xname', thm') = if symmetric then (sym_prefix ^ xname, thm RS sym) else (xname, thm); - in Rule.Thm (xname', numerals_to_Free thm') end; + in Rule.Thm (xname', thm') end; fun antiquotation binding sym = ML_Antiquotation.value_embedded binding diff -r dcb37736d573 -r cbad4e18e91b src/Tools/isac/ProgLang/ListC.thy --- a/src/Tools/isac/ProgLang/ListC.thy Mon Jul 19 17:29:35 2021 +0200 +++ b/src/Tools/isac/ProgLang/ListC.thy Mon Jul 19 18:29:46 2021 +0200 @@ -133,49 +133,49 @@ val prog_expr = Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [], - rules = [Rule_Def.Thm ("refl", ThmC_Def.numerals_to_Free @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*) - Rule_Def.Thm ("o_apply", ThmC_Def.numerals_to_Free @{thm o_apply}), + rules = [Rule_Def.Thm ("refl", @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*) + Rule_Def.Thm ("o_apply", @{thm o_apply}), - Rule_Def.Thm ("NTH_CONS",ThmC_Def.numerals_to_Free @{thm NTH_CONS}),(*erls for cond. in Atools.ML*) - Rule_Def.Thm ("NTH_NIL",ThmC_Def.numerals_to_Free @{thm NTH_NIL}), - Rule_Def.Thm ("append_Cons",ThmC_Def.numerals_to_Free @{thm append_Cons}), - Rule_Def.Thm ("append_Nil",ThmC_Def.numerals_to_Free @{thm append_Nil}), + Rule_Def.Thm ("NTH_CONS", @{thm NTH_CONS}),(*erls for cond. in Atools.ML*) + Rule_Def.Thm ("NTH_NIL", @{thm NTH_NIL}), + Rule_Def.Thm ("append_Cons", @{thm append_Cons}), + Rule_Def.Thm ("append_Nil", @{thm append_Nil}), (* Thm ("butlast_Cons",num_str @{thm butlast_Cons}), Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*) - Rule_Def.Thm ("concat_Cons",ThmC_Def.numerals_to_Free @{thm concat_Cons}), - Rule_Def.Thm ("concat_Nil",ThmC_Def.numerals_to_Free @{thm concat_Nil}), + Rule_Def.Thm ("concat_Cons", @{thm concat_Cons}), + Rule_Def.Thm ("concat_Nil", @{thm concat_Nil}), (* Rule_Def.Thm ("del_base",num_str @{thm del_base}), Rule_Def.Thm ("del_rec",num_str @{thm del_rec}), *) - Rule_Def.Thm ("distinct_Cons",ThmC_Def.numerals_to_Free @{thm distinct_Cons}), - Rule_Def.Thm ("distinct_Nil",ThmC_Def.numerals_to_Free @{thm distinct_Nil}), - Rule_Def.Thm ("dropWhile_Cons",ThmC_Def.numerals_to_Free @{thm dropWhile_Cons}), - Rule_Def.Thm ("dropWhile_Nil",ThmC_Def.numerals_to_Free @{thm dropWhile_Nil}), - Rule_Def.Thm ("filter_Cons",ThmC_Def.numerals_to_Free @{thm filter_Cons}), - Rule_Def.Thm ("filter_Nil",ThmC_Def.numerals_to_Free @{thm filter_Nil}), - Rule_Def.Thm ("foldr_Cons",ThmC_Def.numerals_to_Free @{thm foldr_Cons}), - Rule_Def.Thm ("foldr_Nil",ThmC_Def.numerals_to_Free @{thm foldr_Nil}), - Rule_Def.Thm ("hd_thm",ThmC_Def.numerals_to_Free @{thm hd_thm}), - Rule_Def.Thm ("LAST",ThmC_Def.numerals_to_Free @{thm LAST}), - Rule_Def.Thm ("LENGTH_CONS",ThmC_Def.numerals_to_Free @{thm LENGTH_CONS}), - Rule_Def.Thm ("LENGTH_NIL",ThmC_Def.numerals_to_Free @{thm LENGTH_NIL}), + Rule_Def.Thm ("distinct_Cons", @{thm distinct_Cons}), + Rule_Def.Thm ("distinct_Nil", @{thm distinct_Nil}), + Rule_Def.Thm ("dropWhile_Cons", @{thm dropWhile_Cons}), + Rule_Def.Thm ("dropWhile_Nil", @{thm dropWhile_Nil}), + Rule_Def.Thm ("filter_Cons", @{thm filter_Cons}), + Rule_Def.Thm ("filter_Nil", @{thm filter_Nil}), + Rule_Def.Thm ("foldr_Cons", @{thm foldr_Cons}), + Rule_Def.Thm ("foldr_Nil", @{thm foldr_Nil}), + Rule_Def.Thm ("hd_thm", @{thm hd_thm}), + Rule_Def.Thm ("LAST", @{thm LAST}), + Rule_Def.Thm ("LENGTH_CONS", @{thm LENGTH_CONS}), + Rule_Def.Thm ("LENGTH_NIL", @{thm LENGTH_NIL}), (* Rule_Def.Thm ("list_diff_def",num_str @{thm list_diff_def}),*) - Rule_Def.Thm ("map_Cons",ThmC_Def.numerals_to_Free @{thm map_Cons}), - Rule_Def.Thm ("map_Nil",ThmC_Def.numerals_to_Free @{thm map_Cons}), -(* Rule_Def.Thm ("mem_Cons",ThmC_Def.numerals_to_Free @{thm mem_Cons}), - Rule_Def.Thm ("mem_Nil",ThmC_Def.numerals_to_Free @{thm mem_Nil}), *) -(* Rule_Def.Thm ("null_Cons",ThmC_Def.numerals_to_Free @{thm null_Cons}), - Rule_Def.Thm ("null_Nil",ThmC_Def.numerals_to_Free @{thm null_Nil}),*) - Rule_Def.Thm ("remdups_Cons",ThmC_Def.numerals_to_Free @{thm remdups_Cons}), - Rule_Def.Thm ("remdups_Nil",ThmC_Def.numerals_to_Free @{thm remdups_Nil}), - Rule_Def.Thm ("rev_Cons",ThmC_Def.numerals_to_Free @{thm rev_Cons}), - Rule_Def.Thm ("rev_Nil",ThmC_Def.numerals_to_Free @{thm rev_Nil}), - Rule_Def.Thm ("take_Nil",ThmC_Def.numerals_to_Free @{thm take_Nil}), - Rule_Def.Thm ("take_Cons",ThmC_Def.numerals_to_Free @{thm take_Cons}), - Rule_Def.Thm ("tl_Cons",ThmC_Def.numerals_to_Free @{thm tl_Cons}), - Rule_Def.Thm ("tl_Nil",ThmC_Def.numerals_to_Free @{thm tl_Nil}), - Rule_Def.Thm ("zip_Cons",ThmC_Def.numerals_to_Free @{thm zip_Cons}), - Rule_Def.Thm ("zip_Nil",ThmC_Def.numerals_to_Free @{thm zip_Nil})], + Rule_Def.Thm ("map_Cons", @{thm map_Cons}), + Rule_Def.Thm ("map_Nil", @{thm map_Cons}), +(* Rule_Def.Thm ("mem_Cons", @{thm mem_Cons}), + Rule_Def.Thm ("mem_Nil", @{thm mem_Nil}), *) +(* Rule_Def.Thm ("null_Cons", @{thm null_Cons}), + Rule_Def.Thm ("null_Nil", @{thm null_Nil}),*) + Rule_Def.Thm ("remdups_Cons", @{thm remdups_Cons}), + Rule_Def.Thm ("remdups_Nil", @{thm remdups_Nil}), + Rule_Def.Thm ("rev_Cons", @{thm rev_Cons}), + Rule_Def.Thm ("rev_Nil", @{thm rev_Nil}), + Rule_Def.Thm ("take_Nil", @{thm take_Nil}), + Rule_Def.Thm ("take_Cons", @{thm take_Cons}), + Rule_Def.Thm ("tl_Cons", @{thm tl_Cons}), + Rule_Def.Thm ("tl_Nil", @{thm tl_Nil}), + Rule_Def.Thm ("zip_Cons", @{thm zip_Cons}), + Rule_Def.Thm ("zip_Nil", @{thm zip_Nil})], scr = Rule_Def.Empty_Prog}: Rule_Set.T; \ rule_set_knowledge prog_expr = prog_expr diff -r dcb37736d573 -r cbad4e18e91b src/Tools/isac/ProgLang/Program.thy --- a/src/Tools/isac/ProgLang/Program.thy Mon Jul 19 17:29:35 2021 +0200 +++ b/src/Tools/isac/ProgLang/Program.thy Mon Jul 19 18:29:46 2021 +0200 @@ -67,8 +67,7 @@ |> Thm.prop_of |> HOLogic.dest_Trueprop |> Logic.unvarify_global - |> TermC.inst_abs - |> ThmC_Def.num_to_Free (*for numbers in the program*)) + |> TermC.inst_abs) handle TERM _ => raise TERM ("prep_program", [Thm.prop_of thm]) (* get identifier of partial_function *) diff -r dcb37736d573 -r cbad4e18e91b test/Tools/isac/BaseDefinitions/termC.sml --- a/test/Tools/isac/BaseDefinitions/termC.sml Mon Jul 19 17:29:35 2021 +0200 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Mon Jul 19 18:29:46 2021 +0200 @@ -14,7 +14,6 @@ "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------------------"; "----------- fun TermC.vars_of -----------------------------------------------------------------"; "----------- fun TermC.vars --------------------------------------------------------------------"; -"----------- uminus_to_string ---------------------------"; "----------- *** Problem.prep_input: syntax error in '#Where' of [v"; "----------- check writeln, tracing for string markup ---"; "----------- build fun TermC.is_bdv_subst ------------------------------------------------------------"; @@ -30,7 +29,6 @@ "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------"; "----------- fun TermC.is_list -----------------------------------------------------------------------"; "----------- fun inst_abs ----------------------------------------------------------------------"; -"----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------"; "--------------------------------------------------------"; "--------------------------------------------------------"; @@ -184,17 +182,17 @@ "----------- inst_bdv -----------------------------------"; "----------- inst_bdv -----------------------------------"; "----------- inst_bdv -----------------------------------"; - if (UnparseC.term o Thm.prop_of o ThmC.numerals_to_Free) @{thm d1_isolate_add2} = + if (UnparseC.term o Thm.prop_of) @{thm d1_isolate_add2} = "\ ?bdv occurs_in ?a \\n(?a + ?bdv = 0) = (?bdv = - 1 * ?a)" then () else error "termC.sml d1_isolate_add2"; val subst = [(TermC.str2term "bdv", TermC.str2term "x")]; - val t = (Eval.norm o Thm.prop_of) (ThmC.numerals_to_Free @{thm d1_isolate_add2}); + val t = (Eval.norm o Thm.prop_of) @{thm d1_isolate_add2}; val t' = TermC.inst_bdv subst t; if UnparseC.term t' = "\ x occurs_in ?a \ (?a + x = 0) = (x = - 1 * ?a)" then () else error "termC.sml inst_bdv 1"; -if (UnparseC.term o Thm.prop_of o ThmC.numerals_to_Free) @{thm separate_bdvs_add} = +if (UnparseC.term o Thm.prop_of) @{thm separate_bdvs_add} = "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0,\n " ^ "?bdv_4.0] occur_exactly_in ?a \\n(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)" then () else error "termC.sml separate_bdvs_add"; @@ -205,7 +203,7 @@ (TermC.str2term "bdv_2", TermC.str2term "c_2"), (TermC.str2term "bdv_3", TermC.str2term "c_3"), (TermC.str2term "bdv_4", TermC.str2term "c_4")]; -val t = (Eval.norm o Thm.prop_of) (ThmC.numerals_to_Free @{thm separate_bdvs_add}); +val t = (Eval.norm o Thm.prop_of) @{thm separate_bdvs_add}; val t' = TermC.inst_bdv subst t; if UnparseC.term t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a \\n" ^ @@ -360,9 +358,8 @@ TermC.parse thy str; "---------------"; val str = "x + 2*z"; - val t = (Syntax.read_term_global thy str); - val t = ThmC_Def.num_to_Free (Syntax.read_term_global thy str); - val t = (TermC.typ_a2real o ThmC_Def.num_to_Free) (Syntax.read_term_global thy str); + val t = Syntax.read_term_global thy str; + val t = TermC.typ_a2real (Syntax.read_term_global thy str); Thm.global_cterm_of thy t; case TermC.parse thy str of SOME t' => t' @@ -417,23 +414,13 @@ | _ => error "TermC.vars_of (3 = 3 * AA / 4) ..changed (! use only for polynomials, not equations!)"; -"----------- uminus_to_string ---------------------------"; -"----------- uminus_to_string ---------------------------"; -"----------- uminus_to_string ---------------------------"; - val t1 = ThmC_Def.num_to_Free @{term "-2::real"}; - val t2 = ThmC_Def.num_to_Free @{term "- 2::real"}; - if TermC.uminus_to_string t2 = t1 - then () - else error "termC.sml diff.behav. in uminus_to_string"; - "----------- *** Problem.prep_input: syntax error in '#Where' of [v"; "----------- *** Problem.prep_input: syntax error in '#Where' of [v"; "----------- *** Problem.prep_input: syntax error in '#Where' of [v"; "===== deconstruct datatype typ ==="; val str = "?a"; val t = (thy, str) |>> ThyC.to_ctxt - |-> Proof_Context.read_term_pattern - |> ThmC_Def.num_to_Free; + |-> Proof_Context.read_term_pattern; val Var (("a", 0), ty) = t; val TVar ((str, i), srt) = ty; if str = "'a" andalso i = 1 andalso srt = [] @@ -443,8 +430,7 @@ "----- real type in pattern ---"; val str = "?a :: real"; val t = (thy, str) |>> ThyC.to_ctxt - |-> Proof_Context.read_term_pattern - |> ThmC_Def.num_to_Free; + |-> Proof_Context.read_term_pattern; val Var (("a", 0), ty) = t; val Type (str, tys) = ty; if str = \<^type_name>\real\ andalso tys = [] andalso ty = HOLogic.realT @@ -460,8 +446,7 @@ val ctxt = Config.put show_types true ctxt; "----- read_term_pattern ---"; val t = (thy, str) |>> ThyC.to_ctxt - |-> Proof_Context.read_term_pattern - |> ThmC_Def.num_to_Free; + |-> Proof_Context.read_term_pattern; val t_real = TermC.typ_a2real t; if UnparseC.term_in_ctxt ctxt t_real = "\ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) \\n " @@ -646,7 +631,7 @@ val SOME t' = TermC.strip_imp_prems' t; if UnparseC.term t' = "(\) (?k \ 0)" then () else error "TermC.strip_imp_prems' changed"; -val thm = ThmC.numerals_to_Free @{thm frac_sym_conv}; +val thm = @{thm frac_sym_conv}; val prop = Thm.prop_of thm; val concl = Logic.strip_imp_concl prop; val SOME prems = TermC.strip_imp_prems' prop; @@ -685,24 +670,6 @@ val ty = (Term.type_of o Thm.term_of) ct; if TermC.is_list t = true then () else error "TermC.is_list [a, b, c]"; -"----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------"; -"----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------"; -"----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------"; -case ThmC_Def.num_to_Free @{term "123::real"} of - Const (\<^const_name>\numeral\, _) $ - (Const (\<^const_name>\num.Bit1\, _) $ - (Const (\<^const_name>\num.Bit1\, _) $ - (Const (\<^const_name>\num.Bit0\, _) $ (Const (\<^const_name>\num.Bit1\, _) $ (Const (\<^const_name>\num.Bit1\, _) $ (Const (\<^const_name>\num.Bit1\, _) $ Const (\<^const_name>\num.One\, _))))))) => () -| _ => error "ThmC_Def.num_to_Free '123' changed"; - -case ThmC_Def.num_to_Free @{term "1::real"} of - Const (\<^const_name>\one_class.one\, _) => () -| _ => error "ThmC_Def.num_to_Free '1' changed"; - -case ThmC_Def.num_to_Free @{term "0::real"} of - Const (\<^const_name>\zero_class.zero\, _) => () -| _ => error "ThmC_Def.num_to_Free '0' changed"; - "----------- fun mk_frac, proper term with uminus ----------------------------------------------"; "----------- fun mk_frac, proper term with uminus ----------------------------------------------"; "----------- fun mk_frac, proper term with uminus ----------------------------------------------"; diff -r dcb37736d573 -r cbad4e18e91b test/Tools/isac/BridgeLibisabelle/thy-present.sml --- a/test/Tools/isac/BridgeLibisabelle/thy-present.sml Mon Jul 19 17:29:35 2021 +0200 +++ b/test/Tools/isac/BridgeLibisabelle/thy-present.sml Mon Jul 19 18:29:46 2021 +0200 @@ -126,7 +126,7 @@ "----------- fun is_contained_in ------------------------"; "----------- fun is_contained_in ------------------------"; "----------- fun is_contained_in ------------------------"; -val r1 = Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}); +val r1 = Thm ("real_diff_minus", @{thm real_diff_minus}); if Rule_Set.contains r1 Test_simplify then () else error "rewtools.sml Rule_Set.contains Thm"; diff -r dcb37736d573 -r cbad4e18e91b test/Tools/isac/BridgeLibisabelle/use-cases.sml --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon Jul 19 17:29:35 2021 +0200 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon Jul 19 18:29:46 2021 +0200 @@ -710,7 +710,7 @@ autoCalculate 1 (Steps 1); fetchProposedTactic 1; setNextTactic 1 (Apply_Method ["PolyEq", "normalise_poly"]); autoCalculate 1 (Steps 1); fetchProposedTactic 1; - setNextTactic 1 (Rewrite ("all_left", ThmC.numerals_to_Free @{thm all_left})); + setNextTactic 1 (Rewrite ("all_left", @{thm all_left})); autoCalculate 1 (Steps 1); fetchProposedTactic 1; setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "make_ratpoly_in")); autoCalculate 1 (Steps 1); fetchProposedTactic 1; diff -r dcb37736d573 -r cbad4e18e91b test/Tools/isac/Knowledge/diophanteq.sml --- a/test/Tools/isac/Knowledge/diophanteq.sml Mon Jul 19 17:29:35 2021 +0200 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Mon Jul 19 18:29:46 2021 +0200 @@ -34,7 +34,7 @@ | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1"; val SOME (t,_) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst - (ThmC.numerals_to_Free @{thm "int_isolate_add"}) t; UnparseC.term t; + @{thm "int_isolate_add"} t; UnparseC.term t; val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; UnparseC.term t; diff -r dcb37736d573 -r cbad4e18e91b test/Tools/isac/Knowledge/polyminus.sml --- a/test/Tools/isac/Knowledge/polyminus.sml Mon Jul 19 17:29:35 2021 +0200 +++ b/test/Tools/isac/Knowledge/polyminus.sml Mon Jul 19 18:29:46 2021 +0200 @@ -706,9 +706,9 @@ (*"(?a | True) = True"*) Thm ("or_false",@{thm or_false}), (*"(?a | False) = ?a"*) - Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}), + Thm ("not_true", @{thm not_true}), (*"(~ True) = False"*) - Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}) + Thm ("not_false", @{thm not_false}) (*"(~ False) = True"*)]; (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*) val SOME (t', _) = rewrite_set_ thy false prls t; diff -r dcb37736d573 -r cbad4e18e91b test/Tools/isac/MathEngBasic/rewrite.sml --- a/test/Tools/isac/MathEngBasic/rewrite.sml Mon Jul 19 17:29:35 2021 +0200 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Mon Jul 19 18:29:46 2021 +0200 @@ -474,7 +474,7 @@ "----------- 2011 thms with axclasses ----------------------------------------------------------"; "----------- 2011 thms with axclasses ----------------------------------------------------------"; "----------- 2011 thms with axclasses ----------------------------------------------------------"; -val thm = ThmC.numerals_to_Free @{thm div_by_1}; +val thm = @{thm div_by_1}; val prop = Thm.prop_of thm; TermC.atomty prop; (*Type 'a*) val t = TermC.str2term "(2*x)/1"; (*Type real*) diff -r dcb37736d573 -r cbad4e18e91b test/Tools/isac/MathEngBasic/thmC.sml --- a/test/Tools/isac/MathEngBasic/thmC.sml Mon Jul 19 17:29:35 2021 +0200 +++ b/test/Tools/isac/MathEngBasic/thmC.sml Mon Jul 19 18:29:46 2021 +0200 @@ -63,7 +63,7 @@ then () else error "fun revert_sym_rule changed 1"; val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy - (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus})) + (Thm ("real_diff_minus", @{thm real_diff_minus})) ; if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + - 1 * ?b" then () else error "fun revert_sym_rule changed 2" diff -r dcb37736d573 -r cbad4e18e91b test/Tools/isac/ProgLang/auto_prog.sml --- a/test/Tools/isac/ProgLang/auto_prog.sml Mon Jul 19 17:29:35 2021 +0200 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Mon Jul 19 18:29:46 2021 +0200 @@ -241,7 +241,7 @@ "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------"; "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------"; "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------"; -val t = rule2stac @{theory} (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus})); +val t = rule2stac @{theory} (Thm ("real_diff_minus", @{thm real_diff_minus})); if UnparseC.term t = "Try (Repeat (Rewrite ''real_diff_minus''))" then () else error "rule2stac Thm.. changed"; @@ -253,7 +253,7 @@ if UnparseC.term t = "Try (Rewrite_Set ''rearrange_assoc'')" then () else error "rule2stac Rls_.. changed"; -val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", ThmC.numerals_to_Free @{thm risolate_bdv_add})); +val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", @{thm risolate_bdv_add})); if UnparseC.term t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then () else error "rule2stac_inst Thm.. changed"; case t of diff -r dcb37736d573 -r cbad4e18e91b test/Tools/isac/ProgLang/evaluate.sml --- a/test/Tools/isac/ProgLang/evaluate.sml Mon Jul 19 17:29:35 2021 +0200 +++ b/test/Tools/isac/ProgLang/evaluate.sml Mon Jul 19 18:29:46 2021 +0200 @@ -117,7 +117,7 @@ *) val thy = @{theory "Test"}; val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE")); - val ct = ThmC_Def.num_to_Free @{term + val ct = @{term "sqrt (x \ 2 + -3 * x) = (-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))"}; case calculate_ thy op_ ct of SOME _ => () diff -r dcb37736d573 -r cbad4e18e91b test/Tools/isac/ProgLang/listC.sml --- a/test/Tools/isac/ProgLang/listC.sml Mon Jul 19 17:29:35 2021 +0200 +++ b/test/Tools/isac/ProgLang/listC.sml Mon Jul 19 18:29:46 2021 +0200 @@ -48,9 +48,9 @@ val t = TermC.str2term "NTH 1 [a,b,c,d,e]"; TermC.atomty t; -val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_NIL}; +val thm = Thm.prop_of @{thm NTH_NIL}; TermC.atomty thm; -val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_NIL}) t; +val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false @{thm NTH_NIL} t; if UnparseC.term t' = "a" then () else error "NTH 1 [a,b,c,d,e] = a ..changed"; @@ -63,9 +63,9 @@ (Const (\<^const_name>\Cons\, _) $ Free ("d", _) $ (Const (\<^const_name>\Cons\, _) $ Free ("e", _) $ Const (\<^const_name>\Nil\, _)))))) => () | _ => error "ListC.NTH changed"; -val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_CONS}; +val thm = Thm.prop_of @{thm NTH_CONS}; TermC.atomty thm; -val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_CONS}) t; +val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false @{thm NTH_CONS} t; if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed"; diff -r dcb37736d573 -r cbad4e18e91b test/Tools/isac/Test_Isac_Short.thy --- a/test/Tools/isac/Test_Isac_Short.thy Mon Jul 19 17:29:35 2021 +0200 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Jul 19 18:29:46 2021 +0200 @@ -329,9 +329,7 @@ ML \"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\ ML \ \ ML \ -@{term Let} \ ML \ -val Const (\<^const_name>\Let\, _) = @{term Let} \ ML \ \ ML \ \ ML \ diff -r dcb37736d573 -r cbad4e18e91b test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Mon Jul 19 17:29:35 2021 +0200 +++ b/test/Tools/isac/Test_Some.thy Mon Jul 19 18:29:46 2021 +0200 @@ -1631,8 +1631,8 @@ rules = [(*for rewriting conditions in Thm's*) Eval ("Prog_Expr.occurs_in", eval_occurs_in "#occurs_in_"), - Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}), - Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})], + Thm ("not_true", @{thm not_true}), + Thm ("not_false", @{thm not_false})], scr = Empty_Prog}; val subs = [(str2t "bdv::real", str2t "x::real")]; \ ML \ @@ -1803,20 +1803,20 @@ val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")]; val rls = (Rule_Set.append_rules "separate_bdv" collect_bdv - [Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}), + [Thm ("separate_bdv", @{thm separate_bdv}), (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) - Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}), + Thm ("separate_bdv_n", @{thm separate_bdv_n}), (*"?a * ?bdv \ ?n / ?b = ?a / ?b * ?bdv \ ?n"*) - Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}), + Thm ("separate_1_bdv", @{thm separate_1_bdv}), (*"?bdv / ?b = (1 / ?b) * ?bdv"*) - Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n}) + Thm ("separate_1_bdv_n", @{thm separate_1_bdv_n}) (*"?bdv \ ?n / ?b = 1 / ?b * ?bdv \ ?n"*) ]); (*show_types := true; --- do we need type-constraint in thms? *) @{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*) @{thm separate_bdv_n}; (*::real ..because of \ , rewrites*) @{thm separate_1_bdv}; (*::?'a*) -val xxx = ThmC.numerals_to_Free @{thm separate_1_bdv}; (*::?'a*) +val xxx = @{thm separate_1_bdv}; (*::?'a*) @{thm separate_1_bdv_n}; (*::real ..because of \ *) (*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*) @@ -2200,8 +2200,8 @@ val t = TermC.str2term "Length [x+y=1,y=2] = 2"; TermC.atomty t; val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty - [(Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL})), - (Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS})), + [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})), + (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})), Eval ("Groups.plus_class.plus", eval_binop "#add_"), Eval ("HOL.eq",eval_equal "#equal_") ]; @@ -2894,9 +2894,9 @@ "0 = (2 * c_2 + 2 * L * c + - 1 * L \ 2 * q_0) / 2, " ^ "0 = c_4, " ^ "0 = c_3]"); -val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false (ThmC.numerals_to_Free @{thm commute_0_equality}) t; -val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false (ThmC.numerals_to_Free @{thm commute_0_equality}) t; -val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false (ThmC.numerals_to_Free @{thm commute_0_equality}) t; +val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t; +val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t; +val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t; if UnparseC.term t = "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \ 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]" then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";