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