# HG changeset patch
# User bulwahn
# Date 1306395724 -7200
# Node ID 859fe9cc08386e3b75efeb375b1d21a16ce676db
# Parent  5b9e16259341d61072491b0a472b5e073cb9801c
improving code_int setup in Quickcheck_Narrowing; adding partial_term_of class in Quickcheck_Narrowing

diff -r 5b9e16259341 -r 859fe9cc0838 src/HOL/Library/Quickcheck_Narrowing.thy
--- a/src/HOL/Library/Quickcheck_Narrowing.thy	Thu May 26 09:42:02 2011 +0200
+++ b/src/HOL/Library/Quickcheck_Narrowing.thy	Thu May 26 09:42:04 2011 +0200
@@ -85,6 +85,10 @@
 where
   "nat_of i = nat (int_of i)"
 
+
+code_datatype "number_of \<Colon> int \<Rightarrow> code_numeral"
+  
+  
 instantiation code_int :: "{minus, linordered_semidom, semiring_div, linorder}"
 begin
 
@@ -120,19 +124,19 @@
 qed (auto simp add: code_int left_distrib zmult_zless_mono2)
 
 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 ..
+  by (simp add: number_of_code_int_def Pls_def)
+lemma [code_post]: "Numeral0 = (0\<Colon>code_int)"
+  using zero_code_int_code ..
 
-lemma one_code_numeral_code [code, code_unfold]:
+lemma one_code_int_code [code, code_unfold]:
   "(1\<Colon>code_int) = Numeral1"
-  by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
+  by (simp add: number_of_code_int_def Pls_def Bit1_def)
 lemma [code_post]: "Numeral1 = (1\<Colon>code_int)"
-  using one_code_numeral_code ..
-*)
+  using one_code_int_code ..
+
 
 definition div_mod_code_int :: "code_int \<Rightarrow> code_int \<Rightarrow> code_int \<times> code_int" where
   [code del]: "div_mod_code_int n m = (n div m, n mod m)"
@@ -202,6 +206,11 @@
 
 datatype 'a cons = C type "(term list => 'a) list"
 
+subsubsection {* From narrowing's deep representation of terms to Code_Evaluation's terms *}
+
+class partial_term_of = typerep +
+  fixes partial_term_of :: "'a itself => term => Code_Evaluation.term"
+
 subsubsection {* Auxilary functions for Narrowing *}
 
 consts nth :: "'a list => code_int => 'a"