1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Mon Jul 19 17:29:35 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Mon Jul 19 18:29:46 2021 +0200
1.3 @@ -90,9 +90,6 @@
1.4 val raise_type_conflicts: term list -> unit
1.5 val strip_trueprop: term -> term
1.6
1.7 - val numbers_to_string: term -> term
1.8 - val uminus_to_string: term -> term
1.9 -
1.10 val var2free: term -> term
1.11 val vars: term -> term list (* recognises numerals, should replace "fun vars_of" TODOO*)
1.12 val vars': term list -> term list
1.13 @@ -494,9 +491,6 @@
1.14 end;
1.15
1.16 (** transform binary numeralsstrings **)
1.17 -val numbers_to_string = ThmC_Def.num_to_Free
1.18 -val uminus_to_string = ThmC_Def.uminus_to_string
1.19 -
1.20 fun mk_Free (s,T) = Free (s, T);
1.21 fun mk_free T s = Free (s, T);
1.22
1.23 @@ -542,21 +536,21 @@
1.24 (* TODO clarify parse with Test_Isac *)
1.25 fun parseold thy str = (* before 2002 *)
1.26 \<^try>\<open>
1.27 - let val t = ((*typ_a2real o*) numbers_to_string) (Syntax.read_term_global thy str)
1.28 + let val t = Syntax.read_term_global thy str
1.29 in Thm.global_cterm_of thy t end\<close>;
1.30 fun parseN thy str = (* introduced 2002 *)
1.31 \<^try>\<open>
1.32 let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)
1.33 in Thm.global_cterm_of thy t end\<close>;
1.34
1.35 -fun parse_strict thy str = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
1.36 +fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str);
1.37 fun parse thy str = (* introduced 2010 *)
1.38 \<^try>\<open>
1.39 let val t = parse_strict thy str
1.40 in Thm.global_cterm_of thy t end\<close>;
1.41
1.42 (*WN110317 parseNEW will replace parse after introduction of ctxt completed*)
1.43 -fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str |> numbers_to_string\<close>;
1.44 +fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str\<close>;
1.45 fun parseNEW' ctxt str =
1.46 case parseNEW ctxt str of
1.47 SOME t => t
2.1 --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml Mon Jul 19 17:29:35 2021 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml Mon Jul 19 18:29:46 2021 +0200
2.3 @@ -16,9 +16,6 @@
2.4
2.5 (* required in ProgLang BEFORE definition in ---------------vvv *)
2.6 val int_opt_of_string: string -> int option (* belongs to TermC *)
2.7 - val numerals_to_Free: thm -> thm (* belongs to ThmC *)
2.8 - val num_to_Free: term -> term (* belongs to TermC *)
2.9 - val uminus_to_string: term -> term (* belongs to TermC *)
2.10 end
2.11
2.12 (**)
2.13 @@ -47,51 +44,4 @@
2.14 case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE
2.15 end;
2.16
2.17 -
2.18 -(** transform Isabelle's binary numerals to "Free (string, T)" **)
2.19 -
2.20 -val num_to_Free = (**)I(* Makarius 100308 *)
2.21 -(** )
2.22 - let
2.23 - fun dest_num t =
2.24 - (case try HOLogic.dest_number t of
2.25 - SOME (T, i) => SOME (Free (signed_string_of_int i, T))
2.26 - | NONE => NONE);
2.27 - fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)
2.28 - | to_str (t as (u1 $ u2)) =
2.29 - (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2)
2.30 - | to_str t = perhaps dest_num t;
2.31 - in to_str end
2.32 -( **)
2.33 -
2.34 -val uminus_to_string = (**)I
2.35 -(** )
2.36 - let
2.37 - fun dest_num t =
2.38 - case t of
2.39 - (Const (\<^const_name>\<open>uminus\<close>, _) $ Free (s, T)) =>
2.40 - (case int_opt_of_string s of
2.41 - SOME i => SOME (Free (signed_string_of_int (~1 * i), T))
2.42 - | NONE => NONE)
2.43 - | _ => NONE;
2.44 - fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)
2.45 - | to_str (t as (u1 $ u2)) =
2.46 - (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2)
2.47 - | to_str t = perhaps dest_num t;
2.48 - in to_str end;
2.49 -( **)
2.50 -
2.51 -fun numerals_to_Free thm = (**)thm
2.52 -(** )
2.53 - let
2.54 - val prop = Thm.plain_prop_of thm
2.55 - val prop' = num_to_Free prop;
2.56 - in
2.57 - if prop = prop' then thm
2.58 - else
2.59 - Skip_Proof.make_thm (Thm.theory_of_thm thm) prop'
2.60 - |> Thm.put_name_hint (Thm.get_name_hint thm)
2.61 - end;
2.62 -( **)
2.63 -
2.64 (**)end(**)
3.1 --- a/src/Tools/isac/Interpret/derive.sml Mon Jul 19 17:29:35 2021 +0200
3.2 +++ b/src/Tools/isac/Interpret/derive.sml Mon Jul 19 18:29:46 2021 +0200
3.3 @@ -84,7 +84,7 @@
3.4 (msg_3 t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
3.5 | Rule.Eval (c as (op_, _)) =>
3.6 (msg_4 op_;
3.7 - case Eval.adhoc_thm thy c (TermC.uminus_to_string t) of
3.8 + case Eval.adhoc_thm thy c t of
3.9 NONE => rew_once lim rts t apno rs'
3.10 | SOME (thmid, tm) =>
3.11 (let
4.1 --- a/src/Tools/isac/Knowledge/Diff.thy Mon Jul 19 17:29:35 2021 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Mon Jul 19 18:29:46 2021 +0200
4.3 @@ -156,8 +156,8 @@
4.4 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"),
4.5 Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),
4.6 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
4.7 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
4.8 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true})],
4.9 + Rule.Thm ("not_false", @{thm not_false}),
4.10 + Rule.Thm ("not_true", @{thm not_true})],
4.11 srls = Rule_Set.Empty, calc = [], errpatts = [],
4.12 rules = [\<^rule_thm>\<open>frac_sym_conv\<close>,
4.13 \<^rule_thm>\<open>sqrt_sym_conv\<close>,
5.1 --- a/src/Tools/isac/Knowledge/Poly.thy Mon Jul 19 17:29:35 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Mon Jul 19 18:29:46 2021 +0200
5.3 @@ -739,8 +739,8 @@
5.4 Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),
5.5 Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"),
5.6 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
5.7 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
5.8 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
5.9 + Rule.Thm ("not_false", @{thm not_false}),
5.10 + Rule.Thm ("not_true", @{thm not_true}),
5.11 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
5.12 ],
5.13 scr = Rule.Empty_Prog
5.14 @@ -753,7 +753,7 @@
5.15 rules =
5.16 [\<^rule_thm>\<open>real_diff_minus\<close>,
5.17 (*"a - b = a + -1 * b"*)
5.18 - Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym}))
5.19 + Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym}))
5.20 (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)],
5.21 scr = Rule.Empty_Prog};
5.22
5.23 @@ -790,9 +790,9 @@
5.24 \<^rule_thm>\<open>realpow_pow\<close>,
5.25 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
5.26 (**)
5.27 - Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}),
5.28 + Rule.Thm ("realpow_minus_even", @{thm realpow_minus_even}),
5.29 (*"n is_even ==> (- r) \<up> n = r \<up> n"*)
5.30 - Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd})
5.31 + Rule.Thm ("realpow_minus_odd", @{thm realpow_minus_odd})
5.32 (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)
5.33 (**)
5.34 ], scr = Rule.Empty_Prog};
5.35 @@ -803,8 +803,8 @@
5.36 erls = Rule_Set.append_rules "Rule_Set.empty-expand_poly_rat_" Rule_Set.empty
5.37 [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp ""),
5.38 Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"),
5.39 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
5.40 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true})
5.41 + Rule.Thm ("not_false", @{thm not_false}),
5.42 + Rule.Thm ("not_true", @{thm not_true})
5.43 ],
5.44 srls = Rule_Set.Empty,
5.45 calc = [], errpatts = [],
5.46 @@ -832,11 +832,11 @@
5.47 \<^rule_thm>\<open>realpow_multI_poly\<close>,
5.48 (*"[| r is_polyexp; s is_polyexp |] ==>
5.49 (r * s) \<up> n = r \<up> n * s \<up> n"*)
5.50 - Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}),
5.51 + Rule.Thm ("realpow_pow", @{thm realpow_pow}),
5.52 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
5.53 - Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}),
5.54 + Rule.Thm ("realpow_minus_even", @{thm realpow_minus_even}),
5.55 (*"n is_even ==> (- r) \<up> n = r \<up> n"*)
5.56 - Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd})
5.57 + Rule.Thm ("realpow_minus_odd", @{thm realpow_minus_odd})
5.58 (*"\<not> (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)
5.59 ], scr = Rule.Empty_Prog};
5.60
5.61 @@ -962,11 +962,11 @@
5.62 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
5.63 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
5.64 rules =
5.65 - [Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
5.66 + [Rule.Thm ("distrib_right" , @{thm distrib_right}),
5.67 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
5.68 \<^rule_thm>\<open>distrib_left\<close>,
5.69 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
5.70 - (*Rule.Thm ("distrib_right1",ThmC.numerals_to_Free @{thm distrib_right}1),
5.71 + (*Rule.Thm ("distrib_right1", @{thm distrib_right}1),
5.72 ....... 18.3.03 undefined???*)
5.73
5.74 \<^rule_thm>\<open>real_plus_binom_pow2\<close>,
5.75 @@ -982,7 +982,7 @@
5.76 (*"- (- ?z) = ?z"*)
5.77 \<^rule_thm>\<open>real_diff_minus\<close>,
5.78 (*"a - b = a + -1 * b"*)
5.79 - Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym}))
5.80 + Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym}))
5.81 (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)
5.82
5.83 (*\<^rule_thm>\<open>real_minus_add_distrib\<close>,*)
5.84 @@ -1043,7 +1043,7 @@
5.85 (*"1 * z = z"*)
5.86 (*\<^rule_thm>\<open>real_mult_minus1\<close>,14.3.03*)
5.87 (*"-1 * z = - z"*)
5.88 - Rule.Thm ("minus_mult_left", ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})),
5.89 + Rule.Thm ("minus_mult_left", (@{thm minus_mult_left} RS @{thm sym})),
5.90 (*- (?x * ?y) = "- ?x * ?y"*)
5.91 (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>,
5.92 (*"- ?x * - ?y = ?x * ?y"*)---*)
6.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Mon Jul 19 17:29:35 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Mon Jul 19 18:29:46 2021 +0200
6.3 @@ -337,12 +337,12 @@
6.4 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
6.5 Rule.Eval ("RootEq.is_rootTerm_in", eval_is_rootTerm_in ""),
6.6 Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in ""),
6.7 - Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
6.8 - Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
6.9 - Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
6.10 - Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
6.11 - Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),
6.12 - Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false})
6.13 + Rule.Thm ("not_true", @{thm not_true}),
6.14 + Rule.Thm ("not_false", @{thm not_false}),
6.15 + Rule.Thm ("and_true", @{thm and_true}),
6.16 + Rule.Thm ("and_false", @{thm and_false}),
6.17 + Rule.Thm ("or_true", @{thm or_true}),
6.18 + Rule.Thm ("or_false", @{thm or_false})
6.19 ];
6.20
6.21 val PolyEq_erls =
7.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Jul 19 17:29:35 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Jul 19 18:29:46 2021 +0200
7.3 @@ -410,8 +410,8 @@
7.4 [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"),
7.5 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
7.6 Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
7.7 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
7.8 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
7.9 + Rule.Thm ("not_true", @{thm not_true}),
7.10 + Rule.Thm ("not_false", @{thm not_false})],
7.11 scr = Rule.Empty_Prog});
7.12
7.13 (* simplifies expressions with numerals;
7.14 @@ -425,7 +425,7 @@
7.15 rules =
7.16 [\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
7.17
7.18 - Rule.Thm ("minus_divide_left", ThmC.numerals_to_Free (@{thm minus_divide_left} RS @{thm sym})),
7.19 + Rule.Thm ("minus_divide_left", (@{thm minus_divide_left} RS @{thm sym})),
7.20 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
7.21 \<^rule_thm>\<open>rat_add\<close>,
7.22 (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \
8.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Mon Jul 19 17:29:35 2021 +0200
8.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Mon Jul 19 18:29:46 2021 +0200
8.3 @@ -20,7 +20,7 @@
8.4 (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
8.5 \<^rule_thm>\<open>mult_1_left\<close>,
8.6 (* 1 * z = z *)
8.7 - Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym})),
8.8 + Rule.Thm ("real_mult_minus1_sym", (@{thm real_mult_minus1_sym})),
8.9 (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)
8.10 Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_")
8.11 ];
9.1 --- a/src/Tools/isac/Knowledge/Test.thy Mon Jul 19 17:29:35 2021 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Jul 19 18:29:46 2021 +0200
9.3 @@ -457,7 +457,7 @@
9.4 scr = Rule.Empty_Prog
9.5 };
9.6
9.7 -(*todo: replace by Rewrite("rnorm_equation_add",ThmC.numerals_to_Free @{thm rnorm_equation_add)*)
9.8 +(*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*)
9.9 val norm_equation =
9.10 Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
9.11 erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [],
10.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Mon Jul 19 17:29:35 2021 +0200
10.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Mon Jul 19 18:29:46 2021 +0200
10.3 @@ -167,8 +167,7 @@
10.4 rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
10.5 (* once again try the same rule, e.g. associativity against "()"*)
10.6 | Rule.Eval (cc as (op_, _)) =>
10.7 - let val _= trace_in1 i "try calc" op_;
10.8 - val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
10.9 + let val _ = trace_in1 i "try calc" op_;
10.10 in case Eval.adhoc_thm thy cc ct of
10.11 NONE => rew_once ruls asm ct apno thms
10.12 | SOME (_, thm') =>
10.13 @@ -181,8 +180,7 @@
10.14 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
10.15 end
10.16 | Rule.Cal1 (cc as (op_, _)) =>
10.17 - let val _= trace_in1 i "try cal1" op_;
10.18 - val ct = TermC.uminus_to_string ct
10.19 + let val _ = trace_in1 i "try cal1" op_;
10.20 in case Eval.adhoc_thm1_ thy cc ct of
10.21 NONE => (ct, asm)
10.22 | SOME (_, thm') =>
10.23 @@ -282,16 +280,14 @@
10.24
10.25 (* search ct for adjacent numerals and calculate them by operator isa_fn *)
10.26 fun calculate_ thy isa_fn ct =
10.27 - let val ct = TermC.uminus_to_string ct
10.28 - in case Eval.adhoc_thm thy isa_fn ct of
10.29 - NONE => NONE
10.30 - | SOME (thmID, thm) =>
10.31 - (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of
10.32 - SOME (rew, _) => rew
10.33 - | NONE => raise ERROR ""
10.34 - in SOME (rew, (thmID, thm)) end)
10.35 - handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite")
10.36 - end;
10.37 + case Eval.adhoc_thm thy isa_fn ct of
10.38 + NONE => NONE
10.39 + | SOME (thmID, thm) =>
10.40 + (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of
10.41 + SOME (rew, _) => rew
10.42 + | NONE => raise ERROR ""
10.43 + in SOME (rew, (thmID, thm)) end)
10.44 + handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite");
10.45
10.46 fun eval_prog_expr thy srls t =
10.47 let val rew = rewrite_set_ thy false srls t;
11.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Mon Jul 19 17:29:35 2021 +0200
11.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Mon Jul 19 18:29:46 2021 +0200
11.3 @@ -20,8 +20,6 @@
11.4 val from_rule : Rule.rule -> T
11.5 val member': id list -> Rule.rule -> bool
11.6
11.7 - val numerals_to_Free: thm -> thm
11.8 -
11.9 val is_sym: id -> bool
11.10 val thm_from_thy: theory -> ThmC_Def.id -> thm
11.11
11.12 @@ -67,11 +65,6 @@
11.13 handle ERROR _ => false
11.14
11.15
11.16 -(** convert Isabelle's numerals to ISAC's specific format, LEGACY **)
11.17 -
11.18 -val numerals_to_Free = ThmC_Def.numerals_to_Free; (* numeral \<rightarrow> Free ("int", T) *)
11.19 -
11.20 -
11.21 (** handle symmetric equalities, generated by deriving input terms **)
11.22
11.23 fun is_sym id =
11.24 @@ -91,11 +84,11 @@
11.25 "s" :: "y" :: "m" :: "_" :: "#" :: _ =>
11.26 raise ERROR ("thm_from_thy not impl.for " ^ thmid)
11.27 | "s" :: "y" :: "m" :: "_" :: id =>
11.28 - ((numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
11.29 + ((Global_Theory.get_thm thy) (implode id)) RS sym
11.30 | "#" :: _ =>
11.31 raise ERROR ("thm_from_thy not impl.for " ^ thmid)
11.32 | _ =>
11.33 - thmid |> Global_Theory.get_thm thy |> numerals_to_Free
11.34 + thmid |> Global_Theory.get_thm thy
11.35
11.36 fun dest_eq_concl thm =
11.37 (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) thm of
11.38 @@ -179,7 +172,7 @@
11.39 if dynamic then error ("Bad dynamic fact " ^ quote name ^ Position.here pos)
11.40 else Facts.the_single (name, pos) thms;
11.41 val (xname', thm') = if symmetric then (sym_prefix ^ xname, thm RS sym) else (xname, thm);
11.42 - in Rule.Thm (xname', numerals_to_Free thm') end;
11.43 + in Rule.Thm (xname', thm') end;
11.44
11.45 fun antiquotation binding sym =
11.46 ML_Antiquotation.value_embedded binding
12.1 --- a/src/Tools/isac/ProgLang/ListC.thy Mon Jul 19 17:29:35 2021 +0200
12.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Mon Jul 19 18:29:46 2021 +0200
12.3 @@ -133,49 +133,49 @@
12.4 val prog_expr =
12.5 Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
12.6 erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [],
12.7 - rules = [Rule_Def.Thm ("refl", ThmC_Def.numerals_to_Free @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
12.8 - Rule_Def.Thm ("o_apply", ThmC_Def.numerals_to_Free @{thm o_apply}),
12.9 + rules = [Rule_Def.Thm ("refl", @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
12.10 + Rule_Def.Thm ("o_apply", @{thm o_apply}),
12.11
12.12 - Rule_Def.Thm ("NTH_CONS",ThmC_Def.numerals_to_Free @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
12.13 - Rule_Def.Thm ("NTH_NIL",ThmC_Def.numerals_to_Free @{thm NTH_NIL}),
12.14 - Rule_Def.Thm ("append_Cons",ThmC_Def.numerals_to_Free @{thm append_Cons}),
12.15 - Rule_Def.Thm ("append_Nil",ThmC_Def.numerals_to_Free @{thm append_Nil}),
12.16 + Rule_Def.Thm ("NTH_CONS", @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
12.17 + Rule_Def.Thm ("NTH_NIL", @{thm NTH_NIL}),
12.18 + Rule_Def.Thm ("append_Cons", @{thm append_Cons}),
12.19 + Rule_Def.Thm ("append_Nil", @{thm append_Nil}),
12.20 (* Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
12.21 Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*)
12.22 - Rule_Def.Thm ("concat_Cons",ThmC_Def.numerals_to_Free @{thm concat_Cons}),
12.23 - Rule_Def.Thm ("concat_Nil",ThmC_Def.numerals_to_Free @{thm concat_Nil}),
12.24 + Rule_Def.Thm ("concat_Cons", @{thm concat_Cons}),
12.25 + Rule_Def.Thm ("concat_Nil", @{thm concat_Nil}),
12.26 (* Rule_Def.Thm ("del_base",num_str @{thm del_base}),
12.27 Rule_Def.Thm ("del_rec",num_str @{thm del_rec}), *)
12.28
12.29 - Rule_Def.Thm ("distinct_Cons",ThmC_Def.numerals_to_Free @{thm distinct_Cons}),
12.30 - Rule_Def.Thm ("distinct_Nil",ThmC_Def.numerals_to_Free @{thm distinct_Nil}),
12.31 - Rule_Def.Thm ("dropWhile_Cons",ThmC_Def.numerals_to_Free @{thm dropWhile_Cons}),
12.32 - Rule_Def.Thm ("dropWhile_Nil",ThmC_Def.numerals_to_Free @{thm dropWhile_Nil}),
12.33 - Rule_Def.Thm ("filter_Cons",ThmC_Def.numerals_to_Free @{thm filter_Cons}),
12.34 - Rule_Def.Thm ("filter_Nil",ThmC_Def.numerals_to_Free @{thm filter_Nil}),
12.35 - Rule_Def.Thm ("foldr_Cons",ThmC_Def.numerals_to_Free @{thm foldr_Cons}),
12.36 - Rule_Def.Thm ("foldr_Nil",ThmC_Def.numerals_to_Free @{thm foldr_Nil}),
12.37 - Rule_Def.Thm ("hd_thm",ThmC_Def.numerals_to_Free @{thm hd_thm}),
12.38 - Rule_Def.Thm ("LAST",ThmC_Def.numerals_to_Free @{thm LAST}),
12.39 - Rule_Def.Thm ("LENGTH_CONS",ThmC_Def.numerals_to_Free @{thm LENGTH_CONS}),
12.40 - Rule_Def.Thm ("LENGTH_NIL",ThmC_Def.numerals_to_Free @{thm LENGTH_NIL}),
12.41 + Rule_Def.Thm ("distinct_Cons", @{thm distinct_Cons}),
12.42 + Rule_Def.Thm ("distinct_Nil", @{thm distinct_Nil}),
12.43 + Rule_Def.Thm ("dropWhile_Cons", @{thm dropWhile_Cons}),
12.44 + Rule_Def.Thm ("dropWhile_Nil", @{thm dropWhile_Nil}),
12.45 + Rule_Def.Thm ("filter_Cons", @{thm filter_Cons}),
12.46 + Rule_Def.Thm ("filter_Nil", @{thm filter_Nil}),
12.47 + Rule_Def.Thm ("foldr_Cons", @{thm foldr_Cons}),
12.48 + Rule_Def.Thm ("foldr_Nil", @{thm foldr_Nil}),
12.49 + Rule_Def.Thm ("hd_thm", @{thm hd_thm}),
12.50 + Rule_Def.Thm ("LAST", @{thm LAST}),
12.51 + Rule_Def.Thm ("LENGTH_CONS", @{thm LENGTH_CONS}),
12.52 + Rule_Def.Thm ("LENGTH_NIL", @{thm LENGTH_NIL}),
12.53 (* Rule_Def.Thm ("list_diff_def",num_str @{thm list_diff_def}),*)
12.54 - Rule_Def.Thm ("map_Cons",ThmC_Def.numerals_to_Free @{thm map_Cons}),
12.55 - Rule_Def.Thm ("map_Nil",ThmC_Def.numerals_to_Free @{thm map_Cons}),
12.56 -(* Rule_Def.Thm ("mem_Cons",ThmC_Def.numerals_to_Free @{thm mem_Cons}),
12.57 - Rule_Def.Thm ("mem_Nil",ThmC_Def.numerals_to_Free @{thm mem_Nil}), *)
12.58 -(* Rule_Def.Thm ("null_Cons",ThmC_Def.numerals_to_Free @{thm null_Cons}),
12.59 - Rule_Def.Thm ("null_Nil",ThmC_Def.numerals_to_Free @{thm null_Nil}),*)
12.60 - Rule_Def.Thm ("remdups_Cons",ThmC_Def.numerals_to_Free @{thm remdups_Cons}),
12.61 - Rule_Def.Thm ("remdups_Nil",ThmC_Def.numerals_to_Free @{thm remdups_Nil}),
12.62 - Rule_Def.Thm ("rev_Cons",ThmC_Def.numerals_to_Free @{thm rev_Cons}),
12.63 - Rule_Def.Thm ("rev_Nil",ThmC_Def.numerals_to_Free @{thm rev_Nil}),
12.64 - Rule_Def.Thm ("take_Nil",ThmC_Def.numerals_to_Free @{thm take_Nil}),
12.65 - Rule_Def.Thm ("take_Cons",ThmC_Def.numerals_to_Free @{thm take_Cons}),
12.66 - Rule_Def.Thm ("tl_Cons",ThmC_Def.numerals_to_Free @{thm tl_Cons}),
12.67 - Rule_Def.Thm ("tl_Nil",ThmC_Def.numerals_to_Free @{thm tl_Nil}),
12.68 - Rule_Def.Thm ("zip_Cons",ThmC_Def.numerals_to_Free @{thm zip_Cons}),
12.69 - Rule_Def.Thm ("zip_Nil",ThmC_Def.numerals_to_Free @{thm zip_Nil})],
12.70 + Rule_Def.Thm ("map_Cons", @{thm map_Cons}),
12.71 + Rule_Def.Thm ("map_Nil", @{thm map_Cons}),
12.72 +(* Rule_Def.Thm ("mem_Cons", @{thm mem_Cons}),
12.73 + Rule_Def.Thm ("mem_Nil", @{thm mem_Nil}), *)
12.74 +(* Rule_Def.Thm ("null_Cons", @{thm null_Cons}),
12.75 + Rule_Def.Thm ("null_Nil", @{thm null_Nil}),*)
12.76 + Rule_Def.Thm ("remdups_Cons", @{thm remdups_Cons}),
12.77 + Rule_Def.Thm ("remdups_Nil", @{thm remdups_Nil}),
12.78 + Rule_Def.Thm ("rev_Cons", @{thm rev_Cons}),
12.79 + Rule_Def.Thm ("rev_Nil", @{thm rev_Nil}),
12.80 + Rule_Def.Thm ("take_Nil", @{thm take_Nil}),
12.81 + Rule_Def.Thm ("take_Cons", @{thm take_Cons}),
12.82 + Rule_Def.Thm ("tl_Cons", @{thm tl_Cons}),
12.83 + Rule_Def.Thm ("tl_Nil", @{thm tl_Nil}),
12.84 + Rule_Def.Thm ("zip_Cons", @{thm zip_Cons}),
12.85 + Rule_Def.Thm ("zip_Nil", @{thm zip_Nil})],
12.86 scr = Rule_Def.Empty_Prog}: Rule_Set.T;
12.87 \<close>
12.88 rule_set_knowledge prog_expr = prog_expr
13.1 --- a/src/Tools/isac/ProgLang/Program.thy Mon Jul 19 17:29:35 2021 +0200
13.2 +++ b/src/Tools/isac/ProgLang/Program.thy Mon Jul 19 18:29:46 2021 +0200
13.3 @@ -67,8 +67,7 @@
13.4 |> Thm.prop_of
13.5 |> HOLogic.dest_Trueprop
13.6 |> Logic.unvarify_global
13.7 - |> TermC.inst_abs
13.8 - |> ThmC_Def.num_to_Free (*for numbers in the program*))
13.9 + |> TermC.inst_abs)
13.10 handle TERM _ => raise TERM ("prep_program", [Thm.prop_of thm])
13.11
13.12 (* get identifier of partial_function *)
14.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Mon Jul 19 17:29:35 2021 +0200
14.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Mon Jul 19 18:29:46 2021 +0200
14.3 @@ -14,7 +14,6 @@
14.4 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------------------";
14.5 "----------- fun TermC.vars_of -----------------------------------------------------------------";
14.6 "----------- fun TermC.vars --------------------------------------------------------------------";
14.7 -"----------- uminus_to_string ---------------------------";
14.8 "----------- *** Problem.prep_input: syntax error in '#Where' of [v";
14.9 "----------- check writeln, tracing for string markup ---";
14.10 "----------- build fun TermC.is_bdv_subst ------------------------------------------------------------";
14.11 @@ -30,7 +29,6 @@
14.12 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";
14.13 "----------- fun TermC.is_list -----------------------------------------------------------------------";
14.14 "----------- fun inst_abs ----------------------------------------------------------------------";
14.15 -"----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
14.16 "--------------------------------------------------------";
14.17 "--------------------------------------------------------";
14.18
14.19 @@ -184,17 +182,17 @@
14.20 "----------- inst_bdv -----------------------------------";
14.21 "----------- inst_bdv -----------------------------------";
14.22 "----------- inst_bdv -----------------------------------";
14.23 - if (UnparseC.term o Thm.prop_of o ThmC.numerals_to_Free) @{thm d1_isolate_add2} =
14.24 + if (UnparseC.term o Thm.prop_of) @{thm d1_isolate_add2} =
14.25 "\<not> ?bdv occurs_in ?a \<Longrightarrow>\n(?a + ?bdv = 0) = (?bdv = - 1 * ?a)"
14.26 then ()
14.27 else error "termC.sml d1_isolate_add2";
14.28 val subst = [(TermC.str2term "bdv", TermC.str2term "x")];
14.29 - val t = (Eval.norm o Thm.prop_of) (ThmC.numerals_to_Free @{thm d1_isolate_add2});
14.30 + val t = (Eval.norm o Thm.prop_of) @{thm d1_isolate_add2};
14.31 val t' = TermC.inst_bdv subst t;
14.32 if UnparseC.term t' = "\<not> x occurs_in ?a \<Longrightarrow> (?a + x = 0) = (x = - 1 * ?a)"
14.33 then ()
14.34 else error "termC.sml inst_bdv 1";
14.35 -if (UnparseC.term o Thm.prop_of o ThmC.numerals_to_Free) @{thm separate_bdvs_add} =
14.36 +if (UnparseC.term o Thm.prop_of) @{thm separate_bdvs_add} =
14.37 "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0,\n " ^
14.38 "?bdv_4.0] occur_exactly_in ?a \<Longrightarrow>\n(?a + ?b = ?c) = (?b = ?c + - (1::?'a) * ?a)"
14.39 then () else error "termC.sml separate_bdvs_add";
14.40 @@ -205,7 +203,7 @@
14.41 (TermC.str2term "bdv_2", TermC.str2term "c_2"),
14.42 (TermC.str2term "bdv_3", TermC.str2term "c_3"),
14.43 (TermC.str2term "bdv_4", TermC.str2term "c_4")];
14.44 -val t = (Eval.norm o Thm.prop_of) (ThmC.numerals_to_Free @{thm separate_bdvs_add});
14.45 +val t = (Eval.norm o Thm.prop_of) @{thm separate_bdvs_add};
14.46 val t' = TermC.inst_bdv subst t;
14.47
14.48 if UnparseC.term t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a \<Longrightarrow>\n" ^
14.49 @@ -360,9 +358,8 @@
14.50 TermC.parse thy str;
14.51 "---------------";
14.52 val str = "x + 2*z";
14.53 - val t = (Syntax.read_term_global thy str);
14.54 - val t = ThmC_Def.num_to_Free (Syntax.read_term_global thy str);
14.55 - val t = (TermC.typ_a2real o ThmC_Def.num_to_Free) (Syntax.read_term_global thy str);
14.56 + val t = Syntax.read_term_global thy str;
14.57 + val t = TermC.typ_a2real (Syntax.read_term_global thy str);
14.58 Thm.global_cterm_of thy t;
14.59 case TermC.parse thy str of
14.60 SOME t' => t'
14.61 @@ -417,23 +414,13 @@
14.62 | _ => error "TermC.vars_of (3 = 3 * AA / 4) ..changed (! use only for polynomials, not equations!)";
14.63
14.64
14.65 -"----------- uminus_to_string ---------------------------";
14.66 -"----------- uminus_to_string ---------------------------";
14.67 -"----------- uminus_to_string ---------------------------";
14.68 - val t1 = ThmC_Def.num_to_Free @{term "-2::real"};
14.69 - val t2 = ThmC_Def.num_to_Free @{term "- 2::real"};
14.70 - if TermC.uminus_to_string t2 = t1
14.71 - then ()
14.72 - else error "termC.sml diff.behav. in uminus_to_string";
14.73 -
14.74 "----------- *** Problem.prep_input: syntax error in '#Where' of [v";
14.75 "----------- *** Problem.prep_input: syntax error in '#Where' of [v";
14.76 "----------- *** Problem.prep_input: syntax error in '#Where' of [v";
14.77 "===== deconstruct datatype typ ===";
14.78 val str = "?a";
14.79 val t = (thy, str) |>> ThyC.to_ctxt
14.80 - |-> Proof_Context.read_term_pattern
14.81 - |> ThmC_Def.num_to_Free;
14.82 + |-> Proof_Context.read_term_pattern;
14.83 val Var (("a", 0), ty) = t;
14.84 val TVar ((str, i), srt) = ty;
14.85 if str = "'a" andalso i = 1 andalso srt = []
14.86 @@ -443,8 +430,7 @@
14.87 "----- real type in pattern ---";
14.88 val str = "?a :: real";
14.89 val t = (thy, str) |>> ThyC.to_ctxt
14.90 - |-> Proof_Context.read_term_pattern
14.91 - |> ThmC_Def.num_to_Free;
14.92 + |-> Proof_Context.read_term_pattern;
14.93 val Var (("a", 0), ty) = t;
14.94 val Type (str, tys) = ty;
14.95 if str = \<^type_name>\<open>real\<close> andalso tys = [] andalso ty = HOLogic.realT
14.96 @@ -460,8 +446,7 @@
14.97 val ctxt = Config.put show_types true ctxt;
14.98 "----- read_term_pattern ---";
14.99 val t = (thy, str) |>> ThyC.to_ctxt
14.100 - |-> Proof_Context.read_term_pattern
14.101 - |> ThmC_Def.num_to_Free;
14.102 + |-> Proof_Context.read_term_pattern;
14.103 val t_real = TermC.typ_a2real t;
14.104 if UnparseC.term_in_ctxt ctxt t_real =
14.105 "\<not> (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) \<or>\n "
14.106 @@ -646,7 +631,7 @@
14.107 val SOME t' = TermC.strip_imp_prems' t;
14.108 if UnparseC.term t' = "(\<Longrightarrow>) (?k \<noteq> 0)" then () else error "TermC.strip_imp_prems' changed";
14.109
14.110 -val thm = ThmC.numerals_to_Free @{thm frac_sym_conv};
14.111 +val thm = @{thm frac_sym_conv};
14.112 val prop = Thm.prop_of thm;
14.113 val concl = Logic.strip_imp_concl prop;
14.114 val SOME prems = TermC.strip_imp_prems' prop;
14.115 @@ -685,24 +670,6 @@
14.116 val ty = (Term.type_of o Thm.term_of) ct;
14.117 if TermC.is_list t = true then () else error "TermC.is_list [a, b, c]";
14.118
14.119 -"----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
14.120 -"----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
14.121 -"----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
14.122 -case ThmC_Def.num_to_Free @{term "123::real"} of
14.123 - Const (\<^const_name>\<open>numeral\<close>, _) $
14.124 - (Const (\<^const_name>\<open>num.Bit1\<close>, _) $
14.125 - (Const (\<^const_name>\<open>num.Bit1\<close>, _) $
14.126 - (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))))))) => ()
14.127 -| _ => error "ThmC_Def.num_to_Free '123' changed";
14.128 -
14.129 -case ThmC_Def.num_to_Free @{term "1::real"} of
14.130 - Const (\<^const_name>\<open>one_class.one\<close>, _) => ()
14.131 -| _ => error "ThmC_Def.num_to_Free '1' changed";
14.132 -
14.133 -case ThmC_Def.num_to_Free @{term "0::real"} of
14.134 - Const (\<^const_name>\<open>zero_class.zero\<close>, _) => ()
14.135 -| _ => error "ThmC_Def.num_to_Free '0' changed";
14.136 -
14.137 "----------- fun mk_frac, proper term with uminus ----------------------------------------------";
14.138 "----------- fun mk_frac, proper term with uminus ----------------------------------------------";
14.139 "----------- fun mk_frac, proper term with uminus ----------------------------------------------";
15.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-present.sml Mon Jul 19 17:29:35 2021 +0200
15.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-present.sml Mon Jul 19 18:29:46 2021 +0200
15.3 @@ -126,7 +126,7 @@
15.4 "----------- fun is_contained_in ------------------------";
15.5 "----------- fun is_contained_in ------------------------";
15.6 "----------- fun is_contained_in ------------------------";
15.7 -val r1 = Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus});
15.8 +val r1 = Thm ("real_diff_minus", @{thm real_diff_minus});
15.9 if Rule_Set.contains r1 Test_simplify then ()
15.10 else error "rewtools.sml Rule_Set.contains Thm";
15.11
16.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon Jul 19 17:29:35 2021 +0200
16.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon Jul 19 18:29:46 2021 +0200
16.3 @@ -710,7 +710,7 @@
16.4 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
16.5 setNextTactic 1 (Apply_Method ["PolyEq", "normalise_poly"]);
16.6 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
16.7 - setNextTactic 1 (Rewrite ("all_left", ThmC.numerals_to_Free @{thm all_left}));
16.8 + setNextTactic 1 (Rewrite ("all_left", @{thm all_left}));
16.9 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
16.10 setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "make_ratpoly_in"));
16.11 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
17.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Mon Jul 19 17:29:35 2021 +0200
17.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Mon Jul 19 18:29:46 2021 +0200
17.3 @@ -34,7 +34,7 @@
17.4 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";
17.5
17.6 val SOME (t,_) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst
17.7 - (ThmC.numerals_to_Free @{thm "int_isolate_add"}) t; UnparseC.term t;
17.8 + @{thm "int_isolate_add"} t; UnparseC.term t;
17.9
17.10 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
17.11 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; UnparseC.term t;
18.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Mon Jul 19 17:29:35 2021 +0200
18.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Mon Jul 19 18:29:46 2021 +0200
18.3 @@ -706,9 +706,9 @@
18.4 (*"(?a | True) = True"*)
18.5 Thm ("or_false",@{thm or_false}),
18.6 (*"(?a | False) = ?a"*)
18.7 - Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
18.8 + Thm ("not_true", @{thm not_true}),
18.9 (*"(~ True) = False"*)
18.10 - Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
18.11 + Thm ("not_false", @{thm not_false})
18.12 (*"(~ False) = True"*)];
18.13 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
18.14 val SOME (t', _) = rewrite_set_ thy false prls t;
19.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Mon Jul 19 17:29:35 2021 +0200
19.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Mon Jul 19 18:29:46 2021 +0200
19.3 @@ -474,7 +474,7 @@
19.4 "----------- 2011 thms with axclasses ----------------------------------------------------------";
19.5 "----------- 2011 thms with axclasses ----------------------------------------------------------";
19.6 "----------- 2011 thms with axclasses ----------------------------------------------------------";
19.7 -val thm = ThmC.numerals_to_Free @{thm div_by_1};
19.8 +val thm = @{thm div_by_1};
19.9 val prop = Thm.prop_of thm;
19.10 TermC.atomty prop; (*Type 'a*)
19.11 val t = TermC.str2term "(2*x)/1"; (*Type real*)
20.1 --- a/test/Tools/isac/MathEngBasic/thmC.sml Mon Jul 19 17:29:35 2021 +0200
20.2 +++ b/test/Tools/isac/MathEngBasic/thmC.sml Mon Jul 19 18:29:46 2021 +0200
20.3 @@ -63,7 +63,7 @@
20.4 then () else error "fun revert_sym_rule changed 1";
20.5
20.6 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
20.7 - (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))
20.8 + (Thm ("real_diff_minus", @{thm real_diff_minus}))
20.9 ;
20.10 if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + - 1 * ?b"
20.11 then () else error "fun revert_sym_rule changed 2"
21.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Mon Jul 19 17:29:35 2021 +0200
21.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Mon Jul 19 18:29:46 2021 +0200
21.3 @@ -241,7 +241,7 @@
21.4 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
21.5 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
21.6 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
21.7 -val t = rule2stac @{theory} (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}));
21.8 +val t = rule2stac @{theory} (Thm ("real_diff_minus", @{thm real_diff_minus}));
21.9 if UnparseC.term t = "Try (Repeat (Rewrite ''real_diff_minus''))" then ()
21.10 else error "rule2stac Thm.. changed";
21.11
21.12 @@ -253,7 +253,7 @@
21.13 if UnparseC.term t = "Try (Rewrite_Set ''rearrange_assoc'')" then ()
21.14 else error "rule2stac Rls_.. changed";
21.15
21.16 -val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", ThmC.numerals_to_Free @{thm risolate_bdv_add}));
21.17 +val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", @{thm risolate_bdv_add}));
21.18 if UnparseC.term t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then ()
21.19 else error "rule2stac_inst Thm.. changed";
21.20 case t of
22.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Mon Jul 19 17:29:35 2021 +0200
22.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Mon Jul 19 18:29:46 2021 +0200
22.3 @@ -117,7 +117,7 @@
22.4 *)
22.5 val thy = @{theory "Test"};
22.6 val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
22.7 - val ct = ThmC_Def.num_to_Free @{term
22.8 + val ct = @{term
22.9 "sqrt (x \<up> 2 + -3 * x) = (-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))"};
22.10 case calculate_ thy op_ ct of
22.11 SOME _ => ()
23.1 --- a/test/Tools/isac/ProgLang/listC.sml Mon Jul 19 17:29:35 2021 +0200
23.2 +++ b/test/Tools/isac/ProgLang/listC.sml Mon Jul 19 18:29:46 2021 +0200
23.3 @@ -48,9 +48,9 @@
23.4
23.5 val t = TermC.str2term "NTH 1 [a,b,c,d,e]";
23.6 TermC.atomty t;
23.7 -val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_NIL};
23.8 +val thm = Thm.prop_of @{thm NTH_NIL};
23.9 TermC.atomty thm;
23.10 -val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_NIL}) t;
23.11 +val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false @{thm NTH_NIL} t;
23.12 if UnparseC.term t' = "a" then ()
23.13 else error "NTH 1 [a,b,c,d,e] = a ..changed";
23.14
23.15 @@ -63,9 +63,9 @@
23.16 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("d", _) $
23.17 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("e", _) $ Const (\<^const_name>\<open>Nil\<close>, _)))))) => ()
23.18 | _ => error "ListC.NTH changed";
23.19 -val thm = (Thm.prop_of o ThmC.numerals_to_Free) @{thm NTH_CONS};
23.20 +val thm = Thm.prop_of @{thm NTH_CONS};
23.21 TermC.atomty thm;
23.22 -val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false (ThmC.numerals_to_Free @{thm NTH_CONS}) t;
23.23 +val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false @{thm NTH_CONS} t;
23.24 if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then ()
23.25 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
23.26
24.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Jul 19 17:29:35 2021 +0200
24.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Jul 19 18:29:46 2021 +0200
24.3 @@ -329,9 +329,7 @@
24.4 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
24.5 ML \<open>
24.6 \<close> ML \<open>
24.7 -@{term Let}
24.8 \<close> ML \<open>
24.9 -val Const (\<^const_name>\<open>Let\<close>, _) = @{term Let}
24.10 \<close> ML \<open>
24.11 \<close> ML \<open>
24.12 \<close> ML \<open>
25.1 --- a/test/Tools/isac/Test_Some.thy Mon Jul 19 17:29:35 2021 +0200
25.2 +++ b/test/Tools/isac/Test_Some.thy Mon Jul 19 18:29:46 2021 +0200
25.3 @@ -1631,8 +1631,8 @@
25.4 rules = [(*for rewriting conditions in Thm's*)
25.5 Eval ("Prog_Expr.occurs_in",
25.6 eval_occurs_in "#occurs_in_"),
25.7 - Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
25.8 - Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})],
25.9 + Thm ("not_true", @{thm not_true}),
25.10 + Thm ("not_false", @{thm not_false})],
25.11 scr = Empty_Prog};
25.12 val subs = [(str2t "bdv::real", str2t "x::real")];
25.13 \<close> ML \<open>
25.14 @@ -1803,20 +1803,20 @@
25.15 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
25.16 val rls =
25.17 (Rule_Set.append_rules "separate_bdv" collect_bdv
25.18 - [Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
25.19 + [Thm ("separate_bdv", @{thm separate_bdv}),
25.20 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
25.21 - Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
25.22 + Thm ("separate_bdv_n", @{thm separate_bdv_n}),
25.23 (*"?a * ?bdv \<up> ?n / ?b = ?a / ?b * ?bdv \<up> ?n"*)
25.24 - Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
25.25 + Thm ("separate_1_bdv", @{thm separate_1_bdv}),
25.26 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
25.27 - Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})
25.28 + Thm ("separate_1_bdv_n", @{thm separate_1_bdv_n})
25.29 (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
25.30 ]);
25.31 (*show_types := true; --- do we need type-constraint in thms? *)
25.32 @{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
25.33 @{thm separate_bdv_n}; (*::real ..because of \<up> , rewrites*)
25.34 @{thm separate_1_bdv}; (*::?'a*)
25.35 -val xxx = ThmC.numerals_to_Free @{thm separate_1_bdv}; (*::?'a*)
25.36 +val xxx = @{thm separate_1_bdv}; (*::?'a*)
25.37 @{thm separate_1_bdv_n}; (*::real ..because of \<up> *)
25.38 (*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
25.39
25.40 @@ -2200,8 +2200,8 @@
25.41 val t = TermC.str2term "Length [x+y=1,y=2] = 2";
25.42 TermC.atomty t;
25.43 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty
25.44 - [(Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL})),
25.45 - (Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS})),
25.46 + [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
25.47 + (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
25.48 Eval ("Groups.plus_class.plus", eval_binop "#add_"),
25.49 Eval ("HOL.eq",eval_equal "#equal_")
25.50 ];
25.51 @@ -2894,9 +2894,9 @@
25.52 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
25.53 "0 = c_4, " ^
25.54 "0 = c_3]");
25.55 -val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false (ThmC.numerals_to_Free @{thm commute_0_equality}) t;
25.56 -val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false (ThmC.numerals_to_Free @{thm commute_0_equality}) t;
25.57 -val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false (ThmC.numerals_to_Free @{thm commute_0_equality}) t;
25.58 +val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
25.59 +val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
25.60 +val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
25.61 if UnparseC.term t =
25.62 "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]"
25.63 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";