merged
authorwenzelm
Thu, 07 Apr 2011 18:41:49 +0200
changeset 42276 992892b48296
parent 42275 79be89e07589 (diff)
parent 42268 01401287c3f7 (current diff)
child 42277 7503beeffd8d
child 42291 682b35dc1926
merged
src/Pure/Syntax/type_ext.ML
--- a/src/HOL/Finite_Set.thy	Thu Apr 07 18:24:59 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Apr 07 18:41:49 2011 +0200
@@ -561,14 +561,6 @@
 @{text fold_comm}, @{text fold_reindex} and @{text fold_distrib}.
 The proofs become ugly. It is not worth the effort. (???) *}
 
-
-lemma Diff1_fold_graph:
-  "fold_graph f z (A - {x}) y \<Longrightarrow> x \<in> A \<Longrightarrow> fold_graph f z A (f x y)"
-by (erule insert_Diff [THEN subst], rule fold_graph.intros, auto)
-
-lemma fold_graph_imp_finite: "fold_graph f z A x \<Longrightarrow> finite A"
-by (induct set: fold_graph) auto
-
 lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x"
 by (induct rule: finite_induct) auto
 
@@ -617,13 +609,16 @@
   "fold_graph f z A y \<Longrightarrow> fold f z A = y"
 by (unfold fold_def) (blast intro: fold_graph_determ)
 
-lemma fold_graph_fold: "finite A \<Longrightarrow> fold_graph f z A (fold f z A)"
-unfolding fold_def
-apply (rule theI')
-apply (rule ex_ex1I)
-apply (erule finite_imp_fold_graph)
-apply (erule (1) fold_graph_determ)
-done
+lemma fold_graph_fold:
+  assumes "finite A"
+  shows "fold_graph f z A (fold f z A)"
+proof -
+  from assms have "\<exists>x. fold_graph f z A x" by (rule finite_imp_fold_graph)
+  moreover note fold_graph_determ
+  ultimately have "\<exists>!x. fold_graph f z A x" by (rule ex_ex1I)
+  then have "fold_graph f z A (The (fold_graph f z A))" by (rule theI')
+  then show ?thesis by (unfold fold_def)
+qed
 
 text{* The base case for @{text fold}: *}
 
--- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Apr 07 18:24:59 2011 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Apr 07 18:41:49 2011 +0200
@@ -18,15 +18,6 @@
 class exhaustive = term_of +
 fixes exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
 
-instantiation unit :: exhaustive
-begin
-
-definition "exhaustive f d = f (Code_Evaluation.valtermify ())"
-
-instance ..
-
-end
-
 instantiation code_numeral :: exhaustive
 begin
 
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Apr 07 18:24:59 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Apr 07 18:41:49 2011 +0200
@@ -343,7 +343,7 @@
         val fixes =
           Term.add_free_names (prop_of zapped_th) []
           |> filter is_zapped_var_name
-        val ctxt' = ctxt |> Variable.add_fixes_direct fixes (*###*)
+        val ctxt' = ctxt |> Variable.add_fixes_direct fixes
         val fully_skolemized_t =
           zapped_th
           |> singleton (Variable.export ctxt' ctxt)
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 07 18:24:59 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 07 18:41:49 2011 +0200
@@ -105,7 +105,7 @@
                 | NONE =>
               case strip_prefix_and_unascii schematic_var_prefix v of
                   SOME w => SomeTerm (mk_var (w, HOLogic.typeT))
-                | NONE   => SomeTerm (mk_var (v, HOLogic.typeT)) )
+                | NONE   => SomeTerm (mk_var (v, HOLogic.typeT)))
                     (*Var from Metis with a name like _nnn; possibly a type variable*)
         | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
         | tm_to_tt (t as Metis_Term.Fn (".",_)) =
@@ -128,7 +128,7 @@
                     val nterms = length ts - ntypes
                     val tts = map tm_to_tt ts
                     val tys = types_of (List.take(tts,ntypes))
-                    val j = !new_skolem_var_count + 1
+                    val j = !new_skolem_var_count + 0 (* FIXME ### *)
                     val _ = new_skolem_var_count := j
                     val t =
                       if String.isPrefix new_skolem_const_prefix c then
@@ -594,6 +594,9 @@
   | copy_prems_tac (m :: ms) ns i =
     etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
 
+(* Metis generates variables of the form _nnn. *)
+val is_metis_fresh_variable = String.isPrefix "_"
+
 fun instantiate_forall_tac thy t i st =
   let
     val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
@@ -612,13 +615,32 @@
       | repair t = t
     val t' = t |> repair |> fold (curry absdummy) (map snd params)
     fun do_instantiate th =
-      let
-        val var = Term.add_vars (prop_of th) []
-                  |> the_single
-      in th |> term_instantiate thy [(Var var, t')] end
+      case Term.add_vars (prop_of th) []
+           |> filter_out ((Meson_Clausify.is_zapped_var_name orf
+                           is_metis_fresh_variable) o fst o fst) of
+        [] => th
+      | [var as (_, T)] =>
+        let
+          val var_binder_Ts = T |> binder_types |> take (length params) |> rev
+          val var_body_T = T |> funpow (length params) range_type
+          val tyenv =
+            Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params,
+                                             var_body_T :: var_binder_Ts)
+          val env =
+            Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
+                         tenv = Vartab.empty, tyenv = tyenv}
+          val ty_inst =
+            Vartab.fold (fn (x, (S, T)) =>
+                            cons (pairself (ctyp_of thy) (TVar (x, S), T)))
+                        tyenv []
+          val t_inst =
+            [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
+        in
+          th |> instantiate (ty_inst, t_inst)
+        end
+      | _ => raise Fail "expected a single non-zapped, non-Metis Var"
   in
-    (etac @{thm allE} i
-     THEN rotate_tac ~1 i
+    (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
      THEN PRIMITIVE do_instantiate) st
   end
 
@@ -673,7 +695,7 @@
 structure Int_Pair_Graph =
   Graph(type key = int * int val ord = prod_ord int_ord int_ord)
 
-fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no)
+fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no)
 fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)
 
 (* Attempts to derive the theorem "False" from a theorem of the form
@@ -753,32 +775,36 @@
                     Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
                                                   (Integer.add 1)) substs
         |> Int_Tysubst_Table.dest
-(* for debugging:
+(* for debugging only:
       fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
         "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
         "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
         commas (map ((fn (s, t) => s ^ " |-> " ^ t)
                      o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
+      val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
       val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
       val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
       val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
                        cat_lines (map string_for_subst_info substs))
 *)
+      fun cut_and_ex_tac axiom =
+        cut_rules_tac [axiom] 1
+        THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
       fun rotation_for_subgoal i =
         find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
     in
       Goal.prove ctxt [] [] @{prop False}
-          (K (cut_rules_tac
-                  (map (fst o the o nth axioms o fst o fst) ax_counts) 1
-              THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
-              THEN rename_tac outer_param_names 1
-              THEN copy_prems_tac (map snd ax_counts) [] 1
+          (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst
+                                  o fst) ax_counts)
+                      THEN rename_tac outer_param_names 1
+                      THEN copy_prems_tac (map snd ax_counts) [] 1)
               THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
               THEN match_tac [prems_imp_false] 1
               THEN ALLGOALS (fn i =>
                        rtac @{thm Meson.skolem_COMBK_I} i
                        THEN rotate_tac (rotation_for_subgoal i) i
-                       THEN assume_tac i)))
+                       THEN assume_tac i
+                       THEN flexflex_tac)))
       handle ERROR _ =>
              error ("Cannot replay Metis proof in Isabelle:\n\
                     \Error when discharging Skolem assumptions.")
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Apr 07 18:24:59 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Apr 07 18:41:49 2011 +0200
@@ -202,7 +202,7 @@
       in fold_rev (fn f => fn t => f t) fns start_term end
     fun mk_rhs exprs =
       @{term "If :: bool => bool => bool => bool"} $ size_ge_zero $
