equal
deleted
inserted
replaced
58 |
58 |
59 ML %grayML{*fun translate t = |
59 ML %grayML{*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 "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t $ u => |
63 @{term "(=) :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t $ u => |
64 Buffer.add " (" #> |
64 Buffer.add " (" #> |
65 trans t #> |
65 trans t #> |
66 Buffer.add "<=>" #> |
66 Buffer.add "<=>" #> |
67 trans u #> |
67 trans u #> |
68 Buffer.add ") " |
68 Buffer.add ") " |
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 *} |
122 |
122 |
123 ML %grayML{*val iff_oracle_tac = |
123 ML %grayML{*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 => rtac thm i))*} |
127 | SOME thm => resolve_tac ctxt [thm] i))*} |
128 |
128 |
129 text {* |
129 text {* |
130 and create a new method solely based on this tactic: |
130 and create a new method solely based on this tactic: |
131 *} |
131 *} |
132 |
132 |
133 method_setup iff_oracle = {* |
133 method_setup iff_oracle = {* |
134 Scan.succeed (K (Method.SIMPLE_METHOD' iff_oracle_tac)) |
134 Scan.succeed (fn ctxt => (Method.SIMPLE_METHOD' (iff_oracle_tac ctxt))) |
135 *} "Oracle-based decision procedure for chains of equivalences" |
135 *} "Oracle-based decision procedure for chains of equivalences" |
136 |
136 |
137 text {* |
137 text {* |
138 Finally, we can test our oracle to prove some theorems: |
138 Finally, we can test our oracle to prove some theorems: |
139 *} |
139 *} |