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