equal
deleted
inserted
replaced
28 by (rule comb_rule) |
28 by (rule comb_rule) |
29 thus t2 |
29 thus t2 |
30 by simp |
30 by simp |
31 qed |
31 qed |
32 |
32 |
33 constdefs |
33 definition Pred :: "nat \<Rightarrow> nat" where |
34 Pred :: "nat \<Rightarrow> nat" |
|
35 "Pred n \<equiv> n - (Suc 0)" |
34 "Pred n \<equiv> n - (Suc 0)" |
36 |
35 |
37 lemma Pred_altdef: "Pred = (SOME PRE. PRE 0 = 0 & (ALL n. PRE (Suc n) = n))" |
36 lemma Pred_altdef: "Pred = (SOME PRE. PRE 0 = 0 & (ALL n. PRE (Suc n) = n))" |
38 apply (rule some_equality[symmetric]) |
37 apply (rule some_equality[symmetric]) |
39 apply (simp add: Pred_def) |
38 apply (simp add: Pred_def) |
82 apply (rule ext)+ |
81 apply (rule ext)+ |
83 apply (induct_tac xa) |
82 apply (induct_tac xa) |
84 apply auto |
83 apply auto |
85 done |
84 done |
86 |
85 |
87 constdefs |
86 definition NUMERAL_BIT0 :: "nat \<Rightarrow> nat" where |
88 NUMERAL_BIT0 :: "nat \<Rightarrow> nat" |
|
89 "NUMERAL_BIT0 n \<equiv> n + n" |
87 "NUMERAL_BIT0 n \<equiv> n + n" |
90 |
88 |
91 lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)" |
89 lemma NUMERAL_BIT1_altdef: "NUMERAL_BIT1 n = Suc (n + n)" |
92 by (simp add: NUMERAL_BIT1_def) |
90 by (simp add: NUMERAL_BIT1_def) |
93 |
91 |