misc tuning;
authorwenzelm
Thu Jun 24 12:24:35 2010 +0200 (2010-06-24)
changeset 37525a5ac274798fc
parent 37524 a9e38cdbfe07
child 37526 f4016fca4ff9
misc tuning;
src/Tools/induct.ML
     1.1 --- a/src/Tools/induct.ML	Thu Jun 24 12:16:39 2010 +0200
     1.2 +++ b/src/Tools/induct.ML	Thu Jun 24 12:24:35 2010 +0200
     1.3 @@ -118,14 +118,14 @@
     1.4      fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt
     1.5        | conv1 k ctxt =
     1.6            Conv.rewr_conv @{thm swap_params} then_conv
     1.7 -          Conv.forall_conv (conv1 (k-1) o snd) ctxt
     1.8 +          Conv.forall_conv (conv1 (k - 1) o snd) ctxt
     1.9      fun conv2 0 ctxt = conv1 j ctxt
    1.10 -      | conv2 k ctxt = Conv.forall_conv (conv2 (k-1) o snd) ctxt
    1.11 +      | conv2 k ctxt = Conv.forall_conv (conv2 (k - 1) o snd) ctxt
    1.12    in conv2 i ctxt end;
    1.13  
    1.14  fun swap_prems_conv 0 = Conv.all_conv
    1.15    | swap_prems_conv i =
    1.16 -      Conv.implies_concl_conv (swap_prems_conv (i-1)) then_conv
    1.17 +      Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv
    1.18        Conv.rewr_conv Drule.swap_prems_eq
    1.19  
    1.20  fun drop_judgment ctxt = Object_Logic.drop_judgment (ProofContext.theory_of ctxt);
    1.21 @@ -135,35 +135,40 @@
    1.22      val l = length (Logic.strip_params t);
    1.23      val Hs = Logic.strip_assums_hyp t;
    1.24      fun find (i, t) =
    1.25 -      case Induct_Args.dest_def (drop_judgment ctxt t) of
    1.26 +      (case Induct_Args.dest_def (drop_judgment ctxt t) of
    1.27          SOME (Bound j, _) => SOME (i, j)
    1.28        | SOME (_, Bound j) => SOME (i, j)
    1.29 -      | _ => NONE
    1.30 +      | _ => NONE);
    1.31    in
    1.32 -    case get_first find (map_index I Hs) of
    1.33 +    (case get_first find (map_index I Hs) of
    1.34        NONE => NONE
    1.35      | SOME (0, 0) => NONE
    1.36 -    | SOME (i, j) => SOME (i, l-j-1, j)
    1.37 +    | SOME (i, j) => SOME (i, l - j - 1, j))
    1.38    end;
    1.39  
    1.40 -fun mk_swap_rrule ctxt ct = case find_eq ctxt (term_of ct) of
    1.41 +fun mk_swap_rrule ctxt ct =
    1.42 +  (case find_eq ctxt (term_of ct) of
    1.43      NONE => NONE
    1.44 -  | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct);
    1.45 +  | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
    1.46  
    1.47 -val rearrange_eqs_simproc = Simplifier.simproc
    1.48 -  (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
    1.49 -  (fn thy => fn ss => fn t =>
    1.50 -     mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t))
    1.51 +val rearrange_eqs_simproc =
    1.52 +  Simplifier.simproc
    1.53 +    (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
    1.54 +    (fn thy => fn ss => fn t =>
    1.55 +      mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t));
    1.56 +
    1.57  
    1.58  (* rotate k premises to the left by j, skipping over first j premises *)
    1.59  
    1.60  fun rotate_conv 0 j 0 = Conv.all_conv
    1.61 -  | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k-1)
    1.62 -  | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i-1) j k);
    1.63 +  | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k - 1)
    1.64 +  | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i - 1) j k);
    1.65  
    1.66  fun rotate_tac j 0 = K all_tac
    1.67 -  | rotate_tac j k = SUBGOAL (fn (goal, i) => CONVERSION (rotate_conv
    1.68 -      j (length (Logic.strip_assums_hyp goal) - j - k) k) i);
    1.69 +  | rotate_tac j k = SUBGOAL (fn (goal, i) =>
    1.70 +      CONVERSION (rotate_conv
    1.71 +        j (length (Logic.strip_assums_hyp goal) - j - k) k) i);
    1.72 +
    1.73  
    1.74  (* rulify operators around definition *)
    1.75  
    1.76 @@ -278,8 +283,9 @@
    1.77  fun mk_att f g name arg =
    1.78    let val (x, thm) = g arg in (Data.map (f (name, thm)) x, thm) end;
    1.79  
    1.80 -fun del_att which = Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs =>
    1.81 -  fold Item_Net.remove (filter_rules rs th) rs))));
    1.82 +fun del_att which =
    1.83 +  Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs =>
    1.84 +    fold Item_Net.remove (filter_rules rs th) rs))));
    1.85  
    1.86  fun map1 f (x, y, z, s) = (f x, y, z, s);
    1.87  fun map2 f (x, y, z, s) = (x, f y, z, s);
    1.88 @@ -314,8 +320,8 @@
    1.89  
    1.90  fun induct_simp f =
    1.91    Thm.declaration_attribute (fn thm => fn context =>
    1.92 -      (map_simpset
    1.93 -        (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context));
    1.94 +      map_simpset
    1.95 +        (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context);
    1.96  
    1.97  val induct_simp_add = induct_simp (op addsimps);
    1.98  val induct_simp_del = induct_simp (op delsimps);
    1.99 @@ -419,6 +425,7 @@
   1.100  val unmark_constraints = Conv.fconv_rule
   1.101    (MetaSimplifier.rewrite true [Induct_Args.equal_def]);
   1.102  
   1.103 +
   1.104  (* simplify *)
   1.105  
   1.106  fun simplify_conv' ctxt =