src/Pure/Isar/rule_cases.ML
author blanchet
Fri, 01 Aug 2014 14:43:57 +0200
changeset 57743 0af2d5dfb0ac
parent 56231 b98813774a63
child 58014 47ecbef7274b
permissions -rw-r--r--
pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/rule_cases.ML
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
     3
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
     4
Annotations and local contexts of rules.
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
     5
*)
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
     6
18188
cb53a778455e added THEN_ALL_NEW_CASES;
wenzelm
parents: 18050
diff changeset
     7
infix 1 THEN_ALL_NEW_CASES;
cb53a778455e added THEN_ALL_NEW_CASES;
wenzelm
parents: 18050
diff changeset
     8
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
     9
signature BASIC_RULE_CASES =
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
    10
sig
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
    11
  type cases
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
    12
  type cases_tactic
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
    13
  val CASES: cases -> tactic -> cases_tactic
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
    14
  val NO_CASES: tactic -> cases_tactic
56231
b98813774a63 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents: 55639
diff changeset
    15
  val SUBGOAL_CASES: ((term * int * thm) -> cases_tactic) -> int -> cases_tactic
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
    16
  val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
    17
end
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
    18
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    19
signature RULE_CASES =
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    20
sig
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
    21
  include BASIC_RULE_CASES
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    22
  datatype T = Case of
42496
65ec88b369fd more precise positions via binding;
wenzelm
parents: 41228
diff changeset
    23
   {fixes: (binding * typ) list,
53380
08f3491c50bf cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents: 46219
diff changeset
    24
    assumes: (binding * term list) list,
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    25
    binds: (indexname * term option) list,
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    26
    cases: (string * T) list}
44045
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
    27
  val case_hypsN: string
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    28
  val strip_params: term -> (string * typ) list
