fresh: frees instead of terms, rename corresponding params in rule;
authorwenzelm
Wed Nov 30 14:27:50 2005 +0100 (2005-11-30)
changeset 18297116fe71fad51
parent 18296 3dcc34f18bfa
child 18298 f7899cb24c79
fresh: frees instead of terms, rename corresponding params in rule;
tuned;
src/HOL/Nominal/nominal_induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Wed Nov 30 14:27:09 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Wed Nov 30 14:27:50 2005 +0100
     1.3 @@ -7,7 +7,8 @@
     1.4  structure NominalInduct:
     1.5  sig
     1.6    val nominal_induct_tac: Proof.context -> (string option * term) option list ->
     1.7 -    term list -> (string * typ) list list -> thm -> thm list -> int -> RuleCases.cases_tactic
     1.8 +    (string * typ) list -> (string * typ) list list -> thm ->
     1.9 +    thm list -> int -> RuleCases.cases_tactic
    1.10    val nominal_induct_method: Method.src -> Proof.context -> Method.method
    1.11  end =
    1.12  struct
    1.13 @@ -27,8 +28,9 @@
    1.14      [split_conv, split_paired_all, unit_all_eq1, thm "fresh_unit_elim", thm "fresh_prod_elim"]);
    1.15  
    1.16  
    1.17 -(* inst_rule conclusion: ?P fresh_struct ... insts *)
    1.18 +(* prepare rule *)
    1.19  
    1.20 +(*conclusion: ?P fresh_struct ... insts*)
    1.21  fun inst_rule thy insts fresh rule =
    1.22    let
    1.23      val vars = InductAttrib.vars_of (Thm.concl_of rule);
    1.24 @@ -38,15 +40,21 @@
    1.25      val zs = Library.drop (m - n - 2, ys);
    1.26  
    1.27      val subst =
    1.28 -      (P, tuple_fun (map Term.fastype_of fresh) (Term.dest_Var P)) ::
    1.29 -      (x, tuple fresh) ::
    1.30 +      (P, tuple_fun (map #2 fresh) (Term.dest_Var P)) ::
    1.31 +      (x, tuple (map Free fresh)) ::
    1.32        List.mapPartial (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ insts);
    1.33    in
    1.34      rule
    1.35 -    |> Drule.cterm_instantiate (PolyML.print (map (pairself (Thm.cterm_of thy)) subst))
    1.36 -    |> PolyML.print
    1.37 +    |> Drule.cterm_instantiate (map (pairself (Thm.cterm_of thy)) subst)
    1.38    end;
    1.39  
    1.40 +fun rename_params_prems xs rule =
    1.41 +  let
    1.42 +    val cert = Thm.cterm_of (Thm.theory_of_thm rule);
    1.43 +    val (As, C) = Logic.strip_horn (Thm.prop_of rule);
    1.44 +    val prop = Logic.list_implies (map (curry Logic.list_rename_params xs) As, C);
    1.45 +  in Thm.equal_elim (Thm.reflexive (cert prop)) rule end;
    1.46 +
    1.47  
    1.48  (* nominal_induct_tac *)
    1.49  
    1.50 @@ -58,9 +66,12 @@
    1.51      val ((insts, defs), defs_ctxt) = InductMethod.add_defs def_insts ctxt;
    1.52      val atomized_defs = map ObjectLogic.atomize_thm defs;
    1.53  
    1.54 +    val finish_rule =
    1.55 +      split_all_tuples
    1.56 +      #> rename_params_prems (map (ProofContext.revert_skolem defs_ctxt o #1) fresh);
    1.57      fun rule_cases r = RuleCases.make false (SOME (Thm.prop_of r)) (InductMethod.rulified_term r);
    1.58    in
    1.59 -    SUBGOAL_CASES (fn (goal, i) => fn st =>
    1.60 +    (fn i => fn st =>
    1.61        rule
    1.62        |> `RuleCases.get
    1.63        ||> inst_rule thy insts fresh
    1.64 @@ -70,7 +81,7 @@
    1.65              Method.insert_tac (more_facts @ atomized_defs) j
    1.66              THEN InductMethod.fix_tac defs_ctxt k (Library.nth_list fixing (j - 1)) j))
    1.67            THEN' InductMethod.atomize_tac) i st |> Seq.maps (fn st' =>
    1.68 -            InductMethod.guess_instance (split_all_tuples r) i st'
    1.69 +            InductMethod.guess_instance (finish_rule r) i st'
    1.70              |> Seq.maps (fn r' =>
    1.71                CASES (rule_cases r' cases)
    1.72                  (Tactic.rtac r' i THEN
    1.73 @@ -104,7 +115,7 @@
    1.74  val def_insts = Scan.repeat (unless_more_args def_inst);
    1.75  
    1.76  val fresh = Scan.optional (Scan.lift (Args.$$$ freshN -- Args.colon) |--
    1.77 -  Scan.repeat (unless_more_args Args.local_term)) [];
    1.78 +  Scan.repeat (unless_more_args free)) [];
    1.79  
    1.80  val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
    1.81    Args.and_list1 (Scan.repeat (unless_more_args free))) [];