-        (foldr1 HOLogic.mk_disj exprs) $ @{term "True"}
+        (foldr1 HOLogic.mk_conj exprs) $ @{term "True"}
     val rhss =
       Datatype_Aux.interpret_construction descr vs
         { atyp = mk_call, dtyp = mk_aux_call }
@@ -304,7 +304,7 @@
       Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T)
         $ lambda (Free (s, T)) t $ depth
     fun mk_implies (cond, then_t) =
-      @{term "If :: bool => bool => bool => bool"} $ cond $ then_t $ @{term False}
+      @{term "If :: bool => bool => bool => bool"} $ cond $ then_t $ @{term True}
     fun mk_naive_test_term t = fold_rev mk_bounded_forall (Term.add_frees t []) t 
     fun mk_smart_test_term' concl bound_frees assms =
       let
@@ -387,7 +387,7 @@
 fun compile_validator_exprs ctxt ts =
   let
     val thy = ProofContext.theory_of ctxt
-    val ts' = map (mk_validator_expr ctxt) ts;
+    val ts' = map (mk_validator_expr ctxt) ts
   in
     Code_Runtime.dynamic_value_strict
       (Validator_Batch.get, put_validator_batch, "Exhaustive_Generators.put_validator_batch")
--- a/src/Tools/quickcheck.ML	Thu Apr 07 18:24:59 2011 +0200
+++ b/src/Tools/quickcheck.ML	Thu Apr 07 18:41:49 2011 +0200
@@ -340,7 +340,7 @@
       (* FIXME: why decrement size by one? *)
       let
         val (ts, timing) = cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
-          (fn () => fst (test_fun [card - 1, size - 1]))
+          (fn () => fst (test_fun [card, size - 1]))
         val _ = add_timing timing current_result
       in
         Option.map (pair card) ts