src/HOL/Tools/refute.ML
changeset 36130 9a672f7d488d
parent 35746 9c97d4e2450e
child 36374 19c0c4b8b445
     1.1 --- a/src/HOL/Tools/refute.ML	Tue Apr 13 14:08:58 2010 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Tue Apr 13 15:16:54 2010 +0200
     1.3 @@ -717,8 +717,10 @@
     1.4        | Const (@{const_name Groups.times}, Type ("fun", [Type ("nat", []),
     1.5          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
     1.6        | Const (@{const_name List.append}, _) => t
     1.7 +(* UNSOUND
     1.8        | Const (@{const_name lfp}, _) => t
     1.9        | Const (@{const_name gfp}, _) => t
    1.10 +*)
    1.11        | Const (@{const_name fst}, _) => t
    1.12        | Const (@{const_name snd}, _) => t
    1.13        (* simply-typed lambda calculus *)
    1.14 @@ -896,8 +898,10 @@
    1.15          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    1.16            collect_type_axioms T axs
    1.17        | Const (@{const_name List.append}, T) => collect_type_axioms T axs
    1.18 +(* UNSOUND
    1.19        | Const (@{const_name lfp}, T) => collect_type_axioms T axs
    1.20        | Const (@{const_name gfp}, T) => collect_type_axioms T axs
    1.21 +*)
    1.22        | Const (@{const_name fst}, T) => collect_type_axioms T axs
    1.23        | Const (@{const_name snd}, T) => collect_type_axioms T axs
    1.24        (* simply-typed lambda calculus *)
    1.25 @@ -2093,7 +2097,7 @@
    1.26            val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
    1.27            val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
    1.28            (* Term.term *)
    1.29 -          val HOLogic_empty_set = HOLogic.mk_set HOLogic_prodT []
    1.30 +          val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT)
    1.31            val HOLogic_insert    =
    1.32              Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
    1.33          in
    1.34 @@ -2969,6 +2973,8 @@
    1.35      | _ =>
    1.36        NONE;
    1.37  
    1.38 +(* UNSOUND
    1.39 +
    1.40    (* theory -> model -> arguments -> Term.term ->
    1.41      (interpretation * model * arguments) option *)
    1.42  
    1.43 @@ -3078,6 +3084,7 @@
    1.44        end
    1.45      | _ =>
    1.46        NONE;
    1.47 +*)
    1.48  
    1.49    (* theory -> model -> arguments -> Term.term ->
    1.50      (interpretation * model * arguments) option *)
    1.51 @@ -3163,7 +3170,7 @@
    1.52          val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
    1.53          val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
    1.54          (* Term.term *)
    1.55 -        val HOLogic_empty_set = HOLogic.mk_set HOLogic_prodT []
    1.56 +        val HOLogic_empty_set = Const (@{const_abbrev Set.empty}, HOLogic_setT)
    1.57          val HOLogic_insert    =
    1.58            Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
    1.59        in
    1.60 @@ -3313,8 +3320,10 @@
    1.61       add_interpreter "Nat_HOL.minus"      Nat_minus_interpreter #>
    1.62       add_interpreter "Nat_HOL.times"      Nat_times_interpreter #>
    1.63       add_interpreter "List.append" List_append_interpreter #>
    1.64 +(* UNSOUND
    1.65       add_interpreter "lfp" lfp_interpreter #>
    1.66       add_interpreter "gfp" gfp_interpreter #>
    1.67 +*)
    1.68       add_interpreter "fst" Product_Type_fst_interpreter #>
    1.69       add_interpreter "snd" Product_Type_snd_interpreter #>
    1.70       add_printer "stlc" stlc_printer #>