src/HOL/Library/refute.ML
changeset 58109 6d4695335d41
parent 57820 b510819d58ee
child 58120 a14b8d77b15a
     1.1 --- a/src/HOL/Library/refute.ML	Mon Sep 01 16:17:46 2014 +0200
     1.2 +++ b/src/HOL/Library/refute.ML	Mon Sep 01 16:17:46 2014 +0200
     1.3 @@ -575,10 +575,6 @@
     1.4        | Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
     1.5            Type ("fun", [@{typ nat}, @{typ nat}])])) => t
     1.6        | Const (@{const_name 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 @@ -765,10 +761,6 @@
    1.15          Type ("fun", [@{typ nat}, @{typ nat}])])) =>
    1.16            collect_type_axioms T axs
    1.17        | Const (@{const_name 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 @@ -2709,97 +2701,6 @@
    1.26        end
    1.27    | _ => NONE;
    1.28  
    1.29 -(* only an optimization: 'lfp' could in principle be interpreted with  *)
    1.30 -(* interpreters available already (using its definition), but the code *)
    1.31 -(* below is more efficient                                             *)
    1.32 -
    1.33 -fun lfp_interpreter ctxt model args t =
    1.34 -  case t of
    1.35 -    Const (@{const_name lfp}, Type ("fun", [Type ("fun",
    1.36 -      [Type (@{type_name set}, [T]),
    1.37 -       Type (@{type_name set}, [_])]),
    1.38 -       Type (@{type_name set}, [_])])) =>
    1.39 -      let
    1.40 -        val size_elem = size_of_type ctxt model T
    1.41 -        (* the universe (i.e. the set that contains every element) *)
    1.42 -        val i_univ = Node (replicate size_elem TT)
    1.43 -        (* all sets with elements from type 'T' *)
    1.44 -        val i_sets = make_constants ctxt model (HOLogic.mk_setT T)
    1.45 -        (* all functions that map sets to sets *)
    1.46 -        val i_funs = make_constants ctxt model (Type ("fun",
    1.47 -          [HOLogic.mk_setT T, HOLogic.mk_setT T]))
    1.48 -        (* "lfp(f) == Inter({u. f(u) <= u})" *)
    1.49 -        fun is_subset (Node subs, Node sups) =
    1.50 -              forall (fn (sub, sup) => (sub = FF) orelse (sup = TT)) (subs ~~ sups)
    1.51 -          | is_subset (_, _) =
    1.52 -              raise REFUTE ("lfp_interpreter",
    1.53 -                "is_subset: interpretation for set is not a node")
    1.54 -        fun intersection (Node xs, Node ys) =
    1.55 -              Node (map (fn (x, y) => if x=TT andalso y=TT then TT else FF)
    1.56 -                (xs ~~ ys))
    1.57 -          | intersection (_, _) =
    1.58 -              raise REFUTE ("lfp_interpreter",
    1.59 -                "intersection: interpretation for set is not a node")
    1.60 -        fun lfp (Node resultsets) =
    1.61 -              fold (fn (set, resultset) => fn acc =>
    1.62 -                if is_subset (resultset, set) then
    1.63 -                  intersection (acc, set)
    1.64 -                else
    1.65 -                  acc) (i_sets ~~ resultsets) i_univ
    1.66 -          | lfp _ =
    1.67 -              raise REFUTE ("lfp_interpreter",
    1.68 -                "lfp: interpretation for function is not a node")
    1.69 -      in
    1.70 -        SOME (Node (map lfp i_funs), model, args)
    1.71 -      end
    1.72 -  | _ => NONE;
    1.73 -
    1.74 -(* only an optimization: 'gfp' could in principle be interpreted with  *)
    1.75 -(* interpreters available already (using its definition), but the code *)
    1.76 -(* below is more efficient                                             *)
    1.77 -
    1.78 -fun gfp_interpreter ctxt model args t =
    1.79 -  case t of
    1.80 -    Const (@{const_name gfp}, Type ("fun", [Type ("fun",
    1.81 -      [Type (@{type_name set}, [T]),
    1.82 -       Type (@{type_name set}, [_])]),
    1.83 -       Type (@{type_name set}, [_])])) =>
    1.84 -      let
    1.85 -        val size_elem = size_of_type ctxt model T
    1.86 -        (* the universe (i.e. the set that contains every element) *)
    1.87 -        val i_univ = Node (replicate size_elem TT)
    1.88 -        (* all sets with elements from type 'T' *)
    1.89 -        val i_sets = make_constants ctxt model (HOLogic.mk_setT T)
    1.90 -        (* all functions that map sets to sets *)
    1.91 -        val i_funs = make_constants ctxt model (Type ("fun",
    1.92 -          [HOLogic.mk_setT T, HOLogic.mk_setT T]))
    1.93 -        (* "gfp(f) == Union({u. u <= f(u)})" *)
    1.94 -        fun is_subset (Node subs, Node sups) =
    1.95 -              forall (fn (sub, sup) => (sub = FF) orelse (sup = TT))
    1.96 -                (subs ~~ sups)
    1.97 -          | is_subset (_, _) =
    1.98 -              raise REFUTE ("gfp_interpreter",
    1.99 -                "is_subset: interpretation for set is not a node")
   1.100 -        fun union (Node xs, Node ys) =
   1.101 -              Node (map (fn (x,y) => if x=TT orelse y=TT then TT else FF)
   1.102 -                   (xs ~~ ys))
   1.103 -          | union (_, _) =
   1.104 -              raise REFUTE ("gfp_interpreter",
   1.105 -                "union: interpretation for set is not a node")
   1.106 -        fun gfp (Node resultsets) =
   1.107 -              fold (fn (set, resultset) => fn acc =>
   1.108 -                if is_subset (set, resultset) then
   1.109 -                  union (acc, set)
   1.110 -                else
   1.111 -                  acc) (i_sets ~~ resultsets) i_univ
   1.112 -          | gfp _ =
   1.113 -              raise REFUTE ("gfp_interpreter",
   1.114 -                "gfp: interpretation for function is not a node")
   1.115 -      in
   1.116 -        SOME (Node (map gfp i_funs), model, args)
   1.117 -      end
   1.118 -  | _ => NONE;
   1.119 -
   1.120  (* only an optimization: 'fst' could in principle be interpreted with  *)
   1.121  (* interpreters available already (using its definition), but the code *)
   1.122  (* below is more efficient                                             *)
   1.123 @@ -3053,10 +2954,6 @@
   1.124     add_interpreter "Nat_HOL.minus"      Nat_minus_interpreter #>
   1.125     add_interpreter "Nat_HOL.times"      Nat_times_interpreter #>
   1.126     add_interpreter "List.append" List_append_interpreter #>
   1.127 -(* UNSOUND
   1.128 -   add_interpreter "lfp" lfp_interpreter #>
   1.129 -   add_interpreter "gfp" gfp_interpreter #>
   1.130 -*)
   1.131     add_interpreter "Product_Type.prod.fst" Product_Type_fst_interpreter #>
   1.132     add_interpreter "Product_Type.prod.snd" Product_Type_snd_interpreter #>
   1.133     add_printer "stlc" stlc_printer #>