src/HOL/Code_Numeral.thy
changeset 55428 0ab52bf7b5e6
parent 55427 ff54d22fe357
parent 55416 dd7992d4a61a
child 55642 63beb38e9258
     1.1 --- a/src/HOL/Code_Numeral.thy	Wed Feb 12 09:06:04 2014 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Wed Feb 12 10:59:25 2014 +0100
     1.3 @@ -384,7 +384,7 @@
     1.4      by (auto simp add: sgn_if)
     1.5    have aux2: "\<And>q::int. - int_of_integer k = int_of_integer l * q \<longleftrightarrow> int_of_integer k = int_of_integer l * - q" by auto
     1.6    show ?thesis
     1.7 -    by (simp add: prod_eq_iff integer_eq_iff prod_case_beta aux1)
     1.8 +    by (simp add: prod_eq_iff integer_eq_iff case_prod_beta aux1)
     1.9        (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2)
    1.10  qed
    1.11  
    1.12 @@ -475,7 +475,7 @@
    1.13    }
    1.14    note aux = this
    1.15    show ?thesis
    1.16 -    by (auto simp add: num_of_integer_def nat_of_integer_def Let_def prod_case_beta
    1.17 +    by (auto simp add: num_of_integer_def nat_of_integer_def Let_def case_prod_beta
    1.18        not_le integer_eq_iff less_eq_integer_def
    1.19        nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib
    1.20         mult_2 [where 'a=nat] aux add_One)
    1.21 @@ -792,7 +792,7 @@
    1.22    by (rule is_measure_trivial)
    1.23  
    1.24  
    1.25 -subsection {* Inductive represenation of target language naturals *}
    1.26 +subsection {* Inductive representation of target language naturals *}
    1.27  
    1.28  lift_definition Suc :: "natural \<Rightarrow> natural"
    1.29    is Nat.Suc
    1.30 @@ -803,7 +803,7 @@
    1.31  rep_datatype "0::natural" Suc
    1.32    by (transfer, fact nat.induct nat.inject nat.distinct)+
    1.33  
    1.34 -lemma natural_case [case_names nat, cases type: natural]:
    1.35 +lemma natural_cases [case_names nat, cases type: natural]:
    1.36    fixes m :: natural
    1.37    assumes "\<And>n. m = of_nat n \<Longrightarrow> P"
    1.38    shows P
    1.39 @@ -885,7 +885,7 @@
    1.40    by transfer (simp add: fun_eq_iff)
    1.41  
    1.42  lemma [code, code_unfold]:
    1.43 -  "natural_case f g n = (if n = 0 then f else g (n - 1))"
    1.44 +  "case_natural f g n = (if n = 0 then f else g (n - 1))"
    1.45    by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def)
    1.46  
    1.47  declare natural.recs [code del]