src/HOL/Nominal/nominal_induct.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45328 e5b33eecbf6e
child 51717 9e7d1c139569
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30092
9c3b1c136d1f Added lemmas for normalizing freshness results involving fresh_star.
berghofe
parents: 29581
diff changeset
     1
(*  Author:     Christian Urban and Makarius
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
     2
18288
feb79a6b274b proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents: 18283
diff changeset
     3
The nominal induct proof method.
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
     4
*)
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
     5
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
     6
structure NominalInduct:
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
     7
sig
34907
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
     8
  val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
18583
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
     9
    (string * typ) list -> (string * typ) list list -> thm list ->
33368
b1cf34f1855c modernized structure Rule_Cases;
wenzelm
parents: 32952
diff changeset
    10
    thm list -> int -> Rule_Cases.cases_tactic
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    11
  val nominal_induct_method: (Proof.context -> Proof.method) context_parser
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
    12
end =
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
    13
struct
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
    14
18288
feb79a6b274b proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents: 18283
diff changeset
    15
(* proper tuples -- nested left *)
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
    16
18288
feb79a6b274b proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents: 18283
diff changeset
    17
fun tupleT Ts = HOLogic.unitT |> fold (fn T => fn U => HOLogic.mk_prodT (U, T)) Ts;
feb79a6b274b proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents: 18283
diff changeset
    18
fun tuple ts = HOLogic.unit |> fold (fn t => fn u => HOLogic.mk_prod (u, t)) ts;
feb79a6b274b proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents: 18283
diff changeset
    19
feb79a6b274b proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents: 18283
diff changeset
    20
fun tuple_fun Ts (xi, T) =
feb79a6b274b proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents: 18283
diff changeset
    21
  Library.funpow (length Ts) HOLogic.mk_split
feb79a6b274b proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents: 18283
diff changeset
    22
    (Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T));
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
    23
18288
feb79a6b274b proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents: 18283
diff changeset
    24
