equal
deleted
inserted
replaced
46 "f(x,y) = (if x \<le> y then x else f(x,y+1))" |
46 "f(x,y) = (if x \<le> y then x else f(x,y+1))" |
47 (hints recdef_simp: termi_lem) |
47 (hints recdef_simp: termi_lem) |
48 (*<*)local(*>*) |
48 (*<*)local(*>*) |
49 text{*\noindent |
49 text{*\noindent |
50 This time everything works fine. Now @{thm[source]f.simps} contains precisely |
50 This time everything works fine. Now @{thm[source]f.simps} contains precisely |
51 the stated recursion equation for @{term f}, which has been stored as a |
51 the stated recursion equation for @{text f}, which has been turned into a |
52 simplification rule. Thus we can automatically prove results such as this one: |
52 simplification rule. Thus we can automatically prove results such as this one: |
53 *} |
53 *} |
54 |
54 |
55 theorem "f(1,0) = f(1,1)" |
55 theorem "f(1,0) = f(1,1)" |
56 apply(simp) |
56 apply(simp) |