Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Normalization_by_Evaluation.thy
changeset 82774 2865a6618cba
parent 82444 7a9164068583 
--- a/src/HOL/ex/Normalization_by_Evaluation.thy	Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -26,12 +26,13 @@
  | "add2 (S m) n = S(add2 m n)"
 
 declare add2.simps [code]
+lemma [code]: "add2 n Z = n"
+  by(induct n) auto
+lemma [code]: "add2 n (S m) =  S (add2 n m)"
+  by(induct n) auto
 lemma [code nbe]: "add2 (add2 n m) k = add2 n (add2 m k)"
   by (induct n) auto
-lemma [code]: "add2 n (S m) =  S (add2 n m)"
-  by(induct n) auto
-lemma [code]: "add2 n Z = n"
-  by(induct n) auto
+
 
 lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization
 lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
isabelle