equal
deleted
inserted
replaced
128 fun transform_elim th = |
128 fun transform_elim th = |
129 if is_elimR th then |
129 if is_elimR th then |
130 let val tm = elimR2Fol th |
130 let val tm = elimR2Fol th |
131 val ctm = cterm_of (sign_of_thm th) tm |
131 val ctm = cterm_of (sign_of_thm th) tm |
132 in |
132 in |
133 prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th]) |
133 OldGoals.prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th]) |
134 end |
134 end |
135 else th; |
135 else th; |
136 |
136 |
137 |
137 |
138 (**** Transformation of Clasets and Simpsets into First-Order Axioms ****) |
138 (**** Transformation of Clasets and Simpsets into First-Order Axioms ****) |
238 val {sign,t, ...} = rep_cterm chil |
238 val {sign,t, ...} = rep_cterm chil |
239 val (Const ("Hilbert_Choice.Eps", Type("fun",[_,T]))) = t |
239 val (Const ("Hilbert_Choice.Eps", Type("fun",[_,T]))) = t |
240 val cex = Thm.cterm_of sign (HOLogic.exists_const T) |
240 val cex = Thm.cterm_of sign (HOLogic.exists_const T) |
241 val ex_tm = c_mkTrueprop (Thm.capply cex cabs) |
241 val ex_tm = c_mkTrueprop (Thm.capply cex cabs) |
242 and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees))); |
242 and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees))); |
243 in prove_goalw_cterm [def] (Drule.mk_implies (ex_tm, conc)) |
243 in OldGoals.prove_goalw_cterm [def] (Drule.mk_implies (ex_tm, conc)) |
244 (fn [prem] => [ rtac (prem RS someI_ex) 1 ]) |
244 (fn [prem] => [ rtac (prem RS someI_ex) 1 ]) |
245 end; |
245 end; |
246 |
246 |
247 |
247 |
248 (*Converts an Isabelle theorem (intro, elim or simp format) into nnf.*) |
248 (*Converts an Isabelle theorem (intro, elim or simp format) into nnf.*) |