src/HOL/Library/Efficient_Nat.thy
 changeset 31954 8db19c99b00a parent 31377 a48f9ef9de15 child 31998 2c7a24f74db9
```     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jul 07 07:56:24 2009 +0200
1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jul 07 17:37:00 2009 +0200
1.3 @@ -105,15 +105,9 @@
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 -  f n = (if n = 0 then g else h (n - 1))"
1.9 -  by (cases n) simp_all
1.10 -
1.11  lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
1.12    f n \<equiv> if n = 0 then g else h (n - 1)"
1.13 -  by (rule eq_reflection, rule Suc_if_eq')
1.14 -    (rule meta_eq_to_obj_eq, assumption,
1.15 -     rule meta_eq_to_obj_eq, assumption)
1.16 +  by (rule eq_reflection) (cases n, simp_all)
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 @@ -129,14 +123,14 @@
1.21  setup {*
1.22  let
1.23
1.24 -fun gen_remove_suc Suc_if_eq dest_judgement thy thms =
1.25 +fun remove_suc thy thms =
1.26    let
1.27      val vname = Name.variant (map fst
1.28        (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n";
1.29      val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
1.30      fun lhs_of th = snd (Thm.dest_comb
1.31 -      (fst (Thm.dest_comb (dest_judgement (cprop_of th)))));
1.32 -    fun rhs_of th = snd (Thm.dest_comb (dest_judgement (cprop_of th)));
1.33 +      (fst (Thm.dest_comb (cprop_of th))));
1.34 +    fun rhs_of th = snd (Thm.dest_comb (cprop_of th));
1.35      fun find_vars ct = (case term_of ct of
1.36          (Const (@{const_name Suc}, _) \$ Var _) => [(cv, snd (Thm.dest_comb ct))]
1.37        | _ \$ _ =>
1.38 @@ -156,7 +150,7 @@
1.39               (Drule.instantiate'
1.40                 [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
1.41                   SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
1.42 -               Suc_if_eq)) (Thm.forall_intr cv' th)
1.43 +               @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
1.44        in
1.45          case map_filter (fn th'' =>
1.46              SOME (th'', singleton
1.47 @@ -169,21 +163,19 @@
1.48        end
1.49    in get_first mk_thms eqs end;
1.50
1.51 -fun gen_eqn_suc_preproc Suc_if_eq dest_judgement dest_lhs thy thms =
1.52 +fun eqn_suc_preproc thy thms =
1.53    let
1.54 -    val dest = dest_lhs o prop_of;
1.55 +    val dest = fst o Logic.dest_equals o prop_of;
1.56      val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
1.57    in
1.58      if forall (can dest) thms andalso exists (contains_suc o dest) thms
1.59 -      then perhaps_loop (gen_remove_suc Suc_if_eq dest_judgement thy) thms
1.60 +      then perhaps_loop (remove_suc thy) thms
1.61         else NONE
1.62    end;
1.63
1.64 -val eqn_suc_preproc = Code_Preproc.simple_functrans (gen_eqn_suc_preproc
1.65 -  @{thm Suc_if_eq} I (fst o Logic.dest_equals));
1.66 +val eqn_suc_preproc1 = Code_Preproc.simple_functrans eqn_suc_preproc;
1.67
1.68 -fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc
1.69 -  @{thm Suc_if_eq'} (snd o Thm.dest_comb) (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) thy thms
1.70 +fun eqn_suc_preproc2 thy thms = eqn_suc_preproc thy thms
1.71    |> the_default thms;
1.72
1.73  fun remove_suc_clause thy thms =
1.74 @@ -227,9 +219,9 @@
1.75    end;
1.76  in
1.77