1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Mon Apr 13 13:27:55 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Mon Apr 13 15:31:23 2020 +0200
1.3 @@ -59,25 +59,25 @@
1.4 \<close> ML \<open>
1.5 val Atools_erls = Rule_Set.append_rules "Atools_erls" Rule_Set.empty
1.6 [ Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.7 - Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
1.8 + Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.9 (*"(~ True) = False"*)
1.10 - Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
1.11 + Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
1.12 (*"(~ False) = True"*)
1.13 - Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
1.14 + Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),
1.15 (*"(?a & True) = ?a"*)
1.16 - Rule.Thm ("and_false", TermC.num_str @{thm and_false}),
1.17 + Rule.Thm ("and_false", ThmC.numerals_to_Free @{thm and_false}),
1.18 (*"(?a & False) = False"*)
1.19 - Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
1.20 + Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
1.21 (*"(?a | True) = True"*)
1.22 - Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
1.23 + Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
1.24 (*"(?a | False) = ?a"*)
1.25
1.26 - Rule.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
1.27 - Rule.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
1.28 - Rule.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3}),
1.29 - Rule.Thm ("refl", TermC.num_str @{thm refl}),
1.30 - Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
1.31 - Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
1.32 + Rule.Thm ("rat_leq1", ThmC.numerals_to_Free @{thm rat_leq1}),
1.33 + Rule.Thm ("rat_leq2", ThmC.numerals_to_Free @{thm rat_leq2}),
1.34 + Rule.Thm ("rat_leq3", ThmC.numerals_to_Free @{thm rat_leq3}),
1.35 + Rule.Thm ("refl", ThmC.numerals_to_Free @{thm refl}),
1.36 + Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),
1.37 + Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
1.38
1.39 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.40 Rule.Num_Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
1.41 @@ -91,19 +91,19 @@
1.42 ML \<open>
1.43 val Atools_crls = Rule_Set.append_rules "Atools_crls" Rule_Set.empty
1.44 [ Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.45 - Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
1.46 - Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
1.47 - Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
1.48 - Rule.Thm ("and_false", TermC.num_str @{thm and_false}),
1.49 - Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
1.50 - Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
1.51 + Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.52 + Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
1.53 + Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),
1.54 + Rule.Thm ("and_false", ThmC.numerals_to_Free @{thm and_false}),
1.55 + Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
1.56 + Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
1.57
1.58 - Rule.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
1.59 - Rule.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
1.60 - Rule.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3}),
1.61 - Rule.Thm ("refl", TermC.num_str @{thm refl}),
1.62 - Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
1.63 - Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
1.64 + Rule.Thm ("rat_leq1", ThmC.numerals_to_Free @{thm rat_leq1}),
1.65 + Rule.Thm ("rat_leq2", ThmC.numerals_to_Free @{thm rat_leq2}),
1.66 + Rule.Thm ("rat_leq3", ThmC.numerals_to_Free @{thm rat_leq3}),
1.67 + Rule.Thm ("refl", ThmC.numerals_to_Free @{thm refl}),
1.68 + Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),
1.69 + Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
1.70
1.71 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.72 Rule.Num_Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
1.73 @@ -127,8 +127,8 @@
1.74
1.75 Rule.Num_Calc ("Prog_Expr.Vars",Prog_Expr.eval_var "#Vars_"),
1.76
1.77 - Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
1.78 - Rule.Thm ("if_False",TermC.num_str @{thm if_False})];
1.79 + Rule.Thm ("if_True",ThmC.numerals_to_Free @{thm if_True}),
1.80 + Rule.Thm ("if_False",ThmC.numerals_to_Free @{thm if_False})];
1.81
1.82 val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge "list_erls"
1.83 (Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),