changing hotel trace definition; adding simple handling of numerals on natural numbers
authorbulwahn
Wed Aug 25 16:59:53 2010 +0200 (2010-08-25)
changeset 38734e5508a74b11f
parent 38733 4b8fd91ea59a
child 38735 cb9031a9dccf
changing hotel trace definition; adding simple handling of numerals on natural numbers
src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
src/HOL/Tools/Predicate_Compile/code_prolog.ML
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:51 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:53 2010 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4  | "hotel (e # s) = (hotel s & (case e of
     1.5    Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s |
     1.6    Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
     1.7 -  Exit g r \<Rightarrow> False))"
     1.8 +  Exit g r \<Rightarrow> g : isin s r))"
     1.9  
    1.10  lemma issued_nil: "issued [] = {Key0}"
    1.11  by (auto simp add: initk_def)
    1.12 @@ -86,7 +86,7 @@
    1.13  
    1.14  ML {* Code_Prolog.options := {ensure_groundness = true} *}
    1.15  
    1.16 -values 10 "{s. hotel s}"
    1.17 +values 40 "{s. hotel s}"
    1.18  
    1.19  
    1.20  setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
     2.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:51 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Aug 25 16:59:53 2010 +0200
     2.3 @@ -120,9 +120,16 @@
     2.4    | translate_arith_const @{const_name "Groups.minus_class.minus"} = SOME Minus
     2.5    | translate_arith_const _ = NONE
     2.6  
     2.7 +fun mk_nat_term constant_table n =
     2.8 +  let
     2.9 +    val zero = translate_const constant_table @{const_name "Groups.zero_class.zero"}
    2.10 +    val Suc = translate_const constant_table @{const_name "Suc"}
    2.11 +  in funpow n (fn t => AppF (Suc, [t])) (Cons zero) end
    2.12 +
    2.13  fun translate_term ctxt constant_table t =
    2.14    case try HOLogic.dest_number t of
    2.15      SOME (@{typ "int"}, n) => Number n
    2.16 +  | SOME (@{typ "nat"}, n) => mk_nat_term constant_table n
    2.17    | NONE =>
    2.18        (case strip_comb t of
    2.19          (Free (v, T), []) => Var v 
    2.20 @@ -183,6 +190,7 @@
    2.21      val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const)
    2.22      val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt
    2.23      val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table
    2.24 +      |> declare_consts [@{const_name "Groups.zero_class.zero"}, @{const_name "Suc"}]
    2.25      fun translate_intro intro =
    2.26        let
    2.27          val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro)