(*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 \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)" by autolemma list_induct_hol4: fixes P :: "'a list \<Rightarrow> bool" assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))" shows "\<forall>l. (P l)" using a apply (rule_tac allI) apply (induct_tac "l") apply (simp) apply (metis) doneML {*val no_vars = Thm.rule_attribute (fn context => fn th => let val ctxt = Variable.set_body false (Context.proof_of context); val ((_, [th']), _) = Variable.import true [th] ctxt; in th' end);*}(*lemma equality_twice: "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"by auto*)