--- a/Admin/churn Fri Oct 29 16:16:10 2010 +0200
+++ b/Admin/churn Fri Oct 29 16:51:20 2010 +0200
@@ -2,4 +2,4 @@
ADMIN="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; pwd)"
cd "$ADMIN"
-hg churn --aliases user-aliases --progress
+hg churn --aliases user-aliases
--- a/Admin/user-aliases Fri Oct 29 16:16:10 2010 +0200
+++ b/Admin/user-aliases Fri Oct 29 16:51:20 2010 +0200
@@ -7,3 +7,8 @@
immler@in.tum.de immler
tsewell@rubicon.NSW.bigpond.net.au tsewell
tsewell@nicta.com.au tsewell
+kaliszyk@in.tum.de kaliszyk
+Philipp\ Meyer meyerp
+Timothy\ Bourke tbourke
+noschinl@in.tum.de noschinl
+brianh@cs.pdx.edu huffman
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Oct 29 16:16:10 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Oct 29 16:51:20 2010 +0200
@@ -16,6 +16,10 @@
and transform the heap, or fail *}
datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
+lemma [code, code del]:
+ "(Code_Evaluation.term_of :: 'a::typerep Heap \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of"
+ ..
+
primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where
[code del]: "execute (Heap f) = f"
@@ -398,6 +402,82 @@
ultimately show ?case by (simp, simp only: execute_bind(1), simp add: execute_simps)
qed
+
+subsection {* Partial function definition setup *}
+
+definition Heap_ord :: "'a Heap \<Rightarrow> 'a Heap \<Rightarrow> bool" where
+ "Heap_ord = img_ord execute (fun_ord option_ord)"
+
+definition Heap_lub :: "('a Heap \<Rightarrow> bool) \<Rightarrow> 'a Heap" where
+ "Heap_lub = img_lub execute Heap (fun_lub (flat_lub None))"
+
+interpretation heap!: partial_function_definitions Heap_ord Heap_lub
+proof -
+ have "partial_function_definitions (fun_ord option_ord) (fun_lub (flat_lub None))"
+ by (rule partial_function_lift) (rule flat_interpretation)
+ then have "partial_function_definitions (img_ord execute (fun_ord option_ord))
+ (img_lub execute Heap (fun_lub (flat_lub None)))"
+ by (rule partial_function_image) (auto intro: Heap_eqI)
+ then show "partial_function_definitions Heap_ord Heap_lub"
+ by (simp only: Heap_ord_def Heap_lub_def)
+qed
+
+abbreviation "mono_Heap \<equiv> monotone (fun_ord Heap_ord) Heap_ord"
+
+lemma Heap_ordI:
+ assumes "\<And>h. execute x h = None \<or> execute x h = execute y h"
+ shows "Heap_ord x y"
+ using assms unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def
+ by blast
+
+lemma Heap_ordE:
+ assumes "Heap_ord x y"
+ obtains "execute x h = None" | "execute x h = execute y h"
+ using assms unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def
+ by atomize_elim blast
+
+lemma bind_mono[partial_function_mono]:
+ assumes mf: "mono_Heap B" and mg: "\<And>y. mono_Heap (\<lambda>f. C y f)"
+ shows "mono_Heap (\<lambda>f. B f \<guillemotright>= (\<lambda>y. C y f))"
+proof (rule monotoneI)
+ fix f g :: "'a \<Rightarrow> 'b Heap" assume fg: "fun_ord Heap_ord f g"
+ from mf
+ have 1: "Heap_ord (B f) (B g)" by (rule monotoneD) (rule fg)
+ from mg
+ have 2: "\<And>y'. Heap_ord (C y' f) (C y' g)" by (rule monotoneD) (rule fg)
+
+ have "Heap_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y. C y f))"
+ (is "Heap_ord ?L ?R")
+ proof (rule Heap_ordI)
+ fix h
+ from 1 show "execute ?L h = None \<or> execute ?L h = execute ?R h"
+ by (rule Heap_ordE[where h = h]) (auto simp: execute_bind_case)
+ qed
+ also
+ have "Heap_ord (B g \<guillemotright>= (\<lambda>y'. C y' f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))"
+ (is "Heap_ord ?L ?R")
+ proof (rule Heap_ordI)
+ fix h
+ show "execute ?L h = None \<or> execute ?L h = execute ?R h"
+ proof (cases "execute (B g) h")
+ case None
+ then have "execute ?L h = None" by (auto simp: execute_bind_case)
+ thus ?thesis ..
+ next
+ case Some
+ then obtain r h' where "execute (B g) h = Some (r, h')"
+ by (metis surjective_pairing)
+ then have "execute ?L h = execute (C r f) h'"
+ "execute ?R h = execute (C r g) h'"
+ by (auto simp: execute_bind_case)
+ with 2[of r] show ?thesis by (auto elim: Heap_ordE)
+ qed
+ qed
+ finally (heap.leq_trans)
+ show "Heap_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))" .
+qed
+
+
subsection {* Code generator setup *}
subsubsection {* Logical intermediate layer *}
@@ -593,76 +673,6 @@
*}
-
-section {* Partial function definition setup *}
-
-definition "Heap_ord = img_ord execute (fun_ord option_ord)"
-definition "Heap_lub = img_lub execute Heap (fun_lub (flat_lub None))"
-
-interpretation heap!:
- partial_function_definitions Heap_ord Heap_lub
-unfolding Heap_ord_def Heap_lub_def
-apply (rule partial_function_image)
-apply (rule partial_function_lift)
-apply (rule flat_interpretation)
-by (auto intro: Heap_eqI)
-
-abbreviation "mono_Heap \<equiv> monotone (fun_ord Heap_ord) Heap_ord"
-
-lemma Heap_ordI:
- assumes "\<And>h. execute x h = None \<or> execute x h = execute y h"
- shows "Heap_ord x y"
-using assms unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def
-by blast
-
-lemma Heap_ordE:
- assumes "Heap_ord x y"
- obtains "execute x h = None" | "execute x h = execute y h"
-using assms unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def
-by atomize_elim blast
-
-
-lemma bind_mono[partial_function_mono]:
-assumes mf: "mono_Heap B" and mg: "\<And>y. mono_Heap (\<lambda>f. C y f)"
-shows "mono_Heap (\<lambda>f. B f \<guillemotright>= (\<lambda>y. C y f))"
-proof (rule monotoneI)
- fix f g :: "'a \<Rightarrow> 'b Heap" assume fg: "fun_ord Heap_ord f g"
- from mf
- have 1: "Heap_ord (B f) (B g)" by (rule monotoneD) (rule fg)
- from mg
- have 2: "\<And>y'. Heap_ord (C y' f) (C y' g)" by (rule monotoneD) (rule fg)
-
- have "Heap_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y. C y f))"
- (is "Heap_ord ?L ?R")
- proof (rule Heap_ordI)
- fix h
- from 1 show "execute ?L h = None \<or> execute ?L h = execute ?R h"
- by (rule Heap_ordE[where h = h]) (auto simp: execute_bind_case)
- qed
- also
- have "Heap_ord (B g \<guillemotright>= (\<lambda>y'. C y' f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))"
- (is "Heap_ord ?L ?R")
- proof (rule Heap_ordI)
- fix h
- show "execute ?L h = None \<or> execute ?L h = execute ?R h"
- proof (cases "execute (B g) h")
- case None
- then have "execute ?L h = None" by (auto simp: execute_bind_case)
- thus ?thesis ..
- next
- case Some
- then obtain r h' where "execute (B g) h = Some (r, h')"
- by (metis surjective_pairing)
- then have "execute ?L h = execute (C r f) h'"
- "execute ?R h = execute (C r g) h'"
- by (auto simp: execute_bind_case)
- with 2[of r] show ?thesis by (auto elim: Heap_ordE)
- qed
- qed
- finally (heap.leq_trans)
- show "Heap_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))" .
-qed
-
hide_const (open) Heap heap guard raise' fold_map
end
--- a/src/HOL/Tools/Meson/meson.ML Fri Oct 29 16:16:10 2010 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Fri Oct 29 16:51:20 2010 +0200
@@ -111,39 +111,57 @@
SOME th => th
| NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
-(* Applying "choice" swaps the bound variable names. We tweak
- "Thm.rename_boundvars"'s input to get the desired names. *)
-fun fix_bounds (_ $ (Const (@{const_name Ex}, _)
- $ Abs (_, _, Const (@{const_name All}, _) $ _)))
- (t0 $ (Const (@{const_name All}, T1)
- $ Abs (a1, T1', Const (@{const_name Ex}, T2)
- $ Abs (a2, T2', t')))) =
- t0 $ (Const (@{const_name All}, T1)
- $ Abs (a2, T1', Const (@{const_name Ex}, T2) $ Abs (a1, T2', t')))
- | fix_bounds _ t = t
+(* Hack to make it less likely that we lose our precious bound variable names in
+ "rename_bound_vars_RS" below, because of a clash. *)
+val protect_prefix = "Meson_xyzzy"
+
+fun protect_bound_var_names (t $ u) =
+ protect_bound_var_names t $ protect_bound_var_names u
+ | protect_bound_var_names (Abs (s, T, t')) =
+ Abs (protect_prefix ^ s, T, protect_bound_var_names t')
+ | protect_bound_var_names t = t
-(* Hack to make it less likely that we lose our precious bound variable names in
- "rename_bvs_RS" below, because of a clash. *)
-val protect_prefix = "_"
+fun fix_bound_var_names old_t new_t =
+ let
+ fun quant_of @{const_name All} = SOME true
+ | quant_of @{const_name Ball} = SOME true
+ | quant_of @{const_name Ex} = SOME false
+ | quant_of @{const_name Bex} = SOME false
+ | quant_of _ = NONE
+ val flip_quant = Option.map not
+ fun some_eq (SOME x) (SOME y) = x = y
+ | some_eq _ _ = false
+ fun add_names quant (Const (quant_s, _) $ Abs (s, _, t')) =
+ add_names quant t' #> some_eq quant (quant_of quant_s) ? cons s
+ | add_names quant (@{const Not} $ t) = add_names (flip_quant quant) t
+ | add_names quant (@{const implies} $ t1 $ t2) =
+ add_names (flip_quant quant) t1 #> add_names quant t2
+ | add_names quant (t1 $ t2) = fold (add_names quant) [t1, t2]
+ | add_names _ _ = I
+ fun lost_names quant =
+ subtract (op =) (add_names quant new_t []) (add_names quant old_t [])
+ fun aux ((t1 as Const (quant_s, _)) $ (Abs (s, T, t'))) =
+ t1 $ Abs (s |> String.isPrefix protect_prefix s
+ ? perhaps (try (fn _ => hd (lost_names (quant_of quant_s)))),
+ T, aux t')
+ | aux (t1 $ t2) = aux t1 $ aux t2
+ | aux t = t
+ in aux new_t end
-fun protect_bounds (t $ u) = protect_bounds t $ protect_bounds u
- | protect_bounds (Abs (s, T, t')) =
- Abs (protect_prefix ^ s, T, protect_bounds t')
- | protect_bounds t = t
-
-(* Forward proof while preserving bound variables names*)
-fun rename_bvs_RS th rl =
+(* Forward proof while preserving bound variables names *)
+fun rename_bound_vars_RS th rl =
let
val t = concl_of th
val r = concl_of rl
- val th' = th RS Thm.rename_boundvars r (protect_bounds r) rl
+ val th' = th RS Thm.rename_boundvars r (protect_bound_var_names r) rl
val t' = concl_of th'
- in Thm.rename_boundvars t' (fix_bounds t' t) th' end
+ in Thm.rename_boundvars t' (fix_bound_var_names t t') th' end
(*raises exception if no rules apply*)
fun tryres (th, rls) =
let fun tryall [] = raise THM("tryres", 0, th::rls)
- | tryall (rl::rls) = (rename_bvs_RS th rl handle THM _ => tryall rls)
+ | tryall (rl::rls) =
+ (rename_bound_vars_RS th rl handle THM _ => tryall rls)
in tryall rls end;
(*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
@@ -577,7 +595,7 @@
|> forward_res ctxt aux
|> aux
handle THM ("tryres", _, _) =>
- rename_bvs_RS th ex_forward
+ rename_bound_vars_RS th ex_forward
|> forward_res ctxt aux
in aux o make_nnf ctxt end
--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Oct 29 16:16:10 2010 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Oct 29 16:51:20 2010 +0200
@@ -233,7 +233,7 @@
fun zapped_var_name ((ax_no, cluster_no), skolem) index_no s =
(if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^
"_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^
- string_of_int index_no ^ "_" ^ s
+ string_of_int index_no ^ "_" ^ Name.desymbolize false s
fun cluster_of_zapped_var_name s =
let val get_int = the o Int.fromString o nth (space_explode "_" s) in
@@ -241,10 +241,11 @@
String.isPrefix new_skolem_var_prefix s)
end
-fun zap (cluster as (cluster_no, cluster_skolem)) index_no pos ct =
- ct
- |> (case term_of ct of
- Const (s, _) $ Abs (s', _, _) =>
+fun rename_bound_vars_to_be_zapped ax_no =
+ let
+ fun aux (cluster as (cluster_no, cluster_skolem)) index_no pos t =
+ case t of
+ (t1 as Const (s, _)) $ Abs (s', T, t') =>
if s = @{const_name all} orelse s = @{const_name All} orelse
s = @{const_name Ex} then
let
@@ -252,34 +253,53 @@
val (cluster, index_no) =
if skolem = cluster_skolem then (cluster, index_no)
else ((cluster_no ||> cluster_skolem ? Integer.add 1, skolem), 0)
- in
- Thm.dest_comb #> snd
- #> Thm.dest_abs (SOME (zapped_var_name cluster index_no s'))
- #> snd #> zap cluster (index_no + 1) pos
- end
+ val s' = zapped_var_name cluster index_no s'
+ in t1 $ Abs (s', T, aux cluster (index_no + 1) pos t') end
+ else
+ t
+ | (t1 as Const (s, _)) $ t2 $ t3 =>
+ if s = @{const_name "==>"} orelse s = @{const_name HOL.implies} then
+ t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3
+ else if s = @{const_name HOL.conj} orelse
+ s = @{const_name HOL.disj} then
+ t1 $ aux cluster index_no pos t2 $ aux cluster index_no pos t3
+ else
+ t
+ | (t1 as Const (s, _)) $ t2 =>
+ if s = @{const_name Trueprop} then
+ t1 $ aux cluster index_no pos t2
+ else if s = @{const_name Not} then
+ t1 $ aux cluster index_no (not pos) t2
+ else
+ t
+ | _ => t
+ in aux ((ax_no, 0), true) 0 true end
+
+fun zap pos ct =
+ ct
+ |> (case term_of ct of
+ Const (s, _) $ Abs (s', _, _) =>
+ if s = @{const_name all} orelse s = @{const_name All} orelse
+ s = @{const_name Ex} then
+ Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos
else
Conv.all_conv
| Const (s, _) $ _ $ _ =>
if s = @{const_name "==>"} orelse s = @{const_name implies} then
- Conv.combination_conv (Conv.arg_conv (zap cluster index_no (not pos)))
- (zap cluster index_no pos)
+ Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos)
else if s = @{const_name conj} orelse s = @{const_name disj} then
- Conv.combination_conv (Conv.arg_conv (zap cluster index_no pos))
- (zap cluster index_no pos)
+ Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos)
else
Conv.all_conv
| Const (s, _) $ _ =>
- if s = @{const_name Trueprop} then
- Conv.arg_conv (zap cluster index_no pos)
- else if s = @{const_name Not} then
- Conv.arg_conv (zap cluster index_no (not pos))
- else
- Conv.all_conv
+ if s = @{const_name Trueprop} then Conv.arg_conv (zap pos)
+ else if s = @{const_name Not} then Conv.arg_conv (zap (not pos))
+ else Conv.all_conv
| _ => Conv.all_conv)
fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths
-val no_choice =
+val cheat_choice =
@{prop "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"}
|> Logic.varify_global
|> Skip_Proof.make_thm @{theory}
@@ -304,29 +324,34 @@
#> simplify (ss_only @{thms all_simps[symmetric]})
val pull_out =
simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]})
- val (discharger_th, fully_skolemized_th) =
- if null choice_ths then
- th |> `I |>> pull_out ||> skolemize [no_choice]
- else
- th |> skolemize choice_ths |> `I
- val t =
- fully_skolemized_th |> cprop_of
- |> zap ((ax_no, 0), true) 0 true |> Drule.export_without_context
+ val no_choice = null choice_ths
+ val discharger_th =
+ th |> (if no_choice then pull_out else skolemize choice_ths)
+ val fully_skolemized_t =
+ discharger_th |> prop_of |> rename_bound_vars_to_be_zapped ax_no
+ |> (if no_choice then
+ Skip_Proof.make_thm thy #> skolemize [cheat_choice] #> cprop_of
+ else
+ cterm_of thy)
+ |> zap true |> Drule.export_without_context
|> cprop_of |> Thm.dest_equals |> snd |> term_of
in
if exists_subterm (fn Var ((s, _), _) =>
String.isPrefix new_skolem_var_prefix s
- | _ => false) t then
+ | _ => false) fully_skolemized_t then
let
- val (ct, ctxt) =
- Variable.import_terms true [t] ctxt
+ val (fully_skolemized_ct, ctxt) =
+ Variable.import_terms true [fully_skolemized_t] ctxt
|>> the_single |>> cterm_of thy
- in (SOME (discharger_th, ct), Thm.assume ct, ctxt) end
+ in
+ (SOME (discharger_th, fully_skolemized_ct),
+ (Thm.assume fully_skolemized_ct, ctxt))
+ end
else
- (NONE, th, ctxt)
+ (NONE, (th, ctxt))
end
else
- (NONE, th, ctxt)
+ (NONE, (th, ctxt))
end
(* Convert a theorem to CNF, with additional premises due to skolemization. *)
@@ -334,7 +359,8 @@
let
val thy = ProofContext.theory_of ctxt0
val choice_ths = choice_theorems thy
- val (opt, nnf_th, ctxt) = nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
+ val (opt, (nnf_th, ctxt)) =
+ nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
fun clausify th =
make_cnf (if new_skolemizer orelse null choice_ths then
[]
@@ -344,6 +370,7 @@
val (cnf_ths, ctxt) =
clausify nnf_th
|> (fn ([], _) =>
+ (* FIXME: This probably doesn't work with the new Skolemizer *)
clausify (to_definitional_cnf_with_quantifiers thy nnf_th)
| p => p)
fun intr_imp ct th =
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Oct 29 16:16:10 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Oct 29 16:51:20 2010 +0200
@@ -16,7 +16,7 @@
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
val untyped_aconv : term -> term -> bool
val replay_one_inference :
- Proof.context -> mode -> (string * term) list
+ Proof.context -> mode -> (string * term) list * int Unsynchronized.ref
-> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
-> (Metis_Thm.thm * thm) list
val discharge_skolem_premises :
@@ -93,7 +93,7 @@
| NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
(*Maps metis terms to isabelle terms*)
-fun hol_term_from_metis_PT ctxt fol_tm =
+fun hol_term_from_metis_PT ctxt new_skolem_var_count fol_tm =
let val thy = ProofContext.theory_of ctxt
val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^
Metis_Term.toString fol_tm)
@@ -126,9 +126,11 @@
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 _ = new_skolem_var_count := j
val t =
if String.isPrefix new_skolem_const_prefix c then
- Var (new_skolem_var_from_const c,
+ Var ((new_skolem_var_name_from_const c, j),
Type_Infer.paramify_vars (tl tys ---> hd tys))
else
Const (c, dummyT)
@@ -162,7 +164,7 @@
end
(*Maps fully-typed metis terms to isabelle terms*)
-fun hol_term_from_metis_FT ctxt fol_tm =
+fun hol_term_from_metis_FT ctxt new_skolem_var_count fol_tm =
let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
Metis_Term.toString fol_tm)
fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
@@ -193,17 +195,17 @@
SOME v => Free (v, dummyT)
| NONE => (trace_msg ctxt (fn () =>
"hol_term_from_metis_FT bad const: " ^ x);
- hol_term_from_metis_PT ctxt t))
+ hol_term_from_metis_PT ctxt new_skolem_var_count t))
| cvt t = (trace_msg ctxt (fn () =>
"hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
- hol_term_from_metis_PT ctxt t)
+ hol_term_from_metis_PT ctxt new_skolem_var_count t)
in fol_tm |> cvt end
fun hol_term_from_metis FT = hol_term_from_metis_FT
| hol_term_from_metis _ = hol_term_from_metis_PT
-fun hol_terms_from_fol ctxt mode old_skolems fol_tms =
- let val ts = map (hol_term_from_metis mode ctxt) fol_tms
+fun hol_terms_from_metis ctxt mode (old_skolems, new_skolem_var_count) fol_tms =
+ let val ts = map (hol_term_from_metis mode ctxt new_skolem_var_count) fol_tms
val _ = trace_msg ctxt (fn () => " calling type inference:")
val _ = app (fn t => trace_msg ctxt
(fn () => Syntax.string_of_term ctxt t)) ts
@@ -249,17 +251,18 @@
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
in cterm_instantiate substs th end;
-fun assume_inf ctxt mode old_skolems atm =
+fun assume_inf ctxt mode skolem_params atm =
inst_excluded_middle
(ProofContext.theory_of ctxt)
- (singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm))
+ (singleton (hol_terms_from_metis ctxt mode skolem_params)
+ (Metis_Term.Fn atm))
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
to reconstruct them admits new possibilities of errors, e.g. concerning
sorts. Instead we try to arrange that new TVars are distinct and that types
can be inferred from terms. *)
-fun inst_inf ctxt mode old_skolems thpairs fsubst th =
+fun inst_inf ctxt mode (old_skolems, new_skolem_var_count) thpairs fsubst th =
let val thy = ProofContext.theory_of ctxt
val i_th = lookth thpairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
@@ -267,7 +270,7 @@
fun subst_translation (x,y) =
let val v = find_var x
(* We call "reveal_old_skolem_terms" and "infer_types" below. *)
- val t = hol_term_from_metis mode ctxt y
+ val t = hol_term_from_metis mode ctxt new_skolem_var_count y
in SOME (cterm_of thy (Var v), t) end
handle Option.Option =>
(trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
@@ -375,7 +378,7 @@
(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
val select_literal = negate_head oo make_last
-fun resolve_inf ctxt mode old_skolems thpairs atm th1 th2 =
+fun resolve_inf ctxt mode skolem_params thpairs atm th1 th2 =
let
val thy = ProofContext.theory_of ctxt
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
@@ -390,7 +393,7 @@
else
let
val i_atm =
- singleton (hol_terms_from_fol ctxt mode old_skolems)
+ singleton (hol_terms_from_metis ctxt mode skolem_params)
(Metis_Term.Fn atm)
val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
val prems_th1 = prems_of i_th1
@@ -415,9 +418,9 @@
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
-fun refl_inf ctxt mode old_skolems t =
+fun refl_inf ctxt mode skolem_params t =
let val thy = ProofContext.theory_of ctxt
- val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t
+ val i_t = singleton (hol_terms_from_metis ctxt mode skolem_params) t
val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
@@ -433,10 +436,10 @@
| get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
| get_ty_arg_size _ _ = 0;
-fun equality_inf ctxt mode old_skolems (pos, atm) fp fr =
+fun equality_inf ctxt mode skolem_params (pos, atm) fp fr =
let val thy = ProofContext.theory_of ctxt
val m_tm = Metis_Term.Fn atm
- val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr]
+ val [i_atm,i_tm] = hol_terms_from_metis ctxt mode skolem_params [m_tm, fr]
val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
fun replace_item_list lx 0 (_::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
@@ -515,17 +518,17 @@
val factor = Seq.hd o distinct_subgoals_tac;
-fun step ctxt mode old_skolems thpairs p =
+fun step ctxt mode skolem_params thpairs p =
case p of
(fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
- | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode old_skolems f_atm
+ | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolem_params f_atm
| (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
- factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1)
+ factor (inst_inf ctxt mode skolem_params thpairs f_subst f_th1)
| (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
- factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2)
- | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm
+ factor (resolve_inf ctxt mode skolem_params thpairs f_atm f_th1 f_th2)
+ | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolem_params f_tm
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
- equality_inf ctxt mode old_skolems f_lit f_p f_r
+ equality_inf ctxt mode skolem_params f_lit f_p f_r
fun flexflex_first_order th =
case Thm.tpairs_of th of
@@ -545,12 +548,12 @@
fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
-fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs =
+fun replay_one_inference ctxt mode skolem_params (fol_th, inf) thpairs =
let
val _ = trace_msg ctxt (fn () => "=============================================")
val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
- val th = step ctxt mode old_skolems thpairs (fol_th, inf)
+ val th = step ctxt mode skolem_params thpairs (fol_th, inf)
|> flexflex_first_order
val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
val _ = trace_msg ctxt (fn () => "=============================================")
@@ -609,10 +612,6 @@
| _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u])
in th |> term_instantiate thy (unify_terms (prem, concl) []) end
-fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no)
-fun shuffle_ord p =
- rev_order (prod_ord int_ord int_ord (pairself shuffle_key p))
-
val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
fun copy_prems_tac [] ns i =
@@ -622,13 +621,21 @@
| 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
-fun instantiate_forall_tac thy params t i =
+fun instantiate_forall_tac thy t i st =
let
+ val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
fun repair (t as (Var ((s, _), _))) =
- (case find_index (fn ((s', _), _) => s' = s) params of
+ (case find_index (fn (s', _) => s' = s) params of
~1 => t
| j => Bound j)
- | repair (t $ u) = repair t $ repair u
+ | repair (t $ u) =
+ (case (repair t, repair u) of
+ (t as Bound j, u as Bound k) =>
+ (* This is a rather subtle trick to repair the discrepancy between
+ the fully skolemized term that MESON gives us (where existentials
+ were pulled out) and the reality. *)
+ if k > j then t else t $ u
+ | (t, u) => t $ u)
| repair t = t
val t' = t |> repair |> fold (curry absdummy) (map snd params)
fun do_instantiate th =
@@ -636,41 +643,50 @@
th |> term_instantiate thy [(Var var, t')]
end
in
- etac @{thm allE} i
- THEN rotate_tac ~1 i
- THEN PRIMITIVE do_instantiate
+ (etac @{thm allE} i
+ THEN rotate_tac ~1 i
+ THEN PRIMITIVE do_instantiate) st
end
-fun release_clusters_tac _ _ _ _ [] = K all_tac
- | release_clusters_tac thy ax_counts substs params
+fun fix_exists_tac thy t =
+ etac @{thm exE}
+ THEN' rename_tac [t |> dest_Var |> fst |> fst]
+
+fun release_quantifier_tac thy (skolem, t) =
+ (if skolem then fix_exists_tac else instantiate_forall_tac) thy t
+
+fun release_clusters_tac _ _ _ [] = K all_tac
+ | release_clusters_tac thy ax_counts substs
((ax_no, cluster_no) :: clusters) =
let
- fun in_right_cluster s =
- (s |> Meson_Clausify.cluster_of_zapped_var_name |> fst |> snd |> fst)
- = cluster_no
+ val cluster_of_var =
+ Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var
+ fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no
val cluster_substs =
substs
|> map_filter (fn (ax_no', (_, (_, tsubst))) =>
if ax_no' = ax_no then
- tsubst |> filter (in_right_cluster
- o fst o fst o dest_Var o fst)
- |> map snd |> SOME
- else
- NONE)
- val n = length cluster_substs
+ tsubst |> map (apfst cluster_of_var)
+ |> filter (in_right_cluster o fst)
+ |> map (apfst snd)
+ |> SOME
+ else
+ NONE)
fun do_cluster_subst cluster_subst =
- map (instantiate_forall_tac thy params) cluster_subst @ [rotate_tac 1]
- val params' = params (* FIXME ### existentials! *)
+ map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]
val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
in
rotate_tac first_prem
THEN' (EVERY' (maps do_cluster_subst cluster_substs))
THEN' rotate_tac (~ first_prem - length cluster_substs)
- THEN' release_clusters_tac thy ax_counts substs params' clusters
+ THEN' release_clusters_tac thy ax_counts substs clusters
end
-val cluster_ord =
- prod_ord (prod_ord int_ord (prod_ord int_ord int_ord)) bool_ord
+fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =
+ (ax_no, (cluster_no, (skolem, index_no)))
+fun cluster_ord p =
+ prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord))
+ (pairself cluster_key p)
val tysubst_ord =
list_ord (prod_ord Term_Ord.fast_indexname_ord
@@ -683,6 +699,9 @@
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_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)
+
(* Attempts to derive the theorem "False" from a theorem of the form
"P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
@@ -694,6 +713,7 @@
let
val thy = ProofContext.theory_of ctxt
(* distinguish variables with same name but different types *)
+ (* ### FIXME: needed? *)
val prems_imp_false' =
prems_imp_false |> try (forall_intr_vars #> gen_all)
|> the_default prems_imp_false
@@ -757,12 +777,12 @@
handle Int_Pair_Graph.CYCLES _ =>
error "Cannot replay Metis proof in Isabelle without \
\\"Hilbert_Choice\"."
- val params0 =
- [] |> fold (Term.add_vars o snd) (map_filter I axioms)
- |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst o fst))
+ val outer_param_names =
+ [] |> fold (Term.add_var_names o snd) (map_filter I axioms)
+ |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
|> filter (fn (((_, (cluster_no, _)), skolem), _) =>
cluster_no = 0 andalso skolem)
- |> sort shuffle_ord |> map snd
+ |> sort shuffle_ord |> map (fst o snd)
val ax_counts =
Int_Tysubst_Table.empty
|> fold (fn (ax_no, (_, (tysubst, _))) =>
@@ -775,11 +795,10 @@
"; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
commas (map ((fn (s, t) => s ^ " |-> " ^ t)
o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
+ 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))
- val _ = tracing ("OUTERMOST SKOLEMS: " ^ PolyML.makestring params0)
- val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
- val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
*)
fun rotation_for_subgoal i =
find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
@@ -788,14 +807,14 @@
(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
- THEN release_clusters_tac thy ax_counts substs params0
- ordered_clusters 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 PRIMITIVE (unify_first_prem_with_concl thy i) ###*)
+(* THEN PRIMITIVE (unify_first_prem_with_concl thy i) ### FIXME: needed? *)
THEN assume_tac i)))
handle ERROR _ =>
error ("Cannot replay Metis proof in Isabelle:\n\
--- a/src/HOL/Tools/Metis/metis_tactics.ML Fri Oct 29 16:16:10 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Fri Oct 29 16:51:20 2010 +0200
@@ -91,9 +91,11 @@
Metis_Thm.toString mth)
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
(*add constraints arising from converting goal to clause form*)
+ val new_skolem_var_count = Unsynchronized.ref 1
val proof = Metis_Proof.proof mth
val result =
- fold (replay_one_inference ctxt' mode old_skolems) proof axioms
+ fold (replay_one_inference ctxt' mode
+ (old_skolems, new_skolem_var_count)) proof axioms
and used = map_filter (used_axioms axioms) proof
val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
--- a/src/HOL/Tools/Metis/metis_translate.ML Fri Oct 29 16:16:10 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Fri Oct 29 16:51:20 2010 +0200
@@ -59,7 +59,7 @@
val make_fixed_type_const : string -> string
val make_type_class : string -> string
val num_type_args: theory -> string -> int
- val new_skolem_var_from_const: string -> indexname
+ val new_skolem_var_name_from_const : string -> string
val type_literals_for_types : typ list -> type_literal list
val make_class_rel_clauses :
theory -> class list -> class list -> class_rel_clause list
@@ -214,9 +214,9 @@
else
(s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
-fun new_skolem_var_from_const s =
+fun new_skolem_var_name_from_const s =
let val ss = s |> space_explode Long_Name.separator in
- (nth ss (length ss - 2), 0)
+ nth ss (length ss - 2)
end
--- a/src/HOL/Tools/Nitpick/kodkod.ML Fri Oct 29 16:16:10 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Fri Oct 29 16:51:20 2010 +0200
@@ -1036,12 +1036,7 @@
val outcome =
let
val code =
- bash ("cd " ^ File.shell_quote temp_dir ^ ";\n" ^
- "env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \
- \JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
- \$JAVA_LIBRARY_PATH\" \
- \LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
- \$LD_LIBRARY_PATH\" \
+ bash ("cd " ^ File.shell_quote temp_dir ^ ";\n\
\\"$KODKODI\"/bin/kodkodi" ^
(if ms >= 0 then " -max-msecs " ^ string_of_int ms
else "") ^
--- a/src/Tools/Code/code_runtime.ML Fri Oct 29 16:16:10 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML Fri Oct 29 16:51:20 2010 +0200
@@ -64,7 +64,7 @@
fun exec verbose code =
(if ! trace then tracing code else ();
- ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false code));
+ ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code));
fun value ctxt (get, put, put_ml) (prelude, value) =
let