33 |
33 |
34 lemma "min i (max j k) = max (min k i) (min i (j::nat))" |
34 lemma "min i (max j k) = max (min k i) (min i (j::nat))" |
35 by(arith) |
35 by(arith) |
36 |
36 |
37 text{*Not proved automatically because it involves multiplication:*} |
37 text{*Not proved automatically because it involves multiplication:*} |
38 |
|
39 lemma "n*n = n \<Longrightarrow> n=0 \<or> n=(1::int)" |
38 lemma "n*n = n \<Longrightarrow> n=0 \<or> n=(1::int)" |
40 (*<*)oops(*>*) |
39 (*<*)oops(*>*) |
41 |
40 |
42 |
41 |
43 subsubsection{*Pairs*} |
42 subsubsection{*Pairs*} |
44 |
43 |
45 lemma "fst(x,y) = snd(z,x)" |
44 lemma "fst(x,y) = snd(z,x)" |
46 by auto |
45 by auto |
47 |
|
48 |
46 |
49 |
47 |
50 subsection{*Definitions*} |
48 subsection{*Definitions*} |
51 |
49 |
52 consts xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
50 consts xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
90 |
88 |
91 lemma "rev(rev(xs @ [])) = xs" |
89 lemma "rev(rev(xs @ [])) = xs" |
92 apply (simp del: rev_rev_ident) |
90 apply (simp del: rev_rev_ident) |
93 (*<*)oops(*>*) |
91 (*<*)oops(*>*) |
94 |
92 |
95 subsubsection{*Assumptions*} |
|
96 |
|
97 lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs" |
|
98 by simp |
|
99 |
|
100 lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []" |
|
101 by(simp (no_asm)) |
|
102 |
93 |
103 subsubsection{*Rewriting with Definitions*} |
94 subsubsection{*Rewriting with Definitions*} |
104 |
95 |
105 lemma "xor A (\<not>A)" |
96 lemma "xor A (\<not>A)" |
106 apply(simp only: xor_def) |
97 apply(simp only: xor_def) |
108 done |
99 done |
109 |
100 |
110 |
101 |
111 subsubsection{*Conditional Equations*} |
102 subsubsection{*Conditional Equations*} |
112 |
103 |
113 lemma hd_Cons_tl[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs" |
104 (*<*)thm hd_Cons_tl(*>*) |
114 by(case_tac xs, simp_all) |
105 text{*A pre-proved simplification rule: @{thm hd_Cons_tl[no_vars]}*} |
115 |
106 lemma "hd(xs @ [x]) # tl(xs @ [x]) = xs @ [x]" |
116 lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs" |
|
117 by simp |
107 by simp |
118 |
108 |
119 |
109 |
120 subsubsection{*Automatic Case Splits*} |
110 subsubsection{*Automatic Case Splits*} |
121 |
111 |
122 lemma "\<forall>xs. if xs = [] then A else B" |
112 lemma "\<forall>xs. if xs = [] then A else B" |
123 apply simp |
113 apply simp |
124 (*<*)oops(*>*)text_raw{* \isanewline\isanewline *} |
114 (*<*)oops(*>*) |
125 |
115 text{*Case-expressions are only split on demand.*} |
126 lemma "case xs @ [] of [] \<Rightarrow> P | y#ys \<Rightarrow> Q ys y" |
|
127 apply simp |
|
128 apply(simp split: list.split) |
|
129 (*<*)oops(*>*) |
|
130 |
116 |
131 |
117 |
132 subsubsection{*Arithmetic*} |
118 subsubsection{*Arithmetic*} |
133 |
119 |
134 text{*Is simple enough for the default arithmetic:*} |
120 text{*Only simple arithmetic:*} |
135 lemma "\<lbrakk> \<not> m < n; m < n+(1::nat) \<rbrakk> \<Longrightarrow> m = n" |
121 lemma "\<lbrakk> \<not> m < n; m < n+(1::nat) \<rbrakk> \<Longrightarrow> m = n" |
136 by simp |
122 by simp |
137 |
123 text{*\noindent Complex goals need @{text arith}-method.*} |
138 text{*Contains boolean combinations and needs full arithmetic:*} |
|
139 lemma "\<not> m < n \<and> m < n+(1::nat) \<Longrightarrow> m = n" |
|
140 apply simp |
|
141 by(arith) |
|
142 |
124 |
143 (*<*) |
125 (*<*) |
144 subsubsection{*Tracing*} |
126 subsubsection{*Tracing*} |
145 |
127 |
146 lemma "rev [a] = []" |
128 lemma "rev [a] = []" |