src/CCL/Term.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5062 fbdb0b541314
child 17456 bcf7544875b2
permissions -rw-r--r--
tidying
clasohm@1459
     1
(*  Title:      CCL/terms
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     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
wenzelm@5062
    24
Goalw [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@1087
    27
bind_thm("letB", result() RS mp);
clasohm@0
    28
wenzelm@5062
    29
Goalw [let_def] "let x be bot in f(x) = bot";
lcp@642
    30
by (rtac caseBbot 1);
clasohm@757
    31
qed "letBabot";
clasohm@0
    32
wenzelm@5062
    33
Goalw [let_def] "let x be t in bot = bot";
lcp@642
    34
by (resolve_tac ([caseBbot] RL [term_case]) 1);
lcp@8
    35
by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
clasohm@757
    36
qed "letBbbot";
clasohm@0
    37
wenzelm@5062
    38
Goalw [apply_def] "(lam x. b(x)) ` a = b(a)";
lcp@8
    39
by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
clasohm@757
    40
qed "applyB";
clasohm@0
    41
wenzelm@5062
    42
Goalw [apply_def] "bot ` a = bot";
lcp@642
    43
by (rtac caseBbot 1);
clasohm@757
    44
qed "applyBbot";
clasohm@0
    45
wenzelm@5062
    46
Goalw [fix_def] "fix(f) = f(fix(f))";
lcp@642
    47
by (resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
clasohm@757
    48
qed "fixB";
clasohm@0
    49
wenzelm@5062
    50
Goalw [letrec_def]
wenzelm@3837
    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 
lcp@642
    53
    resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
clasohm@757
    54
qed "letrecB";
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
paulson@2035
    59
           (fn _ => [stac letrecB 1,
clasohm@1459
    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 
paulson@2035
    65
                               setloop (stac letrecB)) 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@289
    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@289
    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) = \
wenzelm@3837
   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) = \
wenzelm@3837
   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 
clasohm@1459
   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@289
   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@289
   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@289
   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);