neuper@52122: (* Title:  functions on lists for Programs
neuper@37965:    Author: Walther Neuper 0108
neuper@37965:    (c) due to copyright terms
neuper@37906: *)
neuper@37906: 
neuper@52122: theory ListC 
wneuper@59206: imports "~~/src/Tools/isac/KEStore"
neuper@37906: begin
neuper@52122: 
neuper@52122: ML_file "~~/src/Tools/isac/ProgLang/termC.sml"
neuper@52122: ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
neuper@52122: ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
wneuper@59472: ML \<open>
wneuper@59472: \<close> ML \<open>
wneuper@59472: \<close> 
neuper@37906: 
wneuper@59472: subsection \<open>Notes on Isac's programming language\<close>
wneuper@59472: text \<open>
wneuper@59234:   Isac's programming language combines tacticals (TRY, etc) and 
wneuper@59234:   tactics (Rewrite, etc) with list processing.
wneuper@59234: 
wneuper@59234:   In order to distinguish list expressions of the meta (programming)
wneuper@59234:   language from the object language in Lucas-Interpretation, a 
wneuper@59234:   new 'type xlist' is introduced.
wneuper@59234:   TODO: Switch the role of 'xlist' and 'list' (the former only used
wneuper@59234:   by InsSort.thy)
wneuper@59234: 
wneuper@59234:   Isac's programming language preceeded the function package
neuper@52148:   in 2002. For naming "axiomatization" is used for reasons of uniformity
neuper@52148:   with the other replacements for "axioms".
neuper@52148:   Another reminiscence from Isabelle2002 are Isac-specific numerals,
neuper@52148:   introduced in order to have floating point numerals at a time, 
neuper@52148:   when Isabelle did not consider that requirement. For the sake of uniformity
wneuper@59234:   'nat' from List.thy is replaced by 'real' by 'fun parse',
wneuper@59234:   however, 'fun parseNEW' has started to replace this fix (after finishing
wneuper@59234:   this fix, there will be a 'rename all parseNEW --> parse).
neuper@52148: 
neuper@52148:   Note: *one* "axiomatization" over all equations caused strange "'a list list"
neuper@52148:   types.
wneuper@59472: \<close>
neuper@37906: 
wneuper@59472: subsection \<open>Type 'xlist' for Lucas-Interpretation\<close>
wneuper@59457: (* cp fom ~~/src/HOL/List.thy
wneuper@59457:    TODO: ask for shorter deliminters in xlist *)
wneuper@59457: datatype  'a xlist =
wneuper@59457:     XNil  ("{|| ||}")
wneuper@59457:   | XCons (xhd: 'a)  (xtl: "'a xlist")  (infixr "@#" 65)
wneuper@59234: 
wneuper@59234: syntax
wneuper@59457:    \<comment> \<open>list Enumeration\<close>
wneuper@59244:   "_xlist" :: "args => 'a xlist"    ("{|| (_) ||}")
wneuper@59234: 
wneuper@59234: translations
wneuper@59244:   "{||x, xs||}" == "x@#{||xs||}"
wneuper@59244:   "{||x||}" == "x@#{|| ||}"
wneuper@59234: 
wneuper@59244: term "{|| ||}"
wneuper@59244: term "{||1,2,3||}"
wneuper@59234: 
wneuper@59472: subsection \<open>Functions for 'xlist'\<close>
wneuper@59234: (* TODO: 
wneuper@59234: (1) revise, if definition of identifiers like LENGTH_NIL are still required.
wneuper@59234: (2) switch the role of 'xlist' and 'list' in the functions below, in particular for
wneuper@59234:   'foldr', 'foldr_Nil', 'foldr_Cons' and 'xfoldr', 'xfoldr_Nil', 'xfoldr_Cons'.
wneuper@59234:   For transition phase just outcomment InsSort.thy and inssort.sml.
wneuper@59234: *)
wneuper@59234: 
wneuper@59234: primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
wneuper@59244: xfoldr_Nil:  "xfoldr f {|| ||} = id" |
wneuper@59234: xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
wneuper@59234: 
neuper@37997: primrec LENGTH   :: "'a list => real"
neuper@37906: where
neuper@52148: LENGTH_NIL:	"LENGTH [] = 0" |
neuper@52148: LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
neuper@37906: 
neuper@52148: consts NTH ::  "[real, 'a list] => 'a"
neuper@52148: axiomatization where
neuper@52148: NTH_NIL: "NTH 1 (x # xs) = x" and
neuper@52148: NTH_CONS: (*NO primrec, fun ..*)"1 < n ==> NTH n (x # xs) = NTH (n + -1) xs"
neuper@37906: 
wneuper@59457: (* redefine together with identifiers (still) required for KEStore ..*)
neuper@52148: axiomatization where
neuper@52148: hd_thm:	"hd (x # xs) = x"
t@42197: 
neuper@52148: axiomatization where
neuper@52148: tl_Nil:	"tl []  = []" and
neuper@52148: tl_Cons: "tl (x # xs) = xs"
neuper@37906: 
neuper@52148: axiomatization where
neuper@52148: LAST:	"last (x # xs) = (if xs = [] then x else last xs)"
neuper@37906: 
neuper@52148: axiomatization where
neuper@52148: butlast_Nil: "butlast []    = []" and
neuper@52148: butlast_Cons:	"butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
neuper@52148: 
neuper@52148: axiomatization where
neuper@52148: map_Nil:"map f [] = []" and
neuper@52148: map_Cons:	"map f (x # xs) = f x  #  map f xs"
neuper@52148: 
neuper@52148: axiomatization where
neuper@52148: rev_Nil: "rev [] = []" and
neuper@52148: rev_Cons:	"rev (x # xs) = rev xs @ [x]"
neuper@52148: 
neuper@52148: axiomatization where
neuper@52148: filter_Nil:	"filter P [] = []" and
neuper@52148: filter_Cons: "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)" 
neuper@52148: 
neuper@52148: axiomatization where
neuper@52148: concat_Nil:	"concat [] = []" and
neuper@52148: concat_Cons: "concat (x # xs) = x @ concat xs"
neuper@52148: 
neuper@52148: axiomatization where
neuper@52148: takeWhile_Nil: "takeWhile P []     = []" and
neuper@52148: takeWhile_Cons: "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
neuper@52148: 
neuper@52148: axiomatization where
neuper@52148: dropWhile_Nil: "dropWhile P [] = []" and
neuper@52148: dropWhile_Cons: "dropWhile P (x # xs) = (if P x then dropWhile P xs else x#xs)"
neuper@52148: 
neuper@52148: axiomatization where
neuper@52148: zip_Nil: "zip xs [] = []" and
neuper@52148: zip_Cons:	"zip xs (y # ys) = (case xs of [] => [] | z # zs => (z,y) # zip zs ys)"
neuper@52148: 
neuper@52148: axiomatization where
neuper@52148: distinct_Nil:	"distinct []     = True" and
neuper@52148: distinct_Cons:	"distinct (x # xs) = (x ~: set xs & distinct xs)"
neuper@52148: 
neuper@52148: axiomatization where
neuper@52148: remdups_Nil:	"remdups [] = []" and
neuper@52148: remdups_Cons:	"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" 
neuper@37906: 
wneuper@59484: ML\<open>
wneuper@59484: (** rule set for evaluating listexpr in scripts, will be extended in several thys **)
neuper@37906: val list_rls = 
wneuper@59416:   Rule.Rls {id = "list_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 
wneuper@59416:     erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
wneuper@59416:     rules = [Rule.Thm ("refl", TermC.num_str @{thm refl}),  (*'a<>b -> FALSE' by fun eval_equal*)
wneuper@59416:        Rule.Thm ("o_apply", TermC.num_str @{thm o_apply}),
neuper@37906: 
wneuper@59416:        Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
wneuper@59416:        Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
wneuper@59416:        Rule.Thm ("append_Cons",TermC.num_str @{thm append_Cons}),
wneuper@59416:        Rule.Thm ("append_Nil",TermC.num_str @{thm append_Nil}),
neuper@52148: (*       Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
neuper@52148:        Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*)
wneuper@59416:        Rule.Thm ("concat_Cons",TermC.num_str @{thm concat_Cons}),
wneuper@59416:        Rule.Thm ("concat_Nil",TermC.num_str @{thm concat_Nil}),
wneuper@59416: (*       Rule.Thm ("del_base",num_str @{thm del_base}),
wneuper@59416:        Rule.Thm ("del_rec",num_str @{thm del_rec}), *)
neuper@37906: 
wneuper@59416:        Rule.Thm ("distinct_Cons",TermC.num_str @{thm distinct_Cons}),
wneuper@59416:        Rule.Thm ("distinct_Nil",TermC.num_str @{thm distinct_Nil}),
wneuper@59416:        Rule.Thm ("dropWhile_Cons",TermC.num_str @{thm dropWhile_Cons}),
wneuper@59416:        Rule.Thm ("dropWhile_Nil",TermC.num_str @{thm dropWhile_Nil}),
wneuper@59416:        Rule.Thm ("filter_Cons",TermC.num_str @{thm filter_Cons}),
wneuper@59416:        Rule.Thm ("filter_Nil",TermC.num_str @{thm filter_Nil}),
wneuper@59416:        Rule.Thm ("foldr_Cons",TermC.num_str @{thm foldr_Cons}),
wneuper@59416:        Rule.Thm ("foldr_Nil",TermC.num_str @{thm foldr_Nil}),
wneuper@59416:        Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
wneuper@59416:        Rule.Thm ("LAST",TermC.num_str @{thm LAST}),
wneuper@59416:        Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
wneuper@59416:        Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
wneuper@59416: (*       Rule.Thm ("list_diff_def",num_str @{thm list_diff_def}),*)
wneuper@59416:        Rule.Thm ("map_Cons",TermC.num_str @{thm map_Cons}),
wneuper@59416:        Rule.Thm ("map_Nil",TermC.num_str @{thm map_Cons}),
wneuper@59416: (*       Rule.Thm ("mem_Cons",TermC.num_str @{thm mem_Cons}),
wneuper@59416:        Rule.Thm ("mem_Nil",TermC.num_str @{thm mem_Nil}), *)
wneuper@59416: (*       Rule.Thm ("null_Cons",TermC.num_str @{thm null_Cons}),
wneuper@59416:        Rule.Thm ("null_Nil",TermC.num_str @{thm null_Nil}),*)
wneuper@59416:        Rule.Thm ("remdups_Cons",TermC.num_str @{thm remdups_Cons}),
wneuper@59416:        Rule.Thm ("remdups_Nil",TermC.num_str @{thm remdups_Nil}),
wneuper@59416:        Rule.Thm ("rev_Cons",TermC.num_str @{thm rev_Cons}),
wneuper@59416:        Rule.Thm ("rev_Nil",TermC.num_str @{thm rev_Nil}),
wneuper@59416:        Rule.Thm ("take_Nil",TermC.num_str @{thm take_Nil}),
wneuper@59416:        Rule.Thm ("take_Cons",TermC.num_str @{thm take_Cons}),
wneuper@59416:        Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
wneuper@59416:        Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
wneuper@59416:        Rule.Thm ("zip_Cons",TermC.num_str @{thm zip_Cons}),
wneuper@59416:        Rule.Thm ("zip_Nil",TermC.num_str @{thm zip_Nil})],
wneuper@59416:     scr = Rule.EmptyScr}: Rule.rls;
wneuper@59472: \<close>
wneuper@59472: setup \<open>KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))]\<close>
neuper@52122: 
neuper@37906: end