# HG changeset patch # User wenzelm # Date 938609809 -7200 # Node ID 57c4cea8b1373b435d1defd6fcdb9a089152ae7b # Parent 0408848fa7d460c2a11c827be4af056035e9aadb bind_thms; diff -r 0408848fa7d4 -r 57c4cea8b137 src/HOLCF/Tr.ML --- a/src/HOLCF/Tr.ML Wed Sep 29 14:56:19 1999 +0200 +++ b/src/HOLCF/Tr.ML Wed Sep 29 14:56:49 1999 +0200 @@ -34,7 +34,7 @@ (* tactic for tr-thms with case split *) (* ------------------------------------------------------------------------ *) -val tr_defs = [andalso_def,orelse_def,neg_def,ifte_def,TT_def,FF_def]; +bind_thms ("tr_defs", [andalso_def,orelse_def,neg_def,ifte_def,TT_def,FF_def]); fun prover t = prove_goal thy t (fn prems => @@ -48,45 +48,45 @@ (* distinctness for type tr *) (* ------------------------------------------------------------------------ *) -val dist_less_tr = map prover [ +bind_thms ("dist_less_tr", map prover [ "~TT << UU", "~FF << UU", "~TT << FF", "~FF << TT" - ]; + ]); val dist_eq_tr = map prover ["TT~=UU","FF~=UU","TT~=FF"]; -val dist_eq_tr = dist_eq_tr @ (map (fn thm => (thm RS not_sym)) dist_eq_tr); +bind_thms ("dist_eq_tr", dist_eq_tr @ (map (fn thm => (thm RS not_sym)) dist_eq_tr)); (* ------------------------------------------------------------------------ *) (* lemmas about andalso, orelse, neg and if *) (* ------------------------------------------------------------------------ *) -val andalso_thms = map prover [ +bind_thms ("andalso_thms", map prover [ "(TT andalso y) = y", "(FF andalso y) = FF", "(UU andalso y) = UU", "(y andalso TT) = y", "(y andalso y) = y" - ]; + ]); -val orelse_thms = map prover [ +bind_thms ("orelse_thms", map prover [ "(TT orelse y) = TT", "(FF orelse y) = y", "(UU orelse y) = UU", "(y orelse FF) = y", - "(y orelse y) = y"]; + "(y orelse y) = y"]); -val neg_thms = map prover [ +bind_thms ("neg_thms", map prover [ "neg`TT = FF", "neg`FF = TT", "neg`UU = UU" - ]; + ]); -val ifte_thms = map prover [ +bind_thms ("ifte_thms", map prover [ "If UU then e1 else e2 fi = UU", "If FF then e1 else e2 fi = e2", - "If TT then e1 else e2 fi = e1"]; + "If TT then e1 else e2 fi = e1"]); Addsimps (dist_less_tr @ dist_eq_tr @ andalso_thms @ orelse_thms @ neg_thms @ ifte_thms); @@ -173,7 +173,7 @@ by (TRYALL (Asm_full_simp_tac)); qed"adm_trick_2"; -val adm_tricks = [adm_trick_1,adm_trick_2]; +bind_thms ("adm_tricks", [adm_trick_1,adm_trick_2]); Goal "cont(f) ==> adm (%x. (f x)~=TT)";