1.1 --- a/src/Tools/isac/ProgLang/ListC.thy Mon Apr 13 13:27:55 2020 +0200
1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Mon Apr 13 15:31:23 2020 +0200
1.3 @@ -133,49 +133,49 @@
1.4 val prog_expr =
1.5 Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.6 erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [],
1.7 - rules = [Rule_Def.Thm ("refl", TermC.num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
1.8 - Rule_Def.Thm ("o_apply", TermC.num_str @{thm o_apply}),
1.9 + rules = [Rule_Def.Thm ("refl", ThmC_Def.numerals_to_Free @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
1.10 + Rule_Def.Thm ("o_apply", ThmC_Def.numerals_to_Free @{thm o_apply}),
1.11
1.12 - Rule_Def.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
1.13 - Rule_Def.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.14 - Rule_Def.Thm ("append_Cons",TermC.num_str @{thm append_Cons}),
1.15 - Rule_Def.Thm ("append_Nil",TermC.num_str @{thm append_Nil}),
1.16 + Rule_Def.Thm ("NTH_CONS",ThmC_Def.numerals_to_Free @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
1.17 + Rule_Def.Thm ("NTH_NIL",ThmC_Def.numerals_to_Free @{thm NTH_NIL}),
1.18 + Rule_Def.Thm ("append_Cons",ThmC_Def.numerals_to_Free @{thm append_Cons}),
1.19 + Rule_Def.Thm ("append_Nil",ThmC_Def.numerals_to_Free @{thm append_Nil}),
1.20 (* Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
1.21 Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*)
1.22 - Rule_Def.Thm ("concat_Cons",TermC.num_str @{thm concat_Cons}),
1.23 - Rule_Def.Thm ("concat_Nil",TermC.num_str @{thm concat_Nil}),
1.24 + Rule_Def.Thm ("concat_Cons",ThmC_Def.numerals_to_Free @{thm concat_Cons}),
1.25 + Rule_Def.Thm ("concat_Nil",ThmC_Def.numerals_to_Free @{thm concat_Nil}),
1.26 (* Rule_Def.Thm ("del_base",num_str @{thm del_base}),
1.27 Rule_Def.Thm ("del_rec",num_str @{thm del_rec}), *)
1.28
1.29 - Rule_Def.Thm ("distinct_Cons",TermC.num_str @{thm distinct_Cons}),
1.30 - Rule_Def.Thm ("distinct_Nil",TermC.num_str @{thm distinct_Nil}),
1.31 - Rule_Def.Thm ("dropWhile_Cons",TermC.num_str @{thm dropWhile_Cons}),
1.32 - Rule_Def.Thm ("dropWhile_Nil",TermC.num_str @{thm dropWhile_Nil}),
1.33 - Rule_Def.Thm ("filter_Cons",TermC.num_str @{thm filter_Cons}),
1.34 - Rule_Def.Thm ("filter_Nil",TermC.num_str @{thm filter_Nil}),
1.35 - Rule_Def.Thm ("foldr_Cons",TermC.num_str @{thm foldr_Cons}),
1.36 - Rule_Def.Thm ("foldr_Nil",TermC.num_str @{thm foldr_Nil}),
1.37 - Rule_Def.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.38 - Rule_Def.Thm ("LAST",TermC.num_str @{thm LAST}),
1.39 - Rule_Def.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.40 - Rule_Def.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.41 + Rule_Def.Thm ("distinct_Cons",ThmC_Def.numerals_to_Free @{thm distinct_Cons}),
1.42 + Rule_Def.Thm ("distinct_Nil",ThmC_Def.numerals_to_Free @{thm distinct_Nil}),
1.43 + Rule_Def.Thm ("dropWhile_Cons",ThmC_Def.numerals_to_Free @{thm dropWhile_Cons}),
1.44 + Rule_Def.Thm ("dropWhile_Nil",ThmC_Def.numerals_to_Free @{thm dropWhile_Nil}),
1.45 + Rule_Def.Thm ("filter_Cons",ThmC_Def.numerals_to_Free @{thm filter_Cons}),
1.46 + Rule_Def.Thm ("filter_Nil",ThmC_Def.numerals_to_Free @{thm filter_Nil}),
1.47 + Rule_Def.Thm ("foldr_Cons",ThmC_Def.numerals_to_Free @{thm foldr_Cons}),
1.48 + Rule_Def.Thm ("foldr_Nil",ThmC_Def.numerals_to_Free @{thm foldr_Nil}),
1.49 + Rule_Def.Thm ("hd_thm",ThmC_Def.numerals_to_Free @{thm hd_thm}),
1.50 + Rule_Def.Thm ("LAST",ThmC_Def.numerals_to_Free @{thm LAST}),
1.51 + Rule_Def.Thm ("LENGTH_CONS",ThmC_Def.numerals_to_Free @{thm LENGTH_CONS}),
1.52 + Rule_Def.Thm ("LENGTH_NIL",ThmC_Def.numerals_to_Free @{thm LENGTH_NIL}),
1.53 (* Rule_Def.Thm ("list_diff_def",num_str @{thm list_diff_def}),*)
1.54 - Rule_Def.Thm ("map_Cons",TermC.num_str @{thm map_Cons}),
1.55 - Rule_Def.Thm ("map_Nil",TermC.num_str @{thm map_Cons}),
1.56 -(* Rule_Def.Thm ("mem_Cons",TermC.num_str @{thm mem_Cons}),
1.57 - Rule_Def.Thm ("mem_Nil",TermC.num_str @{thm mem_Nil}), *)
1.58 -(* Rule_Def.Thm ("null_Cons",TermC.num_str @{thm null_Cons}),
1.59 - Rule_Def.Thm ("null_Nil",TermC.num_str @{thm null_Nil}),*)
1.60 - Rule_Def.Thm ("remdups_Cons",TermC.num_str @{thm remdups_Cons}),
1.61 - Rule_Def.Thm ("remdups_Nil",TermC.num_str @{thm remdups_Nil}),
1.62 - Rule_Def.Thm ("rev_Cons",TermC.num_str @{thm rev_Cons}),
1.63 - Rule_Def.Thm ("rev_Nil",TermC.num_str @{thm rev_Nil}),
1.64 - Rule_Def.Thm ("take_Nil",TermC.num_str @{thm take_Nil}),
1.65 - Rule_Def.Thm ("take_Cons",TermC.num_str @{thm take_Cons}),
1.66 - Rule_Def.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.67 - Rule_Def.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
1.68 - Rule_Def.Thm ("zip_Cons",TermC.num_str @{thm zip_Cons}),
1.69 - Rule_Def.Thm ("zip_Nil",TermC.num_str @{thm zip_Nil})],
1.70 + Rule_Def.Thm ("map_Cons",ThmC_Def.numerals_to_Free @{thm map_Cons}),
1.71 + Rule_Def.Thm ("map_Nil",ThmC_Def.numerals_to_Free @{thm map_Cons}),
1.72 +(* Rule_Def.Thm ("mem_Cons",ThmC_Def.numerals_to_Free @{thm mem_Cons}),
1.73 + Rule_Def.Thm ("mem_Nil",ThmC_Def.numerals_to_Free @{thm mem_Nil}), *)
1.74 +(* Rule_Def.Thm ("null_Cons",ThmC_Def.numerals_to_Free @{thm null_Cons}),
1.75 + Rule_Def.Thm ("null_Nil",ThmC_Def.numerals_to_Free @{thm null_Nil}),*)
1.76 + Rule_Def.Thm ("remdups_Cons",ThmC_Def.numerals_to_Free @{thm remdups_Cons}),
1.77 + Rule_Def.Thm ("remdups_Nil",ThmC_Def.numerals_to_Free @{thm remdups_Nil}),
1.78 + Rule_Def.Thm ("rev_Cons",ThmC_Def.numerals_to_Free @{thm rev_Cons}),
1.79 + Rule_Def.Thm ("rev_Nil",ThmC_Def.numerals_to_Free @{thm rev_Nil}),
1.80 + Rule_Def.Thm ("take_Nil",ThmC_Def.numerals_to_Free @{thm take_Nil}),
1.81 + Rule_Def.Thm ("take_Cons",ThmC_Def.numerals_to_Free @{thm take_Cons}),
1.82 + Rule_Def.Thm ("tl_Cons",ThmC_Def.numerals_to_Free @{thm tl_Cons}),
1.83 + Rule_Def.Thm ("tl_Nil",ThmC_Def.numerals_to_Free @{thm tl_Nil}),
1.84 + Rule_Def.Thm ("zip_Cons",ThmC_Def.numerals_to_Free @{thm zip_Cons}),
1.85 + Rule_Def.Thm ("zip_Nil",ThmC_Def.numerals_to_Free @{thm zip_Nil})],
1.86 scr = Rule_Def.EmptyScr}: Rule_Set.T;
1.87 \<close>
1.88 setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]\<close>