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