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