src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 34126 8a2c5d7aff51
parent 34124 c4628a1dcf75
child 34936 c4f04bee79f3
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Dec 17 15:22:27 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Dec 18 12:00:29 2009 +0100
     1.3 @@ -40,6 +40,8 @@
     1.4  open Nitpick_Rep
     1.5  open Nitpick_Nut
     1.6  
     1.7 +structure KK = Kodkod
     1.8 +
     1.9  type params = {
    1.10    show_skolems: bool,
    1.11    show_datatypes: bool,
    1.12 @@ -71,19 +73,22 @@
    1.13    else
    1.14      Const (atom_name "" T j, T)
    1.15  
    1.16 +(* term -> real *)
    1.17 +fun extract_real_number (Const (@{const_name HOL.divide}, _) $ t1 $ t2) =
    1.18 +    real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
    1.19 +  | extract_real_number t = real (snd (HOLogic.dest_number t))
    1.20  (* term * term -> order *)
    1.21  fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2)
    1.22 -  | nice_term_ord (t1, t2) =
    1.23 -    int_ord (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
    1.24 +  | nice_term_ord tp = Real.compare (pairself extract_real_number tp)
    1.25      handle TERM ("dest_number", _) =>
    1.26 -           case (t1, t2) of
    1.27 +           case tp of
    1.28               (t11 $ t12, t21 $ t22) =>
    1.29               (case nice_term_ord (t11, t21) of
    1.30                  EQUAL => nice_term_ord (t12, t22)
    1.31                | ord => ord)
    1.32 -           | _ => TermOrd.term_ord (t1, t2)
    1.33 +           | _ => TermOrd.fast_term_ord tp
    1.34  
    1.35 -(* nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list *)
    1.36 +(* nut NameTable.table -> KK.raw_bound list -> nut -> int list list *)
    1.37  fun tuple_list_for_name rel_table bounds name =
    1.38    the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
    1.39  
    1.40 @@ -240,8 +245,8 @@
    1.41    | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
    1.42  
    1.43  (* string * string * string * string -> scope -> nut list -> nut list
    1.44 -   -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> typ -> typ
    1.45 -   -> rep -> int list list -> term *)
    1.46 +   -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep
    1.47 +   -> int list list -> term *)
    1.48  fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
    1.49          ({ext_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
    1.50           : scope) sel_names rel_table bounds =
    1.51 @@ -324,7 +329,7 @@
    1.52               | _ => t
    1.53      (* bool -> typ -> typ -> typ -> term list -> term list -> term *)
    1.54      fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
    1.55 -      ts1 ~~ ts2 |> T1 = @{typ bisim_iterator} ? rev
    1.56 +      ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
    1.57                   |> make_plain_fun (maybe_opt andalso not for_auto) T1 T2
    1.58                   |> unbit_and_unbox_term
    1.59                   |> typecast_fun (unbit_and_unbox_type T')
    1.60 @@ -506,7 +511,7 @@
    1.61      oooo term_for_rep []
    1.62    end
    1.63  
    1.64 -(* scope -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> nut
    1.65 +(* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
    1.66     -> term *)
    1.67  fun term_for_name scope sel_names rel_table bounds name =
    1.68    let val T = type_of name in
    1.69 @@ -563,7 +568,7 @@
    1.70      end
    1.71  
    1.72  (* params -> scope -> (term option * int list) list -> styp list -> nut list
    1.73 -  -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
    1.74 +  -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
    1.75    -> Pretty.T * bool *)
    1.76  fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
    1.77          ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
    1.78 @@ -704,7 +709,7 @@
    1.79    end
    1.80  
    1.81  (* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
    1.82 -   -> Kodkod.raw_bound list -> term -> bool option *)
    1.83 +   -> KK.raw_bound list -> term -> bool option *)
    1.84  fun prove_hol_model (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns, ...})
    1.85                      auto_timeout free_names sel_names rel_table bounds prop =
    1.86    let