(* use_thy_only"../ProgLang/ListC";

   use_thy_only"ProgLang/ListC";

   use_thy"ProgLang/ListC";

   use_thy_only"ListC";

   W.N. 8.01

   attaches identifiers to definition of listfuns,

   for storing them in list_rls

WN.29.4.03: 

*)

theory ListC imports Complex_Main

uses ("library.sml")("calcelems.sml")

("ProgLang/term.sml")("ProgLang/calculate.sml")

("ProgLang/rewrite.sml")

begin

use "library.sml"        (*indent,...*)

use "calcelems.sml"      (*str_of_type, Thm,...*)

use "ProgLang/term.sml"  (*num_str,...*)

use "ProgLang/calculate.sml" (*???*)

use "ProgLang/rewrite.sml"   (*?*** At command "end" (line 205../ListC.thy*)

text {* 'nat' in List.thy replaced by 'real' *}

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

where

  LENGTH_NIL:	"length_' [] = 0"     (*length: 'a list => nat*)

| LENGTH_CONS: "length_' (x#xs) = 1 + length_' xs"

primrec del :: "['a list, 'a] => 'a list"

where

  del_base: "del [] x = []"

| del_rec:  "del (y#ys) x = (if x = y then ys else y#(del ys x))"

definition

  list_diff :: "['a list, 'a list] => 'a list"         (* as -- bs *)

              ("(_ --/ _)" [66, 66] 65)

  where "a -- b == foldl del a b"

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

axioms

 (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*)

  NTH_NIL:      "nth_' 1 (x#xs) = x"

(*  NTH_CONS:     "nth_' n (x#xs) = nth_' (n+ -1) xs"  *)

(*rewriter does not reach base case   ......    ;

  the condition involves another rule set (erls, eval_binop in Atools):*)

  NTH_CONS:     "1 < n ==> nth_' n (x#xs) = nth_' (n+ - 1) xs"

(*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*)

(*primrec*)

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

(*primrec*)

  tl_Nil:	"tl([])   = []"

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

(*primrec*)

  null_Nil:	"null([])   = True"

  null_Cons:	"null(x#xs) = False"

(*primrec*)

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

(*primrec*)

  butlast_Nil:	"butlast []    = []"

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

(*primrec*)

  mem_Nil:	"x mem []     = False"

  mem_Cons:	"x mem (y#ys) = (if y=x then True else x mem ys)"

(*primrec-------already named---

  "set [] = {}"

  "set (x#xs) = insert x (set xs)"

  primrec

  list_all_Nil  "list_all P [] = True"

  list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"

----------------*)

(*primrec*)

  map_Nil:	"map f []     = []"

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

(*primrec*)

  append_Nil:  "[]    @ys = ys"

  append_Cons: "(x#xs)@ys = x#(xs@ys)"

(*primrec*)

  rev_Nil:	"rev([])   = []"

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

(*primrec*)

  filter_Nil:	"filter P []     = []"

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

(*primrec-------already named---

  foldl_Nil  "foldl f a [] = a"

  foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"

----------------*)

(*primrec*)

  foldr_Nil:	"foldr f [] a     = a"

  foldr_Cons:	"foldr f (x#xs) a = f x (foldr f xs a)"

(*primrec*)

  concat_Nil:	"concat([])   = []"

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

(*primrec-------already named---

  drop_Nil  "drop n [] = []"

  drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"

  (* Warning: simpset does not contain this definition but separate theorems 

     for n=0 / n=Suc k*)

(*primrec*)

  take_Nil  "take n [] = []"

  take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"

  (* Warning: simpset does not contain this definition but separate theorems 

     for n=0 / n=Suc k*)

(*primrec*) 

  nth_Cons  "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"

  (* Warning: simpset does not contain this definition but separate theorems 

     for n=0 / n=Suc k*)

(*primrec*)

 "    [][i:=v] = []"

 "(x#xs)[i:=v] = (case i of 0     => v # xs 

			  | Suc j => x # xs[j:=v])"

----------------*)

(*primrec*)

  takeWhile_Nil:	"takeWhile P []     = []"

  takeWhile_Cons:

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

(*primrec*)

  dropWhile_Nil:	"dropWhile P []     = []"

  dropWhile_Cons:

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

(*primrec*)

  zip_Nil:	"zip xs []     = []"

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

  (* Warning: simpset does not contain this definition but separate theorems 

     for xs=[] / xs=z#zs *)

(*primrec

  upt_0   "[i..0(] = []"

  upt_Suc "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"

*)

(*primrec*)

  distinct_Nil:	"distinct []     = True"

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

(*primrec*)

  remdups_Nil:	"remdups [] = []"

  remdups_Cons:	"remdups (x#xs) =

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

(*primrec-------already named---

  replicate_0   "replicate  0      x = []"

  replicate_Suc "replicate (Suc n) x = x # replicate n x"

----------------*)

(** 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 = e_rls, srls = Erls, calc = [], (*asm_thm=[],*)

      rules = (*8.01: copied from*)

      [Thm ("refl", num_str 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;

*}

ML{*

ruleset' := overwritelthy @{theory} (!ruleset',

  [("list_rls",list_rls)

   ]);

*}

end