# HG changeset patch
# User blanchet
# Date 1233924199 -3600
# Node ID 07f53494cf2075be4d823d8ab59b24094e3bf11d
# Parent  d201a838d0f7e16e7570899c97b0594483f3067f
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.

diff -r d201a838d0f7 -r 07f53494cf20 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Wed Feb 04 18:10:07 2009 +0100
+++ b/src/HOL/Main.thy	Fri Feb 06 13:43:19 2009 +0100
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Plain Code_Eval Map Nat_Int_Bij Recdef
+imports Plain Code_Eval Map Nat_Int_Bij Recdef SAT
 begin
 
 text {*
diff -r d201a838d0f7 -r 07f53494cf20 src/HOL/Plain.thy
--- a/src/HOL/Plain.thy	Wed Feb 04 18:10:07 2009 +0100
+++ b/src/HOL/Plain.thy	Fri Feb 06 13:43:19 2009 +0100
@@ -1,7 +1,7 @@
 header {* Plain HOL *}
 
 theory Plain
-imports Datatype FunDef Record SAT Extraction Divides
+imports Datatype FunDef Record Extraction Divides
 begin
 
 text {*
diff -r d201a838d0f7 -r 07f53494cf20 src/HOL/Refute.thy
--- a/src/HOL/Refute.thy	Wed Feb 04 18:10:07 2009 +0100
+++ b/src/HOL/Refute.thy	Fri Feb 06 13:43:19 2009 +0100
@@ -9,7 +9,7 @@
 header {* Refute *}
 
 theory Refute
-imports Inductive
+imports Hilbert_Choice List Record
 uses
   "Tools/prop_logic.ML"
   "Tools/sat_solver.ML"
diff -r d201a838d0f7 -r 07f53494cf20 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Wed Feb 04 18:10:07 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Fri Feb 06 13:43:19 2009 +0100
@@ -685,7 +685,7 @@
         Const (@{const_name False}, _) => t
       | Const (@{const_name undefined}, _) => t
       | Const (@{const_name The}, _) => t
-      | Const ("Hilbert_Choice.Eps", _) => t
+      | Const (@{const_name Hilbert_Choice.Eps}, _) => t
       | Const (@{const_name All}, _) => t
       | Const (@{const_name Ex}, _) => t
       | Const (@{const_name "op ="}, _) => t
@@ -696,8 +696,8 @@
       | Const (@{const_name Collect}, _) => t
       | Const (@{const_name "op :"}, _) => t
       (* other optimizations *)
-      | Const ("Finite_Set.card", _) => t
-      | Const ("Finite_Set.finite", _) => t
+      | Const (@{const_name Finite_Set.card}, _) => t
+      | Const (@{const_name Finite_Set.finite}, _) => t
       | Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
       | Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
@@ -706,11 +706,11 @@
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
       | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
-      | Const ("List.append", _) => t
+      | Const (@{const_name List.append}, _) => t
       | Const (@{const_name lfp}, _) => t
       | Const (@{const_name gfp}, _) => t
-      | Const ("Product_Type.fst", _) => t
-      | Const ("Product_Type.snd", _) => t
+      | Const (@{const_name fst}, _) => t
+      | Const (@{const_name snd}, _) => t
       (* simply-typed lambda calculus *)
       | Const (s, T) =>
         (if is_IDT_constructor thy (s, T)
@@ -726,7 +726,8 @@
           (* check this.  However, getting this really right seems   *)
           (* difficult because the user may state arbitrary axioms,  *)
           (* which could interact with overloading to create loops.  *)
-          ((*Output.immediate_output (" unfolding: " ^ axname);*)unfold_loop rhs)
+          ((*Output.immediate_output (" unfolding: " ^ axname);*)
+           unfold_loop rhs)
         | NONE => t)
       | Free _           => t
       | Var _            => t
@@ -864,9 +865,9 @@
         in
           collect_this_axiom ("HOL.the_eq_trivial", ax) axs
         end
-      | Const ("Hilbert_Choice.Eps", T) =>
+      | Const (@{const_name Hilbert_Choice.Eps}, T) =>
         let
-          val ax = specialize_type thy ("Hilbert_Choice.Eps", T)
+          val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T)
             (the (AList.lookup (op =) axioms "Hilbert_Choice.someI"))
         in
           collect_this_axiom ("Hilbert_Choice.someI", ax) axs
@@ -881,8 +882,9 @@
       | Const (@{const_name Collect}, T) => collect_type_axioms (axs, T)
       | Const (@{const_name "op :"}, T) => collect_type_axioms (axs, T)
       (* other optimizations *)
-      | Const ("Finite_Set.card", T) => collect_type_axioms (axs, T)
-      | Const ("Finite_Set.finite", T) => collect_type_axioms (axs, T)
+      | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms (axs, T)
+      | Const (@{const_name Finite_Set.finite}, T) =>
+        collect_type_axioms (axs, T)
       | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
           collect_type_axioms (axs, T)
@@ -895,11 +897,11 @@
       | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
           collect_type_axioms (axs, T)
-      | Const ("List.append", T) => collect_type_axioms (axs, T)
+      | Const (@{const_name List.append}, T) => collect_type_axioms (axs, T)
       | Const (@{const_name lfp}, T) => collect_type_axioms (axs, T)
       | Const (@{const_name gfp}, T) => collect_type_axioms (axs, T)
-      | Const ("Product_Type.fst", T) => collect_type_axioms (axs, T)
-      | Const ("Product_Type.snd", T) => collect_type_axioms (axs, T)
+      | Const (@{const_name fst}, T) => collect_type_axioms (axs, T)
+      | Const (@{const_name snd}, T) => collect_type_axioms (axs, T)
       (* simply-typed lambda calculus *)
       | Const (s, T) =>
           if is_const_of_class thy (s, T) then
@@ -1316,9 +1318,12 @@
     (* interpretation which includes values for the (formerly)           *)
     (* quantified variables.                                             *)
     (* maps  !!x1...xn. !xk...xm. t   to   t  *)
-    fun strip_all_body (Const (@{const_name all}, _) $ Abs (_, _, t)) = strip_all_body t
-      | strip_all_body (Const (@{const_name Trueprop}, _) $ t) = strip_all_body t
-      | strip_all_body (Const (@{const_name All}, _) $ Abs (_, _, t)) = strip_all_body t
+    fun strip_all_body (Const (@{const_name all}, _) $ Abs (_, _, t)) =
+        strip_all_body t
+      | strip_all_body (Const (@{const_name Trueprop}, _) $ t) =
+        strip_all_body t
+      | strip_all_body (Const (@{const_name All}, _) $ Abs (_, _, t)) =
+        strip_all_body t
       | strip_all_body t = t
     (* maps  !!x1...xn. !xk...xm. t   to   [x1, ..., xn, xk, ..., xm]  *)
     fun strip_all_vars (Const (@{const_name all}, _) $ Abs (a, T, t)) =
@@ -1665,7 +1670,8 @@
       fun interpret_groundtype () =
       let
         (* the model must specify a size for ground types *)
-        val size = if T = Term.propT then 2 else the (AList.lookup (op =) typs T)
+        val size = if T = Term.propT then 2
+          else the (AList.lookup (op =) typs T)
         val next = next_idx+size
         (* check if 'maxvars' is large enough *)
         val _    = (if next-1>maxvars andalso maxvars>0 then
@@ -2662,7 +2668,7 @@
 
   fun Finite_Set_card_interpreter thy model args t =
     case t of
-      Const ("Finite_Set.card",
+      Const (@{const_name Finite_Set.card},
         Type ("fun", [Type ("set", [T]), Type ("nat", [])])) =>
       let
         (* interpretation -> int *)
@@ -2709,12 +2715,12 @@
 
   fun Finite_Set_finite_interpreter thy model args t =
     case t of
-      Const ("Finite_Set.finite",
+      Const (@{const_name Finite_Set.finite},
         Type ("fun", [Type ("set", [T]), Type ("bool", [])])) $ _ =>
         (* we only consider finite models anyway, hence EVERY set is *)
         (* "finite"                                                  *)
         SOME (TT, model, args)
-    | Const ("Finite_Set.finite",
+    | Const (@{const_name Finite_Set.finite},
         Type ("fun", [Type ("set", [T]), Type ("bool", [])])) =>
       let
         val size_of_set = size_of_type thy model (Type ("set", [T]))
@@ -2848,7 +2854,7 @@
 
   fun List_append_interpreter thy model args t =
     case t of
-      Const ("List.append", Type ("fun", [Type ("List.list", [T]), Type ("fun",
+      Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun",
         [Type ("List.list", [_]), Type ("List.list", [_])])])) =>
       let
         val size_elem   = size_of_type thy model T
@@ -3044,7 +3050,7 @@
 
   fun Product_Type_fst_interpreter thy model args t =
     case t of
-      Const ("Product_Type.fst", Type ("fun", [Type ("*", [T, U]), _])) =>
+      Const (@{const_name fst}, Type ("fun", [Type ("*", [T, U]), _])) =>
       let
         val constants_T = make_constants thy model T
         val size_U      = size_of_type thy model U
@@ -3064,7 +3070,7 @@
 
   fun Product_Type_snd_interpreter thy model args t =
     case t of
-      Const ("Product_Type.snd", Type ("fun", [Type ("*", [T, U]), _])) =>
+      Const (@{const_name snd}, Type ("fun", [Type ("*", [T, U]), _])) =>
       let
         val size_T      = size_of_type thy model T
         val constants_U = make_constants thy model U