src/HOL/Nominal/nominal_induct.ML
changeset 34907 b0aaec87751c
parent 33957 e9afca2118d4
child 36960 01594f816e3a
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Sat Jan 09 23:22:56 2010 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Sun Jan 10 18:01:04 2010 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  structure NominalInduct:
     1.6  sig
     1.7 -  val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
     1.8 +  val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
     1.9      (string * typ) list -> (string * typ) list list -> thm list ->
    1.10      thm list -> int -> Rule_Cases.cases_tactic
    1.11    val nominal_induct_method: (Proof.context -> Proof.method) context_parser
    1.12 @@ -74,26 +74,29 @@
    1.13            else map (tune o #1) (take (p - n) ps) @ xs;
    1.14        in Logic.list_rename_params (ys, prem) end;
    1.15      fun rename_prems prop =
    1.16 -      let val (As, C) = Logic.strip_horn (Thm.prop_of rule)
    1.17 +      let val (As, C) = Logic.strip_horn prop
    1.18        in Logic.list_implies (map rename As, C) end;
    1.19    in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
    1.20  
    1.21  
    1.22  (* nominal_induct_tac *)
    1.23  
    1.24 -fun nominal_induct_tac ctxt def_insts avoiding fixings rules facts =
    1.25 +fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts =
    1.26    let
    1.27      val thy = ProofContext.theory_of ctxt;
    1.28      val cert = Thm.cterm_of thy;
    1.29  
    1.30      val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
    1.31 -    val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
    1.32 +    val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs;
    1.33  
    1.34      val finish_rule =
    1.35        split_all_tuples
    1.36        #> rename_params_rule true
    1.37          (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding);
    1.38 -    fun rule_cases r = Rule_Cases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
    1.39 +
    1.40 +    fun rule_cases ctxt r =
    1.41 +      let val r' = if simp then Induct.simplified_rule ctxt r else r
    1.42 +      in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end;
    1.43    in
    1.44      (fn i => fn st =>
    1.45        rules
    1.46 @@ -102,19 +105,32 @@
    1.47        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
    1.48          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
    1.49            (CONJUNCTS (ALLGOALS
    1.50 -            (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
    1.51 -              THEN' Induct.fix_tac defs_ctxt
    1.52 -                (nth concls (j - 1) + more_consumes)
    1.53 -                (nth_list fixings (j - 1))))
    1.54 +            let
    1.55 +              val adefs = nth_list atomized_defs (j - 1);
    1.56 +              val frees = fold (Term.add_frees o prop_of) adefs [];
    1.57 +              val xs = nth_list fixings (j - 1);
    1.58 +              val k = nth concls (j - 1) + more_consumes
    1.59 +            in
    1.60 +              Method.insert_tac (more_facts @ adefs) THEN'
    1.61 +                (if simp then
    1.62 +                   Induct.rotate_tac k (length adefs) THEN'
    1.63 +                   Induct.fix_tac defs_ctxt k
    1.64 +                     (List.partition (member op = frees) xs |> op @)
    1.65 +                 else
    1.66 +                   Induct.fix_tac defs_ctxt k xs)
    1.67 +            end)
    1.68            THEN' Induct.inner_atomize_tac) j))
    1.69          THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>
    1.70              Induct.guess_instance ctxt
    1.71                (finish_rule (Induct.internalize more_consumes rule)) i st'
    1.72              |> Seq.maps (fn rule' =>
    1.73 -              CASES (rule_cases rule' cases)
    1.74 +              CASES (rule_cases ctxt rule' cases)
    1.75                  (Tactic.rtac (rename_params_rule false [] rule') i THEN
    1.76                    PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
    1.77 -    THEN_ALL_NEW_CASES Induct.rulify_tac
    1.78 +    THEN_ALL_NEW_CASES
    1.79 +      ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
    1.80 +        else K all_tac)
    1.81 +       THEN_ALL_NEW Induct.rulify_tac)
    1.82    end;
    1.83  
    1.84  
    1.85 @@ -128,11 +144,14 @@
    1.86  val fixingN = "arbitrary";  (* to be consistent with induct; hopefully this changes again *)
    1.87  val ruleN = "rule";
    1.88  
    1.89 -val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
    1.90 +val inst = Scan.lift (Args.$$$ "_") >> K NONE ||
    1.91 +  Args.term >> (SOME o rpair false) ||
    1.92 +  Scan.lift (Args.$$$ "(") |-- (Args.term >> (SOME o rpair true)) --|
    1.93 +    Scan.lift (Args.$$$ ")");
    1.94  
    1.95  val def_inst =
    1.96    ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
    1.97 -      -- Args.term) >> SOME ||
    1.98 +      -- (Args.term >> rpair false)) >> SOME ||
    1.99      inst >> Option.map (pair NONE);
   1.100  
   1.101  val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
   1.102 @@ -153,11 +172,11 @@
   1.103  in
   1.104  
   1.105  val nominal_induct_method =
   1.106 -  P.and_list' (Scan.repeat (unless_more_args def_inst)) --
   1.107 -  avoiding -- fixing -- rule_spec >>
   1.108 -  (fn (((x, y), z), w) => fn ctxt =>
   1.109 +  Args.mode Induct.no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
   1.110 +  avoiding -- fixing -- rule_spec) >>
   1.111 +  (fn (no_simp, (((x, y), z), w)) => fn ctxt =>
   1.112      RAW_METHOD_CASES (fn facts =>
   1.113 -      HEADGOAL (nominal_induct_tac ctxt x y z w facts)));
   1.114 +      HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)));
   1.115  
   1.116  end;
   1.117