1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon Feb 16 19:11:15 2009 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Mon Feb 16 19:11:16 2009 +0100
     1.3 @@ -105,10 +105,16 @@
     1.4    This can be accomplished by applying the following transformation rules:
     1.5  *}
     1.6  
     1.7 -lemma Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
     1.8 +lemma Suc_if_eq': "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
     1.9    f n = (if n = 0 then g else h (n - 1))"
    1.10    by (cases n) simp_all
    1.11  
    1.12 +lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
    1.13 +  f n \<equiv> if n = 0 then g else h (n - 1)"
    1.14 +  by (rule eq_reflection, rule Suc_if_eq')
    1.15 +    (rule meta_eq_to_obj_eq, assumption,
    1.16 +     rule meta_eq_to_obj_eq, assumption)
    1.17 +
    1.18  lemma Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
    1.19    by (cases n) simp_all
    1.20  
    1.21 @@ -123,14 +129,14 @@
    1.22  setup {*
    1.23  let
    1.24  
    1.25 -fun remove_suc thy thms =
    1.26 +fun gen_remove_suc Suc_if_eq dest_judgement thy thms =
    1.27    let
    1.28      val vname = Name.variant (map fst
    1.29 -      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
    1.30 +      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n";
    1.31      val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
    1.32      fun lhs_of th = snd (Thm.dest_comb
    1.33 -      (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
    1.34 -    fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
    1.35 +      (fst (Thm.dest_comb (dest_judgement (cprop_of th)))));
    1.36 +    fun rhs_of th = snd (Thm.dest_comb (dest_judgement (cprop_of th)));
    1.37      fun find_vars ct = (case term_of ct of
    1.38          (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
    1.39        | _ $ _ =>
    1.40 @@ -150,7 +156,7 @@
    1.41               (Drule.instantiate'
    1.42                 [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
    1.43                   SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
    1.44 -               @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
    1.45 +               Suc_if_eq)) (Thm.forall_intr cv' th)
    1.46        in
    1.47          case map_filter (fn th'' =>
    1.48              SOME (th'', singleton
    1.49 @@ -161,20 +167,26 @@
    1.50                let val (ths1, ths2) = split_list thps
    1.51                in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
    1.52        end
    1.53 -  in case get_first mk_thms eqs of
    1.54 -      NONE => thms
    1.55 -    | SOME x => remove_suc thy x
    1.56 +  in get_first mk_thms eqs end;
    1.57 +
    1.58 +fun gen_eqn_suc_preproc Suc_if_eq dest_judgement dest_lhs thy thms =
    1.59 +  let
    1.60 +    val dest = dest_lhs o prop_of;
    1.61 +    val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
    1.62 +  in
    1.63 +    if forall (can dest) thms andalso exists (contains_suc o dest) thms
    1.64 +      then perhaps_loop (gen_remove_suc Suc_if_eq dest_judgement thy) thms
    1.65 +       else NONE
    1.66    end;
    1.67  
    1.68 -fun eqn_suc_preproc thy ths =
    1.69 -  let
    1.70 -    val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
    1.71 -    val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
    1.72 -  in
    1.73 -    if forall (can dest) ths andalso
    1.74 -      exists (contains_suc o dest) ths
    1.75 -    then remove_suc thy ths else ths
    1.76 -  end;
    1.77 +fun eqn_suc_preproc thy = map fst
    1.78 +  #> gen_eqn_suc_preproc
    1.79 +      @{thm Suc_if_eq} I (fst o Logic.dest_equals) thy
    1.80 +  #> (Option.map o map) (Code_Unit.mk_eqn thy);
    1.81 +
    1.82 +fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc
    1.83 +  @{thm Suc_if_eq'} (snd o Thm.dest_comb) (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) thy thms
    1.84 +  |> the_default thms;
    1.85  
    1.86  fun remove_suc_clause thy thms =
    1.87    let
    1.88 @@ -215,27 +227,11 @@
    1.89          (map_filter (try dest) (concl_of th :: prems_of th))) ths
    1.90      then remove_suc_clause thy ths else ths
    1.91    end;
    1.92 -
    1.93 -fun lift f thy eqns1 =
    1.94 -  let
    1.95 -    val eqns2 = burrow_fst Drule.zero_var_indexes_list eqns1;
    1.96 -    val thms3 = try (map fst
    1.97 -      #> map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
    1.98 -      #> f thy
    1.99 -      #> map (fn thm => thm RS @{thm eq_reflection})
   1.100 -      #> map (Conv.fconv_rule Drule.beta_eta_conversion)) eqns2;
   1.101 -    val thms4 = Option.map Drule.zero_var_indexes_list thms3;
   1.102 -  in case thms4
   1.103 -   of NONE => NONE
   1.104 -    | SOME thms4 => if Thm.eq_thms (map fst eqns2, thms4)
   1.105 -        then NONE else SOME (map (apfst (AxClass.overload thy) o Code_Unit.mk_eqn thy) thms4)
   1.106 -  end
   1.107 -
   1.108  in
   1.109  
   1.110 -  Codegen.add_preprocessor eqn_suc_preproc
   1.111 +  Codegen.add_preprocessor eqn_suc_preproc'
   1.112    #> Codegen.add_preprocessor clause_suc_preproc
   1.113 -  #> Code.add_functrans ("eqn_Suc", lift eqn_suc_preproc)
   1.114 +  #> Code.add_functrans ("eqn_Suc", eqn_suc_preproc)
   1.115  
   1.116  end;
   1.117  *}