Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
authorblanchet
Fri Feb 06 13:43:19 2009 +0100 (2009-02-06)
changeset 2982007f53494cf20
parent 29802 d201a838d0f7
child 29821 ab8c54355f2e
child 29863 dadad1831e9d
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
find/fix Product_Type.{fst,snd}, which are now called simply fst and snd.
src/HOL/Main.thy
src/HOL/Plain.thy
src/HOL/Refute.thy
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Main.thy	Wed Feb 04 18:10:07 2009 +0100
     1.2 +++ b/src/HOL/Main.thy	Fri Feb 06 13:43:19 2009 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  header {* Main HOL *}
     1.5  
     1.6  theory Main
     1.7 -imports Plain Code_Eval Map Nat_Int_Bij Recdef
     1.8 +imports Plain Code_Eval Map Nat_Int_Bij Recdef SAT
     1.9  begin
    1.10  
    1.11  text {*
     2.1 --- a/src/HOL/Plain.thy	Wed Feb 04 18:10:07 2009 +0100
     2.2 +++ b/src/HOL/Plain.thy	Fri Feb 06 13:43:19 2009 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  header {* Plain HOL *}
     2.5  
     2.6  theory Plain
     2.7 -imports Datatype FunDef Record SAT Extraction Divides
     2.8 +imports Datatype FunDef Record Extraction Divides
     2.9  begin
    2.10  
    2.11  text {*
     3.1 --- a/src/HOL/Refute.thy	Wed Feb 04 18:10:07 2009 +0100
     3.2 +++ b/src/HOL/Refute.thy	Fri Feb 06 13:43:19 2009 +0100
     3.3 @@ -9,7 +9,7 @@
     3.4  header {* Refute *}
     3.5  
     3.6  theory Refute
     3.7 -imports Inductive
     3.8 +imports Hilbert_Choice List Record
     3.9  uses
    3.10    "Tools/prop_logic.ML"
    3.11    "Tools/sat_solver.ML"
     4.1 --- a/src/HOL/Tools/refute.ML	Wed Feb 04 18:10:07 2009 +0100
     4.2 +++ b/src/HOL/Tools/refute.ML	Fri Feb 06 13:43:19 2009 +0100
     4.3 @@ -685,7 +685,7 @@
     4.4          Const (@{const_name False}, _) => t
     4.5        | Const (@{const_name undefined}, _) => t
     4.6        | Const (@{const_name The}, _) => t
     4.7 -      | Const ("Hilbert_Choice.Eps", _) => t
     4.8 +      | Const (@{const_name Hilbert_Choice.Eps}, _) => t
     4.9        | Const (@{const_name All}, _) => t
    4.10        | Const (@{const_name Ex}, _) => t
    4.11        | Const (@{const_name "op ="}, _) => t
    4.12 @@ -696,8 +696,8 @@
    4.13        | Const (@{const_name Collect}, _) => t
    4.14        | Const (@{const_name "op :"}, _) => t
    4.15        (* other optimizations *)
    4.16 -      | Const ("Finite_Set.card", _) => t
    4.17 -      | Const ("Finite_Set.finite", _) => t
    4.18 +      | Const (@{const_name Finite_Set.card}, _) => t
    4.19 +      | Const (@{const_name Finite_Set.finite}, _) => t
    4.20        | Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
    4.21          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
    4.22        | Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
    4.23 @@ -706,11 +706,11 @@
    4.24          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
    4.25        | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
    4.26          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
    4.27 -      | Const ("List.append", _) => t
    4.28 +      | Const (@{const_name List.append}, _) => t
    4.29        | Const (@{const_name lfp}, _) => t
    4.30        | Const (@{const_name gfp}, _) => t
    4.31 -      | Const ("Product_Type.fst", _) => t
    4.32 -      | Const ("Product_Type.snd", _) => t
    4.33 +      | Const (@{const_name fst}, _) => t
    4.34 +      | Const (@{const_name snd}, _) => t
    4.35        (* simply-typed lambda calculus *)
    4.36        | Const (s, T) =>
    4.37          (if is_IDT_constructor thy (s, T)
    4.38 @@ -726,7 +726,8 @@
    4.39            (* check this.  However, getting this really right seems   *)
    4.40            (* difficult because the user may state arbitrary axioms,  *)
    4.41            (* which could interact with overloading to create loops.  *)
    4.42 -          ((*Output.immediate_output (" unfolding: " ^ axname);*)unfold_loop rhs)
    4.43 +          ((*Output.immediate_output (" unfolding: " ^ axname);*)
    4.44 +           unfold_loop rhs)
    4.45          | NONE => t)
    4.46        | Free _           => t
    4.47        | Var _            => t
    4.48 @@ -864,9 +865,9 @@
    4.49          in
    4.50            collect_this_axiom ("HOL.the_eq_trivial", ax) axs
    4.51          end
    4.52 -      | Const ("Hilbert_Choice.Eps", T) =>
    4.53 +      | Const (@{const_name Hilbert_Choice.Eps}, T) =>
    4.54          let
    4.55 -          val ax = specialize_type thy ("Hilbert_Choice.Eps", T)
    4.56 +          val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T)
    4.57              (the (AList.lookup (op =) axioms "Hilbert_Choice.someI"))
    4.58          in
    4.59            collect_this_axiom ("Hilbert_Choice.someI", ax) axs
    4.60 @@ -881,8 +882,9 @@
    4.61        | Const (@{const_name Collect}, T) => collect_type_axioms (axs, T)
    4.62        | Const (@{const_name "op :"}, T) => collect_type_axioms (axs, T)
    4.63        (* other optimizations *)
    4.64 -      | Const ("Finite_Set.card", T) => collect_type_axioms (axs, T)
    4.65 -      | Const ("Finite_Set.finite", T) => collect_type_axioms (axs, T)
    4.66 +      | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms (axs, T)
    4.67 +      | Const (@{const_name Finite_Set.finite}, T) =>
    4.68 +        collect_type_axioms (axs, T)
    4.69        | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []),
    4.70          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
    4.71            collect_type_axioms (axs, T)
    4.72 @@ -895,11 +897,11 @@
    4.73        | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []),
    4.74          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
    4.75            collect_type_axioms (axs, T)
    4.76 -      | Const ("List.append", T) => collect_type_axioms (axs, T)
    4.77 +      | Const (@{const_name List.append}, T) => collect_type_axioms (axs, T)
    4.78        | Const (@{const_name lfp}, T) => collect_type_axioms (axs, T)
    4.79        | Const (@{const_name gfp}, T) => collect_type_axioms (axs, T)
    4.80 -      | Const ("Product_Type.fst", T) => collect_type_axioms (axs, T)
    4.81 -      | Const ("Product_Type.snd", T) => collect_type_axioms (axs, T)
    4.82 +      | Const (@{const_name fst}, T) => collect_type_axioms (axs, T)
    4.83 +      | Const (@{const_name snd}, T) => collect_type_axioms (axs, T)
    4.84        (* simply-typed lambda calculus *)
    4.85        | Const (s, T) =>
    4.86            if is_const_of_class thy (s, T) then
    4.87 @@ -1316,9 +1318,12 @@
    4.88      (* interpretation which includes values for the (formerly)           *)
    4.89      (* quantified variables.                                             *)
    4.90      (* maps  !!x1...xn. !xk...xm. t   to   t  *)
    4.91 -    fun strip_all_body (Const (@{const_name all}, _) $ Abs (_, _, t)) = strip_all_body t
    4.92 -      | strip_all_body (Const (@{const_name Trueprop}, _) $ t) = strip_all_body t
    4.93 -      | strip_all_body (Const (@{const_name All}, _) $ Abs (_, _, t)) = strip_all_body t
    4.94 +    fun strip_all_body (Const (@{const_name all}, _) $ Abs (_, _, t)) =
    4.95 +        strip_all_body t
    4.96 +      | strip_all_body (Const (@{const_name Trueprop}, _) $ t) =
    4.97 +        strip_all_body t
    4.98 +      | strip_all_body (Const (@{const_name All}, _) $ Abs (_, _, t)) =
    4.99 +        strip_all_body t
   4.100        | strip_all_body t = t
   4.101      (* maps  !!x1...xn. !xk...xm. t   to   [x1, ..., xn, xk, ..., xm]  *)
   4.102      fun strip_all_vars (Const (@{const_name all}, _) $ Abs (a, T, t)) =
   4.103 @@ -1665,7 +1670,8 @@
   4.104        fun interpret_groundtype () =
   4.105        let
   4.106          (* the model must specify a size for ground types *)
   4.107 -        val size = if T = Term.propT then 2 else the (AList.lookup (op =) typs T)
   4.108 +        val size = if T = Term.propT then 2
   4.109 +          else the (AList.lookup (op =) typs T)
   4.110          val next = next_idx+size
   4.111          (* check if 'maxvars' is large enough *)
   4.112          val _    = (if next-1>maxvars andalso maxvars>0 then
   4.113 @@ -2662,7 +2668,7 @@
   4.114  
   4.115    fun Finite_Set_card_interpreter thy model args t =
   4.116      case t of
   4.117 -      Const ("Finite_Set.card",
   4.118 +      Const (@{const_name Finite_Set.card},
   4.119          Type ("fun", [Type ("set", [T]), Type ("nat", [])])) =>
   4.120        let
   4.121          (* interpretation -> int *)
   4.122 @@ -2709,12 +2715,12 @@
   4.123  
   4.124    fun Finite_Set_finite_interpreter thy model args t =
   4.125      case t of
   4.126 -      Const ("Finite_Set.finite",
   4.127 +      Const (@{const_name Finite_Set.finite},
   4.128          Type ("fun", [Type ("set", [T]), Type ("bool", [])])) $ _ =>
   4.129          (* we only consider finite models anyway, hence EVERY set is *)
   4.130          (* "finite"                                                  *)
   4.131          SOME (TT, model, args)
   4.132 -    | Const ("Finite_Set.finite",
   4.133 +    | Const (@{const_name Finite_Set.finite},
   4.134          Type ("fun", [Type ("set", [T]), Type ("bool", [])])) =>
   4.135        let
   4.136          val size_of_set = size_of_type thy model (Type ("set", [T]))
   4.137 @@ -2848,7 +2854,7 @@
   4.138  
   4.139    fun List_append_interpreter thy model args t =
   4.140      case t of
   4.141 -      Const ("List.append", Type ("fun", [Type ("List.list", [T]), Type ("fun",
   4.142 +      Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun",
   4.143          [Type ("List.list", [_]), Type ("List.list", [_])])])) =>
   4.144        let
   4.145          val size_elem   = size_of_type thy model T
   4.146 @@ -3044,7 +3050,7 @@
   4.147  
   4.148    fun Product_Type_fst_interpreter thy model args t =
   4.149      case t of
   4.150 -      Const ("Product_Type.fst", Type ("fun", [Type ("*", [T, U]), _])) =>
   4.151 +      Const (@{const_name fst}, Type ("fun", [Type ("*", [T, U]), _])) =>
   4.152        let
   4.153          val constants_T = make_constants thy model T
   4.154          val size_U      = size_of_type thy model U
   4.155 @@ -3064,7 +3070,7 @@
   4.156  
   4.157    fun Product_Type_snd_interpreter thy model args t =
   4.158      case t of
   4.159 -      Const ("Product_Type.snd", Type ("fun", [Type ("*", [T, U]), _])) =>
   4.160 +      Const (@{const_name snd}, Type ("fun", [Type ("*", [T, U]), _])) =>
   4.161        let
   4.162          val size_T      = size_of_type thy model T
   4.163          val constants_U = make_constants thy model U