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: 
wenzelm@60192: theory ListC imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
wneuper@59586: 
neuper@37906: begin
neuper@52122: 
walther@59630: text \<open>Abstract:
walther@59630:   There are examples in the Knowledge, which demonstrate list processing, e.g. InsSort.thy.
neuper@37906: 
walther@59630:   Lists in example calculations must have a different type for list processing in Isac programs.
walther@59630:   Presently the lists in examples have a new type xlist with the unfamiliar list
walther@59630:   notation "{||a, b, c||}". One could expect math-authors to use such unfamiliar notation 
walther@59630:   and expose students to familiar notation in calculations, and not vice versa as done presently.
wneuper@59234: 
walther@59630:   Thus this theory resides in ProgLang so far.
wneuper@59472: \<close>
neuper@37906: 
walther@59620: subsection \<open>General constants\<close>
walther@59620: consts
walther@59620:   EmptyList :: "bool list" 
walther@59620:   UniversalList :: "bool list" 
walther@59620: 
walther@59620: ML \<open>
walther@59620: \<close> ML \<open>
walther@59620: val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";
walther@59620: val EmptyList = (Thm.term_of o the o (TermC.parse @{theory}))  "[]::bool list";     
walther@59620: \<close> ML \<open>
walther@59620: \<close>
walther@59620: 
walther@59620: subsection \<open>Type 'xlist' for Lucas-Interpretation | for InsSort.thy\<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: 
walther@60121: primrec Length   :: "'a list => real"
neuper@37906: where
walther@60121: LENGTH_NIL:	"Length [] = 0" |
walther@60121: LENGTH_CONS: "Length (x#xs) = 1 + Length xs"
neuper@37906: 
walther@59620: subsection \<open>Functions for 'list'\<close>
walther@59620: 
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: 
walther@59887: (* redefine together with identifiers (still) required for Know_Store ..*)
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@59602: consts lastI :: "'a list \<Rightarrow> 'a"
wneuper@59602: axiomatization where
wneuper@59602: last_thmI: "lastI (x#xs) = (if xs = [] then x else lastI xs)"
wneuper@59602: 
walther@59620: subsection \<open>rule set for evaluating Porg_Expr, will be extended in several thys\<close>
walther@59620: ML \<open>
walther@59630: \<close> ML \<open>
walther@59850: val prog_expr =
walther@59857:   Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
walther@59851:     erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [],
walther@59871:     rules = [Rule_Def.Thm ("refl", ThmC_Def.numerals_to_Free @{thm refl}),  (*'a<>b -> FALSE' by fun eval_equal*)
walther@59871:        Rule_Def.Thm ("o_apply", ThmC_Def.numerals_to_Free @{thm o_apply}),
neuper@37906: 
walther@59871:        Rule_Def.Thm ("NTH_CONS",ThmC_Def.numerals_to_Free @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
walther@59871:        Rule_Def.Thm ("NTH_NIL",ThmC_Def.numerals_to_Free @{thm NTH_NIL}),
walther@59871:        Rule_Def.Thm ("append_Cons",ThmC_Def.numerals_to_Free @{thm append_Cons}),
walther@59871:        Rule_Def.Thm ("append_Nil",ThmC_Def.numerals_to_Free @{thm append_Nil}),
neuper@52148: (*       Thm ("butlast_Cons",num_str @{thm butlast_Cons}),
neuper@52148:        Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*)
walther@59871:        Rule_Def.Thm ("concat_Cons",ThmC_Def.numerals_to_Free @{thm concat_Cons}),
walther@59871:        Rule_Def.Thm ("concat_Nil",ThmC_Def.numerals_to_Free @{thm concat_Nil}),
walther@59850: (*       Rule_Def.Thm ("del_base",num_str @{thm del_base}),
walther@59850:        Rule_Def.Thm ("del_rec",num_str @{thm del_rec}), *)
neuper@37906: 
walther@59871:        Rule_Def.Thm ("distinct_Cons",ThmC_Def.numerals_to_Free @{thm distinct_Cons}),
walther@59871:        Rule_Def.Thm ("distinct_Nil",ThmC_Def.numerals_to_Free @{thm distinct_Nil}),
walther@59871:        Rule_Def.Thm ("dropWhile_Cons",ThmC_Def.numerals_to_Free @{thm dropWhile_Cons}),
walther@59871:        Rule_Def.Thm ("dropWhile_Nil",ThmC_Def.numerals_to_Free @{thm dropWhile_Nil}),
walther@59871:        Rule_Def.Thm ("filter_Cons",ThmC_Def.numerals_to_Free @{thm filter_Cons}),
walther@59871:        Rule_Def.Thm ("filter_Nil",ThmC_Def.numerals_to_Free @{thm filter_Nil}),
walther@59871:        Rule_Def.Thm ("foldr_Cons",ThmC_Def.numerals_to_Free @{thm foldr_Cons}),
walther@59871:        Rule_Def.Thm ("foldr_Nil",ThmC_Def.numerals_to_Free @{thm foldr_Nil}),
walther@59871:        Rule_Def.Thm ("hd_thm",ThmC_Def.numerals_to_Free @{thm hd_thm}),
walther@59871:        Rule_Def.Thm ("LAST",ThmC_Def.numerals_to_Free @{thm LAST}),
walther@59871:        Rule_Def.Thm ("LENGTH_CONS",ThmC_Def.numerals_to_Free @{thm LENGTH_CONS}),
walther@59871:        Rule_Def.Thm ("LENGTH_NIL",ThmC_Def.numerals_to_Free @{thm LENGTH_NIL}),
walther@59850: (*       Rule_Def.Thm ("list_diff_def",num_str @{thm list_diff_def}),*)
walther@59871:        Rule_Def.Thm ("map_Cons",ThmC_Def.numerals_to_Free @{thm map_Cons}),
walther@59871:        Rule_Def.Thm ("map_Nil",ThmC_Def.numerals_to_Free @{thm map_Cons}),
walther@59871: (*       Rule_Def.Thm ("mem_Cons",ThmC_Def.numerals_to_Free @{thm mem_Cons}),
walther@59871:        Rule_Def.Thm ("mem_Nil",ThmC_Def.numerals_to_Free @{thm mem_Nil}), *)
walther@59871: (*       Rule_Def.Thm ("null_Cons",ThmC_Def.numerals_to_Free @{thm null_Cons}),
walther@59871:        Rule_Def.Thm ("null_Nil",ThmC_Def.numerals_to_Free @{thm null_Nil}),*)
walther@59871:        Rule_Def.Thm ("remdups_Cons",ThmC_Def.numerals_to_Free @{thm remdups_Cons}),
walther@59871:        Rule_Def.Thm ("remdups_Nil",ThmC_Def.numerals_to_Free @{thm remdups_Nil}),
walther@59871:        Rule_Def.Thm ("rev_Cons",ThmC_Def.numerals_to_Free @{thm rev_Cons}),
walther@59871:        Rule_Def.Thm ("rev_Nil",ThmC_Def.numerals_to_Free @{thm rev_Nil}),
walther@59871:        Rule_Def.Thm ("take_Nil",ThmC_Def.numerals_to_Free @{thm take_Nil}),
walther@59871:        Rule_Def.Thm ("take_Cons",ThmC_Def.numerals_to_Free @{thm take_Cons}),
walther@59871:        Rule_Def.Thm ("tl_Cons",ThmC_Def.numerals_to_Free @{thm tl_Cons}),
walther@59871:        Rule_Def.Thm ("tl_Nil",ThmC_Def.numerals_to_Free @{thm tl_Nil}),
walther@59871:        Rule_Def.Thm ("zip_Cons",ThmC_Def.numerals_to_Free @{thm zip_Cons}),
walther@59871:        Rule_Def.Thm ("zip_Nil",ThmC_Def.numerals_to_Free @{thm zip_Nil})],
walther@59878:     scr = Rule_Def.Empty_Prog}: Rule_Set.T;
wneuper@59472: \<close>
wenzelm@60289: rule_set_knowledge prog_expr = prog_expr
neuper@52122: 
walther@60278: ML \<open>
walther@60278: \<close> ML \<open>
walther@60278: \<close> ML \<open>
walther@60278: \<close>
neuper@37906: end