+ −
ML {*+ −
fun dest_cbinop t =+ −
let+ −
val (t2, rhs) = Thm.dest_comb t;+ −
val (bop, lhs) = Thm.dest_comb t2;+ −
in+ −
(bop, (lhs, rhs))+ −
end+ −
*}+ −
+ −
ML {*+ −
fun dest_ceq t =+ −
let+ −
val (bop, pair) = dest_cbinop t;+ −
val (bop_s, _) = Term.dest_Const (Thm.term_of bop);+ −
in+ −
if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))+ −
end+ −
*}+ −
+ −
ML {*+ −
fun split_binop_conv t =+ −
let+ −
val (lhs, rhs) = dest_ceq t;+ −
val (bop, _) = dest_cbinop lhs;+ −
val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;+ −
val [cmT, crT] = Thm.dest_ctyp cr2;+ −
in+ −
Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}+ −
end+ −
*}+ −
+ −
+ −
ML {*+ −
fun split_arg_conv t =+ −
let+ −
val (lhs, rhs) = dest_ceq t;+ −
val (lop, larg) = Thm.dest_comb lhs;+ −
val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;+ −
in+ −
Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}+ −
end+ −
*}+ −
+ −
ML {*+ −
fun split_binop_tac n thm =+ −
let+ −
val concl = Thm.cprem_of thm n;+ −
val (_, cconcl) = Thm.dest_comb concl;+ −
val rewr = split_binop_conv cconcl;+ −
in+ −
rtac rewr n thm+ −
end+ −
handle CTERM _ => Seq.empty+ −
*}+ −
+ −
+ −
ML {*+ −
fun split_arg_tac n thm =+ −
let+ −
val concl = Thm.cprem_of thm n;+ −
val (_, cconcl) = Thm.dest_comb concl;+ −
val rewr = split_arg_conv cconcl;+ −
in+ −
rtac rewr n thm+ −
end+ −
handle CTERM _ => Seq.empty+ −
*}+ −
+ −
+ −
lemma trueprop_cong:+ −
shows "(a ≡ b) ⟹ (Trueprop a ≡ Trueprop b)"+ −
by auto+ −