src/CCL/Term.ML
changeset 0 a5a9c433f639
child 8 c3d2c6dcf3f0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/Term.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,146 @@
     1.4 +(*  Title: 	CCL/terms
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Martin Coen, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +For terms.thy.
    1.10 +*)
    1.11 +
    1.12 +open Term;
    1.13 +
    1.14 +val simp_can_defs = [one_def,inl_def,inr_def];
    1.15 +val simp_ncan_defs = [if_def,when_def,split_def,fst_def,snd_def,thd_def];
    1.16 +val simp_defs = simp_can_defs @ simp_ncan_defs;
    1.17 +
    1.18 +val ind_can_defs = [zero_def,succ_def,nil_def,cons_def];
    1.19 +val ind_ncan_defs = [ncase_def,nrec_def,lcase_def,lrec_def];
    1.20 +val ind_defs = ind_can_defs @ ind_ncan_defs;
    1.21 +
    1.22 +val data_defs = simp_defs @ ind_defs @ [napply_def];
    1.23 +val genrec_defs = [letrec_def,letrec2_def,letrec3_def];
    1.24 +
    1.25 +val term_congs = ccl_mk_congs Term.thy 
    1.26 +    ["inl","inr","succ","op .","split","if","when","ncase","nrec","lcase","lrec",
    1.27 +     "fst","snd","thd","let","letrec","letrec2","letrec3","napply"];
    1.28 +
    1.29 +(*** Beta Rules, including strictness ***)
    1.30 +
    1.31 +goalw Term.thy [let_def] "~ t=bot--> let x be t in f(x) = f(t)";
    1.32 +by (res_inst_tac [("t","t")] term_case 1);
    1.33 +by (ALLGOALS(SIMP_TAC(CCL_ss addrews [caseBtrue,caseBfalse,caseBpair,caseBlam])));
    1.34 +val letB = result() RS mp;
    1.35 +
    1.36 +goalw Term.thy [let_def] "let x be bot in f(x) = bot";
    1.37 +br caseBbot 1;
    1.38 +val letBabot = result();
    1.39 +
    1.40 +goalw Term.thy [let_def] "let x be t in bot = bot";
    1.41 +brs ([caseBbot] RL [term_case]) 1;
    1.42 +by (ALLGOALS(SIMP_TAC(CCL_ss addrews [caseBtrue,caseBfalse,caseBpair,caseBlam])));
    1.43 +val letBbbot = result();
    1.44 +
    1.45 +goalw Term.thy [apply_def] "(lam x.b(x)) ` a = b(a)";
    1.46 +by (ALLGOALS(SIMP_TAC(CCL_ss addrews [caseBtrue,caseBfalse,caseBpair,caseBlam])));
    1.47 +val applyB = result();
    1.48 +
    1.49 +goalw Term.thy [apply_def] "bot ` a = bot";
    1.50 +br caseBbot 1;
    1.51 +val applyBbot = result();
    1.52 +
    1.53 +goalw Term.thy [fix_def] "fix(f) = f(fix(f))";
    1.54 +by (resolve_tac [applyB RS ssubst] 1 THEN resolve_tac [refl] 1);
    1.55 +val fixB = result();
    1.56 +
    1.57 +goalw Term.thy [letrec_def]
    1.58 +      "letrec g x be h(x,g) in g(a) = h(a,%y.letrec g x be h(x,g) in g(y))";
    1.59 +by (resolve_tac [fixB RS ssubst] 1 THEN 
    1.60 +    resolve_tac [applyB RS ssubst] 1 THEN resolve_tac [refl] 1);
    1.61 +val letrecB = result();
    1.62 +
    1.63 +val rawBs = caseBs @ [applyB,applyBbot,letrecB];
    1.64 +
    1.65 +fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
    1.66 +           (fn _ => [SIMP_TAC (CCL_ss addrews rawBs  addcongs term_congs) 1]);
    1.67 +fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
    1.68 +
    1.69 +val ifBtrue    = mk_beta_rl "if true then t else u = t";
    1.70 +val ifBfalse   = mk_beta_rl "if false then t else u = u";
    1.71 +val ifBbot     = mk_beta_rl "if bot then t else u = bot";
    1.72 +
    1.73 +val whenBinl   = mk_beta_rl "when(inl(a),t,u) = t(a)";
    1.74 +val whenBinr   = mk_beta_rl "when(inr(a),t,u) = u(a)";
    1.75 +val whenBbot   = mk_beta_rl "when(bot,t,u) = bot";
    1.76 +
    1.77 +val splitB     = mk_beta_rl "split(<a,b>,h) = h(a,b)";
    1.78 +val splitBbot  = mk_beta_rl "split(bot,h) = bot";
    1.79 +val fstB       = mk_beta_rl "fst(<a,b>) = a";
    1.80 +val fstBbot    = mk_beta_rl "fst(bot) = bot";
    1.81 +val sndB       = mk_beta_rl "snd(<a,b>) = b";
    1.82 +val sndBbot    = mk_beta_rl "snd(bot) = bot";
    1.83 +val thdB       = mk_beta_rl "thd(<a,<b,c>>) = c";
    1.84 +val thdBbot    = mk_beta_rl "thd(bot) = bot";
    1.85 +
    1.86 +val ncaseBzero = mk_beta_rl "ncase(zero,t,u) = t";
    1.87 +val ncaseBsucc = mk_beta_rl "ncase(succ(n),t,u) = u(n)";
    1.88 +val ncaseBbot  = mk_beta_rl "ncase(bot,t,u) = bot";
    1.89 +val nrecBzero  = mk_beta_rl "nrec(zero,t,u) = t";
    1.90 +val nrecBsucc  = mk_beta_rl "nrec(succ(n),t,u) = u(n,nrec(n,t,u))";
    1.91 +val nrecBbot   = mk_beta_rl "nrec(bot,t,u) = bot";
    1.92 +
    1.93 +val lcaseBnil  = mk_beta_rl "lcase([],t,u) = t";
    1.94 +val lcaseBcons = mk_beta_rl "lcase(x.xs,t,u) = u(x,xs)";
    1.95 +val lcaseBbot  = mk_beta_rl "lcase(bot,t,u) = bot";
    1.96 +val lrecBnil   = mk_beta_rl "lrec([],t,u) = t";
    1.97 +val lrecBcons  = mk_beta_rl "lrec(x.xs,t,u) = u(x,xs,lrec(xs,t,u))";
    1.98 +val lrecBbot   = mk_beta_rl "lrec(bot,t,u) = bot";
    1.99 +
   1.100 +val letrec2B = raw_mk_beta_rl (data_defs @ [letrec2_def])
   1.101 +       "letrec g x y be h(x,y,g) in g(p,q) = \
   1.102 +\                     h(p,q,%u v.letrec g x y be h(x,y,g) in g(u,v))";
   1.103 +val letrec3B = raw_mk_beta_rl (data_defs @ [letrec3_def])
   1.104 +       "letrec g x y z be h(x,y,z,g) in g(p,q,r) = \
   1.105 +\                     h(p,q,r,%u v w.letrec g x y z be h(x,y,z,g) in g(u,v,w))";
   1.106 +
   1.107 +val napplyBzero   = mk_beta_rl "f^zero`a = a";
   1.108 +val napplyBsucc   = mk_beta_rl "f^succ(n)`a = f(f^n`a)";
   1.109 +
   1.110 +val termBs = [letB,applyB,applyBbot,splitB,splitBbot,
   1.111 +              fstB,fstBbot,sndB,sndBbot,thdB,thdBbot,
   1.112 +              ifBtrue,ifBfalse,ifBbot,whenBinl,whenBinr,whenBbot,
   1.113 +              ncaseBzero,ncaseBsucc,ncaseBbot,nrecBzero,nrecBsucc,nrecBbot,
   1.114 +              lcaseBnil,lcaseBcons,lcaseBbot,lrecBnil,lrecBcons,lrecBbot,
   1.115 +              napplyBzero,napplyBsucc];
   1.116 +
   1.117 +(*** Constructors are injective ***)
   1.118 +
   1.119 +val term_injs = map (mk_inj_rl Term.thy 
   1.120 +                             [applyB,splitB,whenBinl,whenBinr,ncaseBsucc,lcaseBcons] 
   1.121 +                             (ccl_congs @ term_congs))
   1.122 +               ["(inl(a) = inl(a')) <-> (a=a')",
   1.123 +                "(inr(a) = inr(a')) <-> (a=a')",
   1.124 +                "(succ(a) = succ(a')) <-> (a=a')",
   1.125 +                "(a.b = a'.b') <-> (a=a' & b=b')"];
   1.126 +
   1.127 +(*** Constructors are distinct ***)
   1.128 +
   1.129 +val term_dstncts = mkall_dstnct_thms Term.thy data_defs (ccl_injs @ term_injs)
   1.130 +                    [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op ."]];
   1.131 +
   1.132 +(*** Rules for pre-order [= ***)
   1.133 +
   1.134 +local
   1.135 +  fun mk_thm s = prove_goalw Term.thy data_defs s (fn _ => 
   1.136 +                  [SIMP_TAC (ccl_ss addrews (ccl_porews)) 1]);
   1.137 +in
   1.138 +  val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
   1.139 +                                "inr(b) [= inr(b') <-> b [= b'",
   1.140 +                                "succ(n) [= succ(n') <-> n [= n'",
   1.141 +                                "x.xs [= x'.xs' <-> x [= x'  & xs [= xs'"];
   1.142 +end;
   1.143 +
   1.144 +(*** Rewriting and Proving ***)
   1.145 +
   1.146 +val term_rews = termBs @ term_injs @ term_dstncts @ ccl_porews @ term_porews;
   1.147 +val term_ss = ccl_ss addrews term_rews addcongs term_congs;
   1.148 +
   1.149 +val term_cs = ccl_cs addSEs (term_dstncts RL [notE]) addSDs (XH_to_Ds term_injs);