added capabilities to handle mutual inductions
authorurbanc
Tue Jan 16 10:25:38 2007 +0100 (2007-01-16)
changeset 22072aabbf8c4de80
parent 22071 ebcfe7c2499d
child 22073 c170dcbe6c9d
added capabilities to handle mutual inductions
src/HOL/Nominal/nominal_induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Tue Jan 16 08:12:09 2007 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Tue Jan 16 10:25:38 2007 +0100
     1.3 @@ -29,23 +29,21 @@
     1.4  
     1.5  (* prepare rule *)
     1.6  
     1.7 -(*conclusions: ?P avoiding_struct ... insts*)
     1.8  fun inst_mutual_rule ctxt insts avoiding rules =
     1.9    let
    1.10 -    val (concls, rule) =
    1.11 -      (case RuleCases.mutual_rule ctxt rules of
    1.12 -        NONE => error "Failed to join given rules into one mutual rule"
    1.13 -      | SOME res => res);
    1.14 -    val (cases, consumes) = RuleCases.get rule;
    1.15 +
    1.16 +    val (nconcls, joined_rule) = RuleCases.strict_mutual_rule ctxt rules;
    1.17 +    val concls = Logic.dest_conjunctions (Thm.concl_of joined_rule);
    1.18 +    val (cases, consumes) = RuleCases.get joined_rule;
    1.19  
    1.20      val l = length rules;
    1.21      val _ =
    1.22        if length insts = l then ()
    1.23        else error ("Bad number of instantiations for " ^ string_of_int l ^ " rules");
    1.24  
    1.25 -    fun subst inst rule =
    1.26 +    fun subst inst concl =
    1.27        let
    1.28 -        val vars = InductAttrib.vars_of (Thm.concl_of rule);
    1.29 +        val vars = InductAttrib.vars_of concl;
    1.30          val m = length vars and n = length inst;
    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 @@ -56,9 +54,11 @@
    1.34          List.mapPartial (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst)
    1.35        end;
    1.36       val substs =
    1.37 -       map2 subst insts rules |> List.concat |> distinct (op =)
    1.38 +       map2 subst insts concls |> List.concat |> distinct (op =)
    1.39         |> map (pairself (Thm.cterm_of (ProofContext.theory_of ctxt)));
    1.40 -  in (((cases, concls), consumes), Drule.cterm_instantiate substs rule) end;
    1.41 +  in 
    1.42 +    (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
    1.43 +  end;
    1.44  
    1.45  fun rename_params_rule internal xs rule =
    1.46    let