44045
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
    29
  val make_common: theory * term ->
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
    30
    ((string * string list) * string list) list -> cases
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
    31
  val make_nested: term -> theory * term ->
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
    32
    ((string * string list) * string list) list -> cases
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    33
  val apply: term list -> T -> T
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53380
diff changeset
    34
  val consume: Proof.context -> thm list -> thm list -> ('a * int) * thm ->
18237
2edb6a1f9c14 consume: proper treatment of defs;
wenzelm
parents: 18229
diff changeset
    35
    (('a * (int * thm list)) * thm) Seq.seq
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 45328
diff changeset
    36
  val get_consumes: thm -> int
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 45328
diff changeset
    37
  val put_consumes: int option -> thm -> thm
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
    38
  val add_consumes: int -> thm -> thm
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 45328
diff changeset
    39
  val default_consumes: int -> thm -> thm
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18608
diff changeset
    40
  val consumes: int -> attribute
34986
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
    41
  val get_constraints: thm -> int
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
    42
  val constraints: int -> attribute
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    43
  val name: string list -> thm -> thm
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18608
diff changeset
    44
  val case_names: string list -> attribute
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 45328
diff changeset
    45
  val cases_hyp_names: string list -> string list list -> attribute
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18608
diff changeset
    46
  val case_conclusion: string * string list -> attribute
33303
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
    47
  val is_inner_rule: thm -> bool
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
    48
  val inner_rule: attribute
12761
b0c39f9837af save: be slightly more about absent tags;
wenzelm
parents: 12166
diff changeset
    49
  val save: thm -> thm -> thm
44045
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
    50
  val get: thm -> ((string * string list) * string list) list * int
8427
wenzelm
parents: 8400
diff changeset
    51
  val rename_params: string list list -> thm -> thm
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18608
diff changeset
    52
  val params: string list list -> attribute
34916
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
    53
  val internalize_params: thm -> thm
20289
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20218
diff changeset
    54
  val mutual_rule: Proof.context -> thm list -> (int list * thm) option
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20218
diff changeset
    55
  val strict_mutual_rule: Proof.context -> thm list -> int list * thm
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    56
end;
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    57
33368
b1cf34f1855c modernized structure Rule_Cases;
wenzelm
parents: 33303
diff changeset
    58
structure Rule_Cases: RULE_CASES =
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    59
struct
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
    60
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    61
(** cases **)
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    62
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    63
datatype T = Case of
42496
65ec88b369fd more precise positions via binding;
wenzelm
parents: 41228
diff changeset
    64
 {fixes: (binding * typ) list,
53380
08f3491c50bf cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents: 46219
diff changeset
    65
  assumes: (binding * term list) list,
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    66
  binds: (indexname * term option) list,
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    67
  cases: (string * T) list};
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    68
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    69
type cases = (string * T option) list;
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    70
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    71
val case_conclN = "case";
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    72
val case_hypsN = "hyps";
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    73
val case_premsN = "prems";
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    74
20087
979f012b5df3 Name.internal;
wenzelm
parents: 19917
diff changeset
    75
val strip_params = map (apfst (perhaps (try Name.dest_skolem))) o Logic.strip_params;
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    76
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    77
local
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    78
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    79
fun app us t = Term.betapplys (t, us);
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    80
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    81
fun dest_binops cs tm =
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    82
  let
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    83
    val n = length cs;
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    84
    fun dest 0 _ = []
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    85
      | dest 1 t = [t]
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    86
      | dest k (_ $ t $ u) = t :: dest (k - 1) u
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    87
      | dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]);
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    88
  in cs ~~ dest n tm end;
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    89
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    90
fun extract_fixes NONE prop = (strip_params prop, [])
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    91
  | extract_fixes (SOME outline) prop =
19012
wenzelm
parents: 18909
diff changeset
    92
      chop (length (Logic.strip_params outline)) (strip_params prop);
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
    93
53380
08f3491c50bf cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents: 46219
diff changeset
    94
fun extract_assumes _ _ NONE prop = ([(Binding.empty, Logic.strip_assums_hyp prop)], [])
08f3491c50bf cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents: 46219
diff changeset
    95
  | extract_assumes qualifier hyp_names (SOME outline) prop =
44045
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
    96
      let
53380
08f3491c50bf cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents: 46219
diff changeset
    97
        val qual = Binding.qualify true qualifier o Binding.name;
44045
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
    98
        val (hyps, prems) =
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
    99
          chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
53380
08f3491c50bf cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents: 46219
diff changeset
   100
        fun extract ((hyp_name, hyp) :: rest) = (qual hyp_name, hyp :: map snd rest);
08f3491c50bf cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents: 46219
diff changeset
   101
        val (hyps1, hyps2) = chop (length hyp_names) hyps;
08f3491c50bf cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents: 46219
diff changeset
   102
        val pairs1 = if null hyps1 then [] else hyp_names ~~ hyps1;
08f3491c50bf cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents: 46219
diff changeset
   103
        val pairs = pairs1 @ map (pair case_hypsN) hyps2;
08f3491c50bf cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents: 46219
diff changeset
   104
        val named_hyps = map extract (partition_eq (eq_fst op =) pairs);
44045
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   105
      in (named_hyps, [(qual case_premsN, prems)]) end;
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   106
42496
65ec88b369fd more precise positions via binding;
wenzelm
parents: 41228
diff changeset
   107
fun bindings args = map (apfst Binding.name) args;
65ec88b369fd more precise positions via binding;
wenzelm
parents: 41228
diff changeset
   108
53380
08f3491c50bf cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents: 46219
diff changeset
   109
fun extract_case thy (case_outline, raw_prop) name hyp_names concls =
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   110
  let
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   111
    val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   112
    val len = length props;
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   113
    val nested = is_some case_outline andalso len > 1;
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   114
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   115
    fun extract prop =
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   116
      let
34916
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   117
        val (fixes1, fixes2) = extract_fixes case_outline prop;
46219
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45525
diff changeset
   118
        val abs_fixes = fold_rev Term.abs (fixes1 @ fixes2);
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   119
        fun abs_fixes1 t =
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   120
          if not nested then abs_fixes t
46219
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45525
diff changeset
   121
          else
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45525
diff changeset
   122
            fold_rev Term.abs fixes1
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45525
diff changeset
   123
              (app (map (Term.dummy_pattern o #2) fixes2) (fold_rev Term.abs fixes2 t));
53380
08f3491c50bf cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents: 46219
diff changeset
   124
        val (assumes1, assumes2) =
08f3491c50bf cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents: 46219
diff changeset
   125
          extract_assumes name hyp_names case_outline prop
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
   126
          |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   127
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 35408
diff changeset
   128
        val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   129
        val binds =
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   130
          (case_conclN, concl) :: dest_binops concls concl
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   131
          |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   132
      in
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   133
       ((fixes1, map (apsnd (map abs_fixes1)) assumes1),
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   134
        ((fixes2, map (apsnd (map abs_fixes)) assumes2), binds))
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   135
      end;
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   136
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   137
    val cases = map extract props;
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   138
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   139
    fun common_case ((fixes1, assumes1), ((fixes2, assumes2), binds)) =
42496
65ec88b369fd more precise positions via binding;
wenzelm
parents: 41228
diff changeset
   140
      Case {fixes = bindings (fixes1 @ fixes2),
65ec88b369fd more precise positions via binding;
wenzelm
parents: 41228
diff changeset
   141
        assumes = assumes1 @ assumes2, binds = binds, cases = []};
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   142
    fun inner_case (_, ((fixes2, assumes2), binds)) =
42496
65ec88b369fd more precise positions via binding;
wenzelm
parents: 41228
diff changeset
   143
      Case {fixes = bindings fixes2, assumes = assumes2, binds = binds, cases = []};
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   144
    fun nested_case ((fixes1, assumes1), _) =
42496
65ec88b369fd more precise positions via binding;
wenzelm
parents: 41228
diff changeset
   145
      Case {fixes = bindings fixes1, assumes = assumes1, binds = [],
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   146
        cases = map string_of_int (1 upto len) ~~ map inner_case cases};
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   147
  in
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   148
    if len = 0 then NONE
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   149
    else if len = 1 then SOME (common_case (hd cases))
19046
bc5c6c9b114e removed distinct, renamed gen_distinct to distinct;
wenzelm
parents: 19012
diff changeset
   150
    else if is_none case_outline orelse length (distinct (op =) (map fst cases)) > 1 then NONE
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   151
    else SOME (nested_case (hd cases))
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   152
  end;
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   153
34916
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   154
fun make rule_struct (thy, prop) cases =
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   155
  let
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   156
    val n = length cases;
21576
8c11b1ce2f05 simplified Logic.count_prems;
wenzelm
parents: 21395
diff changeset
   157
    val nprems = Logic.count_prems prop;
53380
08f3491c50bf cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents: 46219
diff changeset
   158
    fun add_case ((name, hyp_names), concls) (cs, i) =
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   159
      ((case try (fn () =>
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   160
          (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   161
        NONE => (name, NONE)
53380
08f3491c50bf cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents: 46219
diff changeset
   162
      | SOME p => (name, extract_case thy p name hyp_names concls)) :: cs, i - 1);
34058
97fd820dd402 explicit lower bound for index
haftmann
parents: 33957
diff changeset
   163
  in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   164
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   165
in
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   166
34916
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   167
val make_common = make NONE;
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   168
fun make_nested rule_struct = make (SOME rule_struct);
18608
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   169
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   170
fun apply args =
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   171
  let
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   172
    fun appl (Case {fixes, assumes, binds, cases}) =
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   173
      let
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   174
        val assumes' = map (apsnd (map (app args))) assumes;
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   175
        val binds' = map (apsnd (Option.map (app args))) binds;
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   176
        val cases' = map (apsnd appl) cases;
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   177
      in Case {fixes = fixes, assumes = assumes', binds = binds', cases = cases'} end;
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   178
  in appl end;
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   179
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   180
end;
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   181
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   182
9cdcc2a5c8b3 support nested cases;
wenzelm
parents: 18581
diff changeset
   183
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   184
(** tactics with cases **)
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   185
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   186
type cases_tactic = thm -> (cases * thm) Seq.seq;
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   187
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   188
fun CASES cases tac st = Seq.map (pair cases) (tac st);
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   189
fun NO_CASES tac = CASES [] tac;
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   190
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   191
fun SUBGOAL_CASES tac i st =
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   192
  (case try Logic.nth_prem (i, Thm.prop_of st) of
56231
b98813774a63 enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents: 55639
diff changeset
   193
    SOME goal => tac (goal, i, st) st
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   194
  | NONE => Seq.empty);
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   195
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   196
fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   197
  st |> tac1 i |> Seq.maps (fn (cases, st') =>
18237
2edb6a1f9c14 consume: proper treatment of defs;
wenzelm
parents: 18229
diff changeset
   198
    CASES cases (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st)) st');
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   199
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   200
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   201
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   202
(** consume facts **)
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   203
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   204
local
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   205
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53380
diff changeset
   206
fun unfold_prems ctxt n defs th =
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   207
  if null defs then th
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53380
diff changeset
   208
  else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite ctxt true defs)) th;
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   209
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53380
diff changeset
   210
fun unfold_prems_concls ctxt defs th =
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   211
  if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   212
  else
22900
f8a7c10e1bd0 moved conversions to structure Conv;
wenzelm
parents: 22568
diff changeset
   213
    Conv.fconv_rule
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 22900
diff changeset
   214
      (Conv.concl_conv ~1 (Conjunction.convs
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53380
diff changeset
   215
        (Conv.prems_conv ~1 (Raw_Simplifier.rewrite ctxt true defs)))) th;
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   216
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   217
in
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   218
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53380
diff changeset
   219
fun consume ctxt defs facts ((xx, n), th) =
18237
2edb6a1f9c14 consume: proper treatment of defs;
wenzelm
parents: 18229
diff changeset
   220
  let val m = Int.min (length facts, n) in
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   221
    th
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53380
diff changeset
   222
    |> unfold_prems ctxt n defs
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53380
diff changeset
   223
    |> unfold_prems_concls ctxt defs
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
   224
    |> Drule.multi_resolve (take m facts)
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
   225
    |> Seq.map (pair (xx, (n - m, drop m facts)))
18237
2edb6a1f9c14 consume: proper treatment of defs;
wenzelm
parents: 18229
diff changeset
   226
  end;
10811
98f52cb93d93 support ?case binding;
wenzelm
parents: 10530
diff changeset
   227
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   228
end;
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   229
10811
98f52cb93d93 support ?case binding;
wenzelm
parents: 10530
diff changeset
   230
val consumes_tagN = "consumes";
98f52cb93d93 support ?case binding;
wenzelm
parents: 10530
diff changeset
   231
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   232
fun lookup_consumes th =
33303
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   233
  (case AList.lookup (op =) (Thm.get_tags th) consumes_tagN of
23657
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   234
    NONE => NONE
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   235
  | SOME s =>
55639
e4e8cbd9d780 tuned whitespace;
wenzelm
parents: 54742
diff changeset
   236
      (case Lexicon.read_nat s of
e4e8cbd9d780 tuned whitespace;
wenzelm
parents: 54742
diff changeset
   237
        SOME n => SOME n
23657
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   238
      | _ => raise THM ("Malformed 'consumes' tag of theorem", 0, [th])));
10530
df079a585e6d added consumes, consumes_default;
wenzelm
parents: 10407
diff changeset
   239
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   240
fun get_consumes th = the_default 0 (lookup_consumes th);
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   241
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   242
fun put_consumes NONE th = th
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   243
  | put_consumes (SOME n) th = th
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 26923
diff changeset
   244
      |> Thm.untag_rule consumes_tagN
33303
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   245
      |> Thm.tag_rule (consumes_tagN, string_of_int (if n < 0 then Thm.nprems_of th + n else n));
10530
df079a585e6d added consumes, consumes_default;
wenzelm
parents: 10407
diff changeset
   246
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   247
fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   248
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 45328
diff changeset
   249
fun default_consumes n th =
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 45328
diff changeset
   250
  if is_some (lookup_consumes th) then th else put_consumes (SOME n) th;
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 45328
diff changeset
   251
12761
b0c39f9837af save: be slightly more about absent tags;
wenzelm
parents: 12166
diff changeset
   252
val save_consumes = put_consumes o lookup_consumes;
b0c39f9837af save: be slightly more about absent tags;
wenzelm
parents: 12166
diff changeset
   253
45525
59561859c452 tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents: 45375
diff changeset
   254
fun consumes n = Thm.mixed_attribute (apsnd (put_consumes (SOME n)));
21395
f34ac19659ae moved some fundamental concepts to General/basics.ML;
wenzelm
parents: 20289
diff changeset
   255
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
   256
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   257
34986
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   258
(** equality constraints **)
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   259
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   260
val constraints_tagN = "constraints";
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   261
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   262
fun lookup_constraints th =
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   263
  (case AList.lookup (op =) (Thm.get_tags th) constraints_tagN of
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   264
    NONE => NONE
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   265
  | SOME s =>
55639
e4e8cbd9d780 tuned whitespace;
wenzelm
parents: 54742
diff changeset
   266
      (case Lexicon.read_nat s of
e4e8cbd9d780 tuned whitespace;
wenzelm
parents: 54742
diff changeset
   267
        SOME n => SOME n
34986
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   268
      | _ => raise THM ("Malformed 'constraints' tag of theorem", 0, [th])));
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   269
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   270
fun get_constraints th = the_default 0 (lookup_constraints th);
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   271
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   272
fun put_constraints NONE th = th
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   273
  | put_constraints (SOME n) th = th
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   274
      |> Thm.untag_rule constraints_tagN
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   275
      |> Thm.tag_rule (constraints_tagN, string_of_int (if n < 0 then 0 else n));
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   276
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   277
val save_constraints = put_constraints o lookup_constraints;
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   278
45525
59561859c452 tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents: 45375
diff changeset
   279
fun constraints n = Thm.mixed_attribute (apsnd (put_constraints (SOME n)));
34986
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   280
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   281
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   282
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   283
(** case names **)
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   284
23657
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   285
val implode_args = space_implode ";";
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   286
val explode_args = space_explode ";";
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   287
18237
2edb6a1f9c14 consume: proper treatment of defs;
wenzelm
parents: 18229
diff changeset
   288
val case_names_tagN = "case_names";
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
   289
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   290
fun add_case_names NONE = I
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   291
  | add_case_names (SOME names) =
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 26923
diff changeset
   292
      Thm.untag_rule case_names_tagN
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 26923
diff changeset
   293
      #> Thm.tag_rule (case_names_tagN, implode_args names);
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
   294
23657
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   295
fun lookup_case_names th =
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   296
  AList.lookup (op =) (Thm.get_tags th) case_names_tagN
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   297
  |> Option.map explode_args;
10530
df079a585e6d added consumes, consumes_default;
wenzelm
parents: 10407
diff changeset
   298
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   299
val save_case_names = add_case_names o lookup_case_names;
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   300
val name = add_case_names o SOME;
45525
59561859c452 tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents: 45375
diff changeset
   301
fun case_names cs = Thm.mixed_attribute (apsnd (name cs));
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 45328
diff changeset
   302
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
   303
10530
df079a585e6d added consumes, consumes_default;
wenzelm
parents: 10407
diff changeset
   304
44045
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   305
(** hyp names **)
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   306
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   307
val implode_hyps = implode_args o map (suffix "," o space_implode ",");
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   308
val explode_hyps = map (space_explode "," o unsuffix ",") o explode_args;
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   309
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   310
val cases_hyp_names_tagN = "cases_hyp_names";
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   311
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   312
fun add_cases_hyp_names NONE = I
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   313
  | add_cases_hyp_names (SOME namess) =
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   314
      Thm.untag_rule cases_hyp_names_tagN
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   315
      #> Thm.tag_rule (cases_hyp_names_tagN, implode_hyps namess);
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   316
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   317
fun lookup_cases_hyp_names th =
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   318
  AList.lookup (op =) (Thm.get_tags th) cases_hyp_names_tagN
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   319
  |> Option.map explode_hyps;
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   320
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   321
val save_cases_hyp_names = add_cases_hyp_names o lookup_cases_hyp_names;
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 45328
diff changeset
   322
fun cases_hyp_names cs hs =
45525
59561859c452 tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents: 45375
diff changeset
   323
  Thm.mixed_attribute (apsnd (name cs #> add_cases_hyp_names (SOME hs)));
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 45328
diff changeset
   324
44045
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   325
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   326
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   327
(** case conclusions **)
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   328
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   329
val case_concl_tagN = "case_conclusion";
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   330
23657
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   331
fun get_case_concl name (a, b) =
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   332
  if a = case_concl_tagN then
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   333
    (case explode_args b of c :: cs => if c = name then SOME cs else NONE)
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   334
  else NONE;
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   335
21646
c07b5b0e8492 thm/prf: separate official name vs. additional tags;
wenzelm
parents: 21576
diff changeset
   336
fun add_case_concl (name, cs) = Thm.map_tags (fn tags =>
23657
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   337
  filter_out (is_some o get_case_concl name) tags @
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   338
    [(case_concl_tagN, implode_args (name :: cs))]);
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   339
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   340
fun get_case_concls th name =
23657
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   341
  these (get_first (get_case_concl name) (Thm.get_tags th));
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   342
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   343
fun save_case_concls th =
21646
c07b5b0e8492 thm/prf: separate official name vs. additional tags;
wenzelm
parents: 21576
diff changeset
   344
  let val concls = Thm.get_tags th |> map_filter
23657
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   345
    (fn (a, b) =>
55639
e4e8cbd9d780 tuned whitespace;
wenzelm
parents: 54742
diff changeset
   346
      if a = case_concl_tagN
e4e8cbd9d780 tuned whitespace;
wenzelm
parents: 54742
diff changeset
   347
      then (case explode_args b of c :: cs => SOME (c, cs) | _ => NONE)
23657
2332c79f4dc8 thm tag: Markup.property list;
wenzelm
parents: 23584
diff changeset
   348
      else NONE)
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   349
  in fold add_case_concl concls end;
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   350
45525
59561859c452 tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents: 45375
diff changeset
   351
fun case_conclusion concl = Thm.mixed_attribute (apsnd (add_case_concl concl));
33303
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   352
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   353
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   354
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   355
(** inner rule **)
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   356
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   357
val inner_rule_tagN = "inner_rule";
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   358
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   359
fun is_inner_rule th =
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   360
  AList.defined (op =) (Thm.get_tags th) inner_rule_tagN;
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   361
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   362
fun put_inner_rule inner =
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   363
  Thm.untag_rule inner_rule_tagN
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   364
  #> inner ? Thm.tag_rule (inner_rule_tagN, "");
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   365
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   366
val save_inner_rule = put_inner_rule o is_inner_rule;
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   367
45525
59561859c452 tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);
wenzelm
parents: 45375
diff changeset
   368
val inner_rule = Thm.mixed_attribute (apsnd (put_inner_rule true));
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   369
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   370
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   371
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   372
(** case declarations **)
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   373
10530
df079a585e6d added consumes, consumes_default;
wenzelm
parents: 10407
diff changeset
   374
(* access hints *)
df079a585e6d added consumes, consumes_default;
wenzelm
parents: 10407
diff changeset
   375
33303
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   376
fun save th =
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   377
  save_consumes th #>
34986
7f7939c9370f Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents: 34916
diff changeset
   378
  save_constraints th #>
33303
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   379
  save_case_names th #>
44045
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   380
  save_cases_hyp_names th #>
33303
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   381
  save_case_concls th #>
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   382
  save_inner_rule th;
12761
b0c39f9837af save: be slightly more about absent tags;
wenzelm
parents: 12166
diff changeset
   383
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   384
fun get th =
12761
b0c39f9837af save: be slightly more about absent tags;
wenzelm
parents: 12166
diff changeset
   385
  let
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   386
    val n = get_consumes th;
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   387
    val cases =
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   388
      (case lookup_case_names th of
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   389
        NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n))
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   390
      | SOME names => map (fn name => (name, get_case_concls th name)) names);
55639
e4e8cbd9d780 tuned whitespace;
wenzelm
parents: 54742
diff changeset
   391
    val cases_hyps =
e4e8cbd9d780 tuned whitespace;
wenzelm
parents: 54742
diff changeset
   392
      (case lookup_cases_hyp_names th of
44045
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   393
        NONE => replicate (length cases) []
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   394
      | SOME names => names);
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   395
    fun regroup ((name,concls),hyps) = ((name,hyps),concls)
2814ff2a6e3e infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
nipkow
parents: 42496
diff changeset
   396
  in (map regroup (cases ~~ cases_hyps), n) end;
10530
df079a585e6d added consumes, consumes_default;
wenzelm
parents: 10407
diff changeset
   397
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
   398
8427
wenzelm
parents: 8400
diff changeset
   399
(* params *)
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
   400
18229
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   401
fun rename_params xss th =
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   402
  th
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   403
  |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
e5a624483a23 added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
wenzelm
parents: 18188
diff changeset
   404
  |> save th;
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
   405
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18608
diff changeset
   406
fun params xss = Thm.rule_attribute (K (rename_params xss));
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
   407
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   408
34916
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   409
(* internalize parameter names *)
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   410
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   411
fun internalize_params rule =
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   412
  let
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   413
    fun rename prem =
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   414
      let val xs =
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   415
        map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
45328
e5b33eecbf6e tuned signature;
wenzelm
parents: 44045
diff changeset
   416
      in Logic.list_rename_params xs prem end;
34916
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   417
    fun rename_prems prop =
36354
bbd742107f56 eliminanated some unreferenced identifiers;
wenzelm
parents: 35625
diff changeset
   418
      let val (As, C) = Logic.strip_horn prop
34916
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   419
      in Logic.list_implies (map rename As, C) end;
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   420
  in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   421
f625d8d6fcf3 Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents: 34058
diff changeset
   422
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   423
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   424
(** mutual_rule **)
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   425
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   426
local
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   427
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   428
fun equal_cterms ts us =
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 34986
diff changeset
   429
  is_equal (list_ord (Term_Ord.fast_term_ord o pairself Thm.term_of) (ts, us));
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   430
19917
8b4869928f72 mutual_rule: proper context;
wenzelm
parents: 19482
diff changeset
   431
fun prep_rule n th =
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   432
  let
19917
8b4869928f72 mutual_rule: proper context;
wenzelm
parents: 19482
diff changeset
   433
    val th' = Thm.permute_prems 0 n th;
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
   434
    val prems = take (Thm.nprems_of th' - n) (Drule.cprems_of th');
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   435
    val th'' = Drule.implies_elim_list th' (map Thm.assume prems);
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   436
  in (prems, (n, th'')) end;
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   437
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   438
in
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   439
19917
8b4869928f72 mutual_rule: proper context;
wenzelm
parents: 19482
diff changeset
   440
fun mutual_rule _ [] = NONE
8b4869928f72 mutual_rule: proper context;
wenzelm
parents: 19482
diff changeset
   441
  | mutual_rule _ [th] = SOME ([0], th)
8b4869928f72 mutual_rule: proper context;
wenzelm
parents: 19482
diff changeset
   442
  | mutual_rule ctxt (ths as th :: _) =
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   443
      let
31794
71af1fd6a5e4 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents: 30364
diff changeset
   444
        val ((_, ths'), ctxt') = Variable.import true ths ctxt;
19917
8b4869928f72 mutual_rule: proper context;
wenzelm
parents: 19482
diff changeset
   445
        val rules as (prems, _) :: _ = map (prep_rule (get_consumes th)) ths';
8b4869928f72 mutual_rule: proper context;
wenzelm
parents: 19482
diff changeset
   446
        val (ns, rls) = split_list (map #2 rules);
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   447
      in
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   448
        if not (forall (equal_cterms prems o #1) rules) then NONE
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   449
        else
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   450
          SOME (ns,
19917
8b4869928f72 mutual_rule: proper context;
wenzelm
parents: 19482
diff changeset
   451
            rls
23418
c195f6f13769 balanced conjunctions;
wenzelm
parents: 22900
diff changeset
   452
            |> Conjunction.intr_balanced
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   453
            |> Drule.implies_intr_list prems
19917
8b4869928f72 mutual_rule: proper context;
wenzelm
parents: 19482
diff changeset
   454
            |> singleton (Variable.export ctxt' ctxt)
8b4869928f72 mutual_rule: proper context;
wenzelm
parents: 19482
diff changeset
   455
            |> save th
18477
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   456
            |> put_consumes (SOME 0))
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   457
      end;
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   458
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   459
end;
bf2a02c82a55 consume: expand defs in prems of concls;
wenzelm
parents: 18375
diff changeset
   460
19917
8b4869928f72 mutual_rule: proper context;
wenzelm
parents: 19482
diff changeset
   461
fun strict_mutual_rule ctxt ths =
8b4869928f72 mutual_rule: proper context;
wenzelm
parents: 19482
diff changeset
   462
  (case mutual_rule ctxt ths of
18581
6538fdcc98dc added strict_mutual_rule;
wenzelm
parents: 18477
diff changeset
   463
    NONE => error "Failed to join given rules into one mutual rule"
6538fdcc98dc added strict_mutual_rule;
wenzelm
parents: 18477
diff changeset
   464
  | SOME res => res);
6538fdcc98dc added strict_mutual_rule;
wenzelm
parents: 18477
diff changeset
   465
8364
0eb9ee70c8f8 added Isar/rule_cases.ML;
wenzelm
parents:
diff changeset
   466
end;
17113
3b67c1809e1c added NO_CASES;
wenzelm
parents: 16390
diff changeset
   467
33368
b1cf34f1855c modernized structure Rule_Cases;
wenzelm
parents: 33303
diff changeset
   468
structure Basic_Rule_Cases: BASIC_RULE_CASES = Rule_Cases;
33303
1e1210f31207 separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;
wenzelm
parents: 31794
diff changeset
   469
open Basic_Rule_Cases;