--- a/src/HOL/Bali/DefiniteAssignment.thy Sun Aug 07 23:08:07 2011 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Mon Aug 08 07:13:16 2011 +0200
@@ -1056,8 +1056,7 @@
(is "PROP ?Hyp Env B t A")
proof (induct)
case Skip
- from Skip.prems Skip.hyps
- show ?case by cases simp
+ then show ?case by cases simp
next
case Expr
from Expr.prems Expr.hyps
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML Sun Aug 07 23:08:07 2011 +0200
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Mon Aug 08 07:13:16 2011 +0200
@@ -91,7 +91,7 @@
CASES
(Rule_Cases.make_common
(Proof_Context.theory_of ctxt,
- Thm.prop_of (Rule_Cases.internalize_params st)) names)
+ Thm.prop_of (Rule_Cases.internalize_params st)) (map (rpair []) names))
Tactical.all_tac st))
in
val setup_boogie_cases = Method.setup @{binding boogie_cases}
--- a/src/HOL/Nominal/nominal_inductive.ML Sun Aug 07 23:08:07 2011 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon Aug 08 07:13:16 2011 +0200
@@ -158,7 +158,7 @@
[] => ()
| xs => error ("Missing equivariance theorem for predicate(s): " ^
commas_quote xs));
- val induct_cases = map fst (fst (Rule_Cases.get (the
+ val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the
(Induct.lookup_inductP ctxt (hd names)))));
val ([raw_induct'], ctxt') = Variable.import_terms false [prop_of raw_induct] ctxt;
val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
--- a/src/HOL/Nominal/nominal_inductive2.ML Sun Aug 07 23:08:07 2011 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Aug 08 07:13:16 2011 +0200
@@ -165,7 +165,7 @@
[] => ()
| xs => error ("Missing equivariance theorem for predicate(s): " ^
commas_quote xs));
- val induct_cases = map fst (fst (Rule_Cases.get (the
+ val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the
(Induct.lookup_inductP ctxt (hd names)))));
val induct_cases' = if null induct_cases then replicate (length intrs) ""
else induct_cases;
--- a/src/HOL/Tools/inductive_set.ML Sun Aug 07 23:08:07 2011 +0200
+++ b/src/HOL/Tools/inductive_set.ML Mon Aug 08 07:13:16 2011 +0200
@@ -524,7 +524,7 @@
Inductive.declare_rules rec_name coind no_ind cnames (map fst defs)
(map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
(map (fn th => (to_set [] (Context.Proof lthy3) th,
- map fst (fst (Rule_Cases.get th)),
+ map (fst o fst) (fst (Rule_Cases.get th)),
Rule_Cases.get_constraints th)) elims)
(map (to_set [] (Context.Proof lthy3)) eqs) raw_induct' lthy3;
in
--- a/src/Pure/Isar/attrib.ML Sun Aug 07 23:08:07 2011 +0200
+++ b/src/Pure/Isar/attrib.ML Mon Aug 08 07:13:16 2011 +0200
@@ -267,6 +267,22 @@
val elim_format = Thm.rule_attribute (K Tactic.make_elim);
+(* case names *)
+
+fun hname NONE = Rule_Cases.case_hypsN
+ | hname (SOME n) = n;
+
+fun case_names cs =
+ Rule_Cases.case_names (map fst cs) #>
+ Rule_Cases.cases_hyp_names (map (map hname o snd) cs)
+
+val hnamesP =
+ Scan.optional
+ (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]")
+ []
+
+val case_namesP = Scan.lift (Scan.repeat1 (Args.name -- hnamesP))
+
(* misc rules *)
val no_vars = Thm.rule_attribute (fn context => fn th =>
@@ -300,7 +316,7 @@
"number of consumed facts" #>
setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
"number of equality constraints" #>
- setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
+ setup (Binding.name "case_names") (case_namesP >> case_names)
"named rule cases" #>
setup (Binding.name "case_conclusion")
(Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
--- a/src/Pure/Isar/proof.ML Sun Aug 07 23:08:07 2011 +0200
+++ b/src/Pure/Isar/proof.ML Mon Aug 08 07:13:16 2011 +0200
@@ -391,7 +391,7 @@
fun no_goal_cases st = map (rpair NONE) (goals st);
fun goal_cases st =
- Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
+ Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
fun apply_method current_context meth state =
let
--- a/src/Pure/Isar/rule_cases.ML Sun Aug 07 23:08:07 2011 +0200
+++ b/src/Pure/Isar/rule_cases.ML Mon Aug 08 07:13:16 2011 +0200
@@ -24,9 +24,12 @@
assumes: (string * term list) list,
binds: (indexname * term option) list,
cases: (string * T) list}
+ val case_hypsN: string
val strip_params: term -> (string * typ) list
- val make_common: theory * term -> (string * string list) list -> cases
- val make_nested: term -> theory * term -> (string * string list) list -> cases
+ val make_common: theory * term ->
+ ((string * string list) * string list) list -> cases
+ val make_nested: term -> theory * term ->
+ ((string * string list) * string list) list -> cases
val apply: term list -> T -> T
val consume: thm list -> thm list -> ('a * int) * thm ->
(('a * (int * thm list)) * thm) Seq.seq
@@ -38,11 +41,12 @@
val constraints: int -> attribute
val name: string list -> thm -> thm
val case_names: string list -> attribute
+ val cases_hyp_names: string list list -> attribute
val case_conclusion: string * string list -> attribute
val is_inner_rule: thm -> bool
val inner_rule: attribute
val save: thm -> thm -> thm
- val get: thm -> (string * string list) list * int
+ val get: thm -> ((string * string list) * string list) list * int
val rename_params: string list list -> thm -> thm
val params: string list list -> attribute
val internalize_params: thm -> thm
@@ -87,15 +91,21 @@
| extract_fixes (SOME outline) prop =
chop (length (Logic.strip_params outline)) (strip_params prop);
-fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
- | extract_assumes qual (SOME outline) prop =
- let val (hyps, prems) =
- chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
- in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end;
+fun extract_assumes _ _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
+ | extract_assumes qual hnames (SOME outline) prop =
+ let
+ val (hyps, prems) =
+ chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
+ fun extract ((hname,h)::ps) = (qual hname, h :: map snd ps);
+ val (hyps1,hyps2) = chop (length hnames) hyps;
+ val pairs1 = if hyps1 = [] then [] else hnames ~~ 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;
fun bindings args = map (apfst Binding.name) args;
-fun extract_case thy (case_outline, raw_prop) name concls =
+fun extract_case thy (case_outline, raw_prop) name hnames concls =
let
val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
val len = length props;
@@ -108,8 +118,7 @@
fun abs_fixes1 t =
if not nested then abs_fixes t
else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t));
-
- val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) case_outline prop
+ val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) hnames case_outline prop
|> pairself (map (apsnd (maps Logic.dest_conjunctions)));
val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
@@ -142,11 +151,11 @@
let
val n = length cases;
val nprems = Logic.count_prems prop;
- fun add_case (name, concls) (cs, i) =
+ fun add_case ((name, hnames), concls) (cs, i) =
((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 thy p name concls)) :: cs, i - 1);
+ | SOME p => (name, extract_case thy p name hnames concls)) :: cs, i - 1);
in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
in
@@ -286,6 +295,26 @@
fun case_names ss = Thm.rule_attribute (K (name ss));
+(** hyp names **)
+
+val implode_hyps = implode_args o map (suffix "," o space_implode ",");
+val explode_hyps = map (space_explode "," o unsuffix ",") o explode_args;
+
+val cases_hyp_names_tagN = "cases_hyp_names";
+
+fun add_cases_hyp_names NONE = I
+ | add_cases_hyp_names (SOME namess) =
+ Thm.untag_rule cases_hyp_names_tagN
+ #> Thm.tag_rule (cases_hyp_names_tagN, implode_hyps namess);
+
+fun lookup_cases_hyp_names th =
+ AList.lookup (op =) (Thm.get_tags th) cases_hyp_names_tagN
+ |> Option.map explode_hyps;
+
+val save_cases_hyp_names = add_cases_hyp_names o lookup_cases_hyp_names;
+fun cases_hyp_names ss =
+ Thm.rule_attribute (K (add_cases_hyp_names (SOME ss)));
+
(** case conclusions **)
@@ -339,6 +368,7 @@
save_consumes th #>
save_constraints th #>
save_case_names th #>
+ save_cases_hyp_names th #>
save_case_concls th #>
save_inner_rule th;
@@ -349,7 +379,11 @@
(case lookup_case_names th of
NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n))
| SOME names => map (fn name => (name, get_case_concls th name)) names);
- in (cases, n) end;
+ val cases_hyps = (case lookup_cases_hyp_names th of
+ NONE => replicate (length cases) []
+ | SOME names => names);
+ fun regroup ((name,concls),hyps) = ((name,hyps),concls)
+ in (map regroup (cases ~~ cases_hyps), n) end;
(* params *)
--- a/src/Tools/case_product.ML Sun Aug 07 23:08:07 2011 +0200
+++ b/src/Tools/case_product.ML Mon Aug 08 07:13:16 2011 +0200
@@ -90,9 +90,9 @@
fun annotation thm1 thm2 =
let
- val (names1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
- val (names2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
- val names = map_product (fn x => fn y => x ^ "_" ^y) names1 names2
+ val (cases1, cons1) = apfst (map fst) (Rule_Cases.get thm1)
+ val (cases2, cons2) = apfst (map fst) (Rule_Cases.get thm2)
+ val names = map_product (fn (x,_) => fn (y,_) => x ^ "_" ^y) cases1 cases2
in
Rule_Cases.case_names names o Rule_Cases.consumes (cons1 + cons2)
end