src/HOL/Nominal/nominal_induct.ML
changeset 24830 a7b3ab44d993
parent 23591 d32a85385e17
child 24920 2a45e400fdad
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Thu Oct 04 14:42:11 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Thu Oct 04 14:42:47 2007 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4  
     1.5      fun subst inst concl =
     1.6        let
     1.7 -        val vars = InductAttrib.vars_of concl;
     1.8 +        val vars = Induct.vars_of concl;
     1.9          val m = length vars and n = length inst;
    1.10          val _ = if m >= n + 2 then () else error "Too few variables in conclusion of rule";
    1.11          val P :: x :: ys = vars;
    1.12 @@ -87,13 +87,13 @@
    1.13      val thy = ProofContext.theory_of ctxt;
    1.14      val cert = Thm.cterm_of thy;
    1.15  
    1.16 -    val ((insts, defs), defs_ctxt) = fold_map InductMethod.add_defs def_insts ctxt |>> split_list;
    1.17 +    val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
    1.18      val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
    1.19  
    1.20      val finish_rule =
    1.21        split_all_tuples
    1.22        #> rename_params_rule true (map (ProofContext.revert_skolem defs_ctxt o fst) avoiding);
    1.23 -    fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (InductMethod.rulified_term r);
    1.24 +    fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
    1.25    in
    1.26      (fn i => fn st =>
    1.27        rules
    1.28 @@ -103,18 +103,18 @@
    1.29          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
    1.30            (CONJUNCTS (ALLGOALS
    1.31              (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
    1.32 -              THEN' InductMethod.fix_tac defs_ctxt
    1.33 +              THEN' Induct.fix_tac defs_ctxt
    1.34                  (nth concls (j - 1) + more_consumes)
    1.35                  (nth_list fixings (j - 1))))
    1.36 -          THEN' InductMethod.inner_atomize_tac) j))
    1.37 -        THEN' InductMethod.atomize_tac) i st |> Seq.maps (fn st' =>
    1.38 -            InductMethod.guess_instance
    1.39 -              (finish_rule (InductMethod.internalize more_consumes rule)) i st'
    1.40 +          THEN' Induct.inner_atomize_tac) j))
    1.41 +        THEN' Induct.atomize_tac) i st |> Seq.maps (fn st' =>
    1.42 +            Induct.guess_instance
    1.43 +              (finish_rule (Induct.internalize more_consumes rule)) i st'
    1.44              |> Seq.maps (fn rule' =>
    1.45                CASES (rule_cases rule' cases)
    1.46                  (Tactic.rtac (rename_params_rule false [] rule') i THEN
    1.47                    PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
    1.48 -    THEN_ALL_NEW_CASES InductMethod.rulify_tac
    1.49 +    THEN_ALL_NEW_CASES Induct.rulify_tac
    1.50    end;
    1.51  
    1.52