27 i.e. we want to decide whether @{term "P = (Q = P) = Q"} is a tautology. |
27 i.e. we want to decide whether @{term "P = (Q = P) = Q"} is a tautology. |
28 |
28 |
29 Assume, that we have a decision procedure for such formulae, implemented |
29 Assume, that we have a decision procedure for such formulae, implemented |
30 in ML. Since we do not care how it works, we will use it here as an |
30 in ML. Since we do not care how it works, we will use it here as an |
31 ``external solver'': |
31 ``external solver'': |
32 *} |
32 \<close> |
33 |
33 |
34 ML_file "external_solver.ML" |
34 ML_file "external_solver.ML" |
35 |
35 |
36 text {* |
36 text \<open> |
37 We do, however, know that the solver provides a function |
37 We do, however, know that the solver provides a function |
38 @{ML IffSolver.decide}. |
38 @{ML IffSolver.decide}. |
39 It takes a string representation of a formula and returns either |
39 It takes a string representation of a formula and returns either |
40 @{ML true} if the formula is a tautology or |
40 @{ML true} if the formula is a tautology or |
41 @{ML false} otherwise. The input syntax is specified as follows: |
41 @{ML false} otherwise. The input syntax is specified as follows: |
51 is then used to build an oracle, which we will subsequently use as a core |
51 is then used to build an oracle, which we will subsequently use as a core |
52 for an Isar method to be able to apply the oracle in proving theorems. |
52 for an Isar method to be able to apply the oracle in proving theorems. |
53 |
53 |
54 Let us start with the translation function from Isabelle propositions into |
54 Let us start with the translation function from Isabelle propositions into |
55 the solver's string representation. To increase efficiency while building |
55 the solver's string representation. To increase efficiency while building |
56 the string, we use functions from the @{text Buffer} module. |
56 the string, we use functions from the \<open>Buffer\<close> module. |
57 *} |
57 \<close> |
58 |
58 |
59 ML %grayML{*fun translate t = |
59 ML %grayML\<open>fun translate t = |
60 let |
60 let |
61 fun trans t = |
61 fun trans t = |
62 (case t of |
62 (case t of |
63 @{term "(=) :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t $ u => |
63 @{term "(=) :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t $ u => |
64 Buffer.add " (" #> |
64 Buffer.add " (" #> |
89 And here is what it returns for a formula which is not valid: |
89 And here is what it returns for a formula which is not valid: |
90 |
90 |
91 @{ML_response |
91 @{ML_response |
92 "IffSolver.decide (translate @{term \"p = (q = p)\"})" |
92 "IffSolver.decide (translate @{term \"p = (q = p)\"})" |
93 "false"} |
93 "false"} |
94 *} |
94 \<close> |
95 |
95 |
96 text {* |
96 text \<open> |
97 Now, we combine these functions into an oracle. In general, an oracle may |
97 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 |
98 be given any input, but it has to return a certified proposition (a |
99 special term which is type-checked), out of which Isabelle's inference |
99 special term which is type-checked), out of which Isabelle's inference |
100 kernel ``magically'' makes a theorem. |
100 kernel ``magically'' makes a theorem. |
101 |
101 |
102 Here, we take the proposition to be show as input. Note that we have |
102 Here, we take the proposition to be show as input. Note that we have |
103 to first extract the term which is then passed to the translation and |
103 to first extract the term which is then passed to the translation and |
104 decision procedure. If the solver finds this term to be valid, we return |
104 decision procedure. If the solver finds this term to be valid, we return |
105 the given proposition unchanged to be turned then into a theorem: |
105 the given proposition unchanged to be turned then into a theorem: |
106 *} |
106 \<close> |
107 |
107 |
108 oracle iff_oracle = {* fn ct => |
108 oracle iff_oracle = \<open>fn ct => |
109 if IffSolver.decide (translate (HOLogic.dest_Trueprop (Thm.term_of ct))) |
109 if IffSolver.decide (translate (HOLogic.dest_Trueprop (Thm.term_of ct))) |
110 then ct |
110 then ct |
111 else error "Proof failed."*} |
111 else error "Proof failed."\<close> |
112 |
112 |
113 text {* |
113 text \<open> |
114 Here is what we get when applying the oracle: |
114 Here is what we get when applying the oracle: |
115 |
115 |
116 @{ML_response_fake "iff_oracle @{cprop \"p = (p::bool)\"}" "p = p"} |
116 @{ML_response_fake "iff_oracle @{cprop \"p = (p::bool)\"}" "p = p"} |
117 |
117 |
118 (FIXME: is there a better way to present the theorem?) |
118 (FIXME: is there a better way to present the theorem?) |
119 |
119 |
120 To be able to use our oracle for Isar proofs, we wrap it into a tactic: |
120 To be able to use our oracle for Isar proofs, we wrap it into a tactic: |
121 *} |
121 \<close> |
122 |
122 |
123 ML %grayML{*fun iff_oracle_tac ctxt = |
123 ML %grayML\<open>fun iff_oracle_tac ctxt = |
124 CSUBGOAL (fn (goal, i) => |
124 CSUBGOAL (fn (goal, i) => |
125 (case try iff_oracle goal of |
125 (case try iff_oracle goal of |
126 NONE => no_tac |
126 NONE => no_tac |
127 | SOME thm => resolve_tac ctxt [thm] i))*} |
127 | SOME thm => resolve_tac ctxt [thm] i))\<close> |
128 |
128 |
129 text {* |
129 text \<open> |
130 and create a new method solely based on this tactic: |
130 and create a new method solely based on this tactic: |
131 *} |
131 \<close> |
132 |
132 |
133 method_setup iff_oracle = {* |
133 method_setup iff_oracle = \<open> |
134 Scan.succeed (fn ctxt => (Method.SIMPLE_METHOD' (iff_oracle_tac ctxt))) |
134 Scan.succeed (fn ctxt => (Method.SIMPLE_METHOD' (iff_oracle_tac ctxt))) |
135 *} "Oracle-based decision procedure for chains of equivalences" |
135 \<close> "Oracle-based decision procedure for chains of equivalences" |
136 |
136 |
137 text {* |
137 text \<open> |
138 Finally, we can test our oracle to prove some theorems: |
138 Finally, we can test our oracle to prove some theorems: |
139 *} |
139 \<close> |
140 |
140 |
141 lemma "p = (p::bool)" |
141 lemma "p = (p::bool)" |
142 by iff_oracle |
142 by iff_oracle |
143 |
143 |
144 lemma "p = (q = p) = q" |
144 lemma "p = (q = p) = q" |
145 by iff_oracle |
145 by iff_oracle |
146 |
146 |
147 |
147 |
148 text {* |
148 text \<open> |
149 (FIXME: say something about what the proof of the oracle is ... what do you mean?) |
149 (FIXME: say something about what the proof of the oracle is ... what do you mean?) |
150 *} |
150 \<close> |
151 |
151 |
152 |
152 |
153 end |
153 end |