equal
deleted
inserted
replaced
2 theory prime_def = Main:; |
2 theory prime_def = Main:; |
3 consts prime :: "nat \\<Rightarrow> bool" |
3 consts prime :: "nat \\<Rightarrow> bool" |
4 (*>*) |
4 (*>*) |
5 (*<*)term(*>*) |
5 (*<*)term(*>*) |
6 |
6 |
7 "prime(p) \\<equiv> 1 < p \\<and> ((m dvd p) \\<longrightarrow> (m=1 \\<or> m=p))"; |
7 "prime(p) \\<equiv> 1 < p \\<and> (m dvd p \\<longrightarrow> (m=1 \\<or> m=p))"; |
8 text{*\noindent\small |
8 text{*\noindent\small |
9 where \isa{dvd} means ``divides''. |
9 where \isa{dvd} means ``divides''. |
10 Isabelle rejects this ``definition'' because of the extra \isa{m} on the |
10 Isabelle rejects this ``definition'' because of the extra \isa{m} on the |
11 right-hand side, which would introduce an inconsistency. (Why?) What you |
11 right-hand side, which would introduce an inconsistency (why?). What you |
12 should have written is |
12 should have written is |
13 *} |
13 *} |
14 (*<*)term(*>*) |
14 (*<*)term(*>*) |
15 "prime(p) \\<equiv> 1 < p \\<and> (\\<forall>m. (m dvd p) \\<longrightarrow> (m=1 \\<or> m=p))" |
15 "prime(p) \\<equiv> 1 < p \\<and> (\\<forall>m. m dvd p \\<longrightarrow> (m=1 \\<or> m=p))" |
16 (*<*) |
16 (*<*) |
17 end |
17 end |
18 (*>*) |
18 (*>*) |