137 fun translate_prem ctxt constant_table t = |
137 fun translate_prem ctxt constant_table t = |
138 case try HOLogic.dest_not t of |
138 case try HOLogic.dest_not t of |
139 SOME t => NegRel_of (translate_literal ctxt constant_table t) |
139 SOME t => NegRel_of (translate_literal ctxt constant_table t) |
140 | NONE => translate_literal ctxt constant_table t |
140 | NONE => translate_literal ctxt constant_table t |
141 |
141 |
|
142 |
|
143 fun imp_prems_conv cv ct = |
|
144 case Thm.term_of ct of |
|
145 Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct |
|
146 | _ => Conv.all_conv ct |
|
147 |
|
148 fun Trueprop_conv cv ct = |
|
149 case Thm.term_of ct of |
|
150 Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct |
|
151 | _ => raise Fail "Trueprop_conv" |
|
152 |
|
153 fun preprocess_intro thy rule = |
|
154 Conv.fconv_rule |
|
155 (imp_prems_conv |
|
156 (Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq})))) |
|
157 (Thm.transfer thy rule) |
|
158 |
142 fun translate_intros ctxt gr const constant_table = |
159 fun translate_intros ctxt gr const constant_table = |
143 let |
160 let |
144 val intros = Graph.get_node gr const |
161 val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const) |
145 val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt |
162 val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt |
146 val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table |
163 val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table |
147 fun translate_intro intro = |
164 fun translate_intro intro = |
148 let |
165 let |
149 val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro) |
166 val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro) |