diff -r 4e569846524c -r aabc6c8e930a src/Tools/isac/ProgLang/ListC.thy
--- a/src/Tools/isac/ProgLang/ListC.thy	Fri Oct 18 14:36:51 2013 +0200
+++ b/src/Tools/isac/ProgLang/ListC.thy	Mon Oct 21 09:03:50 2013 +0200
@@ -11,130 +11,82 @@
 ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
 ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
 
-text {* 'nat' in List.thy replaced by 'real' *}
+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: 'a list => nat*)
-| LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
+LENGTH_NIL:	"LENGTH [] = 0" |
+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))"
+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"
 
-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"
+axiomatization where
+hd_thm:	"hd (x # xs) = x"
 
-axioms(*axiomatization where*)
- (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*)
-  NTH_NIL:      "NTH 1 (x#xs) = x" (*and*)
-(*  NTH_CONS:     "NTH n (x#xs) = NTH (n+ -1) xs"  *)
+axiomatization where
+tl_Nil:	"tl []  = []" and
+tl_Cons: "tl (x # xs) = 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" (*and*)
+axiomatization where
+LAST:	"last (x # xs) = (if xs = [] then x else last xs)"
 
-(*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*)
-(*primrec*)
-  hd_thm:	"hd(x#xs) = x" (*and*)
-(*primrec*)
-  tl_Nil:	"tl([])   = []" (*and*)
-  tl_Cons:		"tl(x#xs) = xs" (*and*)
-(*primrec*)
-  null_Nil:	"null([])   = True" (*and*)
-  null_Cons:	"null(x#xs) = False" (*and*)
-(*primrec*)
-  LAST:	"last(x#xs) = (if xs=[] then x else last xs)" (*and*)
-(*primrec*)
-  butlast_Nil:	"butlast []    = []" (*and*)
-  butlast_Cons:	"butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" (*and*)
-(*primrec
-  mem_Nil:	"x mem []     = False"
-  mem_Cons:	"x mem (y#ys) = (if y=x then True else x mem ys)"
-*)
-  mem_Nil:	"x : set []     = False" (*and*)
-  mem_Cons:	"x : set (y#ys) = (if y=x then True else x : set ys)" (*and*)
-(*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 []     = []" (*and*)
-  map_Cons:	"map f (x#xs) = f(x)#map f xs" (*and*)
-(*primrec*)
-  append_Nil:  "[]    @ys = ys" (*and*)
-  append_Cons: "(x#xs)@ys = x#(xs@ys)" (*and*)
-(*primrec*)
-  rev_Nil:	"rev([])   = []" (*and*)
-  rev_Cons:	"rev(x#xs) = rev(xs) @ [x]" (*and*)
-(*primrec*)
-  filter_Nil:	"filter P []     = []" (*and*)
-  filter_Cons:	"filter P (x#xs) =(if P x then x#filter P xs else filter P xs)" (*and*)
-(*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" (*and*)
-  foldr_Cons:	"foldr f (x#xs) a = f x (foldr f xs a)" (*and*)
-(*primrec*)
-  concat_Nil:	"concat([])   = []" (*and*)
-  concat_Cons:	"concat(x#xs) = x @ concat(xs)" (*and*)
-(*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 []     = []" (*and*)
-  takeWhile_Cons:
-  "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" (*and*)
-(*primrec*)
-  dropWhile_Nil:	"dropWhile P []     = []" (*and*)
-  dropWhile_Cons:
-  "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" (*and*)
-(*primrec*)
-  zip_Nil:	"zip xs []     = []" (*and*)
-  zip_Cons:	"zip xs (y#ys) =(case xs of [] => [] | z#zs =>(z,y)#zip zs ys)" (*and*)
-  (* 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" (*and*)
-  distinct_Cons:	"distinct (x#xs) = (x ~: set xs & distinct xs)" (*and*)
-(*primrec*)
-  remdups_Nil:	"remdups [] = []" (*and*)
-  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"
-----------------*)
+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 ...!!!**)
 
@@ -150,12 +102,12 @@
        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 ("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 ("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}),
@@ -169,13 +121,13 @@
        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 ("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 ("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}),