equal
deleted
inserted
replaced
23 \end{readmore} |
23 \end{readmore} |
24 |
24 |
25 For our explanation here, we will use the @{text metis} prover for proving |
25 For our explanation here, we will use the @{text metis} prover for proving |
26 propositional formulae. The general method will be roughly as follows: |
26 propositional formulae. The general method will be roughly as follows: |
27 Given a goal @{text G}, we transform it into the syntactical respresentation |
27 Given a goal @{text G}, we transform it into the syntactical respresentation |
28 of @{text "metis"}, build the CNF and then let metis search for a refutation. |
28 of @{text "metis"}, build the CNF of the negated formula and then let metis search |
29 @{text Metis} will either return the proved goal or raise an exception meaning |
29 for a refutation. @{text Metis} will either return the proved goal or raise |
|
30 an exception meaning |
30 that it was unable to prove the goal (FIXME: is this so?). |
31 that it was unable to prove the goal (FIXME: is this so?). |
31 |
32 |
32 The translation function from Isabelle propositions into formulae of |
33 The translation function from Isabelle propositions into formulae of |
33 @{text metis} is as follows: |
34 @{text metis} is as follows: |
34 *} |
35 *} |
72 text {* |
73 text {* |
73 (FIXME: Is there a deep reason why Metis.Normalize.cnf returns a list?) |
74 (FIXME: Is there a deep reason why Metis.Normalize.cnf returns a list?) |
74 |
75 |
75 (FIXME: What does Line 8 do?) |
76 (FIXME: What does Line 8 do?) |
76 |
77 |
77 (FIXME: Can this code improved?) |
78 (FIXME: Can this code be improved?) |
78 |
79 |
79 |
80 |
80 Setting up the resolution. |
81 Setting up the resolution. |
81 *} |
82 *} |
82 |
83 |
102 if solve (trans t) then (Thm.cterm_of thy t) |
103 if solve (trans t) then (Thm.cterm_of thy t) |
103 else error "Proof failed."*} |
104 else error "Proof failed."*} |
104 |
105 |
105 oracle prop_oracle = prop_dp |
106 oracle prop_oracle = prop_dp |
106 |
107 |
107 text {* (FIXME: What does oracle this do?) *} |
108 text {* (FIXME: What does oracle do?) *} |
108 |
109 |
109 |
110 |
110 ML{*fun prop_oracle_tac ctxt = |
111 ML{*fun prop_oracle_tac ctxt = |
111 SUBGOAL (fn (goal, i) => |
112 SUBGOAL (fn (goal, i) => |
112 (case (try prop_oracle (ProofContext.theory_of ctxt, goal)) of |
113 (case (try prop_oracle (ProofContext.theory_of ctxt, goal)) of |
125 text {* (FIXME What does @{ML Method.SIMPLE_METHOD'} do?) *} |
126 text {* (FIXME What does @{ML Method.SIMPLE_METHOD'} do?) *} |
126 |
127 |
127 lemma test: "p \<or> \<not>p" |
128 lemma test: "p \<or> \<not>p" |
128 by prop_oracle |
129 by prop_oracle |
129 |
130 |
130 text {* (FIXME: say something about what the proof of the oracle is) *} |
131 text {* (FIXME: say something about what the proof of the oracle is) |
131 |
132 |
132 ML {* Thm.proof_of @{thm test} *} |
133 @{ML_response_fake [display,gray] "Thm.proof_of @{thm test}" "???"} |
|
134 |
|
135 *} |
|
136 |
|
137 |
133 |
138 |
134 lemma "((p \<longrightarrow> q) \<longrightarrow> p) \<longrightarrow> p" |
139 lemma "((p \<longrightarrow> q) \<longrightarrow> p) \<longrightarrow> p" |
135 by prop_oracle |
140 by prop_oracle |
136 |
141 |
137 lemma "\<forall>x::nat. x \<ge> 0" |
142 lemma "\<forall>x::nat. x \<ge> 0" |