# HG changeset patch # User wenzelm # Date 1435173963 -7200 # Node ID b7ee41f72added84aa1172aad26d5cbdcb87ca2b # Parent 6a363e56ffff6b07fed9c0c59a0fe37d28b9f760 clarified 'case' command; diff -r 6a363e56ffff -r b7ee41f72add NEWS --- 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 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. diff -r 6a363e56ffff -r b7ee41f72add src/Doc/Isar_Ref/Proof.thy --- 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 \ - @@{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 \ x\<^sub>m)"} invokes a named local + \item @{command "case"}~@{text "a: (c x\<^sub>1 \ x\<^sub>m)"} invokes a named local context @{text "c: x\<^sub>1, \, x\<^sub>m, \\<^sub>1, \, \\<^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 \ x\<^sub>m)"}'' abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \ - x\<^sub>m"}~@{command "assume"}~@{text "c: \\<^sub>1 \ \\<^sub>n"}''. + appropriate proof method (such as @{method_ref cases} and @{method_ref + induct}). The command ``@{command "case"}~@{text "a: (c x\<^sub>1 \ x\<^sub>m)"}'' + abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \ x\<^sub>m"}~@{command + "assume"}~@{text "a.c: \\<^sub>1 \ \\<^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 \ x\<^sub>m)"} is the same + as @{command "case"}~@{text "c: (c x\<^sub>1 \ x\<^sub>m)"}. \item @{command "print_cases"} prints all local contexts of the current state, using Isar proof language notation. diff -r 6a363e56ffff -r b7ee41f72add src/HOL/Library/FinFun.thy --- 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 diff -r 6a363e56ffff -r b7ee41f72add src/HOL/MicroJava/J/Eval.thy --- 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 diff -r 6a363e56ffff -r b7ee41f72add src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy --- 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 diff -r 6a363e56ffff -r b7ee41f72add src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r 6a363e56ffff -r b7ee41f72add src/Pure/Isar/isar_syn.ML --- 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 *) diff -r 6a363e56ffff -r b7ee41f72add src/Pure/Isar/proof.ML --- 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; diff -r 6a363e56ffff -r b7ee41f72add src/Pure/Isar/proof_context.ML --- 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 _ _ _ [] = [] diff -r 6a363e56ffff -r b7ee41f72add src/Pure/Isar/rule_cases.ML --- 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