1 

     2 ML {*

     3   fun dest_cbinop t =

     4     let

     5       val (t2, rhs) = Thm.dest_comb t;

     6       val (bop, lhs) = Thm.dest_comb t2;

     7     in

     8       (bop, (lhs, rhs))

     9     end

    10 *}

    11 

    12 ML {*

    13   fun dest_ceq t =

    14     let

    15       val (bop, pair) = dest_cbinop t;

    16       val (bop_s, _) = Term.dest_Const (Thm.term_of bop);

    17     in

    18       if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))

    19     end

    20 *}

    21 

    22 ML {*

    23   fun split_binop_conv t =

    24     let

    25       val (lhs, rhs) = dest_ceq t;

    26       val (bop, _) = dest_cbinop lhs;

    27       val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;

    28       val [cmT, crT] = Thm.dest_ctyp cr2;

    29     in

    30       Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}

    31     end

    32 *}

    33 

    34 

    35 ML {*

    36   fun split_arg_conv t =

    37     let

    38       val (lhs, rhs) = dest_ceq t;

    39       val (lop, larg) = Thm.dest_comb lhs;

    40       val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;

    41     in

    42       Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}

    43     end

    44 *}

    45 

    46 ML {*

    47   fun split_binop_tac n thm =

    48     let

    49       val concl = Thm.cprem_of thm n;

    50       val (_, cconcl) = Thm.dest_comb concl;

    51       val rewr = split_binop_conv cconcl;

    52     in

    53       rtac rewr n thm

    54     end

    55       handle CTERM _ => Seq.empty

    56 *}

    57 

    58 

    59 ML {*

    60   fun split_arg_tac n thm =

    61     let

    62       val concl = Thm.cprem_of thm n;

    63       val (_, cconcl) = Thm.dest_comb concl;

    64       val rewr = split_arg_conv cconcl;

    65     in

    66       rtac rewr n thm

    67     end

    68       handle CTERM _ => Seq.empty

    69 *}

    70 

    71 

    72 lemma trueprop_cong:

    73   shows "(a ≡ b) ⟹ (Trueprop a ≡ Trueprop b)"

    74   by auto