equal
deleted
inserted
replaced
74 in Buffer.content (trans t Buffer.empty) end\<close> |
74 in Buffer.content (trans t Buffer.empty) end\<close> |
75 |
75 |
76 text \<open> |
76 text \<open> |
77 Here is the string representation of the term @{term "p = (q = p)"}: |
77 Here is the string representation of the term @{term "p = (q = p)"}: |
78 |
78 |
79 @{ML_matchresult |
79 @{ML_matchresult \<open>translate @{term "p = (q = p)"}\<close> |
80 "translate @{term \"p = (q = p)\"}" |
80 \<open>" ( p <=> ( q <=> p ) ) "\<close>} |
81 "\" ( p <=> ( q <=> p ) ) \""} |
|
82 |
81 |
83 Let us check, what the solver returns when given a tautology: |
82 Let us check, what the solver returns when given a tautology: |
84 |
83 |
85 @{ML_matchresult |
84 @{ML_matchresult \<open>IffSolver.decide (translate @{term "p = (q = p) = q"})\<close> |
86 "IffSolver.decide (translate @{term \"p = (q = p) = q\"})" |
85 \<open>true\<close>} |
87 "true"} |
|
88 |
86 |
89 And here is what it returns for a formula which is not valid: |
87 And here is what it returns for a formula which is not valid: |
90 |
88 |
91 @{ML_matchresult |
89 @{ML_matchresult \<open>IffSolver.decide (translate @{term "p = (q = p)"})\<close> |
92 "IffSolver.decide (translate @{term \"p = (q = p)\"})" |
90 \<open>false\<close>} |
93 "false"} |
|
94 \<close> |
91 \<close> |
95 |
92 |
96 text \<open> |
93 text \<open> |
97 Now, we combine these functions into an oracle. In general, an oracle may |
94 Now, we combine these functions into an oracle. In general, an oracle may |
98 be given any input, but it has to return a certified proposition (a |
95 be given any input, but it has to return a certified proposition (a |
111 else error "Proof failed."\<close> |
108 else error "Proof failed."\<close> |
112 |
109 |
113 text \<open> |
110 text \<open> |
114 Here is what we get when applying the oracle: |
111 Here is what we get when applying the oracle: |
115 |
112 |
116 @{ML_matchresult_fake "iff_oracle @{cprop \"p = (p::bool)\"}" "p = p"} |
113 @{ML_matchresult_fake \<open>iff_oracle @{cprop "p = (p::bool)"}\<close> \<open>p = p\<close>} |
117 |
114 |
118 (FIXME: is there a better way to present the theorem?) |
115 (FIXME: is there a better way to present the theorem?) |
119 |
116 |
120 To be able to use our oracle for Isar proofs, we wrap it into a tactic: |
117 To be able to use our oracle for Isar proofs, we wrap it into a tactic: |
121 \<close> |
118 \<close> |