--- a/NEWS Wed Jun 24 00:30:03 2015 +0200
+++ b/NEWS Wed Jun 24 21:26:03 2015 +0200
@@ -66,6 +66,17 @@
then show ?thesis <proof>
qed
+* Command 'case' allows fact name and attribute specification like this:
+
+ case a: (c xs)
+ case a [attributes]: (c xs)
+
+Facts that are introduced by invoking the case context are uniformly
+qualified by "a"; the same name is used for the cumulative fact. The old
+form "case (c xs) [attributes]" is no longer supported. Rare
+INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,
+and always put attributes in front.
+
* 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.
--- a/src/Doc/Isar_Ref/Proof.thy Wed Jun 24 00:30:03 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Wed Jun 24 21:26:03 2015 +0200
@@ -1061,11 +1061,8 @@
later.
@{rail \<open>
- @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) *) ')')
+ @@{command case} @{syntax thmdecl}? (nameref | '(' nameref (('_' | @{syntax name}) *) ')')
;
- caseref: nameref attributes?
- ;
-
@@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) +) ']' ) ? ) +)
;
@@{attribute case_conclusion} @{syntax name} (@{syntax name} * )
@@ -1077,12 +1074,18 @@
\begin{description}
- \item @{command "case"}~@{text "(c x\<^sub>1 \<dots> x\<^sub>m)"} invokes a named local
+ \item @{command "case"}~@{text "a: (c x\<^sub>1 \<dots> x\<^sub>m)"} invokes a named local
context @{text "c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m"}, as provided by an
- appropriate proof method (such as @{method_ref cases} and
- @{method_ref induct}). The command ``@{command "case"}~@{text "(c
- x\<^sub>1 \<dots> x\<^sub>m)"}'' abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \<dots>
- x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}''.
+ appropriate proof method (such as @{method_ref cases} and @{method_ref
+ induct}). The command ``@{command "case"}~@{text "a: (c x\<^sub>1 \<dots> x\<^sub>m)"}''
+ abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command
+ "assume"}~@{text "a.c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}''. Each local fact is qualified by the
+ prefix @{text "a"}, and all such facts are collectively bound to the name
+ @{text a}.
+
+ The fact name is specification @{text a} is optional, the default is to
+ re-use @{text c}. So @{command "case"}~@{text "(c x\<^sub>1 \<dots> x\<^sub>m)"} is the same
+ as @{command "case"}~@{text "c: (c x\<^sub>1 \<dots> x\<^sub>m)"}.
\item @{command "print_cases"} prints all local contexts of the
current state, using Isar proof language notation.
--- a/src/HOL/Library/FinFun.thy Wed Jun 24 00:30:03 2015 +0200
+++ b/src/HOL/Library/FinFun.thy Wed Jun 24 21:26:03 2015 +0200
@@ -1361,7 +1361,7 @@
and [simp]: "sorted xs" "distinct xs" by simp_all
show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))"
proof(cases "b = finfun_default f")
- case True [simp]
+ case [simp]: True
show ?thesis
proof(cases "finfun_dom f $ a")
case True
--- a/src/HOL/MicroJava/J/Eval.thy Wed Jun 24 00:30:03 2015 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Wed Jun 24 21:26:03 2015 +0200
@@ -222,22 +222,22 @@
case eval
from eval.prems show thesis
proof(cases (no_simp))
- case LAcc with LAcc_code show ?thesis by auto
+ case LAcc with eval.LAcc_code show ?thesis by auto
next
case (Call a b c d e f g h i j k l m n o p q r s t u v s4)
- with Call_code show ?thesis
+ with eval.Call_code show ?thesis
by(cases "s4") auto
- qed(erule (3) that[OF refl]|assumption)+
+ qed(erule (3) eval.that[OF refl]|assumption)+
next
case evals
from evals.prems show thesis
- by(cases (no_simp))(erule (3) that[OF refl]|assumption)+
+ by(cases (no_simp))(erule (3) evals.that[OF refl]|assumption)+
next
case exec
from exec.prems show thesis
proof(cases (no_simp))
- case LoopT thus ?thesis by(rule LoopT_code[OF refl])
- qed(erule (2) that[OF refl]|assumption)+
+ case LoopT thus ?thesis by(rule exec.LoopT_code[OF refl])
+ qed(erule (2) exec.that[OF refl]|assumption)+
qed
end
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Wed Jun 24 00:30:03 2015 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Wed Jun 24 21:26:03 2015 +0200
@@ -241,10 +241,10 @@
from appending.prems show thesis
proof(cases)
case nil
- from alt_nil nil show thesis by auto
+ from appending.alt_nil nil show thesis by auto
next
case cons
- from alt_cons cons show thesis by fastforce
+ from appending.alt_cons cons show thesis by fastforce
qed
qed
@@ -270,17 +270,17 @@
from ya_even.prems show thesis
proof (cases)
case even_zero
- from even_zero even_0 show thesis by simp
+ from even_zero ya_even.even_0 show thesis by simp
next
case even_plus1
- from even_plus1 even_Suc show thesis by simp
+ from even_plus1 ya_even.even_Suc show thesis by simp
qed
next
case ya_odd
from ya_odd.prems show thesis
proof (cases)
case odd_plus1
- from odd_plus1 odd_Suc show thesis by simp
+ from odd_plus1 ya_odd.odd_Suc show thesis by simp
qed
qed
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Jun 24 00:30:03 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Jun 24 21:26:03 2015 +0200
@@ -1620,9 +1620,6 @@
Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)
"adding alternative introduction rules for code generation of inductive predicates")
-fun qualified_binding a =
- Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));
-
(* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
(* FIXME ... this is important to avoid changing the background theory below *)
fun generic_code_pred prep_const options raw_const lthy =
@@ -1641,14 +1638,14 @@
in mk_casesrule lthy' pred intros end
val cases_rules = map mk_cases preds
val cases =
- map2 (fn pred_name => fn case_rule => Rule_Cases.Case {fixes = [],
- assumes =
- (Binding.name "that", tl (Logic.strip_imp_prems case_rule)) ::
- map_filter (fn (fact_name, fact) =>
- Option.map (fn a => (qualified_binding a, [fact])) fact_name)
- ((SOME (Long_Name.base_name pred_name ^ ".prems") :: names_of ctxt' pred_name) ~~
- Logic.strip_imp_prems case_rule),
- binds = [], cases = []}) preds cases_rules
+ map2 (fn pred_name => fn case_rule =>
+ Rule_Cases.Case {
+ fixes = [],
+ assumes =
+ ("that", tl (Logic.strip_imp_prems case_rule)) ::
+ map_filter (fn (fact_name, fact) => Option.map (fn a => (a, [fact])) fact_name)
+ ((SOME "prems" :: names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule),
+ binds = [], cases = []}) preds cases_rules
val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
val lthy'' = lthy'
|> fold Variable.auto_fixes cases_rules
--- a/src/Pure/Isar/isar_syn.ML Wed Jun 24 00:30:03 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Jun 24 21:26:03 2015 +0200
@@ -595,11 +595,11 @@
val _ =
Outer_Syntax.command @{command_keyword case} "invoke local context"
- ((@{keyword "("} |--
- Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
- --| @{keyword ")"}) ||
- Parse.position Parse.xname >> rpair []) -- Parse.opt_attribs >> (fn ((c, xs), atts) =>
- Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
+ (Parse_Spec.opt_thm_name ":" --
+ (@{keyword "("} |--
+ Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
+ --| @{keyword ")"}) ||
+ Parse.position Parse.xname >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
(* proof structure *)
--- a/src/Pure/Isar/proof.ML Wed Jun 24 00:30:03 2015 +0200
+++ b/src/Pure/Isar/proof.ML Wed Jun 24 21:26:03 2015 +0200
@@ -71,10 +71,8 @@
val using_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
val unfolding: ((thm list * attribute list) list) list -> state -> state
val unfolding_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
- val invoke_case: (string * Position.T) * binding option list * attribute list ->
- state -> state
- val invoke_case_cmd: (string * Position.T) * binding option list * Token.src list ->
- state -> state
+ val case_: Thm.binding * ((string * Position.T) * binding option list) -> state -> state
+ val case_cmd: Attrib.binding * ((string * Position.T) * binding option list) -> state -> state
val begin_block: state -> state
val next_block: state -> state
val end_block: state -> state
@@ -767,24 +765,28 @@
local
-fun gen_invoke_case internal prep_att ((name, pos), xs, raw_atts) state =
+fun gen_case internal prep_att ((raw_binding, raw_atts), ((name, pos), xs)) state =
let
- val atts = map (prep_att (context_of state)) raw_atts;
+ val ctxt = context_of state;
+
+ val binding = if Binding.is_empty raw_binding then Binding.make (name, pos) else raw_binding;
+ val atts = map (prep_att ctxt) raw_atts;
+
val (asms, state') = state |> map_context_result (fn ctxt =>
ctxt |> Proof_Context.apply_case (Proof_Context.check_case ctxt internal (name, pos) xs));
val assumptions =
- asms |> map (fn (b, ts) => ((Binding.set_pos pos b, atts), map (rpair []) ts));
+ asms |> map (fn (a, ts) => ((Binding.qualified true a binding, []), map (rpair []) ts));
in
state'
|> assume assumptions
|> map_context (fold Variable.unbind_term Auto_Bind.no_facts)
- |> `the_facts |-> (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])])
+ |> `the_facts |-> (fn thms => note_thmss [((binding, atts), [(thms, [])])])
end;
in
-val invoke_case = gen_invoke_case true (K I);
-val invoke_case_cmd = gen_invoke_case false Attrib.attribute_cmd;
+val case_ = gen_case true (K I);
+val case_cmd = gen_case false Attrib.attribute_cmd;
end;
--- a/src/Pure/Isar/proof_context.ML Wed Jun 24 00:30:03 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Jun 24 21:26:03 2015 +0200
@@ -141,7 +141,7 @@
Proof.context -> (string * thm list) list * Proof.context
val dest_cases: Proof.context -> (string * (Rule_Cases.T * bool)) list
val update_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
- val apply_case: Rule_Cases.T -> Proof.context -> (binding * term list) list * Proof.context
+ val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
val check_case: Proof.context -> bool ->
string * Position.T -> binding option list -> Rule_Cases.T
val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
@@ -1333,9 +1333,9 @@
[Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1,
Pretty.quote (prt_term t)];
- fun prt_asm (b, ts) =
+ fun prt_asm (a, ts) =
Pretty.block (Pretty.breaks
- ((if Binding.is_empty b then [] else [Binding.pretty b, Pretty.str ":"]) @
+ ((if a = "" then [] else [Pretty.str a, Pretty.str ":"]) @
map (Pretty.quote o prt_term) ts));
fun prt_sect _ _ _ [] = []
--- a/src/Pure/Isar/rule_cases.ML Wed Jun 24 00:30:03 2015 +0200
+++ b/src/Pure/Isar/rule_cases.ML Wed Jun 24 21:26:03 2015 +0200
@@ -22,7 +22,7 @@
include BASIC_RULE_CASES
datatype T = Case of
{fixes: (binding * typ) list,
- assumes: (binding * term list) list,
+ assumes: (string * term list) list,
binds: (indexname * term option) list,
cases: (string * T) list}
val case_hypsN: string
@@ -65,7 +65,7 @@
datatype T = Case of
{fixes: (binding * typ) list,
- assumes: (binding * term list) list,
+ assumes: (string * term list) list,
binds: (indexname * term option) list,
cases: (string * T) list};
@@ -94,22 +94,21 @@
| extract_fixes (SOME outline) prop =
chop (length (Logic.strip_params outline)) (strip_params prop);
-fun extract_assumes _ _ NONE prop = ([(Binding.empty, Logic.strip_assums_hyp prop)], [])
- | extract_assumes qualifier hyp_names (SOME outline) prop =
+fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
+ | extract_assumes hyp_names (SOME outline) prop =
let
- val qual = Binding.qualify true qualifier o Binding.name;
val (hyps, prems) =
chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
- fun extract ((hyp_name, hyp) :: rest) = (qual hyp_name, hyp :: map snd rest);
+ fun extract ((hyp_name, hyp) :: rest) = (hyp_name, hyp :: map snd rest);
val (hyps1, hyps2) = chop (length hyp_names) hyps;
val pairs1 = if null hyps1 then [] else hyp_names ~~ hyps1;
val pairs = pairs1 @ map (pair case_hypsN) hyps2;
val named_hyps = map extract (partition_eq (eq_fst op =) pairs);
- in (named_hyps, [(qual case_premsN, prems)]) end;
+ in (named_hyps, [(case_premsN, prems)]) end;
fun bindings args = map (apfst Binding.name) args;
-fun extract_case ctxt (case_outline, raw_prop) name hyp_names concls =
+fun extract_case ctxt (case_outline, raw_prop) hyp_names concls =
let
val props = Logic.dest_conjunctions (Drule.norm_hhf (Proof_Context.theory_of ctxt) raw_prop);
val len = length props;
@@ -125,7 +124,7 @@
fold_rev Term.abs fixes1
(app (map (Term.dummy_pattern o #2) fixes2) (fold_rev Term.abs fixes2 t));
val (assumes1, assumes2) =
- extract_assumes name hyp_names case_outline prop
+ extract_assumes hyp_names case_outline prop
|> apply2 (map (apsnd (maps Logic.dest_conjunctions)));
val concl = Object_Logic.drop_judgment ctxt (Logic.strip_assums_concl prop);
@@ -162,7 +161,7 @@
((case try (fn () =>
(Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
NONE => (name, NONE)
- | SOME p => (name, extract_case ctxt p name hyp_names concls)) :: cs, i - 1);
+ | SOME p => (name, extract_case ctxt p hyp_names concls)) :: cs, i - 1);
in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
in