val bed = [asm_rl, def_imp_eq, def_imp_eq] MRS box_equals ; fun mk_dist tys (fc1, fc2) = prove_goal lksyn.thy ("(?a :: " ^ tys ^ ") ~= ?b") (fn _ => [(rtac notI 1), (dtac bed 1), (rtac fc1 1), (rtac fc2 1), Full_simp_tac 1]) ; fun pairs (x :: xs) = map (pair x) xs @ pairs xs | pairs [] = [] ; val fc_defs = [ Btimes, Bplus, Bimp, Bneg, Btrue, Bfalse ] ; val fc_dist' = map (mk_dist "formula") (pairs fc_defs) ; val fc_dist = fc_dist' @ (fc_dist' RL [not_sym]) ; val fc_distEs = fc_dist RL [notE] ; val bede = meta_std (prove_goal HOL_Gen.thy "a = c & b = d --> (a = b) = (c = d)" fn_ft1) ; val bedd = [def_imp_eq, def_imp_eq] MRS bede ; fun mk_same def = simplify (simpset ()) ([def, def] MRS bedd) ; fun mk_sameE sames = map (tacthm (ALLGOALS (REPEXP (etac conjE)))) (sames RL [iffD1 RS revcut_rl]) ; val fc_same = map mk_same fc_defs ; val fc_sameEs = mk_sameE fc_same ; val fcEs = (fc_sameEs @ fc_distEs) ; val fc2Es = [sym RSN (2, trans)] RL fcEs ; val thips1 = [ipsubfml.ipsI, [refl, def_imp_eq RS sym] MRS conjI RS (hd prod.inject RS iffD2)] MRS mem_same ; fun mk_ipsI def = disjs 1 (full_simplify (simpset ()) (def RSN (2, thips1))) ; val ipsfIs = [refl] RL BasisLibrary.List.concat (map mk_ipsI fc_defs) ;