--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Fri Feb 12 17:04:36 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Fri Feb 12 22:36:48 2016 +0100
@@ -5722,8 +5722,8 @@
lemma higher_deriv_ident [simp]:
"(deriv ^^ n) (\<lambda>w. w) z = (if n = 0 then z else if n = 1 then 1 else 0)"
- apply (induction n)
- apply (simp_all add: deriv_ident funpow_Suc_right del: funpow.simps, simp)
+ apply (induction n, simp)
+ apply (metis higher_deriv_linear lambda_one)
done
corollary higher_deriv_id [simp]:
@@ -6893,6 +6893,60 @@
text\<open>Proof is based on Dixon's, as presented in Lang's "Complex Analysis" book (page 147).\<close>
+lemma contour_integral_continuous_on_linepath_2D:
+ assumes "open u" and cont_dw: "\<And>w. w \<in> u \<Longrightarrow> F w contour_integrable_on (linepath a b)"
+ and cond_uu: "continuous_on (u \<times> u) (\<lambda>(x,y). F x y)"
+ and abu: "closed_segment a b \<subseteq> u"
+ shows "continuous_on u (\<lambda>w. contour_integral (linepath a b) (F w))"
+proof -
+ have *: "\<exists>d>0. \<forall>x'\<in>u. dist x' w < d \<longrightarrow>
+ dist (contour_integral (linepath a b) (F x'))
+ (contour_integral (linepath a b) (F w)) \<le> \<epsilon>"
+ if "w \<in> u" "0 < \<epsilon>" "a \<noteq> b" for w \<epsilon>
+ proof -
+ obtain \<delta> where "\<delta>>0" and \<delta>: "cball w \<delta> \<subseteq> u" using open_contains_cball \<open>open u\<close> \<open>w \<in> u\<close> by force
+ let ?TZ = "{(t,z) |t z. t \<in> cball w \<delta> \<and> z \<in> closed_segment a b}"
+ have "uniformly_continuous_on ?TZ (\<lambda>(x,y). F x y)"
+ apply (rule compact_uniformly_continuous)
+ apply (rule continuous_on_subset[OF cond_uu])
+ using abu \<delta>
+ apply (auto simp: compact_Times simp del: mem_cball)
+ done
+ then obtain \<eta> where "\<eta>>0"
+ and \<eta>: "\<And>x x'. \<lbrakk>x\<in>?TZ; x'\<in>?TZ; dist x' x < \<eta>\<rbrakk> \<Longrightarrow>
+ dist ((\<lambda>(x,y). F x y) x') ((\<lambda>(x,y). F x y) x) < \<epsilon>/norm(b - a)"
+ apply (rule uniformly_continuous_onE [where e = "\<epsilon>/norm(b - a)"])
+ using \<open>0 < \<epsilon>\<close> \<open>a \<noteq> b\<close> by auto
+ have \<eta>: "\<lbrakk>norm (w - x1) \<le> \<delta>; x2 \<in> closed_segment a b;
+ norm (w - x1') \<le> \<delta>; x2' \<in> closed_segment a b; norm ((x1', x2') - (x1, x2)) < \<eta>\<rbrakk>
+ \<Longrightarrow> norm (F x1' x2' - F x1 x2) \<le> \<epsilon> / cmod (b - a)"
+ for x1 x2 x1' x2'
+ using \<eta> [of "(x1,x2)" "(x1',x2')"] by (force simp add: dist_norm)
+ have le_ee: "cmod (contour_integral (linepath a b) (\<lambda>x. F x' x - F w x)) \<le> \<epsilon>"
+ if "x' \<in> u" "cmod (x' - w) < \<delta>" "cmod (x' - w) < \<eta>" for x'
+ proof -
+ have "cmod (contour_integral (linepath a b) (\<lambda>x. F x' x - F w x)) \<le> \<epsilon>/norm(b - a) * norm(b - a)"
+ apply (rule has_contour_integral_bound_linepath [OF has_contour_integral_integral _ \<eta>])
+ apply (rule contour_integrable_diff [OF cont_dw cont_dw])
+ using \<open>0 < \<epsilon>\<close> \<open>a \<noteq> b\<close> \<open>0 < \<delta>\<close> \<open>w \<in> u\<close> that
+ apply (auto simp: norm_minus_commute)
+ done
+ also have "... = \<epsilon>" using \<open>a \<noteq> b\<close> by simp
+ finally show ?thesis .
+ qed
+ show ?thesis
+ apply (rule_tac x="min \<delta> \<eta>" in exI)
+ using \<open>0 < \<delta>\<close> \<open>0 < \<eta>\<close>
+ apply (auto simp: dist_norm contour_integral_diff [OF cont_dw cont_dw, symmetric] \<open>w \<in> u\<close> intro: le_ee)
+ done
+ qed
+ show ?thesis
+ apply (rule continuous_onI)
+ apply (cases "a=b")
+ apply (auto intro: *)
+ done
+qed
+
text\<open>This version has @{term"polynomial_function \<gamma>"} as an additional assumption.\<close>
lemma Cauchy_integral_formula_global_weak:
assumes u: "open u" and holf: "f holomorphic_on u"
@@ -7065,10 +7119,10 @@
by (meson Lim_at_infinityI)
moreover have "h holomorphic_on UNIV"
proof -
- have con_ff: "continuous (at (x,z)) (\<lambda>y. (f(snd y) - f(fst y)) / (snd y - fst y))"
+ have con_ff: "continuous (at (x,z)) (\<lambda>(x,y). (f y - f x) / (y - x))"
if "x \<in> u" "z \<in> u" "x \<noteq> z" for x z
using that conf
- apply (simp add: continuous_on_eq_continuous_at u)
+ apply (simp add: split_def continuous_on_eq_continuous_at u)
apply (simp | rule continuous_intros continuous_within_compose2 [where g=f])+
done
have con_fstsnd: "continuous_on UNIV (\<lambda>x. (fst x - snd x) ::complex)"
@@ -7083,8 +7137,8 @@
apply (rule continuous_on_interior [of u])
apply (simp add: holf holomorphic_deriv holomorphic_on_imp_continuous_on u)
by (simp add: interior_open that u)
- have tendsto_f': "((\<lambda>x. if snd x = fst x then deriv f (fst x)
- else (f (snd x) - f (fst x)) / (snd x - fst x)) \<longlongrightarrow> deriv f x)
+ have tendsto_f': "((\<lambda>(x,y). if y = x then deriv f (x)
+ else (f (y) - f (x)) / (y - x)) \<longlongrightarrow> deriv f x)
(at (x, x) within u \<times> u)" if "x \<in> u" for x
proof (rule Lim_withinI)
fix e::real assume "0 < e"
@@ -7120,8 +7174,7 @@
qed
show "\<exists>d>0. \<forall>xa\<in>u \<times> u.
0 < dist xa (x, x) \<and> dist xa (x, x) < d \<longrightarrow>
- dist (if snd xa = fst xa then deriv f (fst xa) else (f (snd xa) - f (fst xa)) / (snd xa - fst xa))
- (deriv f x) \<le> e"
+ dist (case xa of (x, y) \<Rightarrow> if y = x then deriv f x else (f y - f x) / (y - x)) (deriv f x) \<le> e"
apply (rule_tac x="min k1 k2" in exI)
using \<open>k1>0\<close> \<open>k2>0\<close> \<open>e>0\<close>
apply (force simp: dist_norm neq intro: dual_order.strict_trans2 k1 less_imp_le norm_fst_le)
@@ -7134,16 +7187,16 @@
using \<gamma>' using path_image_def vector_derivative_at by fastforce
have f_has_cint: "\<And>w. w \<in> v - path_image \<gamma> \<Longrightarrow> ((\<lambda>u. f u / (u - w) ^ 1) has_contour_integral h w) \<gamma>"
by (simp add: V)
- have cond_uu: "continuous_on (u \<times> u) (\<lambda>y. d (fst y) (snd y))"
+ have cond_uu: "continuous_on (u \<times> u) (\<lambda>(x,y). d x y)"
apply (simp add: continuous_on_eq_continuous_within d_def continuous_within tendsto_f')
apply (simp add: Lim_within_open_NO_MATCH open_Times u, clarify)
- apply (rule Lim_transform_within_open [OF _ open_uu_Id, where f = "(\<lambda>x. (f (snd x) - f (fst x)) / (snd x - fst x))"])
+ apply (rule Lim_transform_within_open [OF _ open_uu_Id, where f = "(\<lambda>(x,y). (f y - f x) / (y - x))"])
using con_ff
apply (auto simp: continuous_within)
done
have hol_dw: "(\<lambda>z. d z w) holomorphic_on u" if "w \<in> u" for w
proof -
- have "continuous_on u ((\<lambda>y. d (fst y) (snd y)) o (\<lambda>z. (w,z)))"
+ have "continuous_on u ((\<lambda>(x,y). d x y) o (\<lambda>z. (w,z)))"
by (rule continuous_on_compose continuous_intros continuous_on_subset [OF cond_uu] | force intro: that)+
then have *: "continuous_on u (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z))"
by (rule rev_iffD1 [OF _ continuous_on_cong [OF refl]]) (simp add: d_def field_simps)
@@ -7159,53 +7212,11 @@
qed
{ fix a b
assume abu: "closed_segment a b \<subseteq> u"
- then have cont_dw: "\<And>w. w \<in> u \<Longrightarrow> (\<lambda>z. d z w) contour_integrable_on (linepath a b)"
+ then have "\<And>w. w \<in> u \<Longrightarrow> (\<lambda>z. d z w) contour_integrable_on (linepath a b)"
by (metis hol_dw continuous_on_subset contour_integrable_continuous_linepath holomorphic_on_imp_continuous_on)
- have *: "\<exists>da>0. \<forall>x'\<in>u. dist x' w < da \<longrightarrow>
- dist (contour_integral (linepath a b) (\<lambda>z. d z x'))
- (contour_integral (linepath a b) (\<lambda>z. d z w)) \<le> ee"
- if "w \<in> u" "0 < ee" "a \<noteq> b" for w ee
- proof -
- obtain dd where "dd>0" and dd: "cball w dd \<subseteq> u" using open_contains_cball u \<open>w \<in> u\<close> by force
- let ?abdd = "{(z,t) |z t. z \<in> closed_segment a b \<and> t \<in> cball w dd}"
- have "uniformly_continuous_on ?abdd (\<lambda>y. d (fst y) (snd y))"
- apply (rule compact_uniformly_continuous)
- apply (rule continuous_on_subset[OF cond_uu])
- using abu dd
- apply (auto simp: compact_Times simp del: mem_cball)
- done
- then obtain kk where "kk>0"
- and kk: "\<And>x x'. \<lbrakk>x\<in>?abdd; x'\<in>?abdd; dist x' x < kk\<rbrakk> \<Longrightarrow>
- dist ((\<lambda>y. d (fst y) (snd y)) x') ((\<lambda>y. d (fst y) (snd y)) x) < ee/norm(b - a)"
- apply (rule uniformly_continuous_onE [where e = "ee/norm(b - a)"])
- using \<open>0 < ee\<close> \<open>a \<noteq> b\<close> by auto
- have kk: "\<lbrakk>x1 \<in> closed_segment a b; norm (w - x2) \<le> dd;
- x1' \<in> closed_segment a b; norm (w - x2') \<le> dd; norm ((x1', x2') - (x1, x2)) < kk\<rbrakk>
- \<Longrightarrow> norm (d x1' x2' - d x1 x2) \<le> ee / cmod (b - a)"
- for x1 x2 x1' x2'
- using kk [of "(x1,x2)" "(x1',x2')"] by (force simp add: dist_norm)
- have le_ee: "cmod (contour_integral (linepath a b) (\<lambda>x. d x x' - d x w)) \<le> ee"
- if "x' \<in> u" "cmod (x' - w) < dd" "cmod (x' - w) < kk" for x'
- proof -
- have "cmod (contour_integral (linepath a b) (\<lambda>x. d x x' - d x w)) \<le> ee/norm(b - a) * norm(b - a)"
- apply (rule has_contour_integral_bound_linepath [OF has_contour_integral_integral _ kk])
- apply (rule contour_integrable_diff [OF cont_dw cont_dw])
- using \<open>0 < ee\<close> \<open>a \<noteq> b\<close> \<open>0 < dd\<close> \<open>w \<in> u\<close> that
- apply (auto simp: norm_minus_commute)
- done
- also have "... = ee" using \<open>a \<noteq> b\<close> by simp
- finally show ?thesis .
- qed
- show ?thesis
- apply (rule_tac x="min dd kk" in exI)
- using \<open>0 < dd\<close> \<open>0 < kk\<close>
- apply (auto simp: dist_norm contour_integral_diff [OF cont_dw cont_dw, symmetric] \<open>w \<in> u\<close> intro: le_ee)
- done
- qed
- have cont_cint_d: "continuous_on u (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))"
- apply (rule continuous_onI)
- apply (cases "a=b")
- apply (auto intro: *)
+ then have cont_cint_d: "continuous_on u (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))"
+ apply (rule contour_integral_continuous_on_linepath_2D [OF \<open>open u\<close> _ _ abu])
+ apply (auto simp: intro: continuous_on_swap_args cond_uu)
done
have cont_cint_d\<gamma>: "continuous_on {0..1} ((\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w)) o \<gamma>)"
apply (rule continuous_on_compose)
@@ -7223,7 +7234,6 @@
using abu by (force simp add: h_def intro: contour_integral_eq)
also have "... = contour_integral \<gamma> (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))"
apply (rule contour_integral_swap)
- apply (simp add: split_def)
apply (rule continuous_on_subset [OF cond_uu])
using abu pasz \<open>valid_path \<gamma>\<close>
apply (auto intro!: continuous_intros)
@@ -7243,17 +7253,16 @@
have A2: "\<forall>\<^sub>F n in sequentially. \<forall>xa\<in>path_image \<gamma>. cmod (d (a n) xa - d x xa) < ee" if "0 < ee" for ee
proof -
let ?ddpa = "{(w,z) |w z. w \<in> cball x dd \<and> z \<in> path_image \<gamma>}"
- have "uniformly_continuous_on ?ddpa (\<lambda>y. d (fst y) (snd y))"
+ have "uniformly_continuous_on ?ddpa (\<lambda>(x,y). d x y)"
apply (rule compact_uniformly_continuous [OF continuous_on_subset[OF cond_uu]])
using dd pasz \<open>valid_path \<gamma>\<close>
apply (auto simp: compact_Times compact_valid_path_image simp del: mem_cball)
done
then obtain kk where "kk>0"
and kk: "\<And>x x'. \<lbrakk>x\<in>?ddpa; x'\<in>?ddpa; dist x' x < kk\<rbrakk> \<Longrightarrow>
- dist ((\<lambda>y. d (fst y) (snd y)) x') ((\<lambda>y. d (fst y) (snd y)) x) < ee"
+ dist ((\<lambda>(x,y). d x y) x') ((\<lambda>(x,y). d x y) x) < ee"
apply (rule uniformly_continuous_onE [where e = ee])
using \<open>0 < ee\<close> by auto
-
have kk: "\<lbrakk>norm (w - x) \<le> dd; z \<in> path_image \<gamma>; norm ((w, z) - (x, z)) < kk\<rbrakk> \<Longrightarrow> norm (d w z - d x z) < ee"
for w z
using \<open>dd>0\<close> kk [of "(x,z)" "(w,z)"] by (force simp add: norm_minus_commute dist_norm)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Feb 12 17:04:36 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Feb 12 22:36:48 2016 +0100
@@ -156,284 +156,295 @@
let
val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof0, goal) =
isar_params ()
-
- val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods
+ in
+ if null atp_proof0 then
+ one_line_proof_text ctxt 0 one_line_params
+ else
+ let
+ val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods
- fun massage_methods (meths as meth :: _) =
- if not try0 then [meth]
- else if smt_proofs = SOME true then SMT_Method :: meths
- else meths
-
- val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
- val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
- val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
+ fun massage_methods (meths as meth :: _) =
+ if not try0 then [meth]
+ else if smt_proofs = SOME true then SMT_Method :: meths
+ else meths
- val do_preplay = preplay_timeout <> Time.zeroTime
- val compress =
- (case compress of
- NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0
- | SOME n => n)
+ val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
+ val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
+ val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
- fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem
- fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
+ val do_preplay = preplay_timeout <> Time.zeroTime
+ val compress =
+ (case compress of
+ NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0
+ | SOME n => n)
- fun get_role keep_role ((num, _), role, t, rule, _) =
- if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
-
- val atp_proof =
- fold_rev add_line_pass1 atp_proof0 []
- |> add_lines_pass2 []
+ fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem
+ fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
- val conjs =
- map_filter (fn (name, role, _, _, _) =>
- if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE)
- atp_proof
- val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof
+ fun get_role keep_role ((num, _), role, t, rule, _) =
+ if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
+
+ val atp_proof =
+ fold_rev add_line_pass1 atp_proof0 []
+ |> add_lines_pass2 []
+
+ val conjs =
+ map_filter (fn (name, role, _, _, _) =>
+ if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE)
+ atp_proof
+ val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof
- fun add_lemma ((l, t), rule) ctxt =
- let
- val (skos, meths) =
- (if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods)
- else if is_arith_rule rule then ([], arith_methods)
- else ([], rewrite_methods))
- ||> massage_methods
- in
- (Prove ([], skos, l, t, [], ([], []), meths, ""),
- ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd))
- end
+ fun add_lemma ((l, t), rule) ctxt =
+ let
+ val (skos, meths) =
+ (if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods)
+ else if is_arith_rule rule then ([], arith_methods)
+ else ([], rewrite_methods))
+ ||> massage_methods
+ in
+ (Prove ([], skos, l, t, [], ([], []), meths, ""),
+ ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd))
+ end
- val (lems, _) =
- fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt
-
- val bot = #1 (List.last atp_proof)
-
- val refute_graph =
- atp_proof
- |> map (fn (name, _, _, _, from) => (from, name))
- |> make_refute_graph bot
- |> fold (Atom_Graph.default_node o rpair ()) conjs
-
- val axioms = axioms_of_refute_graph refute_graph conjs
+ val (lems, _) =
+ fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt
- val tainted = tainted_atoms_of_refute_graph refute_graph conjs
- val is_clause_tainted = exists (member (op =) tainted)
- val steps =
- Symtab.empty
- |> fold (fn (name as (s, _), role, t, rule, _) =>
- Symtab.update_new (s, (rule, t
- |> (if is_clause_tainted [name] then
- HOLogic.dest_Trueprop
- #> role <> Conjecture ? s_not
- #> fold exists_of (map Var (Term.add_vars t []))
- #> HOLogic.mk_Trueprop
- else
- I))))
- atp_proof
+ val bot = #1 (List.last atp_proof)
+
+ val refute_graph =
+ atp_proof
+ |> map (fn (name, _, _, _, from) => (from, name))
+ |> make_refute_graph bot
+ |> fold (Atom_Graph.default_node o rpair ()) conjs
+
+ val axioms = axioms_of_refute_graph refute_graph conjs
- fun is_referenced_in_step _ (Let _) = false
- | is_referenced_in_step l (Prove (_, _, _, _, subs, (ls, _), _, _)) =
- member (op =) ls l orelse exists (is_referenced_in_proof l) subs
- and is_referenced_in_proof l (Proof (_, _, steps)) =
- exists (is_referenced_in_step l) steps
+ val tainted = tainted_atoms_of_refute_graph refute_graph conjs
+ val is_clause_tainted = exists (member (op =) tainted)
+ val steps =
+ Symtab.empty
+ |> fold (fn (name as (s, _), role, t, rule, _) =>
+ Symtab.update_new (s, (rule, t
+ |> (if is_clause_tainted [name] then
+ HOLogic.dest_Trueprop
+ #> role <> Conjecture ? s_not
+ #> fold exists_of (map Var (Term.add_vars t []))
+ #> HOLogic.mk_Trueprop
+ else
+ I))))
+ atp_proof
- fun insert_lemma_in_step lem
- (step as Prove (qs, fix, l, t, subs, (ls, gs), meths, comment)) =
- let val l' = the (label_of_isar_step lem) in
- if member (op =) ls l' then
- [lem, step]
- else
- let val refs = map (is_referenced_in_proof l') subs in
- if length (filter I refs) = 1 then
- let
- val subs' = map2 (fn false => I | true => insert_lemma_in_proof lem) refs subs
- in
- [Prove (qs, fix, l, t, subs', (ls, gs), meths, comment)]
- end
- else
+ fun is_referenced_in_step _ (Let _) = false
+ | is_referenced_in_step l (Prove (_, _, _, _, subs, (ls, _), _, _)) =
+ member (op =) ls l orelse exists (is_referenced_in_proof l) subs
+ and is_referenced_in_proof l (Proof (_, _, steps)) =
+ exists (is_referenced_in_step l) steps
+
+ fun insert_lemma_in_step lem
+ (step as Prove (qs, fix, l, t, subs, (ls, gs), meths, comment)) =
+ let val l' = the (label_of_isar_step lem) in
+ if member (op =) ls l' then
[lem, step]
+ else
+ let val refs = map (is_referenced_in_proof l') subs in
+ if length (filter I refs) = 1 then
+ let
+ val subs' = map2 (fn false => I | true => insert_lemma_in_proof lem) refs
+ subs
+ in
+ [Prove (qs, fix, l, t, subs', (ls, gs), meths, comment)]
+ end
+ else
+ [lem, step]
+ end
end
- end
- and insert_lemma_in_steps lem [] = [lem]
- | insert_lemma_in_steps lem (step :: steps) =
- if is_referenced_in_step (the (label_of_isar_step lem)) step then
- insert_lemma_in_step lem step @ steps
- else
- step :: insert_lemma_in_steps lem steps
- and insert_lemma_in_proof lem (Proof (fix, assms, steps)) =
- Proof (fix, assms, insert_lemma_in_steps lem steps)
-
- val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
-
- val finish_off = close_form #> rename_bound_vars
-
- fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off
- | prop_of_clause names =
- let
- val lits =
- map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names)
- in
- (case List.partition (can HOLogic.dest_not) lits of
- (negs as _ :: _, pos as _ :: _) =>
- s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos)
- | _ => fold (curry s_disj) lits @{term False})
- end
- |> HOLogic.mk_Trueprop |> finish_off
-
- fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else []
-
- fun isar_steps outer predecessor accum [] =
- accum
- |> (if tainted = [] then
- (* e.g., trivial, empty proof by Z3 *)
- cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
- sort_facts (the_list predecessor, []), massage_methods systematic_methods', ""))
+ and insert_lemma_in_steps lem [] = [lem]
+ | insert_lemma_in_steps lem (step :: steps) =
+ if is_referenced_in_step (the (label_of_isar_step lem)) step then
+ insert_lemma_in_step lem step @ steps
else
- I)
- |> rev
- | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) =
- let
- val l = label_of_clause c
- val t = prop_of_clause c
- val rule = rule_of_clause_id id
- val skolem = is_skolemize_rule rule
+ step :: insert_lemma_in_steps lem steps
+ and insert_lemma_in_proof lem (Proof (fix, assms, steps)) =
+ Proof (fix, assms, insert_lemma_in_steps lem steps)
+
+ val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
+
+ val finish_off = close_form #> rename_bound_vars
- val deps = ([], [])
- |> fold add_fact_of_dependency gamma
- |> is_maybe_ext_rule rule ? add_global_fact [short_thm_name ctxt ext]
- |> sort_facts
- val meths =
- (if skolem then skolem_methods
- else if is_arith_rule rule then arith_methods
- else if is_datatype_rule rule then datatype_methods
- else systematic_methods')
- |> massage_methods
+ fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off
+ | prop_of_clause names =
+ let
+ val lits =
+ map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names)
+ in
+ (case List.partition (can HOLogic.dest_not) lits of
+ (negs as _ :: _, pos as _ :: _) =>
+ s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs),
+ Library.foldr1 s_disj pos)
+ | _ => fold (curry s_disj) lits @{term False})
+ end
+ |> HOLogic.mk_Trueprop |> finish_off
+
+ fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else []
- fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "")
- fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
- in
- if is_clause_tainted c then
- (case gamma of
- [g] =>
- if skolem andalso is_clause_tainted g then
- let
- val skos = skolems_of ctxt (prop_of_clause g)
- val subproof = Proof (skos, [], rev accum)
- in
- isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
- end
- else
- steps_of_rest (prove [] deps)
- | _ => steps_of_rest (prove [] deps))
- else
- steps_of_rest
- (if skolem then
- (case skolems_of ctxt t of
- [] => prove [] deps
- | skos => Prove ([], skos, l, t, [], deps, meths, ""))
- else
- prove [] deps)
- end
- | isar_steps outer predecessor accum (Cases cases :: infs) =
- let
- fun isar_case (c, subinfs) =
- isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs
- val c = succedent_of_cases cases
- val l = label_of_clause c
- val t = prop_of_clause c
- val step =
- Prove (maybe_show outer c, [], l, t,
- map isar_case (filter_out (null o snd) cases),
- sort_facts (the_list predecessor, []), massage_methods systematic_methods', "")
- in
- isar_steps outer (SOME l) (step :: accum) infs
- end
- and isar_proof outer fix assms lems infs =
- Proof (fix, assms, fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs))
+ fun isar_steps outer predecessor accum [] =
+ accum
+ |> (if tainted = [] then
+ (* e.g., trivial, empty proof by Z3 *)
+ cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
+ sort_facts (the_list predecessor, []), massage_methods systematic_methods',
+ ""))
+ else
+ I)
+ |> rev
+ | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) =
+ let
+ val l = label_of_clause c
+ val t = prop_of_clause c
+ val rule = rule_of_clause_id id
+ val skolem = is_skolemize_rule rule
- val trace = Config.get ctxt trace
+ val deps = ([], [])
+ |> fold add_fact_of_dependency gamma
+ |> is_maybe_ext_rule rule ? add_global_fact [short_thm_name ctxt ext]
+ |> sort_facts
+ val meths =
+ (if skolem then skolem_methods
+ else if is_arith_rule rule then arith_methods
+ else if is_datatype_rule rule then datatype_methods
+ else systematic_methods')
+ |> massage_methods
- val canonical_isar_proof =
- refute_graph
- |> trace ? tap (tracing o prefix "Refute graph:\n" o string_of_refute_graph)
- |> redirect_graph axioms tainted bot
- |> trace ? tap (tracing o prefix "Direct proof:\n" o string_of_direct_proof)
- |> isar_proof true params assms lems
- |> postprocess_isar_proof_remove_show_stuttering
- |> postprocess_isar_proof_remove_unreferenced_steps I
- |> relabel_isar_proof_canonically
-
- val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof
-
- val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
-
- val _ = fold_isar_steps (fn meth =>
- K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
- (steps_of_isar_proof canonical_isar_proof) ()
+ fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "")
+ fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
+ in
+ if is_clause_tainted c then
+ (case gamma of
+ [g] =>
+ if skolem andalso is_clause_tainted g then
+ let
+ val skos = skolems_of ctxt (prop_of_clause g)
+ val subproof = Proof (skos, [], rev accum)
+ in
+ isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
+ end
+ else
+ steps_of_rest (prove [] deps)
+ | _ => steps_of_rest (prove [] deps))
+ else
+ steps_of_rest
+ (if skolem then
+ (case skolems_of ctxt t of
+ [] => prove [] deps
+ | skos => Prove ([], skos, l, t, [], deps, meths, ""))
+ else
+ prove [] deps)
+ end
+ | isar_steps outer predecessor accum (Cases cases :: infs) =
+ let
+ fun isar_case (c, subinfs) =
+ isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs
+ val c = succedent_of_cases cases
+ val l = label_of_clause c
+ val t = prop_of_clause c
+ val step =
+ Prove (maybe_show outer c, [], l, t,
+ map isar_case (filter_out (null o snd) cases),
+ sort_facts (the_list predecessor, []), massage_methods systematic_methods',
+ "")
+ in
+ isar_steps outer (SOME l) (step :: accum) infs
+ end
+ and isar_proof outer fix assms lems infs =
+ Proof (fix, assms,
+ fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs))
- fun str_of_preplay_outcome outcome =
- if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
- fun str_of_meth l meth =
- string_of_proof_method ctxt [] meth ^ " " ^
- str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
- fun comment_of l = map (str_of_meth l) #> commas
+ val trace = Config.get ctxt trace
- fun trace_isar_proof label proof =
- if trace then
- tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^
- string_of_isar_proof ctxt subgoal subgoal_count
- (comment_isar_proof comment_of proof) ^ "\n")
- else
- ()
+ val canonical_isar_proof =
+ refute_graph
+ |> trace ? tap (tracing o prefix "Refute graph:\n" o string_of_refute_graph)
+ |> redirect_graph axioms tainted bot
+ |> trace ? tap (tracing o prefix "Direct proof:\n" o string_of_direct_proof)
+ |> isar_proof true params assms lems
+ |> postprocess_isar_proof_remove_show_stuttering
+ |> postprocess_isar_proof_remove_unreferenced_steps I
+ |> relabel_isar_proof_canonically
- fun comment_of l (meth :: _) =
- (case (verbose,
- Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of
- (false, Played _) => ""
- | (_, outcome) => string_of_play_outcome outcome)
+ val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof
+
+ val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
+
+ val _ = fold_isar_steps (fn meth =>
+ K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
+ (steps_of_isar_proof canonical_isar_proof) ()
- val (play_outcome, isar_proof) =
- canonical_isar_proof
- |> tap (trace_isar_proof "Original")
- |> compress_isar_proof ctxt compress preplay_timeout preplay_data
- |> tap (trace_isar_proof "Compressed")
- |> postprocess_isar_proof_remove_unreferenced_steps
- (keep_fastest_method_of_isar_step (!preplay_data)
- #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
- |> tap (trace_isar_proof "Minimized")
- |> `(preplay_outcome_of_isar_proof (!preplay_data))
- ||> (comment_isar_proof comment_of
- #> chain_isar_proof
- #> kill_useless_labels_in_isar_proof
- #> relabel_isar_proof_nicely
- #> rationalize_obtains_in_isar_proofs ctxt)
- in
- (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of
- (0, 1) =>
- one_line_proof_text ctxt 0
- (if play_outcome_ord (play_outcome, one_line_play) = LESS then
- (case isar_proof of
- Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
- let
- val used_facts' = filter (fn (s, (sc, _)) =>
- member (op =) gfs s andalso sc <> Chained) used_facts
- in
- ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count)
- end)
- else
- one_line_params) ^
- (if isar_proofs = SOME true then "\n(No Isar proof available.)"
- else "")
- | (_, num_steps) =>
- let
- val msg =
- (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] else []) @
- (if do_preplay then [string_of_play_outcome play_outcome] else [])
+ fun str_of_preplay_outcome outcome =
+ if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
+ fun str_of_meth l meth =
+ string_of_proof_method ctxt [] meth ^ " " ^
+ str_of_preplay_outcome
+ (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
+ fun comment_of l = map (str_of_meth l) #> commas
+
+ fun trace_isar_proof label proof =
+ if trace then
+ tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^
+ string_of_isar_proof ctxt subgoal subgoal_count
+ (comment_isar_proof comment_of proof) ^ "\n")
+ else
+ ()
+
+ fun comment_of l (meth :: _) =
+ (case (verbose,
+ Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of
+ (false, Played _) => ""
+ | (_, outcome) => string_of_play_outcome outcome)
+
+ val (play_outcome, isar_proof) =
+ canonical_isar_proof
+ |> tap (trace_isar_proof "Original")
+ |> compress_isar_proof ctxt compress preplay_timeout preplay_data
+ |> tap (trace_isar_proof "Compressed")
+ |> postprocess_isar_proof_remove_unreferenced_steps
+ (keep_fastest_method_of_isar_step (!preplay_data)
+ #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
+ |> tap (trace_isar_proof "Minimized")
+ |> `(preplay_outcome_of_isar_proof (!preplay_data))
+ ||> (comment_isar_proof comment_of
+ #> chain_isar_proof
+ #> kill_useless_labels_in_isar_proof
+ #> relabel_isar_proof_nicely
+ #> rationalize_obtains_in_isar_proofs ctxt)
in
- one_line_proof_text ctxt 0 one_line_params ^
- "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
- Active.sendback_markup [Markup.padding_command]
- (string_of_isar_proof ctxt subgoal subgoal_count isar_proof)
- end)
+ (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of
+ (0, 1) =>
+ one_line_proof_text ctxt 0
+ (if play_outcome_ord (play_outcome, one_line_play) = LESS then
+ (case isar_proof of
+ Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
+ let
+ val used_facts' = filter (fn (s, (sc, _)) =>
+ member (op =) gfs s andalso sc <> Chained) used_facts
+ in
+ ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count)
+ end)
+ else
+ one_line_params) ^
+ (if isar_proofs = SOME true then "\n(No Isar proof available.)" else "")
+ | (_, num_steps) =>
+ let
+ val msg =
+ (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps]
+ else []) @
+ (if do_preplay then [string_of_play_outcome play_outcome] else [])
+ in
+ one_line_proof_text ctxt 0 one_line_params ^
+ "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
+ Active.sendback_markup [Markup.padding_command]
+ (string_of_isar_proof ctxt subgoal subgoal_count isar_proof)
+ end)
+ end
end
in
if debug then