1.1 --- a/src/Tools/isac/ProgLang/ListC.thy Sun Mar 25 13:59:57 2018 +0200
1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Mon Mar 26 07:28:39 2018 +0200
1.3 @@ -133,52 +133,52 @@
1.4 ML{* (*the former ListC.ML*)
1.5 (** rule set for evaluating listexpr in scripts **)
1.6 val list_rls =
1.7 - Celem.Rls {id = "list_rls", preconds = [], rew_ord = ("dummy_ord", Celem.dummy_ord),
1.8 - erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [],
1.9 - rules = [Celem.Thm ("refl", TermC.num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
1.10 - Celem.Thm ("o_apply", TermC.num_str @{thm o_apply}),
1.11 + Rule.Rls {id = "list_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
1.12 + erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
1.13 + rules = [Rule.Thm ("refl", TermC.num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
1.14 + Rule.Thm ("o_apply", TermC.num_str @{thm o_apply}),
1.15
1.16 - Celem.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
1.17 - Celem.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.18 - Celem.Thm ("append_Cons",TermC.num_str @{thm append_Cons}),
1.19 - Celem.Thm ("append_Nil",TermC.num_str @{thm append_Nil}),
1.20 + Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
1.21 + Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.22 + Rule.Thm ("append_Cons",TermC.num_str @{thm append_Cons}),
1.23 + Rule.Thm ("append_Nil",TermC.num_str @{thm append_Nil}),
1.24 (* Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
1.25 Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*)
1.26 - Celem.Thm ("concat_Cons",TermC.num_str @{thm concat_Cons}),
1.27 - Celem.Thm ("concat_Nil",TermC.num_str @{thm concat_Nil}),
1.28 -(* Celem.Thm ("del_base",num_str @{thm del_base}),
1.29 - Celem.Thm ("del_rec",num_str @{thm del_rec}), *)
1.30 + Rule.Thm ("concat_Cons",TermC.num_str @{thm concat_Cons}),
1.31 + Rule.Thm ("concat_Nil",TermC.num_str @{thm concat_Nil}),
1.32 +(* Rule.Thm ("del_base",num_str @{thm del_base}),
1.33 + Rule.Thm ("del_rec",num_str @{thm del_rec}), *)
1.34
1.35 - Celem.Thm ("distinct_Cons",TermC.num_str @{thm distinct_Cons}),
1.36 - Celem.Thm ("distinct_Nil",TermC.num_str @{thm distinct_Nil}),
1.37 - Celem.Thm ("dropWhile_Cons",TermC.num_str @{thm dropWhile_Cons}),
1.38 - Celem.Thm ("dropWhile_Nil",TermC.num_str @{thm dropWhile_Nil}),
1.39 - Celem.Thm ("filter_Cons",TermC.num_str @{thm filter_Cons}),
1.40 - Celem.Thm ("filter_Nil",TermC.num_str @{thm filter_Nil}),
1.41 - Celem.Thm ("foldr_Cons",TermC.num_str @{thm foldr_Cons}),
1.42 - Celem.Thm ("foldr_Nil",TermC.num_str @{thm foldr_Nil}),
1.43 - Celem.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.44 - Celem.Thm ("LAST",TermC.num_str @{thm LAST}),
1.45 - Celem.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.46 - Celem.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.47 -(* Celem.Thm ("list_diff_def",num_str @{thm list_diff_def}),*)
1.48 - Celem.Thm ("map_Cons",TermC.num_str @{thm map_Cons}),
1.49 - Celem.Thm ("map_Nil",TermC.num_str @{thm map_Cons}),
1.50 -(* Celem.Thm ("mem_Cons",TermC.num_str @{thm mem_Cons}),
1.51 - Celem.Thm ("mem_Nil",TermC.num_str @{thm mem_Nil}), *)
1.52 -(* Celem.Thm ("null_Cons",TermC.num_str @{thm null_Cons}),
1.53 - Celem.Thm ("null_Nil",TermC.num_str @{thm null_Nil}),*)
1.54 - Celem.Thm ("remdups_Cons",TermC.num_str @{thm remdups_Cons}),
1.55 - Celem.Thm ("remdups_Nil",TermC.num_str @{thm remdups_Nil}),
1.56 - Celem.Thm ("rev_Cons",TermC.num_str @{thm rev_Cons}),
1.57 - Celem.Thm ("rev_Nil",TermC.num_str @{thm rev_Nil}),
1.58 - Celem.Thm ("take_Nil",TermC.num_str @{thm take_Nil}),
1.59 - Celem.Thm ("take_Cons",TermC.num_str @{thm take_Cons}),
1.60 - Celem.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.61 - Celem.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
1.62 - Celem.Thm ("zip_Cons",TermC.num_str @{thm zip_Cons}),
1.63 - Celem.Thm ("zip_Nil",TermC.num_str @{thm zip_Nil})],
1.64 - scr = Celem.EmptyScr}: Celem.rls;
1.65 + Rule.Thm ("distinct_Cons",TermC.num_str @{thm distinct_Cons}),
1.66 + Rule.Thm ("distinct_Nil",TermC.num_str @{thm distinct_Nil}),
1.67 + Rule.Thm ("dropWhile_Cons",TermC.num_str @{thm dropWhile_Cons}),
1.68 + Rule.Thm ("dropWhile_Nil",TermC.num_str @{thm dropWhile_Nil}),
1.69 + Rule.Thm ("filter_Cons",TermC.num_str @{thm filter_Cons}),
1.70 + Rule.Thm ("filter_Nil",TermC.num_str @{thm filter_Nil}),
1.71 + Rule.Thm ("foldr_Cons",TermC.num_str @{thm foldr_Cons}),
1.72 + Rule.Thm ("foldr_Nil",TermC.num_str @{thm foldr_Nil}),
1.73 + Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.74 + Rule.Thm ("LAST",TermC.num_str @{thm LAST}),
1.75 + Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.76 + Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.77 +(* Rule.Thm ("list_diff_def",num_str @{thm list_diff_def}),*)
1.78 + Rule.Thm ("map_Cons",TermC.num_str @{thm map_Cons}),
1.79 + Rule.Thm ("map_Nil",TermC.num_str @{thm map_Cons}),
1.80 +(* Rule.Thm ("mem_Cons",TermC.num_str @{thm mem_Cons}),
1.81 + Rule.Thm ("mem_Nil",TermC.num_str @{thm mem_Nil}), *)
1.82 +(* Rule.Thm ("null_Cons",TermC.num_str @{thm null_Cons}),
1.83 + Rule.Thm ("null_Nil",TermC.num_str @{thm null_Nil}),*)
1.84 + Rule.Thm ("remdups_Cons",TermC.num_str @{thm remdups_Cons}),
1.85 + Rule.Thm ("remdups_Nil",TermC.num_str @{thm remdups_Nil}),
1.86 + Rule.Thm ("rev_Cons",TermC.num_str @{thm rev_Cons}),
1.87 + Rule.Thm ("rev_Nil",TermC.num_str @{thm rev_Nil}),
1.88 + Rule.Thm ("take_Nil",TermC.num_str @{thm take_Nil}),
1.89 + Rule.Thm ("take_Cons",TermC.num_str @{thm take_Cons}),
1.90 + Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.91 + Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
1.92 + Rule.Thm ("zip_Cons",TermC.num_str @{thm zip_Cons}),
1.93 + Rule.Thm ("zip_Nil",TermC.num_str @{thm zip_Nil})],
1.94 + scr = Rule.EmptyScr}: Rule.rls;
1.95 *}
1.96 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
1.97