src/CCL/term.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 289 78541329ff35
permissions -rw-r--r--
tidying
     1 (*  Title: 	CCL/terms
     2     ID:         $Id$
     3     Author: 	Martin Coen, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 For terms.thy.
     7 *)
     8 
     9 open Term;
    10 
    11 val simp_can_defs = [one_def,inl_def,inr_def];
    12 val simp_ncan_defs = [if_def,when_def,split_def,fst_def,snd_def,thd_def];
    13 val simp_defs = simp_can_defs @ simp_ncan_defs;
    14 
    15 val ind_can_defs = [zero_def,succ_def,nil_def,cons_def];
    16 val ind_ncan_defs = [ncase_def,nrec_def,lcase_def,lrec_def];
    17 val ind_defs = ind_can_defs @ ind_ncan_defs;
    18 
    19 val data_defs = simp_defs @ ind_defs @ [napply_def];
    20 val genrec_defs = [letrec_def,letrec2_def,letrec3_def];
    21 
    22 (*** Beta Rules, including strictness ***)
    23 
    24 goalw Term.thy [let_def] "~ t=bot--> let x be t in f(x) = f(t)";
    25 by (res_inst_tac [("t","t")] term_case 1);
    26 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
    27 val letB = result() RS mp;
    28 
    29 goalw Term.thy [let_def] "let x be bot in f(x) = bot";
    30 br caseBbot 1;
    31 val letBabot = result();
    32 
    33 goalw Term.thy [let_def] "let x be t in bot = bot";
    34 brs ([caseBbot] RL [term_case]) 1;
    35 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
    36 val letBbbot = result();
    37 
    38 goalw Term.thy [apply_def] "(lam x.b(x)) ` a = b(a)";
    39 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
    40 val applyB = result();
    41 
    42 goalw Term.thy [apply_def] "bot ` a = bot";
    43 br caseBbot 1;
    44 val applyBbot = result();
    45 
    46 goalw Term.thy [fix_def] "fix(f) = f(fix(f))";
    47 by (resolve_tac [applyB RS ssubst] 1 THEN resolve_tac [refl] 1);
    48 val fixB = result();
    49 
    50 goalw Term.thy [letrec_def]
    51       "letrec g x be h(x,g) in g(a) = h(a,%y.letrec g x be h(x,g) in g(y))";
    52 by (resolve_tac [fixB RS ssubst] 1 THEN 
    53     resolve_tac [applyB RS ssubst] 1 THEN resolve_tac [refl] 1);
    54 val letrecB = result();
    55 
    56 val rawBs = caseBs @ [applyB,applyBbot];
    57 
    58 fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
    59            (fn _ => [rtac (letrecB RS ssubst) 1,
    60 		     simp_tac (CCL_ss addsimps rawBs) 1]);
    61 fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
    62 
    63 fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
    64            (fn _ => [simp_tac (CCL_ss addsimps rawBs 
    65 			       setloop (rtac (letrecB RS ssubst))) 1]);
    66 fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
    67 
    68 val ifBtrue    = mk_beta_rl "if true then t else u = t";
    69 val ifBfalse   = mk_beta_rl "if false then t else u = u";
    70 val ifBbot     = mk_beta_rl "if bot then t else u = bot";
    71 
    72 val whenBinl   = mk_beta_rl "when(inl(a),t,u) = t(a)";
    73 val whenBinr   = mk_beta_rl "when(inr(a),t,u) = u(a)";
    74 val whenBbot   = mk_beta_rl "when(bot,t,u) = bot";
    75 
    76 val splitB     = mk_beta_rl "split(<a,b>,h) = h(a,b)";
    77 val splitBbot  = mk_beta_rl "split(bot,h) = bot";
    78 val fstB       = mk_beta_rl "fst(<a,b>) = a";
    79 val fstBbot    = mk_beta_rl "fst(bot) = bot";
    80 val sndB       = mk_beta_rl "snd(<a,b>) = b";
    81 val sndBbot    = mk_beta_rl "snd(bot) = bot";
    82 val thdB       = mk_beta_rl "thd(<a,<b,c>>) = c";
    83 val thdBbot    = mk_beta_rl "thd(bot) = bot";
    84 
    85 val ncaseBzero = mk_beta_rl "ncase(zero,t,u) = t";
    86 val ncaseBsucc = mk_beta_rl "ncase(succ(n),t,u) = u(n)";
    87 val ncaseBbot  = mk_beta_rl "ncase(bot,t,u) = bot";
    88 val nrecBzero  = mk_beta_rl "nrec(zero,t,u) = t";
    89 val nrecBsucc  = mk_beta_rl "nrec(succ(n),t,u) = u(n,nrec(n,t,u))";
    90 val nrecBbot   = mk_beta_rl "nrec(bot,t,u) = bot";
    91 
    92 val lcaseBnil  = mk_beta_rl "lcase([],t,u) = t";
    93 val lcaseBcons = mk_beta_rl "lcase(x$xs,t,u) = u(x,xs)";
    94 val lcaseBbot  = mk_beta_rl "lcase(bot,t,u) = bot";
    95 val lrecBnil   = mk_beta_rl "lrec([],t,u) = t";
    96 val lrecBcons  = mk_beta_rl "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))";
    97 val lrecBbot   = mk_beta_rl "lrec(bot,t,u) = bot";
    98 
    99 val letrec2B = raw_mk_beta_rl (data_defs @ [letrec2_def])
   100        "letrec g x y be h(x,y,g) in g(p,q) = \
   101 \                     h(p,q,%u v.letrec g x y be h(x,y,g) in g(u,v))";
   102 val letrec3B = raw_mk_beta_rl (data_defs @ [letrec3_def])
   103        "letrec g x y z be h(x,y,z,g) in g(p,q,r) = \
   104 \                     h(p,q,r,%u v w.letrec g x y z be h(x,y,z,g) in g(u,v,w))";
   105 
   106 val napplyBzero   = mk_beta_rl "f^zero`a = a";
   107 val napplyBsucc   = mk_beta_rl "f^succ(n)`a = f(f^n`a)";
   108 
   109 val termBs = [letB,applyB,applyBbot,splitB,splitBbot,
   110               fstB,fstBbot,sndB,sndBbot,thdB,thdBbot,
   111               ifBtrue,ifBfalse,ifBbot,whenBinl,whenBinr,whenBbot,
   112               ncaseBzero,ncaseBsucc,ncaseBbot,nrecBzero,nrecBsucc,nrecBbot,
   113               lcaseBnil,lcaseBcons,lcaseBbot,lrecBnil,lrecBcons,lrecBbot,
   114               napplyBzero,napplyBsucc];
   115 
   116 (*** Constructors are injective ***)
   117 
   118 val term_injs = map (mk_inj_rl Term.thy 
   119 		     [applyB,splitB,whenBinl,whenBinr,ncaseBsucc,lcaseBcons])
   120                ["(inl(a) = inl(a')) <-> (a=a')",
   121                 "(inr(a) = inr(a')) <-> (a=a')",
   122                 "(succ(a) = succ(a')) <-> (a=a')",
   123                 "(a$b = a'$b') <-> (a=a' & b=b')"];
   124 
   125 (*** Constructors are distinct ***)
   126 
   127 val term_dstncts = mkall_dstnct_thms Term.thy data_defs (ccl_injs @ term_injs)
   128                     [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op $"]];
   129 
   130 (*** Rules for pre-order [= ***)
   131 
   132 local
   133   fun mk_thm s = prove_goalw Term.thy data_defs s (fn _ => 
   134                   [simp_tac (ccl_ss addsimps (ccl_porews)) 1]);
   135 in
   136   val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
   137                                 "inr(b) [= inr(b') <-> b [= b'",
   138                                 "succ(n) [= succ(n') <-> n [= n'",
   139                                 "x$xs [= x'$xs' <-> x [= x'  & xs [= xs'"];
   140 end;
   141 
   142 (*** Rewriting and Proving ***)
   143 
   144 val term_rews = termBs @ term_injs @ term_dstncts @ ccl_porews @ term_porews;
   145 val term_ss = ccl_ss addsimps term_rews;
   146 
   147 val term_cs = ccl_cs addSEs (term_dstncts RL [notE]) 
   148                      addSDs (XH_to_Ds term_injs);