134 |
134 |
135 fun clause2raw_thm ctxt clause = |
135 fun clause2raw_thm ctxt clause = |
136 let |
136 let |
137 (* eliminates negated disjunctions from the i-th premise, possibly *) |
137 (* eliminates negated disjunctions from the i-th premise, possibly *) |
138 (* adding new premises, then continues with the (i+1)-th premise *) |
138 (* adding new premises, then continues with the (i+1)-th premise *) |
139 (* int -> Thm.thm -> Thm.thm *) |
|
140 fun not_disj_to_prem i thm = |
139 fun not_disj_to_prem i thm = |
141 if i > Thm.nprems_of thm then |
140 if i > Thm.nprems_of thm then |
142 thm |
141 thm |
143 else |
142 else |
144 not_disj_to_prem (i+1) |
143 not_disj_to_prem (i+1) |
145 (Seq.hd (REPEAT_DETERM (resolve_tac ctxt [clause2raw_not_disj] i) thm)) |
144 (Seq.hd (REPEAT_DETERM (resolve_tac ctxt [clause2raw_not_disj] i) thm)) |
146 (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *) |
145 (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *) |
147 (* becomes "[..., A1, ..., An] |- B" *) |
146 (* becomes "[..., A1, ..., An] |- B" *) |
148 (* Thm.thm -> Thm.thm *) |
|
149 fun prems_to_hyps thm = |
147 fun prems_to_hyps thm = |
150 fold (fn cprem => fn thm' => |
148 fold (fn cprem => fn thm' => |
151 Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm |
149 Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm |
152 in |
150 in |
153 (* [...] |- ~(x1 | ... | xn) ==> False *) |
151 (* [...] |- ~(x1 | ... | xn) ==> False *) |
280 (* No simplification is performed below connectives other than & and |. *) |
278 (* No simplification is performed below connectives other than & and |. *) |
281 (* Optimization: The right-hand side of a conjunction (disjunction) is *) |
279 (* Optimization: The right-hand side of a conjunction (disjunction) is *) |
282 (* simplified only if the left-hand side does not simplify to False *) |
280 (* simplified only if the left-hand side does not simplify to False *) |
283 (* (True, respectively). *) |
281 (* (True, respectively). *) |
284 (* ------------------------------------------------------------------------- *) |
282 (* ------------------------------------------------------------------------- *) |
285 |
|
286 (* Theory.theory -> Term.term -> Thm.thm *) |
|
287 |
283 |
288 fun simp_True_False_thm thy (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ x $ y) = |
284 fun simp_True_False_thm thy (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ x $ y) = |
289 let |
285 let |
290 val thm1 = simp_True_False_thm thy x |
286 val thm1 = simp_True_False_thm thy x |
291 val x'= (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm1 |
287 val x'= (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm1 |