--- a/src/HOL/Eisbach/eisbach_rule_insts.ML Sun Jun 14 14:25:01 2015 +0100
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Sun Jun 14 16:22:02 2015 +0200
@@ -81,7 +81,7 @@
val ctxt1 =
ctxt
|> Context_Position.not_really
- |> fold_map Proof_Context.read_var fixes |-> Proof_Context.add_fixes |> #2;
+ |> Proof_Context.add_fixes_cmd fixes |> #2;
val typs =
map snd type_insts
@@ -140,11 +140,10 @@
val inst = Args.maybe Parse_Tools.name_term;
val concl = Args.$$$ "concl" -- Args.colon;
-fun close_unchecked_insts context ((insts,concl_inst), fixes) =
+fun close_unchecked_insts context ((insts, concl_inst), fixes) =
let
val ctxt = Context.proof_of context;
- val ctxt1 = ctxt
- |> fold_map Proof_Context.read_var fixes |-> Proof_Context.add_fixes |> #2;
+ val ctxt1 = ctxt |> Proof_Context.add_fixes_cmd fixes |> #2;
val insts' = insts @ concl_inst;
--- a/src/HOL/Eisbach/match_method.ML Sun Jun 14 14:25:01 2015 +0100
+++ b/src/HOL/Eisbach/match_method.ML Sun Jun 14 16:22:02 2015 +0200
@@ -112,11 +112,10 @@
| SOME _ => error "Unexpected token value in match cartouche"
| NONE =>
let
- val fixes' = map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
- val (fixes'', ctxt1) = fold_map Proof_Context.read_var fixes' ctxt;
- val (fix_names, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
-
- val ctxt3 = Proof_Context.set_mode Proof_Context.mode_schematic ctxt2;
+ val (fix_names, ctxt3) = ctxt
+ |> Proof_Context.add_fixes_cmd
+ (map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes)
+ ||> Proof_Context.set_mode Proof_Context.mode_schematic;
fun parse_term term =
if prop_match match_kind
--- a/src/HOL/Eisbach/method_closure.ML Sun Jun 14 14:25:01 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML Sun Jun 14 16:22:02 2015 +0200
@@ -328,7 +328,7 @@
fn ctxt => evaluate_method_def (match fixes) text (setup_ctxt ctxt)
end;
-fun gen_method_definition prep_var name vars uses attribs methods source lthy =
+fun gen_method_definition add_fixes name vars uses attribs methods source lthy =
let
val (uses_nms, lthy1) = lthy
|> Proof_Context.concealed
@@ -339,8 +339,7 @@
|> fold_map setup_local_fact uses;
val (term_args, lthy2) = lthy1
- |> fold_map prep_var vars |-> Proof_Context.add_fixes
- |-> fold_map Proof_Context.inferred_param |>> map Free;
+ |> add_fixes vars |-> fold_map Proof_Context.inferred_param |>> map Free;
val (named_thms, modifiers) = map (check_attrib lthy2) (attribs @ uses) |> split_list;
val self_name :: method_names = map (Local_Theory.full_name lthy2) (name :: methods);
@@ -384,8 +383,8 @@
|> add_method name ((term_args', named_thms, method_names), text')
end;
-val method_definition = gen_method_definition Proof_Context.cert_var;
-val method_definition_cmd = gen_method_definition Proof_Context.read_var;
+val method_definition = gen_method_definition Proof_Context.add_fixes;
+val method_definition_cmd = gen_method_definition Proof_Context.add_fixes_cmd;
val _ =
Outer_Syntax.local_theory @{command_keyword method} "Eisbach method definition"
--- a/src/HOL/Isar_Examples/Structured_Statements.thy Sun Jun 14 14:25:01 2015 +0100
+++ b/src/HOL/Isar_Examples/Structured_Statements.thy Sun Jun 14 16:22:02 2015 +0200
@@ -8,9 +8,42 @@
imports Main
begin
+subsection \<open>Introduction steps\<close>
+
notepad
begin
+ fix A B :: bool
+ fix P :: "'a \<Rightarrow> bool"
+ have "A \<longrightarrow> B"
+ proof
+ show B if A using that sorry
+ qed
+
+ have "\<not> A"
+ proof
+ show False if A using that sorry
+ qed
+
+ have "\<forall>x. P x"
+ proof
+ show "P x" for x sorry
+ qed
+end
+
+
+subsection \<open>If-and-only-if\<close>
+
+notepad
+begin
+ fix A B :: bool
+
+ have "A \<longleftrightarrow> B"
+ proof
+ show B if A sorry
+ show A if B sorry
+ qed
+next
fix A B :: bool
have iff_comm: "(A \<and> B) \<longleftrightarrow> (B \<and> A)"
@@ -38,7 +71,63 @@
then show "A \<and> B" if "B \<and> A"
by this (rule that)
qed
+end
+
+subsection \<open>Elimination and cases\<close>
+
+notepad
+begin
+ fix A B C D :: bool
+ assume *: "A \<or> B \<or> C \<or> D"
+
+ consider (a) A | (b) B | (c) C | (d) D
+ using * by blast
+ then have something
+ proof cases
+ case a thm \<open>A\<close>
+ then show ?thesis sorry
+ next
+ case b thm \<open>B\<close>
+ then show ?thesis sorry
+ next
+ case c thm \<open>C\<close>
+ then show ?thesis sorry
+ next
+ case d thm \<open>D\<close>
+ then show ?thesis sorry
+ qed
+next
+ fix A :: "'a \<Rightarrow> bool"
+ fix B :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
+ assume *: "(\<exists>x. A x) \<or> (\<exists>y z. B y z)"
+
+ consider (a) x where "A x" | (b) y z where "B y z"
+ using * by blast
+ then have something
+ proof cases
+ case a thm \<open>A x\<close>
+ then show ?thesis sorry
+ next
+ case b thm \<open>B y z\<close>
+ then show ?thesis sorry
+ qed
+end
+
+
+subsection \<open>Induction\<close>
+
+notepad
+begin
+ fix P :: "nat \<Rightarrow> bool"
+ fix n :: nat
+
+ have "P n"
+ proof (induct n)
+ show "P 0" sorry
+ show "P (Suc n)" if "P n" for n thm \<open>P n\<close>
+ using that sorry
+ qed
end
end
\ No newline at end of file
--- a/src/HOL/ROOT Sun Jun 14 14:25:01 2015 +0100
+++ b/src/HOL/ROOT Sun Jun 14 16:22:02 2015 +0200
@@ -623,6 +623,7 @@
Peirce
Puzzle
Summation
+ theories [quick_and_dirty]
Structured_Statements
document_files
"root.bib"
--- a/src/Pure/Isar/bundle.ML Sun Jun 14 14:25:01 2015 +0100
+++ b/src/Pure/Isar/bundle.ML Sun Jun 14 16:22:02 2015 +0200
@@ -57,9 +57,9 @@
local
-fun gen_bundle prep_fact prep_att prep_var (binding, raw_bundle) fixes lthy =
+fun gen_bundle prep_fact prep_att add_fixes (binding, raw_bundle) raw_fixes lthy =
let
- val (_, ctxt') = lthy |> fold_map prep_var fixes |-> Proof_Context.add_fixes;
+ val (_, ctxt') = add_fixes raw_fixes lthy;
val bundle0 = raw_bundle
|> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts));
val bundle =
@@ -75,8 +75,8 @@
in
-val bundle = gen_bundle (K I) (K I) Proof_Context.cert_var;
-val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.read_var;
+val bundle = gen_bundle (K I) (K I) Proof_Context.add_fixes;
+val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.add_fixes_cmd;
end;
--- a/src/Pure/Isar/proof.ML Sun Jun 14 14:25:01 2015 +0100
+++ b/src/Pure/Isar/proof.ML Sun Jun 14 16:22:02 2015 +0200
@@ -594,15 +594,15 @@
local
-fun gen_fix prep_var args =
+fun gen_fix add_fixes raw_fixes =
assert_forward
- #> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (fold_map prep_var args ctxt)) ctxt))
+ #> map_context (snd o add_fixes raw_fixes)
#> reset_facts;
in
-val fix = gen_fix Proof_Context.cert_var;
-val fix_cmd = gen_fix Proof_Context.read_var;
+val fix = gen_fix Proof_Context.add_fixes;
+val fix_cmd = gen_fix Proof_Context.add_fixes_cmd;
end;
--- a/src/Pure/Isar/proof_context.ML Sun Jun 14 14:25:01 2015 +0100
+++ b/src/Pure/Isar/proof_context.ML Sun Jun 14 16:22:02 2015 +0200
@@ -131,6 +131,8 @@
(binding * typ option * mixfix) * Proof.context
val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
string list * Proof.context
+ val add_fixes_cmd: (binding * string option * mixfix) list -> Proof.context ->
+ string list * Proof.context
val add_assms: Assumption.export ->
(Thm.binding * (term * term list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
@@ -1034,14 +1036,14 @@
fun cond_tvars T =
if internal then T
else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
- val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
+ val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T;
val (_, ctxt') = ctxt |> declare_var (x, opt_T, mx);
in ((b, opt_T, mx), ctxt') end;
in
val read_var = prep_var Syntax.read_typ false;
-val cert_var = prep_var (K I) true;
+val cert_var = prep_var cert_typ true;
end;
@@ -1131,16 +1133,26 @@
(* fixes *)
-fun add_fixes raw_vars ctxt =
- let val (vars, _) = fold_map cert_var raw_vars ctxt in
- ctxt
- |> Variable.add_fixes_binding (map #1 vars)
- |-> (fn xs =>
- fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
- #-> (map_syntax_idents o Local_Syntax.add_syntax ctxt o map (pair Local_Syntax.Fixed))
- #> pair xs)
+local
+
+fun gen_fixes prep_var raw_vars ctxt =
+ let
+ val (vars, _) = fold_map prep_var raw_vars ctxt;
+ val (xs, ctxt') = Variable.add_fixes_binding (map #1 vars) ctxt;
+ in
+ ctxt'
+ |> fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
+ |-> (map_syntax_idents o Local_Syntax.add_syntax ctxt o map (pair Local_Syntax.Fixed))
+ |> pair xs
end;
+in
+
+val add_fixes = gen_fixes cert_var;
+val add_fixes_cmd = gen_fixes read_var;
+
+end;
+
(** assumptions **)
--- a/src/Pure/Isar/specification.ML Sun Jun 14 14:25:01 2015 +0100
+++ b/src/Pure/Isar/specification.ML Sun Jun 14 16:22:02 2015 +0200
@@ -87,7 +87,7 @@
fun read_props raw_props raw_fixes ctxt =
let
- val ctxt1 = ctxt |> fold_map Proof_Context.read_var raw_fixes |-> Proof_Context.add_fixes |> #2;
+ val (_, ctxt1) = ctxt |> Proof_Context.add_fixes_cmd raw_fixes;
val props1 = map (Syntax.parse_prop ctxt1) raw_props;
val (props2, ctxt2) = ctxt1 |> fold_map Variable.fix_dummy_patterns props1;
val props3 = Syntax.check_props ctxt2 props2;
@@ -291,13 +291,13 @@
local
-fun gen_theorems prep_fact prep_att prep_var
+fun gen_theorems prep_fact prep_att add_fixes
kind raw_facts raw_fixes int lthy =
let
val facts = raw_facts |> map (fn ((name, atts), bs) =>
((name, map (prep_att lthy) atts),
bs |> map (fn (b, more_atts) => (prep_fact lthy b, map (prep_att lthy) more_atts))));
- val (_, ctxt') = lthy |> fold_map prep_var raw_fixes |-> Proof_Context.add_fixes;
+ val (_, ctxt') = add_fixes raw_fixes lthy;
val facts' = facts
|> Attrib.partial_evaluation ctxt'
@@ -308,8 +308,8 @@
in
-val theorems = gen_theorems (K I) (K I) Proof_Context.cert_var;
-val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.check_src Proof_Context.read_var;
+val theorems = gen_theorems (K I) (K I) Proof_Context.add_fixes;
+val theorems_cmd = gen_theorems Proof_Context.get_fact Attrib.check_src Proof_Context.add_fixes_cmd;
end;
--- a/src/Pure/Tools/rule_insts.ML Sun Jun 14 14:25:01 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML Sun Jun 14 16:22:02 2015 +0200
@@ -113,9 +113,9 @@
val vars = Thm.fold_terms Term.add_vars thm [];
(*eigen-context*)
- val ctxt1 = ctxt
+ val (_, ctxt1) = ctxt
|> Variable.declare_thm thm
- |> fold_map Proof_Context.read_var raw_fixes |-> Proof_Context.add_fixes |> #2;
+ |> Proof_Context.add_fixes_cmd raw_fixes;
(*explicit type instantiations*)
val instT1 = Term_Subst.instantiateT (map (read_type ctxt1 tvars) type_insts);