# HG changeset patch
# User bulwahn
# Date 1282748393 -7200
# Node ID e5508a74b11f1585466774bfcccb52f4fdeb8b2d
# Parent  4b8fd91ea59aae359dbbc1c3fa85f5836ddc8b5c
changing hotel trace definition; adding simple handling of numerals on natural numbers

diff -r 4b8fd91ea59a -r e5508a74b11f src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:53 2010 +0200
@@ -69,7 +69,7 @@
 | "hotel (e # s) = (hotel s & (case e of
   Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s |
   Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
-  Exit g r \<Rightarrow> False))"
+  Exit g r \<Rightarrow> g : isin s r))"
 
 lemma issued_nil: "issued [] = {Key0}"
 by (auto simp add: initk_def)
@@ -86,7 +86,7 @@
 
 ML {* Code_Prolog.options := {ensure_groundness = true} *}
 
-values 10 "{s. hotel s}"
+values 40 "{s. hotel s}"
 
 
 setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
diff -r 4b8fd91ea59a -r e5508a74b11f src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:53 2010 +0200
@@ -120,9 +120,16 @@
   | translate_arith_const @{const_name "Groups.minus_class.minus"} = SOME Minus
   | translate_arith_const _ = NONE
 
+fun mk_nat_term constant_table n =
+  let
+    val zero = translate_const constant_table @{const_name "Groups.zero_class.zero"}
+    val Suc = translate_const constant_table @{const_name "Suc"}
+  in funpow n (fn t => AppF (Suc, [t])) (Cons zero) end
+
 fun translate_term ctxt constant_table t =
   case try HOLogic.dest_number t of
     SOME (@{typ "int"}, n) => Number n
+  | SOME (@{typ "nat"}, n) => mk_nat_term constant_table n
   | NONE =>
       (case strip_comb t of
         (Free (v, T), []) => Var v 
@@ -183,6 +190,7 @@
     val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const)
     val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt
     val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table
+      |> declare_consts [@{const_name "Groups.zero_class.zero"}, @{const_name "Suc"}]
     fun translate_intro intro =
       let
         val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro)