--- 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