val split_all_tuples =
feb79a6b274b proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents: 18283
diff changeset
    25
  Simplifier.full_simplify (HOL_basic_ss addsimps
37137
bac3d00a910a dropped legacy theorem bindings
haftmann
parents: 36960
diff changeset
    26
    [@{thm split_conv}, @{thm split_paired_all}, @{thm unit_all_eq1}, @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @
30092
9c3b1c136d1f Added lemmas for normalizing freshness results involving fresh_star.
berghofe
parents: 29581
diff changeset
    27
    @{thms fresh_star_unit_elim} @ @{thms fresh_star_prod_elim});
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
    28
18288
feb79a6b274b proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents: 18283
diff changeset
    29
18297
116fe71fad51 fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents: 18288
diff changeset
    30
(* prepare rule *)
18288
feb79a6b274b proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents: 18283
diff changeset
    31
19903
158ea5884966 RuleCases.mutual_rule: ctxt;
wenzelm
parents: 19115
diff changeset
    32
fun inst_mutual_rule ctxt insts avoiding rules =
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
    33
  let
33368
b1cf34f1855c modernized structure Rule_Cases;
wenzelm
parents: 32952
diff changeset
    34
    val (nconcls, joined_rule) = Rule_Cases.strict_mutual_rule ctxt rules;
22072
aabbf8c4de80 added capabilities to handle mutual inductions
urbanc
parents: 21879
diff changeset
    35
    val concls = Logic.dest_conjunctions (Thm.concl_of joined_rule);
33368
b1cf34f1855c modernized structure Rule_Cases;
wenzelm
parents: 32952
diff changeset
    36
    val (cases, consumes) = Rule_Cases.get joined_rule;
18583
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
    37
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
    38
    val l = length rules;
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
    39
    val _ =
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
    40
      if length insts = l then ()
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
    41
      else error ("Bad number of instantiations for " ^ string_of_int l ^ " rules");
18288
feb79a6b274b proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents: 18283
diff changeset
    42
22072
aabbf8c4de80 added capabilities to handle mutual inductions
urbanc
parents: 21879
diff changeset
    43
    fun subst inst concl =
18583
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
    44
      let
24830
a7b3ab44d993 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents: 23591
diff changeset
    45
        val vars = Induct.vars_of concl;
18583
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
    46
        val m = length vars and n = length inst;
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
    47
        val _ = if m >= n + 2 then () else error "Too few variables in conclusion of rule";
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
    48
        val P :: x :: ys = vars;
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
    49
        val zs = drop (m - n - 2) ys;
18583
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
    50
      in
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
    51
        (P, tuple_fun (map #2 avoiding) (Term.dest_Var P)) ::
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
    52
        (x, tuple (map Free avoiding)) ::
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 30549
diff changeset
    53
        map_filter (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst)
18583
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
    54
      end;
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
    55
     val substs =
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 30549
diff changeset
    56
       map2 subst insts concls |> flat |> distinct (op =)
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 37137
diff changeset
    57
       |> map (pairself (Thm.cterm_of (Proof_Context.theory_of ctxt)));
22072
aabbf8c4de80 added capabilities to handle mutual inductions
urbanc
parents: 21879
diff changeset
    58
  in 
aabbf8c4de80 added capabilities to handle mutual inductions
urbanc
parents: 21879
diff changeset
    59
    (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
aabbf8c4de80 added capabilities to handle mutual inductions
urbanc
parents: 21879
diff changeset
    60
  end;
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
    61
18299
af72dfc4b9f9 added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents: 18297
diff changeset
    62
fun rename_params_rule internal xs rule =
18297
116fe71fad51 fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents: 18288
diff changeset
    63
  let
18299
af72dfc4b9f9 added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents: 18297
diff changeset
    64
    val tune =
20072
c4710df2c953 Name.internal;
wenzelm
parents: 19903
diff changeset
    65
      if internal then Name.internal
c4710df2c953 Name.internal;
wenzelm
parents: 19903
diff changeset
    66
      else fn x => the_default x (try Name.dest_internal x);
18299
af72dfc4b9f9 added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents: 18297
diff changeset
    67
    val n = length xs;
af72dfc4b9f9 added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents: 18297
diff changeset
    68
    fun rename prem =
af72dfc4b9f9 added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents: 18297
diff changeset
    69
      let
af72dfc4b9f9 added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents: 18297
diff changeset
    70
        val ps = Logic.strip_params prem;
af72dfc4b9f9 added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents: 18297
diff changeset
    71
        val p = length ps;
af72dfc4b9f9 added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents: 18297
diff changeset
    72
        val ys =
af72dfc4b9f9 added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents: 18297
diff changeset
    73
          if p < n then []
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
    74
          else map (tune o #1) (take (p - n) ps) @ xs;
45328
e5b33eecbf6e tuned signature;
wenzelm
parents: 45132
diff changeset
    75
      in Logic.list_rename_params ys prem end;
18299
af72dfc4b9f9 added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents: 18297
diff changeset
    76
    fun rename_prems prop =
34907
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
    77
      let val (As, C) = Logic.strip_horn prop
18299
af72dfc4b9f9 added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents: 18297
diff changeset
    78
      in Logic.list_implies (map rename As, C) end;
af72dfc4b9f9 added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents: 18297
diff changeset
    79
  in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
18297
116fe71fad51 fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents: 18288
diff changeset
    80
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
    81
18288
feb79a6b274b proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents: 18283
diff changeset
    82
(* nominal_induct_tac *)
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
    83
34907
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
    84
fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts =
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
    85
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 37137
diff changeset
    86
    val thy = Proof_Context.theory_of ctxt;
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
    87
    val cert = Thm.cterm_of thy;
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
    88
24830
a7b3ab44d993 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents: 23591
diff changeset
    89
    val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
34907
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
    90
    val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs;
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
    91
19115
bc8da9b4a81c distinct (op =);
wenzelm
parents: 19036
diff changeset
    92
    val finish_rule =
18297
116fe71fad51 fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents: 18288
diff changeset
    93
      split_all_tuples
26712
e2dcda7b0401 adapted to ProofContext.revert_skolem: extra Name.clean required;
wenzelm
parents: 25985
diff changeset
    94
      #> rename_params_rule true
42488
4638622bcaa1 reorganized fixes as specialized (global) name space;
wenzelm
parents: 42361
diff changeset
    95
        (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding);
34907
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
    96
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
    97
    fun rule_cases ctxt r =
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
    98
      let val r' = if simp then Induct.simplified_rule ctxt r else r
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
    99
      in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end;
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
   100
  in
18297
116fe71fad51 fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents: 18288
diff changeset
   101
    (fn i => fn st =>
18583
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
   102
      rules
19903
158ea5884966 RuleCases.mutual_rule: ctxt;
wenzelm
parents: 19115
diff changeset
   103
      |> inst_mutual_rule ctxt insts avoiding
33368
b1cf34f1855c modernized structure Rule_Cases;
wenzelm
parents: 32952
diff changeset
   104
      |> Rule_Cases.consume (flat defs) facts
18583
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
   105
      |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
   106
        (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
   107
          (CONJUNCTS (ALLGOALS
34907
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   108
            let
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   109
              val adefs = nth_list atomized_defs (j - 1);
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   110
              val frees = fold (Term.add_frees o prop_of) adefs [];
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   111
              val xs = nth_list fixings (j - 1);
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   112
              val k = nth concls (j - 1) + more_consumes
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   113
            in
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   114
              Method.insert_tac (more_facts @ adefs) THEN'
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   115
                (if simp then
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   116
                   Induct.rotate_tac k (length adefs) THEN'
45132
09de0d0de645 tuned signature;
wenzelm
parents: 42488
diff changeset
   117
                   Induct.arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
34907
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   118
                 else
45132
09de0d0de645 tuned signature;
wenzelm
parents: 42488
diff changeset
   119
                   Induct.arbitrary_tac defs_ctxt k xs)
34907
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   120
            end)
24830
a7b3ab44d993 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents: 23591
diff changeset
   121
          THEN' Induct.inner_atomize_tac) j))
a7b3ab44d993 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents: 23591
diff changeset
   122
        THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>
26940
80df961f7900 guess_instance: proper context;
wenzelm
parents: 26712
diff changeset
   123
            Induct.guess_instance ctxt
24830
a7b3ab44d993 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents: 23591
diff changeset
   124
              (finish_rule (Induct.internalize more_consumes rule)) i st'
18583
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
   125
            |> Seq.maps (fn rule' =>
34907
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   126
              CASES (rule_cases ctxt rule' cases)
18583
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
   127
                (Tactic.rtac (rename_params_rule false [] rule') i THEN
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 37137
diff changeset
   128
                  PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
34907
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   129
    THEN_ALL_NEW_CASES
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   130
      ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   131
        else K all_tac)
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   132
       THEN_ALL_NEW Induct.rulify_tac)
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
   133
  end;
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
   134
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
   135
18288
feb79a6b274b proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents: 18283
diff changeset
   136
(* concrete syntax *)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   137
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   138
local
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   139
18583
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
   140
val avoidingN = "avoiding";
20998
714a08286899 To be consistent with "induct", I renamed "fixing" to "arbitrary".
urbanc
parents: 20288
diff changeset
   141
val fixingN = "arbitrary";  (* to be consistent with induct; hopefully this changes again *)
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
   142
val ruleN = "rule";
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   143
34907
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   144
val inst = Scan.lift (Args.$$$ "_") >> K NONE ||
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   145
  Args.term >> (SOME o rpair false) ||
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   146
  Scan.lift (Args.$$$ "(") |-- (Args.term >> (SOME o rpair true)) --|
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   147
    Scan.lift (Args.$$$ ")");
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   148
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
   149
val def_inst =
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27809
diff changeset
   150
  ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
34907
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   151
      -- (Args.term >> rpair false)) >> SOME ||
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
   152
    inst >> Option.map (pair NONE);
18099
e956b04fea22 fixed bug with nominal induct
urbanc
parents: 18052
diff changeset
   153
27370
8e8f96dfaf63 Args.context;
wenzelm
parents: 26940
diff changeset
   154
val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
8e8f96dfaf63 Args.context;
wenzelm
parents: 26940
diff changeset
   155
  error ("Bad free variable: " ^ Syntax.string_of_term ctxt t));
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
   156
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
   157
fun unless_more_args scan = Scan.unless (Scan.lift
18583
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
   158
  ((Args.$$$ avoidingN || Args.$$$ fixingN || Args.$$$ ruleN) -- Args.colon)) scan;
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
   159
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   160
18583
96e1ef2f806f proper handling of simultaneous goals and mutual rules;
wenzelm
parents: 18311
diff changeset
   161
val avoiding = Scan.optional (Scan.lift (Args.$$$ avoidingN -- Args.colon) |--
18297
116fe71fad51 fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents: 18288
diff changeset
   162
  Scan.repeat (unless_more_args free)) [];
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   163
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
   164
val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 34907
diff changeset
   165
  Parse.and_list' (Scan.repeat (unless_more_args free))) [];
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   166
19036
73782d21e855 Adapted to Context.generic syntax.
berghofe
parents: 18610
diff changeset
   167
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   168
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   169
in
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   170
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   171
val nominal_induct_method =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 34907
diff changeset
   172
  Args.mode Induct.no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
34907
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   173
  avoiding -- fixing -- rule_spec) >>
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   174
  (fn (no_simp, (((x, y), z), w)) => fn ctxt =>
30510
4120fc59dd85 unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents: 30092
diff changeset
   175
    RAW_METHOD_CASES (fn facts =>
34907
b0aaec87751c Added infrastructure for simplifying equality constraints.
berghofe
parents: 33957
diff changeset
   176
      HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)));
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   177
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   178
end;
18283
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
   179
f8a49f09a202 reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents: 18265
diff changeset
   180
end;