226
+ − 1
(*notation ( output) "prop" ("#_" [1000] 1000) *)
+ − 2
notation ( output) "Trueprop" ("#_" [1000] 1000)
101
+ − 3
+ − 4
ML {*
+ − 5
fun dest_cbinop t =
+ − 6
let
+ − 7
val (t2, rhs) = Thm.dest_comb t;
+ − 8
val (bop, lhs) = Thm.dest_comb t2;
+ − 9
in
+ − 10
(bop, (lhs, rhs))
+ − 11
end
+ − 12
*}
+ − 13
+ − 14
ML {*
+ − 15
fun dest_ceq t =
+ − 16
let
+ − 17
val (bop, pair) = dest_cbinop t;
+ − 18
val (bop_s, _) = Term.dest_Const (Thm.term_of bop);
+ − 19
in
+ − 20
if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))
+ − 21
end
+ − 22
*}
+ − 23
+ − 24
ML {*
+ − 25
fun split_binop_conv t =
+ − 26
let
+ − 27
val (lhs, rhs) = dest_ceq t;
+ − 28
val (bop, _) = dest_cbinop lhs;
+ − 29
val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
+ − 30
val [cmT, crT] = Thm.dest_ctyp cr2;
+ − 31
in
+ − 32
Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}
+ − 33
end
+ − 34
*}
+ − 35
+ − 36
+ − 37
ML {*
+ − 38
fun split_arg_conv t =
+ − 39
let
+ − 40
val (lhs, rhs) = dest_ceq t;
+ − 41
val (lop, larg) = Thm.dest_comb lhs;
+ − 42
val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
+ − 43
in
+ − 44
Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}
+ − 45
end
+ − 46
*}
+ − 47
+ − 48
ML {*
+ − 49
fun split_binop_tac n thm =
+ − 50
let
+ − 51
val concl = Thm.cprem_of thm n;
+ − 52
val (_, cconcl) = Thm.dest_comb concl;
+ − 53
val rewr = split_binop_conv cconcl;
+ − 54
in
+ − 55
rtac rewr n thm
+ − 56
end
+ − 57
handle CTERM _ => Seq.empty
+ − 58
*}
+ − 59
+ − 60
+ − 61
ML {*
+ − 62
fun split_arg_tac n thm =
+ − 63
let
+ − 64
val concl = Thm.cprem_of thm n;
+ − 65
val (_, cconcl) = Thm.dest_comb concl;
+ − 66
val rewr = split_arg_conv cconcl;
+ − 67
in
+ − 68
rtac rewr n thm
+ − 69
end
+ − 70
handle CTERM _ => Seq.empty
+ − 71
*}
+ − 72
+ − 73
+ − 74
lemma trueprop_cong:
303
+ − 75
shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
101
+ − 76
by auto
226
+ − 77
+ − 78
lemma list_induct_hol4:
303
+ − 79
fixes P :: "'a list \<Rightarrow> bool"
+ − 80
assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
+ − 81
shows "\<forall>l. (P l)"
226
+ − 82
using a
+ − 83
apply (rule_tac allI)
+ − 84
apply (induct_tac "l")
+ − 85
apply (simp)
+ − 86
apply (metis)
+ − 87
done
+ − 88
301
+ − 89
ML {*
+ − 90
val no_vars = Thm.rule_attribute (fn context => fn th =>
+ − 91
let
+ − 92
val ctxt = Variable.set_body false (Context.proof_of context);
+ − 93
val ((_, [th']), _) = Variable.import true [th] ctxt;
+ − 94
in th' end);
+ − 95
*}
303
+ − 96
+ − 97
(*lemma equality_twice:
+ − 98
"a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
+ − 99
by auto*)