src/HOL/Nominal/nominal_induct.ML
changeset 18299 af72dfc4b9f9
parent 18297 116fe71fad51
child 18311 b83b00cbaecf
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Wed Nov 30 15:03:15 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Wed Nov 30 15:24:32 2005 +0100
     1.3 @@ -48,12 +48,24 @@
     1.4      |> Drule.cterm_instantiate (map (pairself (Thm.cterm_of thy)) subst)
     1.5    end;
     1.6  
     1.7 -fun rename_params_prems xs rule =
     1.8 +fun rename_params_rule internal xs rule =
     1.9    let
    1.10 -    val cert = Thm.cterm_of (Thm.theory_of_thm rule);
    1.11 -    val (As, C) = Logic.strip_horn (Thm.prop_of rule);
    1.12 -    val prop = Logic.list_implies (map (curry Logic.list_rename_params xs) As, C);
    1.13 -  in Thm.equal_elim (Thm.reflexive (cert prop)) rule end;
    1.14 +    val tune =
    1.15 +      if internal then Syntax.internal
    1.16 +      else fn x => the_default x (try Syntax.dest_internal x);
    1.17 +    val n = length xs;
    1.18 +    fun rename prem =
    1.19 +      let
    1.20 +        val ps = Logic.strip_params prem;
    1.21 +        val p = length ps;
    1.22 +        val ys =
    1.23 +          if p < n then []
    1.24 +          else map (tune o #1) (Library.take (p - n, ps)) @ xs;
    1.25 +      in Logic.list_rename_params (ys, prem) end;
    1.26 +    fun rename_prems prop =
    1.27 +      let val (As, C) = Logic.strip_horn (Thm.prop_of rule)
    1.28 +      in Logic.list_implies (map rename As, C) end;
    1.29 +  in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
    1.30  
    1.31  
    1.32  (* nominal_induct_tac *)
    1.33 @@ -68,8 +80,8 @@
    1.34  
    1.35      val finish_rule =
    1.36        split_all_tuples
    1.37 -      #> rename_params_prems (map (ProofContext.revert_skolem defs_ctxt o #1) fresh);
    1.38 -    fun rule_cases r = RuleCases.make false (SOME (Thm.prop_of r)) (InductMethod.rulified_term r);
    1.39 +      #> rename_params_rule true (map (ProofContext.revert_skolem defs_ctxt o #1) fresh);
    1.40 +    fun rule_cases r = RuleCases.make true (SOME (Thm.prop_of r)) (InductMethod.rulified_term r);
    1.41    in
    1.42      (fn i => fn st =>
    1.43        rule
    1.44 @@ -84,7 +96,7 @@
    1.45              InductMethod.guess_instance (finish_rule r) i st'
    1.46              |> Seq.maps (fn r' =>
    1.47                CASES (rule_cases r' cases)
    1.48 -                (Tactic.rtac r' i THEN
    1.49 +                (Tactic.rtac (rename_params_rule false [] r') i THEN
    1.50                    PRIMSEQ (ProofContext.exports defs_ctxt ctxt)) st'))))
    1.51      THEN_ALL_NEW_CASES InductMethod.rulify_tac
    1.52    end;