src/HOL/Library/Code_Abstract_Nat.thy
changeset 57426 2cd2ccd81f93
parent 56790 f54097170704
child 57427 91f9e4148460
     1.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Sat Jun 28 18:02:33 2014 +0200
     1.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Sat Jun 28 21:09:15 2014 +0200
     1.3 @@ -38,9 +38,11 @@
     1.4    applying the following transformation rule:
     1.5  *}
     1.6  
     1.7 -lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
     1.8 -  f n \<equiv> if n = 0 then g else h (n - 1)"
     1.9 -  by (rule eq_reflection) (cases n, simp_all)
    1.10 +lemma Suc_if_eq:
    1.11 +  assumes "\<And>n. f (Suc n) \<equiv> h n"
    1.12 +  assumes "f 0 \<equiv> g"
    1.13 +  shows "f n \<equiv> if n = 0 then g else h (n - 1)"
    1.14 +  by (rule eq_reflection) (cases n, insert assms, simp_all)
    1.15  
    1.16  text {*
    1.17    The rule above is built into a preprocessor that is plugged into
    1.18 @@ -56,9 +58,8 @@
    1.19      val vname = singleton (Name.variant_list (map fst
    1.20        (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
    1.21      val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
    1.22 -    fun lhs_of th = snd (Thm.dest_comb
    1.23 -      (fst (Thm.dest_comb (cprop_of th))));
    1.24 -    fun rhs_of th = snd (Thm.dest_comb (cprop_of th));
    1.25 +    val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o cprop_of;
    1.26 +    val rhs_of = snd o Thm.dest_comb o cprop_of;
    1.27      fun find_vars ct = (case term_of ct of
    1.28          (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
    1.29        | _ $ _ =>
    1.30 @@ -69,26 +70,26 @@
    1.31          end
    1.32        | _ => []);
    1.33      val eqs = maps
    1.34 -      (fn th => map (pair th) (find_vars (lhs_of th))) thms;
    1.35 -    fun mk_thms (th, (ct, cv')) =
    1.36 +      (fn thm => map (pair thm) (find_vars (lhs_of thm))) thms;
    1.37 +    fun mk_thms (thm, (ct, cv')) =
    1.38        let
    1.39 -        val th' =
    1.40 +        val thm' =
    1.41            Thm.implies_elim
    1.42             (Conv.fconv_rule (Thm.beta_conversion true)
    1.43               (Drule.instantiate'
    1.44                 [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
    1.45 -                 SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv']
    1.46 -               @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
    1.47 +                 SOME (Thm.lambda cv' (rhs_of thm)), NONE, SOME cv']
    1.48 +               @{thm Suc_if_eq})) (Thm.forall_intr cv' thm)
    1.49        in
    1.50 -        case map_filter (fn th'' =>
    1.51 -            SOME (th'', singleton
    1.52 -              (Variable.trade (K (fn [th'''] => [th''' RS th']))
    1.53 -                (Variable.global_thm_context th'')) th'')
    1.54 +        case map_filter (fn thm'' =>
    1.55 +            SOME (thm'', singleton
    1.56 +              (Variable.trade (K (fn [thm'''] => [thm''' RS thm']))
    1.57 +                (Variable.global_thm_context thm'')) thm'')
    1.58            handle THM _ => NONE) thms of
    1.59              [] => NONE
    1.60 -          | thps =>
    1.61 -              let val (ths1, ths2) = split_list thps
    1.62 -              in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
    1.63 +          | thmps =>
    1.64 +              let val (thms1, thms2) = split_list thmps
    1.65 +              in SOME (subtract Thm.eq_thm (thm :: thms1) thms @ thms2) end
    1.66        end
    1.67    in get_first mk_thms eqs end;
    1.68