Added infrastructure for simplifying equality constraints in cases rules.
authorberghofe
Sat Jan 30 16:58:46 2010 +0100 (2010-01-30)
changeset 34987c1e8af37ee75
parent 34986 7f7939c9370f
child 34988 cca208c8d619
Added infrastructure for simplifying equality constraints in cases rules.
src/Tools/induct.ML
     1.1 --- a/src/Tools/induct.ML	Sat Jan 30 16:56:28 2010 +0100
     1.2 +++ b/src/Tools/induct.ML	Sat Jan 30 16:58:46 2010 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4    val atomize: thm list
     1.5    val rulify: thm list
     1.6    val rulify_fallback: thm list
     1.7 +  val equal_def: thm
     1.8    val dest_def: term -> (term * term) option
     1.9    val trivial_tac: int -> tactic
    1.10  end;
    1.11 @@ -69,7 +70,7 @@
    1.12    val rotate_tac: int -> int -> int -> tactic
    1.13    val internalize: int -> thm -> thm
    1.14    val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
    1.15 -  val cases_tac: Proof.context -> term option list list -> thm option ->
    1.16 +  val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
    1.17      thm list -> int -> cases_tactic
    1.18    val get_inductT: Proof.context -> term option list list -> thm list list
    1.19    val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    1.20 @@ -410,6 +411,38 @@
    1.21    | trace_rules ctxt _ rules = Method.trace ctxt rules;
    1.22  
    1.23  
    1.24 +(* mark equality constraints in cases rule *)
    1.25 +
    1.26 +val equal_def' = Thm.symmetric Data.equal_def;
    1.27 +
    1.28 +fun mark_constraints n ctxt = Conv.fconv_rule
    1.29 +  (Conv.prems_conv (~1) (Conv.params_conv ~1 (K (Conv.prems_conv n
    1.30 +     (MetaSimplifier.rewrite false [equal_def']))) ctxt));
    1.31 +
    1.32 +val unmark_constraints = Conv.fconv_rule
    1.33 +  (MetaSimplifier.rewrite true [Data.equal_def]);
    1.34 +
    1.35 +(* simplify *)
    1.36 +
    1.37 +fun simplify_conv' ctxt =
    1.38 +  Simplifier.full_rewrite (Simplifier.context ctxt (#4 (get_local ctxt)));
    1.39 +
    1.40 +fun simplify_conv ctxt ct =
    1.41 +  if exists_subterm (is_some o Data.dest_def) (term_of ct) then
    1.42 +    (Conv.try_conv (rulify_defs_conv ctxt) then_conv simplify_conv' ctxt) ct
    1.43 +  else Conv.all_conv ct;
    1.44 +
    1.45 +fun gen_simplified_rule cv ctxt =
    1.46 +  Conv.fconv_rule (Conv.prems_conv ~1 (cv ctxt));
    1.47 +
    1.48 +val simplified_rule' = gen_simplified_rule simplify_conv';
    1.49 +val simplified_rule = gen_simplified_rule simplify_conv;
    1.50 +
    1.51 +fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt);
    1.52 +
    1.53 +val trivial_tac = Data.trivial_tac;
    1.54 +
    1.55 +
    1.56  
    1.57  (** cases method **)
    1.58  
    1.59 @@ -431,15 +464,17 @@
    1.60  
    1.61  in
    1.62  
    1.63 -fun cases_tac ctxt insts opt_rule facts =
    1.64 +fun cases_tac ctxt simp insts opt_rule facts =
    1.65    let
    1.66      val thy = ProofContext.theory_of ctxt;
    1.67  
    1.68      fun inst_rule r =
    1.69 -      if null insts then `Rule_Cases.get r
    1.70 -      else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
    1.71 -        |> maps (prep_inst ctxt align_left I)
    1.72 -        |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r);
    1.73 +      (if null insts then r
    1.74 +       else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
    1.75 +         |> maps (prep_inst ctxt align_left I)
    1.76 +         |> Drule.cterm_instantiate) r) |>
    1.77 +      (if simp then mark_constraints (Rule_Cases.get_constraints r) ctxt else I) |>
    1.78 +      pair (Rule_Cases.get r);
    1.79  
    1.80      val ruleq =
    1.81        (case opt_rule of
    1.82 @@ -453,9 +488,14 @@
    1.83        ruleq
    1.84        |> Seq.maps (Rule_Cases.consume [] facts)
    1.85        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
    1.86 -        CASES (Rule_Cases.make_common (thy,
    1.87 -            Thm.prop_of (Rule_Cases.internalize_params rule)) cases)
    1.88 -          (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
    1.89 +        let val rule' =
    1.90 +          (if simp then simplified_rule' ctxt #> unmark_constraints else I) rule
    1.91 +        in
    1.92 +          CASES (Rule_Cases.make_common (thy,
    1.93 +              Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
    1.94 +            ((Method.insert_tac more_facts THEN' Tactic.rtac rule' THEN_ALL_NEW
    1.95 +                (if simp then TRY o trivial_tac else K all_tac)) i) st
    1.96 +        end)
    1.97    end;
    1.98  
    1.99  end;
   1.100 @@ -501,22 +541,6 @@
   1.101    (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
   1.102  
   1.103  
   1.104 -(* simplify *)
   1.105 -
   1.106 -fun simplify_conv ctxt ct =
   1.107 -  if exists_subterm (is_some o Data.dest_def) (term_of ct) then
   1.108 -    (Conv.try_conv (rulify_defs_conv ctxt) then_conv
   1.109 -       Simplifier.full_rewrite (Simplifier.context ctxt (#4 (get_local ctxt)))) ct
   1.110 -  else Conv.all_conv ct;
   1.111 -
   1.112 -fun simplified_rule ctxt thm =
   1.113 -  Conv.fconv_rule (Conv.prems_conv ~1 (simplify_conv ctxt)) thm;
   1.114 -
   1.115 -fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt);
   1.116 -
   1.117 -val trivial_tac = Data.trivial_tac;
   1.118 -
   1.119 -
   1.120  (* prepare rule *)
   1.121  
   1.122  fun rule_instance ctxt inst rule =
   1.123 @@ -870,9 +894,11 @@
   1.124  
   1.125  val cases_setup =
   1.126    Method.setup @{binding cases}
   1.127 -    (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >>
   1.128 -      (fn (insts, opt_rule) => fn ctxt =>
   1.129 -        METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts)))))
   1.130 +    (Args.mode no_simpN --
   1.131 +      (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
   1.132 +      (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
   1.133 +        METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
   1.134 +          (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
   1.135      "case analysis on types or predicates/sets";
   1.136  
   1.137  val induct_setup =