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