src/CCL/fix.ML
author wenzelm
Mon, 25 Feb 2002 20:46:09 +0100
changeset 12936 84eb6c75cfe3
parent 8 c3d2c6dcf3f0
permissions -rw-r--r--
clarify module dependencies;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	CCL/fix
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Martin Coen, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
For fix.thy.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open Fix;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
(*** Fixed Point Induction ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
val [base,step,incl] = goalw Fix.thy [INCL_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
    "[| P(bot);  !!x.P(x) ==> P(f(x));  INCL(P) |] ==> P(fix(f))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
br (incl RS spec RS mp) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
by (rtac (Nat_ind RS ballI) 1 THEN atac 1);
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
    17
by (ALLGOALS (simp_tac term_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
by (REPEAT (ares_tac [base,step] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
val fix_ind = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
(*** Inclusive Predicates ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
val prems = goalw Fix.thy [INCL_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
     "INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
br iff_refl 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
val inclXH = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
val prems = goal Fix.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
     "[| !!f.ALL n:Nat.P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x.P(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
by (fast_tac (term_cs addIs (prems @ [XH_to_I inclXH])) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
val inclI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
val incl::prems = goal Fix.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
     "[| INCL(P);  !!n.n:Nat ==> P(f^n`bot) |] ==> P(fix(f))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
by (fast_tac (term_cs addIs ([ballI RS (incl RS (XH_to_D inclXH) RS spec RS mp)] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
                       @ prems)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
val inclD = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
val incl::prems = goal Fix.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
     "[| INCL(P);  (ALL n:Nat.P(f^n`bot))-->P(fix(f)) ==> R |] ==> R";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
by (fast_tac (term_cs addIs ([incl RS inclD] @ prems)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
val inclE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
(*** Lemmas for Inclusive Predicates ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
goal Fix.thy "INCL(%x.~ a(x) [= t)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
br inclI 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
bd bspec 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
br zeroT 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
be contrapos 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
br po_trans 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
ba 2;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
br (napplyBzero RS ssubst) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
by (rtac po_cong 1 THEN rtac po_bot 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
val npo_INCL = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
val prems = goal Fix.thy "[| INCL(P);  INCL(Q) |] ==> INCL(%x.P(x) & Q(x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
val conj_INCL = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
val prems = goal Fix.thy "[| !!a.INCL(P(a)) |] ==> INCL(%x.ALL a.P(a,x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
val all_INCL = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
val prems = goal Fix.thy "[| !!a.a:A ==> INCL(P(a)) |] ==> INCL(%x.ALL a:A.P(a,x))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
val ball_INCL = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
goal Fix.thy "INCL(%x.a(x) = b(x)::'a::prog)";
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
    71
by (simp_tac (term_ss addsimps [eq_iff]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
val eq_INCL = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
(*** Derivation of Reachability Condition ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
(* Fixed points of idgen *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
goal Fix.thy "idgen(fix(idgen)) = fix(idgen)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
br (fixB RS sym) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
val fix_idgenfp = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
goalw Fix.thy [idgen_def] "idgen(lam x.x) = lam x.x";
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
    84
by (simp_tac term_ss 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
br (term_case RS allI) 1;
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
    86
by (ALLGOALS (simp_tac term_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
val id_idgenfp = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
(* All fixed points are lam-expressions *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
val [prem] = goal Fix.thy "idgen(d) = d ==> d = lam x.?f(x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
br (prem RS subst) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
bw idgen_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
br refl 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
val idgenfp_lam = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
(* Lemmas for rewriting fixed points of idgen *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
val prems = goalw Fix.thy [idgen_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
    "[| a = b;  a ` t = u |] ==> b ` t = u";
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   101
by (simp_tac (term_ss addsimps (prems RL [sym])) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
val l_lemma= result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
val idgen_lemmas =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
    let fun mk_thm s = prove_goalw Fix.thy [idgen_def] s
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   106
           (fn [prem] => [rtac (prem RS l_lemma) 1,simp_tac term_ss 1])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
    in map mk_thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
          [    "idgen(d) = d ==> d ` bot = bot",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
               "idgen(d) = d ==> d ` true = true",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
               "idgen(d) = d ==> d ` false = false",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
               "idgen(d) = d ==> d ` <a,b> = <d ` a,d ` b>",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
               "idgen(d) = d ==> d ` (lam x.f(x)) = lam x.d ` f(x)"]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
(* Proof of Reachability law - show that fix and lam x.x both give LEAST fixed points 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
                               of idgen and hence are they same *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
val [p1,p2,p3] = goal CCL.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
    "[| ALL x.t ` x [= u ` x;  EX f.t=lam x.f(x);  EX f.u=lam x.f(x) |] ==> t [= u";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
br (p2 RS cond_eta RS ssubst) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
br (p3 RS cond_eta RS ssubst) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
br (p1 RS (po_lam RS iffD2)) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
val po_eta = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
val [prem] = goalw Fix.thy [idgen_def] "idgen(d) = d ==> d = lam x.?f(x)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
br (prem RS subst) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
br refl 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
val po_eta_lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
val [prem] = goal Fix.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
    "idgen(d) = d ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
\      {p.EX a b.p=<a,b> & (EX t.a=fix(idgen) ` t & b = d ` t)} <=   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
\      POgen({p.EX a b.p=<a,b> & (EX t.a=fix(idgen) ` t  & b = d ` t)})";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
by (REPEAT (step_tac term_cs 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
by (term_case_tac "t" 1);
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   136
by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas)))));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
by (ALLGOALS (fast_tac set_cs));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
val lemma1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
val [prem] = goal Fix.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
    "idgen(d) = d ==> fix(idgen) [= d";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
br (allI RS po_eta) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
br (lemma1 RSN(2,po_coinduct)) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
val fix_least_idgen = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
val [prem] = goal Fix.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
    "idgen(d) = d ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
\      {p.EX a b.p=<a,b> & b = d ` a} <= POgen({p.EX a b.p=<a,b> & b = d ` a})";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
by (REPEAT (step_tac term_cs 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
by (term_case_tac "a" 1);
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   152
by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem] RL idgen_lemmas)))));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
by (ALLGOALS (fast_tac set_cs));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
val lemma2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
val [prem] = goal Fix.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
    "idgen(d) = d ==> lam x.x [= d";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
br (allI RS po_eta) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
br (lemma2 RSN(2,po_coinduct)) 1;
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   160
by (simp_tac term_ss 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
val id_least_idgen = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
goal Fix.thy  "fix(idgen) = lam x.x";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
by (fast_tac (term_cs addIs [eq_iff RS iffD2,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
                             id_idgenfp RS fix_least_idgen,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
                             fix_idgenfp RS id_least_idgen]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
val reachability = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
(********)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
val [prem] = goal Fix.thy "f = lam x.x ==> f`t = t";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
br (prem RS sym RS subst) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
br applyB 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
val id_apply = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
val prems = goal Fix.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
     "[| P(bot);  P(true);  P(false);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
\        !!x y.[| P(x);  P(y) |] ==> P(<x,y>);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
\        !!u.(!!x.P(u(x))) ==> P(lam x.u(x));  INCL(P) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
\     P(t)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
br (reachability RS id_apply RS subst) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
by (res_inst_tac [("x","t")] spec 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
br fix_ind 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
bw idgen_def;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
by (REPEAT_SOME (ares_tac [allI]));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
br (applyBbot RS ssubst) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
brs prems 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
br (applyB RS ssubst )1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
by (res_inst_tac [("t","xa")] term_case 1);
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   191
by (ALLGOALS (simp_tac term_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
by (ALLGOALS (fast_tac (term_cs addIs ([all_INCL,INCL_subst] @ prems))));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
val term_ind = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194