equal
deleted
inserted
replaced
103 bind_thm ("not_not", not_not); |
103 bind_thm ("not_not", not_not); |
104 bind_thm ("imp_cong", imp_cong); |
104 bind_thm ("imp_cong", imp_cong); |
105 |
105 |
106 (* Elimination of True from asumptions: *) |
106 (* Elimination of True from asumptions: *) |
107 |
107 |
108 val True_implies_equals = prove_goal (the_context ()) |
108 local fun rd s = read_cterm (sign_of (the_context())) (s, propT); |
109 "(True ==> PROP P) == PROP P" |
109 in val True_implies_equals = standard' (equal_intr |
110 (fn _ => [rtac equal_intr_rule 1, atac 2, |
110 (implies_intr_hyps (implies_elim (assume (rd "True ==> PROP P")) TrueI)) |
111 METAHYPS (fn prems => resolve_tac prems 1) 1, |
111 (implies_intr_hyps (implies_intr (rd "True") (assume (rd "PROP P"))))); |
112 rtac TrueI 1]); |
112 end; |
113 |
113 |
114 fun prove nm thm = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]); |
114 fun prove nm thm = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]); |
115 |
115 |
116 prove "eq_commute" "(a=b) = (b=a)"; |
116 prove "eq_commute" "(a=b) = (b=a)"; |
117 prove "eq_left_commute" "(P=(Q=R)) = (Q=(P=R))"; |
117 prove "eq_left_commute" "(P=(Q=R)) = (Q=(P=R))"; |