improving code_int setup in Quickcheck_Narrowing; adding partial_term_of class in Quickcheck_Narrowing
--- 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"