--- a/NEWS Mon Jun 22 16:56:03 2015 +0200
+++ b/NEWS Mon Jun 22 21:50:56 2015 +0200
@@ -20,7 +20,8 @@
* Local goals ('have', 'show', 'hence', 'thus') allow structured
statements like fixes/assumes/shows in theorem specifications, but the
-notation is postfix with keywords 'if' and 'for'. For example:
+notation is postfix with keywords 'if' (or 'when') and 'for'. For
+example:
have result: "C x y"
if "A x" and "B y"
@@ -38,6 +39,9 @@
}
note result = this
+The keyword 'when' may be used instead of 'if', to indicate 'presume'
+instead of 'assume' above.
+
* New command 'supply' supports fact definitions during goal refinement
('apply' scripts).
@@ -62,6 +66,22 @@
then show ?thesis <proof>
qed
+* Nesting of Isar goal structure has been clarified: the context after
+the initial backwards refinement is retained for the whole proof, within
+all its context sections (as indicated via 'next'). This is e.g.
+relevant for 'using', 'including', 'supply':
+
+ have "A \<and> A" if a: A for A
+ supply [simp] = a
+ proof
+ show A by simp
+ next
+ show A by simp
+ qed
+
+* Method "sleep" succeeds after a real-time delay (in seconds). This is
+occasionally useful for demonstration and testing purposes.
+
*** Pure ***
--- a/src/CCL/Term.thy Mon Jun 22 16:56:03 2015 +0200
+++ b/src/CCL/Term.thy Mon Jun 22 21:50:56 2015 +0200
@@ -17,7 +17,7 @@
inl :: "i\<Rightarrow>i"
inr :: "i\<Rightarrow>i"
- when :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
+ "when" :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
split :: "[i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
fst :: "i\<Rightarrow>i"
--- a/src/CTT/CTT.thy Mon Jun 22 16:56:03 2015 +0200
+++ b/src/CTT/CTT.thy Mon Jun 22 21:50:56 2015 +0200
@@ -29,7 +29,7 @@
(*Unions*)
inl :: "i\<Rightarrow>i"
inr :: "i\<Rightarrow>i"
- when :: "[i, i\<Rightarrow>i, i\<Rightarrow>i]\<Rightarrow>i"
+ "when" :: "[i, i\<Rightarrow>i, i\<Rightarrow>i]\<Rightarrow>i"
(*General Sum and Binary Product*)
Sum :: "[t, i\<Rightarrow>t]\<Rightarrow>t"
fst :: "i\<Rightarrow>i"
--- a/src/Doc/Isar_Ref/Generic.thy Mon Jun 22 16:56:03 2015 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Mon Jun 22 21:50:56 2015 +0200
@@ -67,8 +67,9 @@
@{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\
@{method_def intro} & : & @{text method} \\
@{method_def elim} & : & @{text method} \\
+ @{method_def fail} & : & @{text method} \\
@{method_def succeed} & : & @{text method} \\
- @{method_def fail} & : & @{text method} \\
+ @{method_def sleep} & : & @{text method} \\
\end{matharray}
@{rail \<open>
@@ -78,6 +79,8 @@
('(' @{syntax nat} ')')? @{syntax thmrefs}
;
(@@{method intro} | @@{method elim}) @{syntax thmrefs}?
+ ;
+ @@{method sleep} @{syntax real}
\<close>}
\begin{description}
@@ -114,13 +117,17 @@
this allows fine-tuned decomposition of a proof problem, in contrast
to common automated tools.
+ \item @{method fail} yields an empty result sequence; it is the
+ identity of the ``@{text "|"}'' method combinator (cf.\
+ \secref{sec:proof-meth}).
+
\item @{method succeed} yields a single (unchanged) result; it is
the identity of the ``@{text ","}'' method combinator (cf.\
\secref{sec:proof-meth}).
- \item @{method fail} yields an empty result sequence; it is the
- identity of the ``@{text "|"}'' method combinator (cf.\
- \secref{sec:proof-meth}).
+ \item @{method sleep}~@{text s} succeeds after a real-time delay of @{text
+ s} seconds. This is occasionally useful for demonstration and testing
+ purposes.
\end{description}
--- a/src/Doc/Isar_Ref/Proof.thy Mon Jun 22 16:56:03 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Mon Jun 22 21:50:56 2015 +0200
@@ -427,13 +427,15 @@
@@{command schematic_corollary}) (stmt | statement)
;
(@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
- stmt (@'if' stmt)? @{syntax for_fixes}
+ stmt cond_stmt @{syntax for_fixes}
;
@@{command print_statement} @{syntax modes}? @{syntax thmrefs}
;
stmt: (@{syntax props} + @'and')
;
+ cond_stmt: ((@'if' | @'when') stmt)?
+ ;
statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
conclusion
;
@@ -516,10 +518,10 @@
@{variable_ref "?thesis"}) to be bound automatically, see also
\secref{sec:term-abbrev}.
- Structured goal statements involving @{keyword_ref "if"} define the
- special fact @{fact_ref that} to refer to these assumptions in the proof
- body. The user may provide separate names according to the syntax of the
- statement.
+ Structured goal statements involving @{keyword_ref "if"} or @{keyword_ref
+ "when"} define the special fact @{fact_ref that} to refer to these
+ assumptions in the proof body. The user may provide separate names
+ according to the syntax of the statement.
\<close>
--- a/src/FOLP/IFOLP.thy Mon Jun 22 16:56:03 2015 +0200
+++ b/src/FOLP/IFOLP.thy Mon Jun 22 21:50:56 2015 +0200
@@ -50,7 +50,7 @@
split :: "[p, [p,p]=>p] =>p"
inl :: "p=>p"
inr :: "p=>p"
- when :: "[p, p=>p, p=>p]=>p"
+ "when" :: "[p, p=>p, p=>p]=>p"
lambda :: "(p => p) => p" (binder "lam " 55)
App :: "[p,p]=>p" (infixl "`" 60)
alll :: "['a=>p]=>p" (binder "all " 55)
--- a/src/HOL/Eisbach/Eisbach_Tools.thy Mon Jun 22 16:56:03 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach_Tools.thy Mon Jun 22 21:50:56 2015 +0200
@@ -14,7 +14,8 @@
fun trace_method parser print =
Scan.lift (Args.mode "dummy") -- parser >>
(fn (dummy, x) => fn ctxt => SIMPLE_METHOD (fn st =>
- (if dummy orelse not (Method_Closure.is_dummy st) then tracing (print ctxt x) else ();
+ (if dummy orelse not (Method.detect_closure_state st)
+ then tracing (print ctxt x) else ();
all_tac st)));
fun setup_trace_method binding parser print =
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML Mon Jun 22 16:56:03 2015 +0200
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Mon Jun 22 21:50:56 2015 +0200
@@ -87,7 +87,7 @@
map snd type_insts
|> Syntax.read_typs ctxt1;
- val typ_insts' = map2 (fn (xi, _) => fn T => (xi,T)) type_insts typs;
+ val typ_insts' = map2 (fn (xi, _) => fn T => (xi, T)) type_insts typs;
val terms =
map snd term_insts
@@ -95,7 +95,7 @@
val term_insts' = map2 (fn (xi, _) => fn t => (xi, t)) term_insts terms;
- in (typ_insts',term_insts') end;
+ in (typ_insts', term_insts') end;
datatype rule_inst =
@@ -153,7 +153,7 @@
val _ =
(insts', term_insts)
|> ListPair.app (fn (SOME p, SOME t) => Parse_Tools.the_parse_fun p t | _ => ());
- val (insts'',concl_insts'') = chop (length insts) term_insts;
+ val (insts'', concl_insts'') = chop (length insts) term_insts;
in Unchecked_Term_Insts (insts'', concl_insts'') end;
fun read_of_insts checked context ((insts, concl_insts), fixes) =
--- a/src/HOL/Eisbach/match_method.ML Mon Jun 22 16:56:03 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML Mon Jun 22 21:50:56 2015 +0200
@@ -342,33 +342,28 @@
val outer_env = morphism_env morphism env;
val thm' = Morphism.thm morphism thm;
in inst_thm ctxt outer_env params ts thm' end
- | export_with_params _ morphism (NONE,_) thm _ = Morphism.thm morphism thm;
+ | export_with_params _ morphism (NONE, _) thm _ = Morphism.thm morphism thm;
fun match_filter_env is_newly_fixed pat_vars fixes params env =
let
val param_vars = map Term.dest_Var params;
val tenv = Envir.term_env env;
-
val params' = map (fn (xi, _) => Vartab.lookup tenv xi) param_vars;
val fixes_vars = map Term.dest_Var fixes;
val all_vars = Vartab.keys tenv;
-
val extra_vars = subtract (fn ((xi, _), xi') => xi = xi') fixes_vars all_vars;
val tenv' = tenv |> fold (Vartab.delete_safe) extra_vars;
-
val env' =
Envir.Envir {maxidx = Envir.maxidx_of env, tenv = tenv', tyenv = Envir.type_env env}
- val all_params_bound = forall (fn SOME (_, Free (x,_)) => is_newly_fixed x | _ => false) params';
-
+ val all_params_bound = forall (fn SOME (_, Free (x, _)) => is_newly_fixed x | _ => false) params';
val all_params_distinct = not (has_duplicates (op =) params');
val pat_fixes = inter (eq_fst (op =)) fixes_vars pat_vars;
-
val all_pat_fixes_bound = forall (fn (xi, _) => is_some (Vartab.lookup tenv' xi)) pat_fixes;
in
if all_params_bound andalso all_pat_fixes_bound andalso all_params_distinct
@@ -413,7 +408,7 @@
val ct = Drule.mk_term (hyp) |> Thm.cprop_of;
in Drule.protect (Conjunction.mk_conjunction (ident, ct)) end;
-fun hyp_from_ctermid ctxt (ident,cterm) =
+fun hyp_from_ctermid ctxt (ident, cterm) =
let
val ident = Thm.cterm_of ctxt (HOLogic.mk_number @{typ nat} ident |> Logic.mk_term);
in Drule.protect (Conjunction.mk_conjunction (ident, cterm)) end;
@@ -468,13 +463,13 @@
fun prem_from_hyp hyp goal =
let
val asm = Thm.assume hyp;
- val (identt,ct) = asm |> Goal.conclude |> Thm.cprop_of |> Conjunction.dest_conjunction;
+ val (identt, ct) = asm |> Goal.conclude |> Thm.cprop_of |> Conjunction.dest_conjunction;
val ident = HOLogic.dest_number (Thm.term_of identt |> Logic.dest_term) |> snd;
val thm = Conjunction.intr (solve_term identt) (solve_term ct) |> Goal.protect 0
val goal' = Thm.implies_elim (Thm.implies_intr hyp goal) thm;
in
- (SOME (ident,ct),goal')
- end handle TERM _ => (NONE,goal) | THM _ => (NONE,goal);
+ (SOME (ident, ct), goal')
+ end handle TERM _ => (NONE, goal) | THM _ => (NONE, goal);
in
fold_map prem_from_hyp chyps goal
|>> map_filter I
@@ -486,7 +481,7 @@
let
val {context, params, prems, asms, concl, schematics} = focus;
- val (prem_ids,ctxt') = context
+ val (prem_ids, ctxt') = context
|> add_focus_params params
|> add_focus_schematics (snd schematics)
|> fold_map add_focus_prem (rev prems)
@@ -495,12 +490,13 @@
val ctxt'' = fold add_premid_hyp local_prems ctxt';
in
- (prem_ids,{context = ctxt'',
- params = params,
- prems = prems,
- concl = concl,
- schematics = schematics,
- asms = asms})
+ (prem_ids,
+ {context = ctxt'',
+ params = params,
+ prems = prems,
+ concl = concl,
+ schematics = schematics,
+ asms = asms})
end;
@@ -541,32 +537,32 @@
forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) (Vartab.dest tenv)
end;
-fun term_eq_wrt (env1,env2) (t1,t2) =
+fun term_eq_wrt (env1, env2) (t1, t2) =
Envir.eta_contract (Envir.norm_term env1 t1) aconv
Envir.eta_contract (Envir.norm_term env2 t2);
-fun type_eq_wrt (env1,env2) (T1,T2) =
- Envir.norm_type (Envir.type_env env1) T1 = Envir.norm_type (Envir.type_env env2) T2
+fun type_eq_wrt (env1, env2) (T1, T2) =
+ Envir.norm_type (Envir.type_env env1) T1 = Envir.norm_type (Envir.type_env env2) T2;
fun eq_env (env1, env2) =
Envir.maxidx_of env1 = Envir.maxidx_of env1 andalso
ListPair.allEq (fn ((var, (_, t)), (var', (_, t'))) =>
- (var = var' andalso term_eq_wrt (env1,env2) (t,t')))
+ (var = var' andalso term_eq_wrt (env1, env2) (t, t')))
(apply2 Vartab.dest (Envir.term_env env1, Envir.term_env env2))
andalso
ListPair.allEq (fn ((var, (_, T)), (var', (_, T'))) =>
- var = var' andalso type_eq_wrt (env1,env2) (T,T'))
+ var = var' andalso type_eq_wrt (env1, env2) (T, T'))
(apply2 Vartab.dest (Envir.type_env env1, Envir.type_env env2));
-fun merge_env (env1,env2) =
+fun merge_env (env1, env2) =
let
val tenv =
Vartab.merge (eq_snd (term_eq_wrt (env1, env2))) (Envir.term_env env1, Envir.term_env env2);
val tyenv =
Vartab.merge (eq_snd (type_eq_wrt (env1, env2)) andf eq_fst (op =))
- (Envir.type_env env1,Envir.type_env env2);
+ (Envir.type_env env1, Envir.type_env env2);
val maxidx = Int.max (Envir.maxidx_of env1, Envir.maxidx_of env2);
in Envir.Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv} end;
@@ -600,7 +596,7 @@
fun do_cut n = if n = ~1 then I else Seq.take n;
val raw_thmss = map (get o snd) prop_pats;
- val (thmss,ctxt') = fold_burrow import_with_tags raw_thmss ctxt;
+ val (thmss, ctxt') = fold_burrow import_with_tags raw_thmss ctxt;
val newly_fixed = Variable.is_newly_fixed ctxt' ctxt;
@@ -619,7 +615,7 @@
|> Seq.filter consistent_env
|> Seq.map_filter (fn env' =>
(case match_filter_env newly_fixed pat_vars fixes params env' of
- SOME env'' => SOME (export_with_params ctxt morphism (ts,params) thm env',env'')
+ SOME env'' => SOME (export_with_params ctxt morphism (ts, params) thm env', env'')
| NONE => NONE))
|> Seq.map (apfst (Thm.map_tags (K (Thm.get_tags thm))))
|> deduplicate (eq_pair Thm.eq_thm_prop eq_env) []
@@ -642,7 +638,7 @@
Seq_retrieve envthms (fn (env, _) => eq_env (env, env'));
in
(case result of
- SOME (_,thms) => SOME ((env', thm :: thms), maximal_set tail seq' envthms')
+ SOME (_, thms) => SOME ((env', thm :: thms), maximal_set tail seq' envthms')
| NONE => Seq.pull (maximal_set (tail @ [(env', [thm])]) seq' envthms'))
end
| NONE => Seq.pull (Seq.append envthms (Seq.of_list tail))));
@@ -660,8 +656,8 @@
else
let
fun just_one (thm, env') =
- (case try_merge (env,env') of
- SOME env'' => SOME ((pat,[thm]) :: pats, env'')
+ (case try_merge (env, env') of
+ SOME env'' => SOME ((pat, [thm]) :: pats, env'')
| NONE => NONE);
in fold (fn seq => Seq.append (Seq.map_filter just_one seq)) thmenvs Seq.empty end);
@@ -713,9 +709,9 @@
| Match_Concl => g
| _ => raise Fail "Match kind fell through");
- val (goal_thins,goal) = get_thinned_prems goal;
+ val (goal_thins, goal) = get_thinned_prems goal;
- val ((local_premids,{context = focus_ctxt, params, asms, concl, ...}), focused_goal) =
+ val ((local_premids, {context = focus_ctxt, params, asms, concl, ...}), focused_goal) =
focus_cases (K Subgoal.focus_prems) (focus_concl) ctxt 1 goal
|>> augment_focus;
@@ -725,7 +721,7 @@
make_fact_matches focus_ctxt
(Item_Net.retrieve (focus_prems focus_ctxt |> snd)
#> filter_out (member (eq_fst (op =)) goal_thins)
- #> is_local ? filter (fn (p,_) => exists (fn id' => id' = p) local_premids)
+ #> is_local ? filter (fn (p, _) => exists (fn id' => id' = p) local_premids)
#> order_list))
(fn _ =>
make_term_matches focus_ctxt (fn _ => [Logic.strip_imp_concl (Thm.term_of concl)]))
@@ -735,7 +731,7 @@
fun do_retrofit inner_ctxt goal' =
let
- val (goal'_thins,goal') = get_thinned_prems goal';
+ val (goal'_thins, goal') = get_thinned_prems goal';
val thinned_prems =
((subtract (eq_fst (op =))
@@ -750,7 +746,7 @@
thinned_prems @
map (fn (id, prem) => (id, (NONE, SOME prem))) (goal'_thins @ goal_thins);
- val (thinned_local_prems,thinned_extra_prems) =
+ val (thinned_local_prems, thinned_extra_prems) =
List.partition (fn (id, _) => member (op =) local_premids id) all_thinned_prems;
val local_thins =
@@ -795,9 +791,8 @@
val match_parser =
parse_match_kind :-- (fn kind =>
Scan.lift @{keyword "in"} |-- Parse.enum1' "\<bar>" (parse_named_pats kind)) >>
- (fn (matches, bodies) => fn ctxt => fn using => fn goal =>
- if Method_Closure.is_dummy goal then Seq.empty
- else
+ (fn (matches, bodies) => fn ctxt => fn using =>
+ Method.RUNTIME (fn st =>
let
fun exec (pats, fixes, text) goal =
let
@@ -805,7 +800,7 @@
fold Variable.declare_term fixes ctxt
|> fold (fn (_, t) => Variable.declare_term t) pats; (*Is this a good idea? We really only care about the maxidx*)
in real_match using ctxt' fixes matches text pats goal end;
- in Seq.flat (Seq.FIRST (map exec bodies) goal) end);
+ in Seq.flat (Seq.FIRST (map exec bodies) st) end));
val _ =
Theory.setup
--- a/src/HOL/Eisbach/method_closure.ML Mon Jun 22 16:56:03 2015 +0200
+++ b/src/HOL/Eisbach/method_closure.ML Mon Jun 22 21:50:56 2015 +0200
@@ -10,7 +10,6 @@
signature METHOD_CLOSURE =
sig
- val is_dummy: thm -> bool
val tag_free_thm: thm -> thm
val is_free_thm: thm -> bool
val dummy_free_thm: thm
@@ -71,11 +70,6 @@
(* free thm *)
-fun is_dummy thm =
- (case try Logic.dest_term (Thm.concl_of (perhaps (try Goal.conclude) thm)) of
- NONE => false
- | SOME t => Term.is_dummy_pattern t);
-
val free_thmN = "Method_Closure.free_thm";
fun tag_free_thm thm = Thm.tag_rule (free_thmN, "") thm;
@@ -91,7 +85,7 @@
if exists is_free_thm (thm :: args) then dummy_free_thm
else f context thm);
-fun free_aware_attribute thy {handle_all_errs,declaration} src (context, thm) =
+fun free_aware_attribute thy {handle_all_errs, declaration} src (context, thm) =
let
val src' = Token.init_assignable_src src;
fun apply_att thm = (Attrib.attribute_global thy src') (context, thm);
@@ -233,12 +227,9 @@
Token.Fact (SOME name, evaluate_dynamic_thm ctxt name)
| x => x);
-fun method_evaluate text ctxt : Method.method = fn facts => fn st =>
- let
- val ctxt' = Config.put Method.closure false ctxt;
- in
- if is_dummy st then Seq.empty
- else Method.evaluate (evaluate_named_theorems ctxt' text) ctxt' facts st
+fun method_evaluate text ctxt facts =
+ let val ctxt' = Config.put Method.closure false ctxt in
+ Method.RUNTIME (fn st => Method.evaluate (evaluate_named_theorems ctxt' text) ctxt' facts st)
end;
fun evaluate_method_def fix_env raw_text ctxt =
@@ -270,16 +261,16 @@
fun dummy_named_thm named_thm ctxt =
let
val ctxt' = empty_named_thm named_thm ctxt;
- val (_,ctxt'') = Thm.proof_attributes [Named_Theorems.add named_thm] dummy_free_thm ctxt';
+ val (_, ctxt'') = Thm.proof_attributes [Named_Theorems.add named_thm] dummy_free_thm ctxt';
in ctxt'' end;
fun parse_method_args method_names =
let
- fun bind_method (name, text) ctxt =
- let
- val method = method_evaluate text;
- val inner_update = method o update_dynamic_method (name,K (method ctxt));
- in update_dynamic_method (name,inner_update) ctxt end;
+ fun bind_method (name, text) ctxt =
+ let
+ val method = method_evaluate text;
+ val inner_update = method o update_dynamic_method (name, K (method ctxt));
+ in update_dynamic_method (name, inner_update) ctxt end;
fun do_parse t = parse_method >> pair t;
fun rep [] x = Scan.succeed [] x
@@ -349,7 +340,7 @@
(parse_term_args args --
parse_method_args method_names --|
(Scan.depend (fn context =>
- Scan.succeed (Context.map_proof (fold empty_named_thm uses_nms) context,())) --
+ Scan.succeed (Context.map_proof (fold empty_named_thm uses_nms) context, ())) --
Method.sections modifiers) >> eval);
val lthy3 = lthy2
--- a/src/HOL/Isar_Examples/Structured_Statements.thy Mon Jun 22 16:56:03 2015 +0200
+++ b/src/HOL/Isar_Examples/Structured_Statements.thy Mon Jun 22 21:50:56 2015 +0200
@@ -130,4 +130,33 @@
qed
end
-end
\ No newline at end of file
+
+subsection \<open>Suffices-to-show\<close>
+
+notepad
+begin
+ fix A B C
+ assume r: "A \<Longrightarrow> B \<Longrightarrow> C"
+
+ have C
+ proof -
+ show ?thesis when A (is ?A) and B (is ?B)
+ using that by (rule r)
+ show ?A sorry
+ show ?B sorry
+ qed
+next
+ fix a :: 'a
+ fix A :: "'a \<Rightarrow> bool"
+ fix C
+
+ have C
+ proof -
+ show ?thesis when "A x" (is ?A) for x :: 'a -- \<open>abstract @{term x}\<close>
+ using that sorry
+ show "?A a" -- \<open>concrete @{term a}\<close>
+ sorry
+ qed
+end
+
+end
--- a/src/HOL/Library/Formal_Power_Series.thy Mon Jun 22 16:56:03 2015 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Mon Jun 22 21:50:56 2015 +0200
@@ -508,9 +508,9 @@
using dist_fps_ge0[of a b] dist_fps_ge0[of a c] dist_fps_ge0[of b c]
by auto
have th1: "\<And>n. (2::real)^n > 0" by auto
- {
- assume h: "dist a b > dist a c + dist b c"
- then have gt: "dist a b > dist a c" "dist a b > dist b c"
+ have False if "dist a b > dist a c + dist b c"
+ proof -
+ from that have gt: "dist a b > dist a c" "dist a b > dist b c"
using pos by auto
from gt have gtn: "n a b < n b c" "n a b < n a c"
unfolding dab dbc dac by (auto simp add: th1)
@@ -518,8 +518,8 @@
have "a $ n a b = b $ n a b" by simp
moreover have "a $ n a b \<noteq> b $ n a b"
unfolding n_def by (rule LeastI_ex) (insert \<open>a \<noteq> b\<close>, simp add: fps_eq_iff)
- ultimately have False by contradiction
- }
+ ultimately show ?thesis by contradiction
+ qed
then show ?thesis
by (auto simp add: not_le[symmetric])
qed
@@ -527,7 +527,7 @@
end
-text \<open>The infinite sums and justification of the notation in textbooks\<close>
+text \<open>The infinite sums and justification of the notation in textbooks.\<close>
lemma reals_power_lt_ex:
fixes x y :: real
@@ -576,19 +576,17 @@
lemma fps_notation: "(\<lambda>n. setsum (\<lambda>i. fps_const(a$i) * X^i) {0..n}) ----> a"
(is "?s ----> a")
proof -
- {
- fix r :: real
- assume "r > 0"
+ have "\<exists>n0. \<forall>n \<ge> n0. dist (?s n) a < r" if "r > 0" for r
+ proof -
obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0"
using reals_power_lt_ex[OF \<open>r > 0\<close>, of 2] by auto
- have "\<exists>n0. \<forall>n \<ge> n0. dist (?s n) a < r"
+ show ?thesis
proof -
- {
- fix n :: nat
- assume nn0: "n \<ge> n0"
- then have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0"
+ have "dist (?s n) a < r" if nn0: "n \<ge> n0" for n
+ proof -
+ from that have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0"
by (simp add: divide_simps)
- have "dist (?s n) a < r"
+ show ?thesis
proof (cases "?s n = a")
case True
then show ?thesis
@@ -610,10 +608,10 @@
using n0 by simp
finally show ?thesis .
qed
- }
+ qed
then show ?thesis by blast
qed
- }
+ qed
then show ?thesis
unfolding lim_sequentially by blast
qed
@@ -623,7 +621,7 @@
declare setsum.cong[fundef_cong]
-instantiation fps :: ("{comm_monoid_add, inverse, times, uminus}") inverse
+instantiation fps :: ("{comm_monoid_add,inverse,times,uminus}") inverse
begin
fun natfun_inverse:: "'a fps \<Rightarrow> nat \<Rightarrow> 'a"
@@ -778,8 +776,8 @@
shows "fps_deriv (f * g) = f * fps_deriv g + fps_deriv f * g"
proof -
let ?D = "fps_deriv"
- {
- fix n :: nat
+ have "(f * ?D g + ?D f * g) $ n = ?D (f*g) $ n" for n
+ proof -
let ?Zn = "{0 ..n}"
let ?Zn1 = "{0 .. n + 1}"
let ?g = "\<lambda>i. of_nat (i+1) * g $ (i+1) * f $ (n - i) +
@@ -806,9 +804,10 @@
apply (rule setsum.cong)
apply (auto simp add: of_nat_diff field_simps)
done
- finally have "(f * ?D g + ?D f * g) $ n = ?D (f*g) $ n" .
- }
- then show ?thesis unfolding fps_eq_iff by auto
+ finally show ?thesis .
+ qed
+ then show ?thesis
+ unfolding fps_eq_iff by auto
qed
lemma fps_deriv_X[simp]: "fps_deriv X = 1"
@@ -1407,9 +1406,10 @@
assumes "h \<le> k"
shows "natpermute n k =
(\<Union>m \<in>{0..n}. {l1 @ l2 |l1 l2. l1 \<in> natpermute m h \<and> l2 \<in> natpermute (n - m) (k - h)})"
- (is "?L = ?R" is "?L = (\<Union>m \<in>{0..n}. ?S m)")
-proof -
- {
+ (is "?L = ?R" is "_ = (\<Union>m \<in>{0..n}. ?S m)")
+proof
+ show "?R \<subseteq> ?L"
+ proof
fix l
assume l: "l \<in> ?R"
from l obtain m xs ys where h: "m \<in> {0..n}"
@@ -1420,16 +1420,16 @@
by (simp add: natpermute_def)
from ys have ys': "listsum ys = n - m"
by (simp add: natpermute_def)
- have "l \<in> ?L" using leq xs ys h
+ show "l \<in> ?L" using leq xs ys h
apply (clarsimp simp add: natpermute_def)
unfolding xs' ys'
using assms xs ys
unfolding natpermute_def
apply simp
done
- }
- moreover
- {
+ qed
+ show "?L \<subseteq> ?R"
+ proof
fix l
assume l: "l \<in> natpermute n k"
let ?xs = "take h l"
@@ -1445,7 +1445,7 @@
using l assms ls by (auto simp add: natpermute_def simp del: append_take_drop_id)
from ls have m: "?m \<in> {0..n}"
by (simp add: l_take_drop del: append_take_drop_id)
- from xs ys ls have "l \<in> ?R"
+ from xs ys ls show "l \<in> ?R"
apply auto
apply (rule bexI [where x = "?m"])
apply (rule exI [where x = "?xs"])
@@ -1454,8 +1454,7 @@
apply (auto simp add: natpermute_def l_take_drop simp del: append_take_drop_id)
apply simp
done
- }
- ultimately show ?thesis by blast
+ qed
qed
lemma natpermute_0: "natpermute n 0 = (if n = 0 then {[]} else {})"
@@ -1486,13 +1485,16 @@
qed
lemma natpermute_contain_maximal:
- "{xs \<in> natpermute n (k+1). n \<in> set xs} = UNION {0 .. k} (\<lambda>i. {(replicate (k+1) 0) [i:=n]})"
+ "{xs \<in> natpermute n (k + 1). n \<in> set xs} = (\<Union>i\<in>{0 .. k}. {(replicate (k + 1) 0) [i:=n]})"
(is "?A = ?B")
-proof -
- {
+proof
+ show "?A \<subseteq> ?B"
+ proof
fix xs
- assume H: "xs \<in> natpermute n (k+1)" and n: "n \<in> set xs"
- from n obtain i where i: "i \<in> {0.. k}" "xs!i = n" using H
+ assume "xs \<in> ?A"
+ then have H: "xs \<in> natpermute n (k + 1)" and n: "n \<in> set xs"
+ by blast+
+ then obtain i where i: "i \<in> {0.. k}" "xs!i = n"
unfolding in_set_conv_nth by (auto simp add: less_Suc_eq_le natpermute_def)
have eqs: "({0..k} - {i}) \<union> {i} = {0..k}"
using i by auto
@@ -1522,33 +1524,34 @@
apply (case_tac "ia = i")
apply (auto simp del: replicate.simps)
done
- then have "xs \<in> ?B" using i by blast
- }
- moreover
- {
- fix i
- assume i: "i \<in> {0..k}"
- let ?xs = "replicate (k+1) 0 [i:=n]"
- have nxs: "n \<in> set ?xs"
+ then show "xs \<in> ?B" using i by blast
+ qed
+ show "?B \<subseteq> ?A"
+ proof
+ fix xs
+ assume "xs \<in> ?B"
+ then obtain i where i: "i \<in> {0..k}" and xs: "xs = replicate (k + 1) 0 [i:=n]"
+ by auto
+ have nxs: "n \<in> set xs"
+ unfolding xs
apply (rule set_update_memI)
using i apply simp
done
- have xsl: "length ?xs = k+1"
- by (simp only: length_replicate length_list_update)
- have "listsum ?xs = setsum (nth ?xs) {0..<k+1}"
+ have xsl: "length xs = k + 1"
+ by (simp only: xs length_replicate length_list_update)
+ have "listsum xs = setsum (nth xs) {0..<k+1}"
unfolding listsum_setsum_nth xsl ..
also have "\<dots> = setsum (\<lambda>j. if j = i then n else 0) {0..< k+1}"
- by (rule setsum.cong) (simp_all del: replicate.simps)
+ by (rule setsum.cong) (simp_all add: xs del: replicate.simps)
also have "\<dots> = n" using i by (simp add: setsum.delta)
- finally have "?xs \<in> natpermute n (k+1)"
+ finally have "xs \<in> natpermute n (k + 1)"
using xsl unfolding natpermute_def mem_Collect_eq by blast
- then have "?xs \<in> ?A"
- using nxs by blast
- }
- ultimately show ?thesis by auto
+ then show "xs \<in> ?A"
+ using nxs by blast
+ qed
qed
-text \<open>The general form\<close>
+text \<open>The general form.\<close>
lemma fps_setprod_nth:
fixes m :: nat
and a :: "nat \<Rightarrow> 'a::comm_ring_1 fps"
@@ -1603,7 +1606,7 @@
qed
qed
-text \<open>The special form for powers\<close>
+text \<open>The special form for powers.\<close>
lemma fps_power_nth_Suc:
fixes m :: nat
and a :: "'a::comm_ring_1 fps"
@@ -1708,8 +1711,8 @@
next
fix r k a n xs i
assume xs: "xs \<in> {xs \<in> natpermute (Suc n) (Suc k). Suc n \<notin> set xs}" and i: "i \<in> {0..k}"
- {
- assume c: "Suc n \<le> xs ! i"
+ have False if c: "Suc n \<le> xs ! i"
+ proof -
from xs i have "xs !i \<noteq> Suc n"
by (auto simp add: in_set_conv_nth natpermute_def)
with c have c': "Suc n < xs!i" by arith
@@ -1727,8 +1730,8 @@
unfolding eqs setsum.union_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)]
unfolding setsum.union_disjoint[OF fths(2) fths(3) d(2)]
by simp
- finally have False using c' by simp
- }
+ finally show ?thesis using c' by simp
+ qed
then show "((r, Suc k, a, xs!i), r, Suc k, a, Suc n) \<in> ?R"
apply auto
apply (metis not_less)
@@ -1775,7 +1778,7 @@
lemma natpermute_max_card:
assumes n0: "n \<noteq> 0"
- shows "card {xs \<in> natpermute n (k+1). n \<in> set xs} = k + 1"
+ shows "card {xs \<in> natpermute n (k + 1). n \<in> set xs} = k + 1"
unfolding natpermute_contain_maximal
proof -
let ?A = "\<lambda>i. {replicate (k + 1) 0[i := n]}"
@@ -1789,16 +1792,16 @@
proof clarify
fix i j
assume i: "i \<in> ?K" and j: "j \<in> ?K" and ij: "i \<noteq> j"
- {
- assume eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]"
+ have False if eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]"
+ proof -
have "(replicate (k+1) 0 [i:=n] ! i) = n"
using i by (simp del: replicate.simps)
moreover
have "(replicate (k+1) 0 [j:=n] ! i) = 0"
using i ij by (simp del: replicate.simps)
- ultimately have False
+ ultimately show ?thesis
using eq n0 by (simp del: replicate.simps)
- }
+ qed
then show "{replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
by auto
qed
@@ -1811,10 +1814,11 @@
fixes a:: "'a::field_char_0 fps"
assumes a0: "a$0 \<noteq> 0"
shows "(r (Suc k) (a$0)) ^ Suc k = a$0 \<longleftrightarrow> (fps_radical r (Suc k) a) ^ (Suc k) = a"
-proof -
+ (is "?lhs \<longleftrightarrow> ?rhs")
+proof
let ?r = "fps_radical r (Suc k) a"
- {
- assume r0: "(r (Suc k) (a$0)) ^ Suc k = a$0"
+ show ?rhs if r0: ?lhs
+ proof -
from a0 r0 have r00: "r (Suc k) (a$0) \<noteq> 0" by auto
have "?r ^ Suc k $ z = a$z" for z
proof (induct z rule: nat_less_induct)
@@ -1865,17 +1869,16 @@
finally show ?thesis .
qed
qed
- then have ?thesis using r0 by (simp add: fps_eq_iff)
- }
- moreover
- {
- assume h: "(fps_radical r (Suc k) a) ^ (Suc k) = a"
- then have "((fps_radical r (Suc k) a) ^ (Suc k))$0 = a$0" by simp
- then have "(r (Suc k) (a$0)) ^ Suc k = a$0"
+ then show ?thesis using r0 by (simp add: fps_eq_iff)
+ qed
+ show ?lhs if ?rhs
+ proof -
+ from that have "((fps_radical r (Suc k) a) ^ (Suc k))$0 = a$0"
+ by simp
+ then show ?thesis
unfolding fps_power_nth_Suc
by (simp add: setprod_constant del: replicate.simps)
- }
- ultimately show ?thesis by blast
+ qed
qed
(*
@@ -2101,16 +2104,17 @@
assumes k: "k > 0"
and ra0: "r k (a $ 0) ^ k = a $ 0"
and rb0: "r k (b $ 0) ^ k = b $ 0"
- and a0: "a$0 \<noteq> 0"
- and b0: "b$0 \<noteq> 0"
+ and a0: "a $ 0 \<noteq> 0"
+ and b0: "b $ 0 \<noteq> 0"
shows "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0) \<longleftrightarrow>
- fps_radical r (k) (a*b) = fps_radical r (k) a * fps_radical r (k) (b)"
-proof -
- {
- assume r0': "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0)"
- then have r0: "(r (k) ((a*b)$0)) ^ k = (a*b)$0"
+ fps_radical r k (a * b) = fps_radical r k a * fps_radical r k b"
+ (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+ show ?rhs if r0': ?lhs
+ proof -
+ from r0' have r0: "(r k ((a * b) $ 0)) ^ k = (a * b) $ 0"
by (simp add: fps_mult_nth ra0 rb0 power_mult_distrib)
- have ?thesis
+ show ?thesis
proof (cases k)
case 0
then show ?thesis using r0' by simp
@@ -2127,16 +2131,14 @@
show ?thesis
by (auto simp add: power_mult_distrib simp del: power_Suc)
qed
- }
- moreover
- {
- assume h: "fps_radical r k (a*b) = fps_radical r k a * fps_radical r k b"
- then have "(fps_radical r k (a*b))$0 = (fps_radical r k a * fps_radical r k b)$0"
+ qed
+ show ?lhs if ?rhs
+ proof -
+ from that have "(fps_radical r k (a * b)) $ 0 = (fps_radical r k a * fps_radical r k b) $ 0"
by simp
- then have "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0)"
+ then show ?thesis
using k by (simp add: fps_mult_nth)
- }
- ultimately show ?thesis by blast
+ qed
qed
(*
@@ -2182,7 +2184,8 @@
(is "?lhs = ?rhs")
proof
let ?r = "fps_radical r k"
- from kp obtain h where k: "k = Suc h" by (cases k) auto
+ from kp obtain h where k: "k = Suc h"
+ by (cases k) auto
have ra0': "r k (a$0) \<noteq> 0" using a0 ra0 k by auto
have rb0': "r k (b$0) \<noteq> 0" using b0 rb0 k by auto
@@ -3122,7 +3125,7 @@
show ?thesis by (simp add: fps_inverse_def)
qed
-text \<open>Vandermonde's Identity as a consequence\<close>
+text \<open>Vandermonde's Identity as a consequence.\<close>
lemma gbinomial_Vandermonde:
"setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n"
proof -
@@ -3162,9 +3165,14 @@
let ?p = "\<lambda>(x::'a). pochhammer (- x)"
from b have bn0: "?p b n \<noteq> 0"
unfolding pochhammer_eq_0_iff by simp
- {
- fix k
- assume kn: "k \<in> {0..n}"
+ have th00:
+ "b gchoose (n - k) =
+ (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
+ (is ?gchoose)
+ "pochhammer (1 + b - of_nat n) k \<noteq> 0"
+ (is ?pochhammer)
+ if kn: "k \<in> {0..n}" for k
+ proof -
have nz: "pochhammer (1 + b - of_nat n) n \<noteq> 0"
proof
assume "pochhammer (1 + b - of_nat n) n = 0"
@@ -3274,15 +3282,12 @@
finally show ?thesis by simp
qed
qed
- then have "b gchoose (n - k) =
- (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
- "pochhammer (1 + b - of_nat n) k \<noteq> 0 "
+ then show ?gchoose and ?pochhammer
apply (cases "n = 0")
using nz'
apply auto
done
- }
- note th00 = this
+ qed
have "?r = ((a + b) gchoose n) * (of_nat (fact n) / (?m1 n * pochhammer (- b) n))"
unfolding gbinomial_pochhammer
using bn0 by (auto simp add: field_simps)
@@ -3308,7 +3313,8 @@
proof -
let ?a = "- a"
let ?b = "c + of_nat n - 1"
- have h: "\<forall> j \<in>{0..< n}. ?b \<noteq> of_nat j" using c
+ have h: "\<forall> j \<in>{0..< n}. ?b \<noteq> of_nat j"
+ using c
apply (auto simp add: algebra_simps of_nat_diff)
apply (erule_tac x = "n - j - 1" in ballE)
apply (auto simp add: of_nat_diff algebra_simps)
@@ -3524,7 +3530,7 @@
done
qed
-text \<open>Connection to E c over the complex numbers --- Euler and De Moivre\<close>
+text \<open>Connection to E c over the complex numbers --- Euler and de Moivre.\<close>
lemma Eii_sin_cos: "E (ii * c) = fps_cos c + fps_const ii * fps_sin c"
(is "?l = ?r")
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Mon Jun 22 16:56:03 2015 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Mon Jun 22 21:50:56 2015 +0200
@@ -132,9 +132,9 @@
by (cases z) auto
from md z have xy: "x\<^sup>2 + y\<^sup>2 = 1"
by (simp add: cmod_def)
- {
- assume C: "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
- from C z xy have "2 * x \<le> 1" "2 * x \<ge> -1" "2 * y \<le> 1" "2 * y \<ge> -1"
+ have False if "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
+ proof -
+ from that z xy have "2 * x \<le> 1" "2 * x \<ge> -1" "2 * y \<le> 1" "2 * y \<ge> -1"
by (simp_all add: cmod_def power2_eq_square algebra_simps)
then have "abs (2 * x) \<le> 1" "abs (2 * y) \<le> 1"
by simp_all
@@ -142,8 +142,9 @@
by - (rule power_mono, simp, simp)+
then have th0: "4 * x\<^sup>2 \<le> 1" "4 * y\<^sup>2 \<le> 1"
by (simp_all add: power_mult_distrib)
- from add_mono[OF th0] xy have False by simp
- }
+ from add_mono[OF th0] xy show ?thesis
+ by simp
+ qed
then show ?thesis
unfolding linorder_not_le[symmetric] by blast
qed
@@ -283,27 +284,24 @@
let ?w = "Complex x y"
from f(1) g(1) have hs: "subseq ?h"
unfolding subseq_def by auto
- {
- fix e :: real
- assume ep: "e > 0"
- then have e2: "e/2 > 0"
+ have "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" if "e > 0" for e
+ proof -
+ from that have e2: "e/2 > 0"
by simp
from x[rule_format, OF e2] y[rule_format, OF e2]
obtain N1 N2 where N1: "\<forall>n\<ge>N1. \<bar>Re (s (f n)) - x\<bar> < e / 2"
and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2"
by blast
- {
- fix n
- assume nN12: "n \<ge> N1 + N2"
- then have nN1: "g n \<ge> N1" and nN2: "n \<ge> N2"
+ have "cmod (s (?h n) - ?w) < e" if "n \<ge> N1 + N2" for n
+ proof -
+ from that have nN1: "g n \<ge> N1" and nN2: "n \<ge> N2"
using seq_suble[OF g(1), of n] by arith+
from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]]
- have "cmod (s (?h n) - ?w) < e"
+ show ?thesis
using metric_bound_lemma[of "s (f (g n))" ?w] by simp
- }
- then have "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e"
- by blast
- }
+ qed
+ then show ?thesis by blast
+ qed
with hs show ?thesis by blast
qed
@@ -374,34 +372,27 @@
by simp
then have mth1: "\<exists>x z. cmod z \<le> r \<and> cmod (poly p z) = - x"
by blast
- {
- fix x z
- assume H: "cmod z \<le> r" "cmod (poly p z) = - x" "\<not> x < 1"
- then have "- x < 0 "
+ have False if "cmod z \<le> r" "cmod (poly p z) = - x" "\<not> x < 1" for x z
+ proof -
+ from that have "- x < 0 "
by arith
- with H(2) norm_ge_zero[of "poly p z"] have False
+ with that(2) norm_ge_zero[of "poly p z"] show ?thesis
by simp
- }
+ qed
then have mth2: "\<exists>z. \<forall>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<longrightarrow> x < z"
by blast
from real_sup_exists[OF mth1 mth2] obtain s where
- s: "\<forall>y. (\<exists>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<and> y < x) \<longleftrightarrow> y < s" by blast
+ s: "\<forall>y. (\<exists>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<and> y < x) \<longleftrightarrow> y < s"
+ by blast
let ?m = "- s"
- {
- fix y
- from s[rule_format, of "-y"]
- have "(\<exists>z x. cmod z \<le> r \<and> - (- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y"
- unfolding minus_less_iff[of y ] equation_minus_iff by blast
- }
- note s1 = this[unfolded minus_minus]
+ have s1[unfolded minus_minus]:
+ "(\<exists>z x. cmod z \<le> r \<and> - (- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y" for y
+ using s[rule_format, of "-y"]
+ unfolding minus_less_iff[of y] equation_minus_iff by blast
from s1[of ?m] have s1m: "\<And>z x. cmod z \<le> r \<Longrightarrow> cmod (poly p z) \<ge> ?m"
by auto
- {
- fix n :: nat
- from s1[rule_format, of "?m + 1/real (Suc n)"]
- have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)"
- by simp
- }
+ have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" for n
+ using s1[rule_format, of "?m + 1/real (Suc n)"] by simp
then have th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" ..
from choice[OF th] obtain g where
g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m + 1 /real(Suc n)"
@@ -420,14 +411,8 @@
from poly_cont[OF e2, of z p] obtain d where
d: "d > 0" "\<forall>w. 0<cmod (w - z)\<and> cmod(w - z) < d \<longrightarrow> cmod(poly p w - poly p z) < ?e/2"
by blast
- {
- fix w
- assume w: "cmod (w - z) < d"
- have "cmod(poly p w - poly p z) < ?e / 2"
- using d(2)[rule_format, of w] w e by (cases "w = z") simp_all
- }
- note th1 = this
-
+ have th1: "cmod(poly p w - poly p z) < ?e / 2" if w: "cmod (w - z) < d" for w
+ using d(2)[rule_format, of w] w e by (cases "w = z") simp_all
from fz(2) d(1) obtain N1 where N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d"
by blast
from reals_Archimedean2[of "2/?e"] obtain N2 :: nat where N2: "2/?e < real N2"
@@ -499,14 +484,13 @@
with pCons.hyps obtain r where r: "\<forall>z. r \<le> norm z \<longrightarrow> d + norm a \<le> norm (poly (pCons c cs) z)"
by blast
let ?r = "1 + \<bar>r\<bar>"
- {
- fix z :: 'a
- assume h: "1 + \<bar>r\<bar> \<le> norm z"
+ have "d \<le> norm (poly (pCons a (pCons c cs)) z)" if "1 + \<bar>r\<bar> \<le> norm z" for z
+ proof -
have r0: "r \<le> norm z"
- using h by arith
+ using that by arith
from r[rule_format, OF r0] have th0: "d + norm a \<le> 1 * norm(poly (pCons c cs) z)"
by arith
- from h have z1: "norm z \<ge> 1"
+ from that have z1: "norm z \<ge> 1"
by arith
from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]]
have th1: "d \<le> norm(z * poly (pCons c cs) z) - norm a"
@@ -514,9 +498,9 @@
from norm_diff_ineq[of "z * poly (pCons c cs) z" a]
have th2: "norm (z * poly (pCons c cs) z) - norm a \<le> norm (poly (pCons a (pCons c cs)) z)"
by (simp add: algebra_simps)
- from th1 th2 have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
+ from th1 th2 show ?thesis
by arith
- }
+ qed
then show ?thesis by blast
next
case True
@@ -596,7 +580,8 @@
from pCons.hyps pCons.prems True show ?thesis
apply auto
apply (rule_tac x="k+1" in exI)
- apply (rule_tac x="a" in exI, clarsimp)
+ apply (rule_tac x="a" in exI)
+ apply clarsimp
apply (rule_tac x="q" in exI)
apply auto
done
@@ -622,15 +607,15 @@
by (simp add: constant_def)
next
case (pCons c cs)
- {
+ have "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0)"
+ proof
assume "\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
then have "poly (pCons c cs) x = poly (pCons c cs) y" for x y
by (cases "x = 0") auto
- with pCons.prems have False
+ with pCons.prems show False
by (auto simp add: constant_def)
- }
- then have th: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0)" ..
- from poly_decompose_lemma[OF th]
+ qed
+ from poly_decompose_lemma[OF this]
show ?case
apply clarsimp
apply (rule_tac x="k+1" in exI)
@@ -699,16 +684,16 @@
by (simp add: poly_eq_iff)
have False if h: "\<And>x y. poly ?r x = poly ?r y"
proof -
- {
- fix x y
+ have "poly q x = poly q y" for x y
+ proof -
from qr[rule_format, of x] have "poly q x = poly ?r x * ?a0"
by auto
also have "\<dots> = poly ?r y * ?a0"
using h by simp
also have "\<dots> = poly q y"
using qr[rule_format, of y] by simp
- finally have "poly q x = poly q y" .
- }
+ finally show ?thesis .
+ qed
with qnc show ?thesis
unfolding constant_def by blast
qed
@@ -833,7 +818,8 @@
then show ?thesis by auto
next
case False
- {
+ have "\<not> constant (poly (pCons c cs))"
+ proof
assume nc: "constant (poly (pCons c cs))"
from nc[unfolded constant_def, rule_format, of 0]
have "\<forall>w. w \<noteq> 0 \<longrightarrow> poly cs w = 0" by auto
@@ -874,10 +860,11 @@
by blast
qed
qed
- }
- then have nc: "\<not> constant (poly (pCons c cs))"
- using pCons.prems False by blast
- from fundamental_theorem_of_algebra[OF nc] show ?thesis .
+ then show False
+ using pCons.prems False by blast
+ qed
+ then show ?thesis
+ by (rule fundamental_theorem_of_algebra)
qed
qed
@@ -901,11 +888,11 @@
and dpn: "degree p = n"
and n0: "n \<noteq> 0"
from dpn n0 have pne: "p \<noteq> 0" by auto
- let ?ths = "p dvd (q ^ n)"
- {
- fix a
- assume a: "poly p a = 0"
- have ?ths if oa: "order a p \<noteq> 0"
+ show "p dvd (q ^ n)"
+ proof (cases "\<exists>a. poly p a = 0")
+ case True
+ then obtain a where a: "poly p a = 0" ..
+ have ?thesis if oa: "order a p \<noteq> 0"
proof -
let ?op = "order a p"
from pne have ap: "([:- a, 1:] ^ ?op) dvd p" "\<not> [:- a, 1:] ^ (Suc ?op) dvd p"
@@ -945,73 +932,69 @@
next
case False
with sne dpn s oa have dsn: "degree s < n"
- apply auto
- apply (erule ssubst)
- apply (simp add: degree_mult_eq degree_linear_power)
- done
- {
- fix x assume h: "poly s x = 0"
- {
- assume xa: "x = a"
- from h[unfolded xa poly_eq_0_iff_dvd] obtain u where u: "s = [:- a, 1:] * u"
- by (rule dvdE)
- have "p = [:- a, 1:] ^ (Suc ?op) * u"
- apply (subst s)
- apply (subst u)
- apply (simp only: power_Suc ac_simps)
- done
- with ap(2)[unfolded dvd_def] have False
- by blast
- }
- note xa = this
- from h have "poly p x = 0"
- by (subst s) simp
- with pq0 have "poly q x = 0"
+ apply auto
+ apply (erule ssubst)
+ apply (simp add: degree_mult_eq degree_linear_power)
+ done
+ have "poly r x = 0" if h: "poly s x = 0" for x
+ proof -
+ have xa: "x \<noteq> a"
+ proof
+ assume "x = a"
+ from h[unfolded this poly_eq_0_iff_dvd] obtain u where u: "s = [:- a, 1:] * u"
+ by (rule dvdE)
+ have "p = [:- a, 1:] ^ (Suc ?op) * u"
+ apply (subst s)
+ apply (subst u)
+ apply (simp only: power_Suc ac_simps)
+ done
+ with ap(2)[unfolded dvd_def] show False
by blast
- with r xa have "poly r x = 0"
- by auto
- }
- note impth = this
- from IH[rule_format, OF dsn, of s r] impth False
- have "s dvd (r ^ (degree s))"
+ qed
+ from h have "poly p x = 0"
+ by (subst s) simp
+ with pq0 have "poly q x = 0"
by blast
- then obtain u where u: "r ^ (degree s) = s * u" ..
- then have u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
- by (simp only: poly_mult[symmetric] poly_power[symmetric])
- let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
- from oop[of a] dsn have "q ^ n = p * ?w"
- apply -
- apply (subst s)
- apply (subst r)
- apply (simp only: power_mult_distrib)
- apply (subst mult.assoc [where b=s])
- apply (subst mult.assoc [where a=u])
- apply (subst mult.assoc [where b=u, symmetric])
- apply (subst u [symmetric])
- apply (simp add: ac_simps power_add [symmetric])
- done
- then show ?thesis
- unfolding dvd_def by blast
+ with r xa show ?thesis
+ by auto
+ qed
+ with IH[rule_format, OF dsn, of s r] False have "s dvd (r ^ (degree s))"
+ by blast
+ then obtain u where u: "r ^ (degree s) = s * u" ..
+ then have u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
+ by (simp only: poly_mult[symmetric] poly_power[symmetric])
+ let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
+ from oop[of a] dsn have "q ^ n = p * ?w"
+ apply -
+ apply (subst s)
+ apply (subst r)
+ apply (simp only: power_mult_distrib)
+ apply (subst mult.assoc [where b=s])
+ apply (subst mult.assoc [where a=u])
+ apply (subst mult.assoc [where b=u, symmetric])
+ apply (subst u [symmetric])
+ apply (simp add: ac_simps power_add [symmetric])
+ done
+ then show ?thesis
+ unfolding dvd_def by blast
qed
qed
qed
- then have ?ths using a order_root pne by blast
- }
- moreover
- {
- assume exa: "\<not> (\<exists>a. poly p a = 0)"
- from fundamental_theorem_of_algebra_alt[of p] exa
+ then show ?thesis
+ using a order_root pne by blast
+ next
+ case False
+ with fundamental_theorem_of_algebra_alt[of p]
obtain c where ccs: "c \<noteq> 0" "p = pCons c 0"
by blast
- then have pp: "\<And>x. poly p x = c"
+ then have pp: "poly p x = c" for x
by simp
let ?w = "[:1/c:] * (q ^ n)"
from ccs have "(q ^ n) = (p * ?w)"
by simp
- then have ?ths
+ then show ?thesis
unfolding dvd_def by blast
- }
- ultimately show ?ths by blast
+ qed
qed
lemma nullstellensatz_univariate:
@@ -1044,43 +1027,43 @@
by blast
next
case 3
- {
- assume "p dvd (q ^ (Suc n))"
- then obtain u where u: "q ^ (Suc n) = p * u" ..
- fix x
- assume h: "poly p x = 0" "poly q x \<noteq> 0"
- then have "poly (q ^ (Suc n)) x \<noteq> 0"
+ have False if dvd: "p dvd (q ^ (Suc n))" and h: "poly p x = 0" "poly q x \<noteq> 0" for x
+ proof -
+ from dvd obtain u where u: "q ^ (Suc n) = p * u" ..
+ from h have "poly (q ^ (Suc n)) x \<noteq> 0"
by simp
- then have False using u h(1)
+ with u h(1) show ?thesis
by (simp only: poly_mult) simp
- }
+ qed
with 3 nullstellensatz_lemma[of p q "degree p"]
show ?thesis by auto
qed
qed
text \<open>Useful lemma\<close>
-
lemma constant_degree:
fixes p :: "'a::{idom,ring_char_0} poly"
shows "constant (poly p) \<longleftrightarrow> degree p = 0" (is "?lhs = ?rhs")
proof
- assume l: ?lhs
- from l[unfolded constant_def, rule_format, of _ "0"]
- have th: "poly p = poly [:poly p 0:]"
- by auto
- then have "p = [:poly p 0:]"
- by (simp add: poly_eq_poly_eq_iff)
- then have "degree p = degree [:poly p 0:]"
- by simp
- then show ?rhs
- by simp
-next
- assume r: ?rhs
- then obtain k where "p = [:k:]"
- by (cases p) (simp split: if_splits)
- then show ?lhs
- unfolding constant_def by auto
+ show ?rhs if ?lhs
+ proof -
+ from that[unfolded constant_def, rule_format, of _ "0"]
+ have th: "poly p = poly [:poly p 0:]"
+ by auto
+ then have "p = [:poly p 0:]"
+ by (simp add: poly_eq_poly_eq_iff)
+ then have "degree p = degree [:poly p 0:]"
+ by simp
+ then show ?thesis
+ by simp
+ qed
+ show ?lhs if ?rhs
+ proof -
+ from that obtain k where "p = [:k:]"
+ by (cases p) (simp split: if_splits)
+ then show ?thesis
+ unfolding constant_def by auto
+ qed
qed
lemma divides_degree:
@@ -1129,7 +1112,7 @@
and lq: "p \<noteq> 0"
shows "p dvd q \<longleftrightarrow> q = 0" (is "?lhs \<longleftrightarrow> ?rhs")
proof
- assume r: ?rhs
+ assume ?rhs
then have "q = p * 0" by simp
then show ?lhs ..
next
@@ -1154,19 +1137,21 @@
shows "p dvd q \<longleftrightarrow> p dvd r" (is "?lhs \<longleftrightarrow> ?rhs")
proof
from pp' obtain t where t: "p' = p * t" ..
- {
- assume l: ?lhs
- then obtain u where u: "q = p * u" ..
+ show ?rhs if ?lhs
+ proof -
+ from that obtain u where u: "q = p * u" ..
have "r = p * (smult a u - t)"
using u qrp' [symmetric] t by (simp add: algebra_simps)
- then show ?rhs ..
- next
- assume r: ?rhs
- then obtain u where u: "r = p * u" ..
+ then show ?thesis ..
+ qed
+ show ?lhs if ?rhs
+ proof -
+ from that obtain u where u: "r = p * u" ..
from u [symmetric] t qrp' [symmetric] a0
- have "q = p * smult (1/a) (u + t)" by (simp add: algebra_simps)
- then show ?lhs ..
- }
+ have "q = p * smult (1/a) (u + t)"
+ by (simp add: algebra_simps)
+ then show ?thesis ..
+ qed
qed
lemma basic_cqe_conv1:
--- a/src/Pure/Isar/element.ML Mon Jun 22 16:56:03 2015 +0200
+++ b/src/Pure/Isar/element.ML Mon Jun 22 21:50:56 2015 +0200
@@ -291,7 +291,7 @@
after_qed (burrow (Proof_Context.export result_ctxt (Proof.context_of state')) results) state';
in
Proof.map_context (K goal_ctxt) #>
- Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) cmd
+ Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) true cmd
NONE after_qed' [] [] (map (pair Thm.empty_binding) propp) #> snd
end;
--- a/src/Pure/Isar/isar_syn.ML Mon Jun 22 16:56:03 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Mon Jun 22 21:50:56 2015 +0200
@@ -491,28 +491,28 @@
val structured_statement =
- Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
- >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
+ Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
+ >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
val _ =
Outer_Syntax.command @{command_keyword have} "state local goal"
- (structured_statement >> (fn (a, b, c) =>
- Toplevel.proof' (fn int => Proof.have_cmd NONE (K I) a b c int #> #2)));
+ (structured_statement >> (fn (a, b, c, d) =>
+ Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2)));
val _ =
Outer_Syntax.command @{command_keyword show} "state local goal, to refine pending subgoals"
- (structured_statement >> (fn (a, b, c) =>
- Toplevel.proof' (fn int => Proof.show_cmd NONE (K I) a b c int #> #2)));
+ (structured_statement >> (fn (a, b, c, d) =>
+ Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2)));
val _ =
Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
- (structured_statement >> (fn (a, b, c) =>
- Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) a b c int #> #2)));
+ (structured_statement >> (fn (a, b, c, d) =>
+ Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2)));
val _ =
Outer_Syntax.command @{command_keyword thus} "old-style alias of \"then show\""
- (structured_statement >> (fn (a, b, c) =>
- Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) a b c int #> #2)));
+ (structured_statement >> (fn (a, b, c, d) =>
+ Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2)));
(* facts *)
--- a/src/Pure/Isar/method.ML Mon Jun 22 16:56:03 2015 +0200
+++ b/src/Pure/Isar/method.ML Mon Jun 22 21:50:56 2015 +0200
@@ -67,6 +67,9 @@
val method_closure: Proof.context -> Token.src -> Token.src
val closure: bool Config.T
val method_cmd: Proof.context -> Token.src -> Proof.context -> method
+ val detect_closure_state: thm -> bool
+ val RUNTIME: cases_tactic -> cases_tactic
+ val sleep: Time.time -> cases_tactic
val evaluate: text -> Proof.context -> method
type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}
val modifier: attribute -> Position.T -> modifier
@@ -419,6 +422,19 @@
method ctxt;
+(* closure vs. runtime state *)
+
+fun detect_closure_state st =
+ (case try Logic.dest_term (Thm.concl_of (perhaps (try Goal.conclude) st)) of
+ NONE => false
+ | SOME t => Term.is_dummy_pattern t);
+
+fun RUNTIME (tac: cases_tactic) st =
+ if detect_closure_state st then Seq.empty else tac st;
+
+fun sleep t = RUNTIME (fn st => (OS.Process.sleep t; Seq.single ([], st)));
+
+
(* evaluate method text *)
local
@@ -657,6 +673,8 @@
val _ = Theory.setup
(setup @{binding fail} (Scan.succeed (K fail)) "force failure" #>
setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #>
+ setup @{binding sleep} (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s)))
+ "succeed after delay (in seconds)" #>
setup @{binding "-"} (Scan.succeed (K insert_facts))
"do nothing (insert current facts only)" #>
setup @{binding insert} (Attrib.thms >> (K o insert))
--- a/src/Pure/Isar/obtain.ML Mon Jun 22 16:56:03 2015 +0200
+++ b/src/Pure/Isar/obtain.ML Mon Jun 22 21:50:56 2015 +0200
@@ -159,7 +159,7 @@
val atts = Rule_Cases.cases_open :: obtains_attributes raw_obtains;
in
state
- |> Proof.have NONE (K I)
+ |> Proof.have true NONE (K I)
[(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
(map (fn (a, A) => ((a, [Context_Rules.intro_query NONE]), [(A, [])])) obtains)
[((Binding.empty, atts), [(thesis, [])])] int
@@ -233,7 +233,7 @@
end;
in
state
- |> Proof.have NONE after_qed
+ |> Proof.have true NONE after_qed
[(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
[((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
[(Thm.empty_binding, [(thesis, [])])] int
@@ -409,7 +409,7 @@
|> Proof.begin_block
|> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
|> Proof.chain_facts chain_facts
- |> Proof.internal_goal print_result Proof_Context.mode_schematic "guess"
+ |> Proof.internal_goal print_result Proof_Context.mode_schematic true "guess"
(SOME before_qed) after_qed
[] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
|> snd
--- a/src/Pure/Isar/parse_spec.ML Mon Jun 22 16:56:03 2015 +0200
+++ b/src/Pure/Isar/parse_spec.ML Mon Jun 22 21:50:56 2015 +0200
@@ -25,6 +25,7 @@
val context_element: Element.context parser
val statement: (Attrib.binding * (string * string list) list) list parser
val if_statement: (Attrib.binding * (string * string list) list) list parser
+ val cond_statement: (bool * (Attrib.binding * (string * string list) list) list) parser
val obtains: Element.obtains parser
val general_statement: (Element.context list * Element.statement) parser
val statement_keyword: string parser
@@ -134,6 +135,11 @@
val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
val if_statement = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
+val cond_statement =
+ Parse.$$$ "if" |-- Parse.!!! statement >> pair true ||
+ Parse.$$$ "when" |-- Parse.!!! statement >> pair false ||
+ Scan.succeed (true, []);
+
val obtain_case =
Parse.parbinding --
(Scan.optional (Parse.and_list1 Parse.fixes --| Parse.where_ >> flat) [] --
--- a/src/Pure/Isar/proof.ML Mon Jun 22 16:56:03 2015 +0200
+++ b/src/Pure/Isar/proof.ML Mon Jun 22 21:50:56 2015 +0200
@@ -105,24 +105,24 @@
val global_skip_proof: bool -> state -> context
val global_done_proof: state -> context
val internal_goal: (context -> (string * string) * (string * thm list) list -> unit) ->
- Proof_Context.mode -> string -> Method.text option ->
+ Proof_Context.mode -> bool -> string -> Method.text option ->
(context * thm list list -> state -> state) ->
(binding * typ option * mixfix) list ->
(Thm.binding * (term * term list) list) list ->
(Thm.binding * (term * term list) list) list -> state -> thm list * state
- val have: Method.text option -> (context * thm list list -> state -> state) ->
+ val have: bool -> Method.text option -> (context * thm list list -> state -> state) ->
(binding * typ option * mixfix) list ->
(Thm.binding * (term * term list) list) list ->
(Thm.binding * (term * term list) list) list -> bool -> state -> thm list * state
- val have_cmd: Method.text option -> (context * thm list list -> state -> state) ->
+ val have_cmd: bool -> Method.text option -> (context * thm list list -> state -> state) ->
(binding * string option * mixfix) list ->
(Attrib.binding * (string * string list) list) list ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> thm list * state
- val show: Method.text option -> (context * thm list list -> state -> state) ->
+ val show: bool -> Method.text option -> (context * thm list list -> state -> state) ->
(binding * typ option * mixfix) list ->
(Thm.binding * (term * term list) list) list ->
(Thm.binding * (term * term list) list) list -> bool -> state -> thm list * state
- val show_cmd: Method.text option -> (context * thm list list -> state -> state) ->
+ val show_cmd: bool -> Method.text option -> (context * thm list list -> state -> state) ->
(binding * string option * mixfix) list ->
(Attrib.binding * (string * string list) list) list ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> thm list * state
@@ -162,8 +162,8 @@
goal: thm, (*subgoals ==> statement*)
before_qed: Method.text option,
after_qed:
- ((context * thm list list) -> state -> state) *
- ((context * thm list list) -> context -> context)};
+ (context * thm list list -> state -> state) *
+ (context * thm list list -> context -> context)};
fun make_goal (statement, using, goal, before_qed, after_qed) =
Goal {statement = statement, using = using, goal = goal,
@@ -234,11 +234,13 @@
val get_facts = #facts o top;
fun the_facts state =
- (case get_facts state of SOME facts => facts
+ (case get_facts state of
+ SOME facts => facts
| NONE => error "No current facts available");
fun the_fact state =
- (case the_facts state of [thm] => thm
+ (case the_facts state of
+ [thm] => thm
| _ => error "Single theorem expected");
fun put_facts facts =
@@ -336,11 +338,13 @@
in State (Stack.make nd' (node' :: nodes')) end
| _ => State stack);
-fun provide_goal goal = map_goal I (fn (statement, using, _, before_qed, after_qed) =>
- (statement, using, goal, before_qed, after_qed)) I;
+fun provide_goal goal =
+ map_goal I (fn (statement, using, _, before_qed, after_qed) =>
+ (statement, using, goal, before_qed, after_qed)) I;
-fun using_facts using = map_goal I (fn (statement, _, goal, before_qed, after_qed) =>
- (statement, using, goal, before_qed, after_qed)) I;
+fun using_facts using =
+ map_goal I (fn (statement, _, goal, before_qed, after_qed) =>
+ (statement, using, goal, before_qed, after_qed)) I;
local
fun find i state =
@@ -388,9 +392,7 @@
val position_markup = Position.markup (Position.thread_data ()) Markup.position;
in
[Pretty.block
- [Pretty.mark_str (position_markup, "proof"),
- Pretty.str (" (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1))],
- Pretty.str ""] @
+ [Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]] @
(if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
(if verbose orelse mode = Forward then
pretty_sep (pretty_facts ctxt "" facts) (prt_goal (try find_goal state))
@@ -463,7 +465,8 @@
fun refine_goals print_rule result_ctxt result state =
let
val (goal_ctxt, (_, goal)) = get_goal state;
- fun refine rule st = (print_rule goal_ctxt rule; FINDGOAL (goal_tac goal_ctxt rule) st);
+ fun refine rule st =
+ (print_rule goal_ctxt rule; FINDGOAL (goal_tac goal_ctxt rule) st);
in
result
|> Proof_Context.goal_export result_ctxt goal_ctxt
@@ -484,11 +487,11 @@
error "Bad background theory of goal state";
val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
- fun lost_structure () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal);
+ fun err_lost () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal);
val th =
(Goal.conclude (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
- handle THM _ => lost_structure ())
+ handle THM _ => err_lost ())
|> Drule.flexflex_unique (SOME ctxt)
|> Thm.check_shyps (Variable.sorts_of ctxt)
|> Thm.check_hyps (Context.Proof ctxt);
@@ -497,7 +500,7 @@
val results =
Conjunction.elim_balanced (length goal_propss) th
|> map2 Conjunction.elim_balanced (map length goal_propss)
- handle THM _ => lost_structure ();
+ handle THM _ => err_lost ();
val _ =
Unify.matches_list (Context.Proof ctxt) (flat goal_propss) (map Thm.prop_of (flat results))
orelse error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th);
@@ -505,7 +508,7 @@
fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
| recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
| recover_result [] [] = []
- | recover_result _ _ = lost_structure ();
+ | recover_result _ _ = err_lost ();
in recover_result propss results end;
val finished_goal_error = "Failed to finish proof";
@@ -836,7 +839,11 @@
fun proof opt_text =
assert_backward
#> refine (the_default Method.default_text opt_text)
- #> Seq.map (using_facts [] #> enter_forward);
+ #> Seq.map
+ (using_facts []
+ #> enter_forward
+ #> open_block
+ #> reset_goal);
fun proof_results arg =
Seq.APPEND (proof (Method.text arg) #> Seq.make_results,
@@ -920,17 +927,11 @@
val chaining = can assert_chain state;
val pos = Position.thread_data ();
- val goal_state =
- state
- |> assert_forward_or_chain
- |> enter_forward
- |> open_block
- |> map_context (K goal_ctxt);
val goal_props = flat goal_propss;
-
val vars = implicit_vars goal_props;
val propss' = vars :: goal_propss;
val goal_propss = filter_out null propss';
+
val goal =
Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
|> Thm.cterm_of goal_ctxt
@@ -940,15 +941,19 @@
val after_qed' = after_qed |>> (fn after_local => fn results =>
map_context (fold Variable.maybe_bind_term result_binds) #> after_local results);
in
- goal_state
- |> map_context (init_context #> Variable.set_body true)
+ state
+ |> assert_forward_or_chain
+ |> enter_forward
+ |> open_block
+ |> enter_backward
+ |> map_context
+ (K goal_ctxt
+ #> init_context
+ #> Variable.set_body true
+ #> Proof_Context.auto_bind_goal goal_props)
|> set_goal (make_goal (statement, [], Goal.init goal, before_qed, after_qed'))
- |> map_context (Proof_Context.auto_bind_goal goal_props)
|> chaining ? (`the_facts #-> using_facts)
|> reset_facts
- |> open_block
- |> reset_goal
- |> enter_backward
|> not (null vars) ? refine_terms (length goal_propss)
|> null goal_props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
end;
@@ -977,11 +982,14 @@
in
-fun local_goal print_results prep_att prep_propp prep_var
+fun local_goal print_results prep_att prep_propp prep_var strict_asm
kind before_qed after_qed raw_fixes raw_assumes raw_shows state =
let
val ctxt = context_of state;
+ val add_assumes =
+ Assumption.add_assms
+ (if strict_asm then Assumption.assume_export else Assumption.presume_export);
val (assumes_bindings, shows_bindings) =
apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows);
val (assumes_propp, shows_propp) = apply2 (map snd) (raw_assumes, raw_shows);
@@ -1007,8 +1015,7 @@
(*prems*)
val (that_fact, goal_ctxt) = params_ctxt
- |> fold_burrow (Assumption.add_assms Assumption.assume_export)
- ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
+ |> fold_burrow add_assumes ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
|> (fn (premss, ctxt') =>
let
val prems = Assumption.local_prems_of ctxt' ctxt;
@@ -1127,12 +1134,12 @@
local
fun gen_have prep_att prep_propp prep_var
- before_qed after_qed fixes assumes shows int =
+ strict_asm before_qed after_qed fixes assumes shows int =
local_goal (Proof_Display.print_results int (Position.thread_data ()))
- prep_att prep_propp prep_var "have" before_qed after_qed fixes assumes shows;
+ prep_att prep_propp prep_var strict_asm "have" before_qed after_qed fixes assumes shows;
fun gen_show prep_att prep_propp prep_var
- before_qed after_qed fixes assumes shows int state =
+ strict_asm before_qed after_qed fixes assumes shows int state =
let
val testing = Unsynchronized.ref false;
val rule = Unsynchronized.ref (NONE: thm option);
@@ -1163,7 +1170,7 @@
|> after_qed (result_ctxt, results);
in
state
- |> local_goal print_results prep_att prep_propp prep_var
+ |> local_goal print_results prep_att prep_propp prep_var strict_asm
"show" before_qed after_qed' fixes assumes shows
||> int ? (fn goal_state =>
(case test_proof (map_context (Context_Position.set_visible false) goal_state) of
--- a/src/Pure/Pure.thy Mon Jun 22 16:56:03 2015 +0200
+++ b/src/Pure/Pure.thy Mon Jun 22 21:50:56 2015 +0200
@@ -12,7 +12,7 @@
"defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
"infixl" "infixr" "is" "notes" "obtains" "open" "output"
"overloaded" "pervasive" "private" "qualified" "shows"
- "structure" "unchecked" "where" "|"
+ "structure" "unchecked" "where" "when" "|"
and "text" "txt" :: document_body
and "text_raw" :: document_raw
and "default_sort" :: thy_decl == ""