QuotProd with product_quotient and a 3 respects and preserves lemmas.
(*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 auto+ −
+ −
lemma 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)+ −
done+ −
+ −
ML {*+ −
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*)+ −