src/HOL/Library/LSC.thy

--- a/src/HOL/Library/LSC.thy	Fri Mar 11 10:37:37 2011 +0100
+++ b/src/HOL/Library/LSC.thy	Fri Mar 11 10:37:37 2011 +0100
@@ -9,39 +9,99 @@
 
 subsection {* Counterexample generator *}
 
+subsubsection {* Type code_int for Haskell's Int type *}
+
+typedef (open) code_int = "UNIV \<Colon> int set"
+  morphisms int_of of_int by rule
+
+lemma int_of_inject [simp]:
+  "int_of k = int_of l \<longleftrightarrow> k = l"
+  by (rule int_of_inject)
+
+
+instantiation code_int :: "{zero, one, minus, linorder}"
+begin
+
+definition [simp, code del]:
+  "0 = of_int 0"
+
+definition [simp, code del]:
+  "1 = of_int 1"
+
+definition [simp, code del]:
+  "n - m = of_int (int_of n - int_of m)"
+
+definition [simp, code del]:
+  "n \<le> m \<longleftrightarrow> int_of n \<le> int_of m"
+
+definition [simp, code del]:
+  "n < m \<longleftrightarrow> int_of n < int_of m"
+
+
+instance proof qed (auto)
+
+end
+(*
+lemma zero_code_int_code [code, code_unfold]:
+  "(0\<Colon>code_int) = Numeral0"
+  by (simp add: number_of_code_numeral_def Pls_def)
+lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
+  using zero_code_numeral_code ..
+
+lemma one_code_numeral_code [code, code_unfold]:
+  "(1\<Colon>code_int) = Numeral1"
+  by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
+lemma [code_post]: "Numeral1 = (1\<Colon>code_int)"
+  using one_code_numeral_code ..
+*)
+
+code_const "0 \<Colon> code_int"
+  (Haskell "0")
+
+code_const "1 \<Colon> code_int"
+  (Haskell "1")
+
+code_const "minus \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> code_int"
+  (Haskell "(_/ -/ _)")
+
+code_const "op \<le> \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
+  (Haskell infix 4 "<=")
+
+code_const "op < \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
+  (Haskell infix 4 "<")
+
+code_type code_int
+  (Haskell "Int")
+
 subsubsection {* LSC's deep representation of types of terms *}
 
 datatype type = SumOfProd "type list list"
 
-datatype "term" = Var "code_numeral list" type | Ctr code_numeral "term list"
+datatype "term" = Var "code_int list" type | Ctr code_int "term list"
 
 datatype 'a cons = C type "(term list => 'a) list"
 
 subsubsection {* auxilary functions for LSC *}
 
-definition nth :: "'a list => code_numeral => 'a"
-where
-  "nth xs i = List.nth xs (Code_Numeral.nat_of i)"
+consts nth :: "'a list => code_int => 'a"
 
-lemma [code]:
-  "nth (x # xs) i = (if i = 0 then x else nth xs (i - 1))"
-unfolding nth_def by (cases i) simp
+code_const nth ("Haskell" infixl 9  "!!")
 
-definition error :: "char list => 'a"
-where
-  "error = undefined"
+consts error :: "char list => 'a"
 
 code_const error ("Haskell" "error")
 
-definition toEnum' :: "code_numeral => char"
-where
-  "toEnum' = undefined"
+consts toEnum :: "code_int => char"
+
+code_const toEnum ("Haskell" "toEnum")
 
-code_const toEnum' ("Haskell" "(toEnum . fromInteger)")
+consts map_index :: "(code_int * 'a => 'b) => 'a list => 'b list"  
 
+consts split_At :: "code_int => 'a list => 'a list * 'a list"
+ 
 subsubsection {* LSC's basic operations *}
 
-type_synonym 'a series = "code_numeral => 'a cons"
+type_synonym 'a series = "code_int => 'a cons"
 
 definition empty :: "'a series"
 where
@@ -53,7 +113,7 @@
 
 fun conv :: "(term list => 'a) list => term => 'a"
 where
-  "conv cs (Var p _) = error (Char Nibble0 Nibble0 # map toEnum' p)"
+  "conv cs (Var p _) = error (Char Nibble0 Nibble0 # map toEnum p)"
 | "conv cs (Ctr i xs) = (nth cs i) xs"
 
 fun nonEmpty :: "type => bool"
@@ -81,11 +141,34 @@
 where
   "cons0 f = cons f"
 
+type_synonym pos = "code_int list"
+
+subsubsection {* Term refinement *}
+
+definition new :: "pos => type list list => term list"
+where
+  "new p ps = map_index (%(c, ts). Ctr c (map_index (%(i, t). Var (p @ [i]) t) ts)) ps"
+
+fun refine :: "term => pos => term list" and refineList :: "term list => pos => (term list) list"
+where
+  "refine (Var p (SumOfProd ss)) [] = new p ss"
+| "refine (Ctr c xs) p = map (Ctr c) (refineList xs p)"
+| "refineList xs (i # is) = (let (ls, xrs) = split_At i xs in (case xrs of x#rs => [ls @ y # rs. y <- refine x is]))"
+
+text {* Find total instantiations of a partial value *}
+
+function total :: "term => term list"
+where
+  "total (Ctr c xs) = [Ctr c ys. ys <- map total xs]"
+| "total (Var p (SumOfProd ss)) = [y. x <- new p ss, y <- total x]"
+by pat_completeness auto
+
+termination sorry
 
 subsubsection {* LSC's type class for enumeration *}
 
 class serial =
-  fixes series :: "code_numeral => 'a cons"
+  fixes series :: "code_int => 'a cons"
 
 definition cons1 :: "('a::serial => 'b) => 'b series"
 where
@@ -212,8 +295,10 @@
 
 subsubsection {* Setting up the counterexample generator *}
   
-use "Tools/LSC/lazysmallcheck.ML"
+use "~~/src/HOL/Tools/LSC/lazysmallcheck.ML"
 
 setup {* Lazysmallcheck.setup *}
 
+hide_const (open) empty
+
 end
\ No newline at end of file