67 The command \isacom{apply}@{text"(auto)"} instructs Isabelle to try |
67 The command \isacom{apply}@{text"(auto)"} instructs Isabelle to try |
68 and prove all subgoals automatically, essentially by simplifying them. |
68 and prove all subgoals automatically, essentially by simplifying them. |
69 Because both subgoals are easy, Isabelle can do it. |
69 Because both subgoals are easy, Isabelle can do it. |
70 The base case @{prop"add 0 0 = 0"} holds by definition of @{const add}, |
70 The base case @{prop"add 0 0 = 0"} holds by definition of @{const add}, |
71 and the induction step is almost as simple: |
71 and the induction step is almost as simple: |
72 @{text"add\<^raw:~>(Suc m) 0 = Suc(add m 0) = Suc m"} |
72 @{text"add\<^latex>\<open>~\<close>(Suc m) 0 = Suc(add m 0) = Suc m"} |
73 using first the definition of @{const add} and then the induction hypothesis. |
73 using first the definition of @{const add} and then the induction hypothesis. |
74 In summary, both subproofs rely on simplification with function definitions and |
74 In summary, both subproofs rely on simplification with function definitions and |
75 the induction hypothesis. |
75 the induction hypothesis. |
76 As a result of that final \isacom{done}, Isabelle associates the lemma |
76 As a result of that final \isacom{done}, Isabelle associates the lemma |
77 just proved with its name. You can now inspect the lemma with the command |
77 just proved with its name. You can now inspect the lemma with the command |