diff -r 000000000000 -r a5a9c433f639 src/CCL/Term.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/CCL/Term.ML Thu Sep 16 12:20:38 1993 +0200 @@ -0,0 +1,146 @@ +(* Title: CCL/terms + ID: $Id$ + Author: Martin Coen, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +For terms.thy. +*) + +open Term; + +val simp_can_defs = [one_def,inl_def,inr_def]; +val simp_ncan_defs = [if_def,when_def,split_def,fst_def,snd_def,thd_def]; +val simp_defs = simp_can_defs @ simp_ncan_defs; + +val ind_can_defs = [zero_def,succ_def,nil_def,cons_def]; +val ind_ncan_defs = [ncase_def,nrec_def,lcase_def,lrec_def]; +val ind_defs = ind_can_defs @ ind_ncan_defs; + +val data_defs = simp_defs @ ind_defs @ [napply_def]; +val genrec_defs = [letrec_def,letrec2_def,letrec3_def]; + +val term_congs = ccl_mk_congs Term.thy + ["inl","inr","succ","op .","split","if","when","ncase","nrec","lcase","lrec", + "fst","snd","thd","let","letrec","letrec2","letrec3","napply"]; + +(*** Beta Rules, including strictness ***) + +goalw Term.thy [let_def] "~ t=bot--> let x be t in f(x) = f(t)"; +by (res_inst_tac [("t","t")] term_case 1); +by (ALLGOALS(SIMP_TAC(CCL_ss addrews [caseBtrue,caseBfalse,caseBpair,caseBlam]))); +val letB = result() RS mp; + +goalw Term.thy [let_def] "let x be bot in f(x) = bot"; +br caseBbot 1; +val letBabot = result(); + +goalw Term.thy [let_def] "let x be t in bot = bot"; +brs ([caseBbot] RL [term_case]) 1; +by (ALLGOALS(SIMP_TAC(CCL_ss addrews [caseBtrue,caseBfalse,caseBpair,caseBlam]))); +val letBbbot = result(); + +goalw Term.thy [apply_def] "(lam x.b(x)) ` a = b(a)"; +by (ALLGOALS(SIMP_TAC(CCL_ss addrews [caseBtrue,caseBfalse,caseBpair,caseBlam]))); +val applyB = result(); + +goalw Term.thy [apply_def] "bot ` a = bot"; +br caseBbot 1; +val applyBbot = result(); + +goalw Term.thy [fix_def] "fix(f) = f(fix(f))"; +by (resolve_tac [applyB RS ssubst] 1 THEN resolve_tac [refl] 1); +val fixB = result(); + +goalw Term.thy [letrec_def] + "letrec g x be h(x,g) in g(a) = h(a,%y.letrec g x be h(x,g) in g(y))"; +by (resolve_tac [fixB RS ssubst] 1 THEN + resolve_tac [applyB RS ssubst] 1 THEN resolve_tac [refl] 1); +val letrecB = result(); + +val rawBs = caseBs @ [applyB,applyBbot,letrecB]; + +fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s + (fn _ => [SIMP_TAC (CCL_ss addrews rawBs addcongs term_congs) 1]); +fun mk_beta_rl s = raw_mk_beta_rl data_defs s; + +val ifBtrue = mk_beta_rl "if true then t else u = t"; +val ifBfalse = mk_beta_rl "if false then t else u = u"; +val ifBbot = mk_beta_rl "if bot then t else u = bot"; + +val whenBinl = mk_beta_rl "when(inl(a),t,u) = t(a)"; +val whenBinr = mk_beta_rl "when(inr(a),t,u) = u(a)"; +val whenBbot = mk_beta_rl "when(bot,t,u) = bot"; + +val splitB = mk_beta_rl "split(,h) = h(a,b)"; +val splitBbot = mk_beta_rl "split(bot,h) = bot"; +val fstB = mk_beta_rl "fst() = a"; +val fstBbot = mk_beta_rl "fst(bot) = bot"; +val sndB = mk_beta_rl "snd() = b"; +val sndBbot = mk_beta_rl "snd(bot) = bot"; +val thdB = mk_beta_rl "thd(>) = c"; +val thdBbot = mk_beta_rl "thd(bot) = bot"; + +val ncaseBzero = mk_beta_rl "ncase(zero,t,u) = t"; +val ncaseBsucc = mk_beta_rl "ncase(succ(n),t,u) = u(n)"; +val ncaseBbot = mk_beta_rl "ncase(bot,t,u) = bot"; +val nrecBzero = mk_beta_rl "nrec(zero,t,u) = t"; +val nrecBsucc = mk_beta_rl "nrec(succ(n),t,u) = u(n,nrec(n,t,u))"; +val nrecBbot = mk_beta_rl "nrec(bot,t,u) = bot"; + +val lcaseBnil = mk_beta_rl "lcase([],t,u) = t"; +val lcaseBcons = mk_beta_rl "lcase(x.xs,t,u) = u(x,xs)"; +val lcaseBbot = mk_beta_rl "lcase(bot,t,u) = bot"; +val lrecBnil = mk_beta_rl "lrec([],t,u) = t"; +val lrecBcons = mk_beta_rl "lrec(x.xs,t,u) = u(x,xs,lrec(xs,t,u))"; +val lrecBbot = mk_beta_rl "lrec(bot,t,u) = bot"; + +val letrec2B = raw_mk_beta_rl (data_defs @ [letrec2_def]) + "letrec g x y be h(x,y,g) in g(p,q) = \ +\ h(p,q,%u v.letrec g x y be h(x,y,g) in g(u,v))"; +val letrec3B = raw_mk_beta_rl (data_defs @ [letrec3_def]) + "letrec g x y z be h(x,y,z,g) in g(p,q,r) = \ +\ h(p,q,r,%u v w.letrec g x y z be h(x,y,z,g) in g(u,v,w))"; + +val napplyBzero = mk_beta_rl "f^zero`a = a"; +val napplyBsucc = mk_beta_rl "f^succ(n)`a = f(f^n`a)"; + +val termBs = [letB,applyB,applyBbot,splitB,splitBbot, + fstB,fstBbot,sndB,sndBbot,thdB,thdBbot, + ifBtrue,ifBfalse,ifBbot,whenBinl,whenBinr,whenBbot, + ncaseBzero,ncaseBsucc,ncaseBbot,nrecBzero,nrecBsucc,nrecBbot, + lcaseBnil,lcaseBcons,lcaseBbot,lrecBnil,lrecBcons,lrecBbot, + napplyBzero,napplyBsucc]; + +(*** Constructors are injective ***) + +val term_injs = map (mk_inj_rl Term.thy + [applyB,splitB,whenBinl,whenBinr,ncaseBsucc,lcaseBcons] + (ccl_congs @ term_congs)) + ["(inl(a) = inl(a')) <-> (a=a')", + "(inr(a) = inr(a')) <-> (a=a')", + "(succ(a) = succ(a')) <-> (a=a')", + "(a.b = a'.b') <-> (a=a' & b=b')"]; + +(*** Constructors are distinct ***) + +val term_dstncts = mkall_dstnct_thms Term.thy data_defs (ccl_injs @ term_injs) + [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op ."]]; + +(*** Rules for pre-order [= ***) + +local + fun mk_thm s = prove_goalw Term.thy data_defs s (fn _ => + [SIMP_TAC (ccl_ss addrews (ccl_porews)) 1]); +in + val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'", + "inr(b) [= inr(b') <-> b [= b'", + "succ(n) [= succ(n') <-> n [= n'", + "x.xs [= x'.xs' <-> x [= x' & xs [= xs'"]; +end; + +(*** Rewriting and Proving ***) + +val term_rews = termBs @ term_injs @ term_dstncts @ ccl_porews @ term_porews; +val term_ss = ccl_ss addrews term_rews addcongs term_congs; + +val term_cs = ccl_cs addSEs (term_dstncts RL [notE]) addSDs (XH_to_Ds term_injs);