src/HOL/Nitpick_Examples/minipick.ML
changeset 46092 287a3cefc21b
parent 45128 5af3a3203a76
child 49026 72dcf53c1ee4
     1.1 --- a/src/HOL/Nitpick_Examples/minipick.ML	Tue Jan 03 18:33:18 2012 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/minipick.ML	Tue Jan 03 18:33:18 2012 +0100
     1.3 @@ -32,8 +32,10 @@
     1.4    | check_type _ _ (TFree (_, @{sort "{}"})) = ()
     1.5    | check_type _ _ (TFree (_, @{sort HOL.type})) = ()
     1.6    | check_type ctxt raw_infinite T =
     1.7 -    if raw_infinite T then ()
     1.8 -    else raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
     1.9 +    if raw_infinite T then
    1.10 +      ()
    1.11 +    else
    1.12 +      error ("Not supported: Type " ^ quote (Syntax.string_of_typ ctxt T) ^ ".")
    1.13  
    1.14  fun atom_schema_of S_Rep card (Type (@{type_name fun}, [T1, T2])) =
    1.15      replicate_list (card T1) (atom_schema_of S_Rep card T2)
    1.16 @@ -160,6 +162,7 @@
    1.17         | @{const HOL.disj} $ t1 $ t2 => Or (to_F pos Ts t1, to_F pos Ts t2)
    1.18         | @{const HOL.implies} $ t1 $ t2 =>
    1.19           Implies (to_F (Option.map not pos) Ts t1, to_F pos Ts t2)
    1.20 +       | Const (@{const_name Set.member}, _) $ t1 $ t2 => to_F pos Ts (t2 $ t1)
    1.21         | t1 $ t2 =>
    1.22           (case pos of
    1.23              NONE => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
    1.24 @@ -225,6 +228,11 @@
    1.25         | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
    1.26         | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
    1.27         | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
    1.28 +       | Const (@{const_name Set.member}, _) $ _ =>
    1.29 +         to_R_rep Ts (eta_expand Ts t 1)
    1.30 +       | Const (@{const_name Set.member}, _) => to_R_rep Ts (eta_expand Ts t 2)
    1.31 +       | Const (@{const_name Collect}, _) $ t' => to_R_rep Ts t'
    1.32 +       | Const (@{const_name Collect}, _) => to_R_rep Ts (eta_expand Ts t 1)
    1.33         | Const (@{const_name bot_class.bot},
    1.34                  T as Type (@{type_name fun}, [T', @{typ bool}])) =>
    1.35           if total then empty_n_ary_rel (arity_of (R_Rep total) card T)
    1.36 @@ -272,7 +280,7 @@
    1.37                        Product (true_core_kt, true_atom))
    1.38               end
    1.39           else
    1.40 -           raise NOT_SUPPORTED "transitive closure for function or pair type"
    1.41 +           error "Not supported: Transitive closure for function or pair type."
    1.42         | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
    1.43         | Const (@{const_name inf_class.inf},
    1.44                  Type (@{type_name fun},
    1.45 @@ -319,7 +327,7 @@
    1.46         | @{const True} => true_atom
    1.47         | Free (x as (_, T)) =>
    1.48           Rel (arity_of (R_Rep total) card T, find_index (curry (op =) x) frees)
    1.49 -       | Term.Var _ => raise NOT_SUPPORTED "schematic variables"
    1.50 +       | Term.Var _ => error "Not supported: Schematic variables."
    1.51         | Bound _ => raise SAME ()
    1.52         | Abs (_, T, t') =>
    1.53           (case (total, fastype_of1 (T :: Ts, t')) of
    1.54 @@ -353,8 +361,8 @@
    1.55                        num_seq arity2 res_arity)
    1.56                  end
    1.57              end)
    1.58 -       | _ => raise NOT_SUPPORTED ("term " ^
    1.59 -                                   quote (Syntax.string_of_term ctxt t)))
    1.60 +       | _ => error ("Not supported: Term " ^
    1.61 +                     quote (Syntax.string_of_term ctxt t) ^ "."))
    1.62        handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
    1.63    in to_F (if total then NONE else SOME true) [] end
    1.64  
    1.65 @@ -379,6 +387,11 @@
    1.66    declarative_axiom_for_rel_expr total card [] T
    1.67        (Rel (arity_of (R_Rep total) card T, i))
    1.68  
    1.69 +(* Hack to make the old code work as is with sets. *)
    1.70 +fun unsetify_type (Type (@{type_name set}, [T])) = unsetify_type T --> bool_T
    1.71 +  | unsetify_type (Type (s, Ts)) = Type (s, map unsetify_type Ts)
    1.72 +  | unsetify_type T = T
    1.73 +
    1.74  fun kodkod_problem_from_term ctxt total raw_card raw_infinite t =
    1.75    let
    1.76      val thy = Proof_Context.theory_of ctxt
    1.77 @@ -395,7 +408,9 @@
    1.78          complete T1 andalso concrete T2
    1.79        | concrete (Type (@{type_name prod}, Ts)) = forall concrete Ts
    1.80        | concrete _ = true
    1.81 -    val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
    1.82 +    val neg_t =
    1.83 +      @{const Not} $ Object_Logic.atomize_term thy t
    1.84 +      |> map_types unsetify_type
    1.85      val _ = fold_types (K o check_type ctxt raw_infinite) neg_t ()
    1.86      val frees = Term.add_frees neg_t []
    1.87      val bounds =