(*notation ( output) "prop" ("#_" [1000] 1000) *)

notation ( output) "Trueprop" ("#_" [1000] 1000)

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

lemma list_induct_hol4:

  fixes P :: "'a list ⇒ bool"

  assumes a: "((P []) ∧ (∀t. (P t) ⟶ (∀h. (P (h # t)))))"

  shows "∀l. (P l)"

  using a

  apply (rule_tac allI)

  apply (induct_tac "l")

  apply (simp)

  apply (metis)

  done