print_depth 25; fun tacthm (Tactic tf) state = case Sequence.pull (tf state) of None => state | Some(x,_) => x ; fun tc th = cterm_of (#sign (rep_thm th)) (#prop (rep_thm th)) handle e => print_exn e ; val to = Type ("o", []) ; val Ict = read_cterm (sign_of thy) ("%P.P", to --> to) ; val II = reflexive Ict; val [prem] = goal thy "x == y ==> x == y"; val Ixy = combination II prem; (* fails tc *) val ctIxy = cprop_of Ixy; val xy = zero_var_indexes (assume ctIxy); val ta = TFree ("'a", []); val xct = read_cterm (sign_of thy) ("x", ta); val yct = read_cterm (sign_of thy) ("y", ta); val nxy = transitive (reflexive xct) xy ; val xey = iff_reflection RS (standard nxy) RS meta_eq_to_obj_eq ; val twoodiff = prove_goal thy "((P) <-> (Q)) | ((P) <-> (R)) | ((Q) <-> (R))" (fn [] => [fast_tac FOL_cs 1]) ; val didi = disj_imp_disj RSN (3, disj_imp_disj); val di3 = tacthm ((etac thin_rl 5) THEN (etac thin_rl 4) THEN atac 3) didi ; val twodiff2 = prove_goal thy "x = y | x = z | y = z" (fn [] => [ rtac di3 1, REPEAT (etac xey 2), rtac twoodiff 1]) ; val disjD1 = tacthm ((atac 4) THEN (atac 3) THEN (etac thin_rl 2)) (notE RSN (2, disjE)); val disjD2 = tacthm ((atac 2) THEN (atac 3) THEN (etac thin_rl 2)) (notE RSN (3, disjE)); val pcs = subset_refl RS (Pow_iff RS iffD2) ; val p0n0 = pcs RS not_emptyI; val l2 = [twodiff2, p0n0] MRS disjD1; val [symn] = compose (sym, 2, contrapos) ; val pe = [l2, p0n0 RS symn] MRS disjD2; val pos = [(Pow_iff RS iffD1), empty_subsetI] MRS equalityI ; val a0 = pcs RS (pe RS equalityD1 RS subsetD RS pos) ; val any = [p0n0, a0] MRS notE ; val sany = standard any ;