src/HOL/Nominal/nominal_induct.ML
changeset 18583 96e1ef2f806f
parent 18311 b83b00cbaecf
child 18610 05a5e950d5f1
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Thu Jan 05 17:16:38 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Thu Jan 05 17:16:40 2006 +0100
     1.3 @@ -6,14 +6,13 @@
     1.4  
     1.5  structure NominalInduct:
     1.6  sig
     1.7 -  val nominal_induct_tac: Proof.context -> (string option * term) option list ->
     1.8 -    (string * typ) list -> (string * typ) list list -> thm ->
     1.9 +  val nominal_induct_tac: Proof.context -> (string option * term) option list list ->
    1.10 +    (string * typ) list -> (string * typ) list list -> thm list ->
    1.11      thm list -> int -> RuleCases.cases_tactic
    1.12    val nominal_induct_method: Method.src -> Proof.context -> Method.method
    1.13  end =
    1.14  struct
    1.15  
    1.16 -
    1.17  (* proper tuples -- nested left *)
    1.18  
    1.19  fun tupleT Ts = HOLogic.unitT |> fold (fn T => fn U => HOLogic.mk_prodT (U, T)) Ts;
    1.20 @@ -30,23 +29,36 @@
    1.21  
    1.22  (* prepare rule *)
    1.23  
    1.24 -(*conclusion: ?P fresh_struct ... insts*)
    1.25 -fun inst_rule thy insts fresh rule =
    1.26 +(*conclusions: ?P avoiding_struct ... insts*)
    1.27 +fun inst_mutual_rule thy insts avoiding rules =
    1.28    let
    1.29 -    val vars = InductAttrib.vars_of (Thm.concl_of rule);
    1.30 -    val m = length vars and n = length insts;
    1.31 -    val _ = if m >= n + 2 then () else error "Too few variables in conclusion of rule";
    1.32 -    val P :: x :: ys = vars;
    1.33 -    val zs = Library.drop (m - n - 2, ys);
    1.34 +    val (concls, rule) =
    1.35 +      (case RuleCases.mutual_rule rules of
    1.36 +        NONE => error "Failed to join given rules into one mutual rule"
    1.37 +      | SOME res => res);
    1.38 +    val (cases, consumes) = RuleCases.get rule;
    1.39 +
    1.40 +    val l = length rules;
    1.41 +    val _ =
    1.42 +      if length insts = l then ()
    1.43 +      else error ("Bad number of instantiations for " ^ string_of_int l ^ " rules");
    1.44  
    1.45 -    val subst =
    1.46 -      (P, tuple_fun (map #2 fresh) (Term.dest_Var P)) ::
    1.47 -      (x, tuple (map Free fresh)) ::
    1.48 -      List.mapPartial (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ insts);
    1.49 -  in
    1.50 -    rule
    1.51 -    |> Drule.cterm_instantiate (map (pairself (Thm.cterm_of thy)) subst)
    1.52 -  end;
    1.53 +    fun subst inst rule =
    1.54 +      let
    1.55 +        val vars = InductAttrib.vars_of (Thm.concl_of rule);
    1.56 +        val m = length vars and n = length inst;
    1.57 +        val _ = if m >= n + 2 then () else error "Too few variables in conclusion of rule";
    1.58 +        val P :: x :: ys = vars;
    1.59 +        val zs = Library.drop (m - n - 2, ys);
    1.60 +      in
    1.61 +        (P, tuple_fun (map #2 avoiding) (Term.dest_Var P)) ::
    1.62 +        (x, tuple (map Free avoiding)) ::
    1.63 +        List.mapPartial (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst)
    1.64 +      end;
    1.65 +     val substs =
    1.66 +       map2 subst insts rules |> List.concat |> distinct
    1.67 +       |> map (pairself (Thm.cterm_of thy));
    1.68 +  in (((cases, concls), consumes), Drule.cterm_instantiate substs rule) end;
    1.69  
    1.70  fun rename_params_rule internal xs rule =
    1.71    let
    1.72 @@ -70,33 +82,36 @@
    1.73  
    1.74  (* nominal_induct_tac *)
    1.75  
    1.76 -fun nominal_induct_tac ctxt def_insts fresh fixing rule facts =
    1.77 +fun nominal_induct_tac ctxt def_insts avoiding fixings rules facts =
    1.78    let
    1.79      val thy = ProofContext.theory_of ctxt;
    1.80      val cert = Thm.cterm_of thy;
    1.81  
    1.82 -    val ((insts, defs), defs_ctxt) = InductMethod.add_defs def_insts ctxt;
    1.83 -    val atomized_defs = map ObjectLogic.atomize_thm defs;
    1.84 +    val ((insts, defs), defs_ctxt) = fold_map InductMethod.add_defs def_insts ctxt |>> split_list;
    1.85 +    val atomized_defs = map (map ObjectLogic.atomize_thm) defs;
    1.86  
    1.87 -    val finish_rule =
    1.88 +    val finish_rule = PolyML.print #>
    1.89        split_all_tuples
    1.90 -      #> rename_params_rule true (map (ProofContext.revert_skolem defs_ctxt o #1) fresh);
    1.91 +      #> rename_params_rule true (map (ProofContext.revert_skolem defs_ctxt o fst) avoiding) #> PolyML.print;
    1.92      fun rule_cases r = RuleCases.make true (SOME (Thm.prop_of r)) (InductMethod.rulified_term r);
    1.93    in
    1.94      (fn i => fn st =>
    1.95 -      rule
    1.96 -      |> `RuleCases.get
    1.97 -      ||> inst_rule thy insts fresh
    1.98 -      |> RuleCases.consume defs facts
    1.99 -      |> Seq.maps (fn ((cases, (k, more_facts)), r) =>
   1.100 -        (CONJUNCTS (ALLGOALS (fn j =>
   1.101 -            Method.insert_tac (more_facts @ atomized_defs) j
   1.102 -            THEN InductMethod.fix_tac defs_ctxt k (Library.nth_list fixing (j - 1)) j))
   1.103 -          THEN' InductMethod.atomize_tac) i st |> Seq.maps (fn st' =>
   1.104 -            InductMethod.guess_instance (finish_rule r) i st'
   1.105 -            |> Seq.maps (fn r' =>
   1.106 -              CASES (rule_cases r' cases)
   1.107 -                (Tactic.rtac (rename_params_rule false [] r') i THEN
   1.108 +      rules
   1.109 +      |> inst_mutual_rule thy insts avoiding
   1.110 +      |> RuleCases.consume (List.concat defs) facts
   1.111 +      |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
   1.112 +        (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
   1.113 +          (CONJUNCTS (ALLGOALS
   1.114 +            (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
   1.115 +              THEN' InductMethod.fix_tac defs_ctxt
   1.116 +                (nth concls (j - 1) + more_consumes)
   1.117 +                (nth_list fixings (j - 1))))
   1.118 +          THEN' InductMethod.inner_atomize_tac) j))
   1.119 +        THEN' InductMethod.atomize_tac) i st |> Seq.maps (fn st' =>
   1.120 +            InductMethod.guess_instance (finish_rule (InductMethod.internalize more_consumes rule)) i (PolyML.print st')
   1.121 +            |> Seq.maps (fn rule' =>
   1.122 +              CASES (rule_cases (PolyML.print rule') cases)
   1.123 +                (Tactic.rtac (rename_params_rule false [] rule') i THEN
   1.124                    PRIMSEQ (ProofContext.exports defs_ctxt ctxt)) st'))))
   1.125      THEN_ALL_NEW_CASES InductMethod.rulify_tac
   1.126    end;
   1.127 @@ -106,7 +121,7 @@
   1.128  
   1.129  local
   1.130  
   1.131 -val freshN = "avoiding";
   1.132 +val avoidingN = "avoiding";
   1.133  val fixingN = "fixing";
   1.134  val ruleN = "rule";
   1.135  
   1.136 @@ -121,23 +136,23 @@
   1.137    error ("Bad free variable: " ^ ProofContext.string_of_term ctxt t));
   1.138  
   1.139  fun unless_more_args scan = Scan.unless (Scan.lift
   1.140 -  ((Args.$$$ freshN || Args.$$$ fixingN || Args.$$$ ruleN) -- Args.colon)) scan;
   1.141 +  ((Args.$$$ avoidingN || Args.$$$ fixingN || Args.$$$ ruleN) -- Args.colon)) scan;
   1.142  
   1.143  
   1.144 -val def_insts = Scan.repeat (unless_more_args def_inst);
   1.145 -
   1.146 -val fresh = Scan.optional (Scan.lift (Args.$$$ freshN -- Args.colon) |--
   1.147 +val avoiding = Scan.optional (Scan.lift (Args.$$$ avoidingN -- Args.colon) |--
   1.148    Scan.repeat (unless_more_args free)) [];
   1.149  
   1.150  val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
   1.151 -  Args.and_list1 (Scan.repeat (unless_more_args free))) [];
   1.152 +  Args.and_list (Scan.repeat (unless_more_args free))) [];
   1.153  
   1.154 -val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thm;
   1.155 +val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thmss;
   1.156  
   1.157  in
   1.158  
   1.159  fun nominal_induct_method src =
   1.160 -  Method.syntax (def_insts -- fresh -- fixing -- rule_spec) src
   1.161 +  Method.syntax
   1.162 +   (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
   1.163 +    avoiding -- fixing -- rule_spec) src
   1.164    #> (fn (ctxt, (((x, y), z), w)) =>
   1.165      Method.RAW_METHOD_CASES (fn facts =>
   1.166        HEADGOAL (nominal_induct_tac ctxt x y z w facts)));