clarified 'case' command;
authorwenzelm
Wed Jun 24 21:26:03 2015 +0200 (2015-06-24)
changeset 60565b7ee41f72add
parent 60564 6a363e56ffff
child 60566 d9682058f7ee
clarified 'case' command;
NEWS
src/Doc/Isar_Ref/Proof.thy
src/HOL/Library/FinFun.thy
src/HOL/MicroJava/J/Eval.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_cases.ML
     1.1 --- a/NEWS	Wed Jun 24 00:30:03 2015 +0200
     1.2 +++ b/NEWS	Wed Jun 24 21:26:03 2015 +0200
     1.3 @@ -66,6 +66,17 @@
     1.4      then show ?thesis <proof>
     1.5    qed
     1.6  
     1.7 +* Command 'case' allows fact name and attribute specification like this:
     1.8 +
     1.9 +  case a: (c xs)
    1.10 +  case a [attributes]: (c xs)
    1.11 +
    1.12 +Facts that are introduced by invoking the case context are uniformly
    1.13 +qualified by "a"; the same name is used for the cumulative fact. The old
    1.14 +form "case (c xs) [attributes]" is no longer supported. Rare
    1.15 +INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,
    1.16 +and always put attributes in front.
    1.17 +
    1.18  * Nesting of Isar goal structure has been clarified: the context after
    1.19  the initial backwards refinement is retained for the whole proof, within
    1.20  all its context sections (as indicated via 'next'). This is e.g.
     2.1 --- a/src/Doc/Isar_Ref/Proof.thy	Wed Jun 24 00:30:03 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Wed Jun 24 21:26:03 2015 +0200
     2.3 @@ -1061,11 +1061,8 @@
     2.4    later.
     2.5  
     2.6    @{rail \<open>
     2.7 -    @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) *) ')')
     2.8 +    @@{command case} @{syntax thmdecl}? (nameref | '(' nameref (('_' | @{syntax name}) *) ')')
     2.9      ;
    2.10 -    caseref: nameref attributes?
    2.11 -    ;
    2.12 -
    2.13      @@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) +) ']' ) ? ) +)
    2.14      ;
    2.15      @@{attribute case_conclusion} @{syntax name} (@{syntax name} * )
    2.16 @@ -1077,12 +1074,18 @@
    2.17  
    2.18    \begin{description}
    2.19  
    2.20 -  \item @{command "case"}~@{text "(c x\<^sub>1 \<dots> x\<^sub>m)"} invokes a named local
    2.21 +  \item @{command "case"}~@{text "a: (c x\<^sub>1 \<dots> x\<^sub>m)"} invokes a named local
    2.22    context @{text "c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m"}, as provided by an
    2.23 -  appropriate proof method (such as @{method_ref cases} and
    2.24 -  @{method_ref induct}).  The command ``@{command "case"}~@{text "(c
    2.25 -  x\<^sub>1 \<dots> x\<^sub>m)"}'' abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \<dots>
    2.26 -  x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}''.
    2.27 +  appropriate proof method (such as @{method_ref cases} and @{method_ref
    2.28 +  induct}). The command ``@{command "case"}~@{text "a: (c x\<^sub>1 \<dots> x\<^sub>m)"}''
    2.29 +  abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command
    2.30 +  "assume"}~@{text "a.c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}''. Each local fact is qualified by the
    2.31 +  prefix @{text "a"}, and all such facts are collectively bound to the name
    2.32 +  @{text a}.
    2.33 +
    2.34 +  The fact name is specification @{text a} is optional, the default is to
    2.35 +  re-use @{text c}. So @{command "case"}~@{text "(c x\<^sub>1 \<dots> x\<^sub>m)"} is the same
    2.36 +  as @{command "case"}~@{text "c: (c x\<^sub>1 \<dots> x\<^sub>m)"}.
    2.37  
    2.38    \item @{command "print_cases"} prints all local contexts of the
    2.39    current state, using Isar proof language notation.
     3.1 --- a/src/HOL/Library/FinFun.thy	Wed Jun 24 00:30:03 2015 +0200
     3.2 +++ b/src/HOL/Library/FinFun.thy	Wed Jun 24 21:26:03 2015 +0200
     3.3 @@ -1361,7 +1361,7 @@
     3.4      and [simp]: "sorted xs" "distinct xs" by simp_all
     3.5    show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))"
     3.6    proof(cases "b = finfun_default f")
     3.7 -    case True [simp]
     3.8 +    case [simp]: True
     3.9      show ?thesis
    3.10      proof(cases "finfun_dom f $ a")
    3.11        case True
     4.1 --- a/src/HOL/MicroJava/J/Eval.thy	Wed Jun 24 00:30:03 2015 +0200
     4.2 +++ b/src/HOL/MicroJava/J/Eval.thy	Wed Jun 24 21:26:03 2015 +0200
     4.3 @@ -222,22 +222,22 @@
     4.4    case eval
     4.5    from eval.prems show thesis
     4.6    proof(cases (no_simp))
     4.7 -    case LAcc with LAcc_code show ?thesis by auto
     4.8 +    case LAcc with eval.LAcc_code show ?thesis by auto
     4.9    next
    4.10      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)
    4.11 -    with Call_code show ?thesis
    4.12 +    with eval.Call_code show ?thesis
    4.13        by(cases "s4") auto
    4.14 -  qed(erule (3) that[OF refl]|assumption)+
    4.15 +  qed(erule (3) eval.that[OF refl]|assumption)+
    4.16  next
    4.17    case evals
    4.18    from evals.prems show thesis
    4.19 -    by(cases (no_simp))(erule (3) that[OF refl]|assumption)+
    4.20 +    by(cases (no_simp))(erule (3) evals.that[OF refl]|assumption)+
    4.21  next
    4.22    case exec
    4.23    from exec.prems show thesis
    4.24    proof(cases (no_simp))
    4.25 -    case LoopT thus ?thesis by(rule LoopT_code[OF refl])
    4.26 -  qed(erule (2) that[OF refl]|assumption)+
    4.27 +    case LoopT thus ?thesis by(rule exec.LoopT_code[OF refl])
    4.28 +  qed(erule (2) exec.that[OF refl]|assumption)+
    4.29  qed
    4.30  
    4.31  end
     5.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Jun 24 00:30:03 2015 +0200
     5.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Jun 24 21:26:03 2015 +0200
     5.3 @@ -241,10 +241,10 @@
     5.4    from appending.prems show thesis
     5.5    proof(cases)
     5.6      case nil
     5.7 -    from alt_nil nil show thesis by auto
     5.8 +    from appending.alt_nil nil show thesis by auto
     5.9    next
    5.10      case cons
    5.11 -    from alt_cons cons show thesis by fastforce
    5.12 +    from appending.alt_cons cons show thesis by fastforce
    5.13    qed
    5.14  qed
    5.15  
    5.16 @@ -270,17 +270,17 @@
    5.17    from ya_even.prems show thesis
    5.18    proof (cases)
    5.19      case even_zero
    5.20 -    from even_zero even_0 show thesis by simp
    5.21 +    from even_zero ya_even.even_0 show thesis by simp
    5.22    next
    5.23      case even_plus1
    5.24 -    from even_plus1 even_Suc show thesis by simp
    5.25 +    from even_plus1 ya_even.even_Suc show thesis by simp
    5.26    qed
    5.27  next
    5.28    case ya_odd
    5.29    from ya_odd.prems show thesis
    5.30    proof (cases)
    5.31      case odd_plus1
    5.32 -    from odd_plus1 odd_Suc show thesis by simp
    5.33 +    from odd_plus1 ya_odd.odd_Suc show thesis by simp
    5.34    qed
    5.35  qed
    5.36  
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Jun 24 00:30:03 2015 +0200
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Jun 24 21:26:03 2015 +0200
     6.3 @@ -1620,9 +1620,6 @@
     6.4      Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)
     6.5        "adding alternative introduction rules for code generation of inductive predicates")
     6.6  
     6.7 -fun qualified_binding a =
     6.8 -  Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));
     6.9 -
    6.10  (* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
    6.11  (* FIXME ... this is important to avoid changing the background theory below *)
    6.12  fun generic_code_pred prep_const options raw_const lthy =
    6.13 @@ -1641,14 +1638,14 @@
    6.14        in mk_casesrule lthy' pred intros end
    6.15      val cases_rules = map mk_cases preds
    6.16      val cases =
    6.17 -      map2 (fn pred_name => fn case_rule => Rule_Cases.Case {fixes = [],
    6.18 -        assumes =
    6.19 -          (Binding.name "that", tl (Logic.strip_imp_prems case_rule)) ::
    6.20 -          map_filter (fn (fact_name, fact) =>
    6.21 -              Option.map (fn a => (qualified_binding a, [fact])) fact_name)
    6.22 -            ((SOME (Long_Name.base_name pred_name ^ ".prems") :: names_of ctxt' pred_name) ~~
    6.23 -              Logic.strip_imp_prems case_rule),
    6.24 -        binds = [], cases = []}) preds cases_rules
    6.25 +      map2 (fn pred_name => fn case_rule =>
    6.26 +        Rule_Cases.Case {
    6.27 +          fixes = [],
    6.28 +          assumes =
    6.29 +            ("that", tl (Logic.strip_imp_prems case_rule)) ::
    6.30 +            map_filter (fn (fact_name, fact) => Option.map (fn a => (a, [fact])) fact_name)
    6.31 +              ((SOME "prems" :: names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule),
    6.32 +          binds = [], cases = []}) preds cases_rules
    6.33      val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
    6.34      val lthy'' = lthy'
    6.35        |> fold Variable.auto_fixes cases_rules
     7.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Jun 24 00:30:03 2015 +0200
     7.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Jun 24 21:26:03 2015 +0200
     7.3 @@ -595,11 +595,11 @@
     7.4  
     7.5  val _ =
     7.6    Outer_Syntax.command @{command_keyword case} "invoke local context"
     7.7 -    ((@{keyword "("} |--
     7.8 -      Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
     7.9 -        --| @{keyword ")"}) ||
    7.10 -      Parse.position Parse.xname >> rpair []) -- Parse.opt_attribs >> (fn ((c, xs), atts) =>
    7.11 -        Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
    7.12 +    (Parse_Spec.opt_thm_name ":" --
    7.13 +      (@{keyword "("} |--
    7.14 +        Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
    7.15 +          --| @{keyword ")"}) ||
    7.16 +        Parse.position Parse.xname >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
    7.17  
    7.18  
    7.19  (* proof structure *)
     8.1 --- a/src/Pure/Isar/proof.ML	Wed Jun 24 00:30:03 2015 +0200
     8.2 +++ b/src/Pure/Isar/proof.ML	Wed Jun 24 21:26:03 2015 +0200
     8.3 @@ -71,10 +71,8 @@
     8.4    val using_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
     8.5    val unfolding: ((thm list * attribute list) list) list -> state -> state
     8.6    val unfolding_cmd: ((Facts.ref * Token.src list) list) list -> state -> state
     8.7 -  val invoke_case: (string * Position.T) * binding option list * attribute list ->
     8.8 -    state -> state
     8.9 -  val invoke_case_cmd: (string * Position.T) * binding option list * Token.src list ->
    8.10 -    state -> state
    8.11 +  val case_: Thm.binding * ((string * Position.T) * binding option list) -> state -> state
    8.12 +  val case_cmd: Attrib.binding * ((string * Position.T) * binding option list) -> state -> state
    8.13    val begin_block: state -> state
    8.14    val next_block: state -> state
    8.15    val end_block: state -> state
    8.16 @@ -767,24 +765,28 @@
    8.17  
    8.18  local
    8.19  
    8.20 -fun gen_invoke_case internal prep_att ((name, pos), xs, raw_atts) state =
    8.21 +fun gen_case internal prep_att ((raw_binding, raw_atts), ((name, pos), xs)) state =
    8.22    let
    8.23 -    val atts = map (prep_att (context_of state)) raw_atts;
    8.24 +    val ctxt = context_of state;
    8.25 +
    8.26 +    val binding = if Binding.is_empty raw_binding then Binding.make (name, pos) else raw_binding;
    8.27 +    val atts = map (prep_att ctxt) raw_atts;
    8.28 +
    8.29      val (asms, state') = state |> map_context_result (fn ctxt =>
    8.30        ctxt |> Proof_Context.apply_case (Proof_Context.check_case ctxt internal (name, pos) xs));
    8.31      val assumptions =
    8.32 -      asms |> map (fn (b, ts) => ((Binding.set_pos pos b, atts), map (rpair []) ts));
    8.33 +      asms |> map (fn (a, ts) => ((Binding.qualified true a binding, []), map (rpair []) ts));
    8.34    in
    8.35      state'
    8.36      |> assume assumptions
    8.37      |> map_context (fold Variable.unbind_term Auto_Bind.no_facts)
    8.38 -    |> `the_facts |-> (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])])
    8.39 +    |> `the_facts |-> (fn thms => note_thmss [((binding, atts), [(thms, [])])])
    8.40    end;
    8.41  
    8.42  in
    8.43  
    8.44 -val invoke_case = gen_invoke_case true (K I);
    8.45 -val invoke_case_cmd = gen_invoke_case false Attrib.attribute_cmd;
    8.46 +val case_ = gen_case true (K I);
    8.47 +val case_cmd = gen_case false Attrib.attribute_cmd;
    8.48  
    8.49  end;
    8.50  
     9.1 --- a/src/Pure/Isar/proof_context.ML	Wed Jun 24 00:30:03 2015 +0200
     9.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Jun 24 21:26:03 2015 +0200
     9.3 @@ -141,7 +141,7 @@
     9.4      Proof.context -> (string * thm list) list * Proof.context
     9.5    val dest_cases: Proof.context -> (string * (Rule_Cases.T * bool)) list
     9.6    val update_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
     9.7 -  val apply_case: Rule_Cases.T -> Proof.context -> (binding * term list) list * Proof.context
     9.8 +  val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
     9.9    val check_case: Proof.context -> bool ->
    9.10      string * Position.T -> binding option list -> Rule_Cases.T
    9.11    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
    9.12 @@ -1333,9 +1333,9 @@
    9.13        [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1,
    9.14          Pretty.quote (prt_term t)];
    9.15  
    9.16 -    fun prt_asm (b, ts) =
    9.17 +    fun prt_asm (a, ts) =
    9.18        Pretty.block (Pretty.breaks
    9.19 -        ((if Binding.is_empty b then [] else [Binding.pretty b, Pretty.str ":"]) @
    9.20 +        ((if a = "" then [] else [Pretty.str a, Pretty.str ":"]) @
    9.21            map (Pretty.quote o prt_term) ts));
    9.22  
    9.23      fun prt_sect _ _ _ [] = []
    10.1 --- a/src/Pure/Isar/rule_cases.ML	Wed Jun 24 00:30:03 2015 +0200
    10.2 +++ b/src/Pure/Isar/rule_cases.ML	Wed Jun 24 21:26:03 2015 +0200
    10.3 @@ -22,7 +22,7 @@
    10.4    include BASIC_RULE_CASES
    10.5    datatype T = Case of
    10.6     {fixes: (binding * typ) list,
    10.7 -    assumes: (binding * term list) list,
    10.8 +    assumes: (string * term list) list,
    10.9      binds: (indexname * term option) list,
   10.10      cases: (string * T) list}
   10.11    val case_hypsN: string
   10.12 @@ -65,7 +65,7 @@
   10.13  
   10.14  datatype T = Case of
   10.15   {fixes: (binding * typ) list,
   10.16 -  assumes: (binding * term list) list,
   10.17 +  assumes: (string * term list) list,
   10.18    binds: (indexname * term option) list,
   10.19    cases: (string * T) list};
   10.20  
   10.21 @@ -94,22 +94,21 @@
   10.22    | extract_fixes (SOME outline) prop =
   10.23        chop (length (Logic.strip_params outline)) (strip_params prop);
   10.24  
   10.25 -fun extract_assumes _ _ NONE prop = ([(Binding.empty, Logic.strip_assums_hyp prop)], [])
   10.26 -  | extract_assumes qualifier hyp_names (SOME outline) prop =
   10.27 +fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
   10.28 +  | extract_assumes hyp_names (SOME outline) prop =
   10.29        let
   10.30 -        val qual = Binding.qualify true qualifier o Binding.name;
   10.31          val (hyps, prems) =
   10.32            chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
   10.33 -        fun extract ((hyp_name, hyp) :: rest) = (qual hyp_name, hyp :: map snd rest);
   10.34 +        fun extract ((hyp_name, hyp) :: rest) = (hyp_name, hyp :: map snd rest);
   10.35          val (hyps1, hyps2) = chop (length hyp_names) hyps;
   10.36          val pairs1 = if null hyps1 then [] else hyp_names ~~ hyps1;
   10.37          val pairs = pairs1 @ map (pair case_hypsN) hyps2;
   10.38          val named_hyps = map extract (partition_eq (eq_fst op =) pairs);
   10.39 -      in (named_hyps, [(qual case_premsN, prems)]) end;
   10.40 +      in (named_hyps, [(case_premsN, prems)]) end;
   10.41  
   10.42  fun bindings args = map (apfst Binding.name) args;
   10.43  
   10.44 -fun extract_case ctxt (case_outline, raw_prop) name hyp_names concls =
   10.45 +fun extract_case ctxt (case_outline, raw_prop) hyp_names concls =
   10.46    let
   10.47      val props = Logic.dest_conjunctions (Drule.norm_hhf (Proof_Context.theory_of ctxt) raw_prop);
   10.48      val len = length props;
   10.49 @@ -125,7 +124,7 @@
   10.50              fold_rev Term.abs fixes1
   10.51                (app (map (Term.dummy_pattern o #2) fixes2) (fold_rev Term.abs fixes2 t));
   10.52          val (assumes1, assumes2) =
   10.53 -          extract_assumes name hyp_names case_outline prop
   10.54 +          extract_assumes hyp_names case_outline prop
   10.55            |> apply2 (map (apsnd (maps Logic.dest_conjunctions)));
   10.56  
   10.57          val concl = Object_Logic.drop_judgment ctxt (Logic.strip_assums_concl prop);
   10.58 @@ -162,7 +161,7 @@
   10.59        ((case try (fn () =>
   10.60            (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
   10.61          NONE => (name, NONE)
   10.62 -      | SOME p => (name, extract_case ctxt p name hyp_names concls)) :: cs, i - 1);
   10.63 +      | SOME p => (name, extract_case ctxt p hyp_names concls)) :: cs, i - 1);
   10.64    in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
   10.65  
   10.66  in