(* Title:  functions on lists for Programs

    Author: Walther Neuper 0108

    (c) due to copyright terms

 *)

 theory ListC 

 imports Complex_Main "~~/src/Tools/isac/KEStore"

 begin

 ML_file "~~/src/Tools/isac/ProgLang/termC.sml"

 ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"

 ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"

 text {* 

   This file gives names to equations of function definitions,

   which are required for Lucas-Interpretation (by Isac's rewriter) of 

   Isac's programming language. This language preceeded the function package

   in 2002. For naming "axiomatization" is used for reasons of uniformity

   with the other replacements for "axioms".

   Another reminiscence from Isabelle2002 are Isac-specific numerals,

   introduced in order to have floating point numerals at a time, 

   when Isabelle did not consider that requirement. For the sake of uniformity

   'nat' from List.thy is replaced by 'real'.

   TODO: shift name-declarations to HOL/List.thy, adopt new names from there

   and remove this ListC.thy.

   Note: *one* "axiomatization" over all equations caused strange "'a list list"

   types.

 *}

 primrec LENGTH   :: "'a list => real"

 where

 LENGTH_NIL:	"LENGTH [] = 0" |

 LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"

 consts NTH ::  "[real, 'a list] => 'a"

 axiomatization where

 NTH_NIL: "NTH 1 (x # xs) = x" and

 NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs"

 axiomatization where

 hd_thm:	"hd (x # xs) = x"

 axiomatization where

 tl_Nil:	"tl []  = []" and

 tl_Cons: "tl (x # xs) = xs"

 axiomatization where

 LAST:	"last (x # xs) = (if xs = [] then x else last xs)"

 axiomatization where

 butlast_Nil: "butlast []    = []" and

 butlast_Cons:	"butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"

 axiomatization where

 map_Nil:"map f [] = []" and

 map_Cons:	"map f (x # xs) = f x  #  map f xs"

 axiomatization where

 rev_Nil: "rev [] = []" and

 rev_Cons:	"rev (x # xs) = rev xs @ [x]"

 axiomatization where

 filter_Nil:	"filter P [] = []" and

 filter_Cons: "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)" 

 axiomatization where

 concat_Nil:	"concat [] = []" and

 concat_Cons: "concat (x # xs) = x @ concat xs"

 axiomatization where

 takeWhile_Nil: "takeWhile P []     = []" and

 takeWhile_Cons: "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"

 axiomatization where

 dropWhile_Nil: "dropWhile P [] = []" and

 dropWhile_Cons: "dropWhile P (x # xs) = (if P x then dropWhile P xs else x#xs)"

 axiomatization where

 zip_Nil: "zip xs [] = []" and

 zip_Cons:	"zip xs (y # ys) = (case xs of [] => [] | z # zs => (z,y) # zip zs ys)"

 axiomatization where

 distinct_Nil:	"distinct []     = True" and

 distinct_Cons:	"distinct (x # xs) = (x ~: set xs & distinct xs)"

 axiomatization where

 remdups_Nil:	"remdups [] = []" and

 remdups_Cons:	"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" 

 (** Lexicographic orderings on lists ...!!!**)

 ML{* (*the former ListC.ML*)

 (** rule set for evaluating listexpr in scripts **)

 val list_rls = 

   Rls{id = "list_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord), 

     erls = Erls, srls = Erls, calc = [], errpatts = [],

     rules = [Thm ("refl", num_str @{thm refl}),  (*'a<>b -> FALSE' by fun eval_equal*)

        Thm ("o_apply", num_str @{thm o_apply}),

        Thm ("NTH_CONS",num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)

        Thm ("NTH_NIL",num_str @{thm NTH_NIL}),

        Thm ("append_Cons",num_str @{thm append_Cons}),

        Thm ("append_Nil",num_str @{thm append_Nil}),

 (*       Thm ("butlast_Cons",num_str @{thm butlast_Cons}),

        Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*)

        Thm ("concat_Cons",num_str @{thm concat_Cons}),

        Thm ("concat_Nil",num_str @{thm concat_Nil}),

 (*       Thm ("del_base",num_str @{thm del_base}),

        Thm ("del_rec",num_str @{thm del_rec}), *)

        Thm ("distinct_Cons",num_str @{thm distinct_Cons}),

        Thm ("distinct_Nil",num_str @{thm distinct_Nil}),

        Thm ("dropWhile_Cons",num_str @{thm dropWhile_Cons}),

        Thm ("dropWhile_Nil",num_str @{thm dropWhile_Nil}),

        Thm ("filter_Cons",num_str @{thm filter_Cons}),

        Thm ("filter_Nil",num_str @{thm filter_Nil}),

        Thm ("foldr_Cons",num_str @{thm foldr_Cons}),

        Thm ("foldr_Nil",num_str @{thm foldr_Nil}),

        Thm ("hd_thm",num_str @{thm hd_thm}),

        Thm ("LAST",num_str @{thm LAST}),

        Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),

        Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),

 (*       Thm ("list_diff_def",num_str @{thm list_diff_def}),*)

        Thm ("map_Cons",num_str @{thm map_Cons}),

        Thm ("map_Nil",num_str @{thm map_Cons}),

 (*       Thm ("mem_Cons",num_str @{thm mem_Cons}),

        Thm ("mem_Nil",num_str @{thm mem_Nil}), *)

 (*       Thm ("null_Cons",num_str @{thm null_Cons}),

        Thm ("null_Nil",num_str @{thm null_Nil}),*)

        Thm ("remdups_Cons",num_str @{thm remdups_Cons}),

        Thm ("remdups_Nil",num_str @{thm remdups_Nil}),

        Thm ("rev_Cons",num_str @{thm rev_Cons}),

        Thm ("rev_Nil",num_str @{thm rev_Nil}),

        Thm ("take_Nil",num_str @{thm take_Nil}),

        Thm ("take_Cons",num_str @{thm take_Cons}),

        Thm ("tl_Cons",num_str @{thm tl_Cons}),

        Thm ("tl_Nil",num_str @{thm tl_Nil}),

        Thm ("zip_Cons",num_str @{thm zip_Cons}),

        Thm ("zip_Nil",num_str @{thm zip_Nil})],

     scr = EmptyScr}:rls;

 *}

 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}

 end