proper handling of mutual rules (esp. for sets);
authorwenzelm
Mon Nov 12 20:23:24 2001 +0100 (2001-11-12)
changeset 121627c74a52da110
parent 12161 ea4fbf26a945
child 12163 04c98351f9af
proper handling of mutual rules (esp. for sets);
src/Provers/induct_method.ML
     1.1 --- a/src/Provers/induct_method.ML	Mon Nov 12 20:22:51 2001 +0100
     1.2 +++ b/src/Provers/induct_method.ML	Mon Nov 12 20:23:24 2001 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4  sig
     1.5    val dest_concls: term -> term list
     1.6    val cases_default: thm
     1.7 +  val local_imp_def: thm
     1.8    val local_impI: thm
     1.9    val conjI: thm
    1.10    val atomize: thm list
    1.11 @@ -149,6 +150,8 @@
    1.12    Tactic.rewrite_goal_tac Data.rulify2 THEN'
    1.13    Tactic.norm_hhf_tac;
    1.14  
    1.15 +val localize_concl = Tactic.simplify false [Thm.symmetric Data.local_imp_def];
    1.16 +
    1.17  
    1.18  (* imp_intr --- limited to atomic prems *)
    1.19  
    1.20 @@ -209,7 +212,7 @@
    1.21        in
    1.22          Unify.smash_unifiers (sign, Envir.empty (#maxidx (Thm.rep_thm rule')),
    1.23            [(Thm.concl_of rule', concl)])
    1.24 -        |> Seq.map (fn env => Thm.instantiate (dest_env sign env) rule')
    1.25 +        |> Seq.map (fn env => Drule.instantiate (dest_env sign env) rule')
    1.26        end
    1.27    end handle Subscript => Seq.empty;
    1.28  
    1.29 @@ -222,7 +225,7 @@
    1.30    ruleq |> Seq.map (fn (rule, (cases, k, more_facts)) => st
    1.31      |> (Method.insert_tac more_facts THEN' atomize_tac) i
    1.32      |> Seq.map (fn st' => divinate_inst (internalize k rule) i st' |> Seq.map (fn rule' =>
    1.33 -          st' |> Tactic.rtac rule' i |> Seq.map (rpair (make (rulify rule') cases))) |> Seq.flat)
    1.34 +          (PolyML.print st') |> Tactic.rtac (PolyML.print rule') i |> Seq.map (rpair (make (rulify rule') cases))) |> Seq.flat)
    1.35      |> Seq.flat)
    1.36    |> Seq.flat;
    1.37  
    1.38 @@ -264,9 +267,11 @@
    1.39            let val rules = find_inductS ctxt facts @ find_inductT ctxt insts in
    1.40              if null rules then error "Unable to figure out induct rule" else ();
    1.41              Method.trace ctxt rules;
    1.42 -            Seq.flat (Seq.map (Seq.try inst_rule) (Seq.of_list rules))
    1.43 +            Seq.flat (Seq.map (Seq.APPEND (Seq.try inst_rule,
    1.44 +              Seq.try (inst_rule o localize_concl))) (Seq.of_list rules))
    1.45            end
    1.46 -      | Some r => Seq.single (inst_rule r));
    1.47 +      | Some r => Seq.make (fn () => Some (inst_rule r,
    1.48 +          Seq.make (fn () => Some (inst_rule (localize_concl r), Seq.empty)))));
    1.49  
    1.50      fun prep_rule (th, (cases, n)) =
    1.51        Seq.map (rpair (cases, n - length facts, drop (n, facts)))
    1.52 @@ -276,7 +281,7 @@
    1.53  
    1.54  in
    1.55  
    1.56 -val induct_meth = Method.METHOD_CASES o (HEADGOAL oo induct_tac);
    1.57 +val induct_meth = Method.RAW_METHOD_CASES o (HEADGOAL oo induct_tac);
    1.58  
    1.59  end;
    1.60