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