src/CCL/fix.ML
changeset 0 a5a9c433f639
child 8 c3d2c6dcf3f0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/fix.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,202 @@
     1.4 +(*  Title: 	CCL/fix
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Martin Coen, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +For fix.thy.
    1.10 +*)
    1.11 +
    1.12 +open Fix;
    1.13 +
    1.14 +val prems = goalw Fix.thy [INCL_def]
    1.15 +     "[| !!x.P(x) <-> Q(x) |] ==> INCL(%x.P(x)) <-> INCL(%x.Q(x))";
    1.16 +by (REPEAT (ares_tac ([refl] @ FOL_congs @ set_congs @ prems) 1));
    1.17 +val INCL_cong = result();
    1.18 +
    1.19 +val fix_congs = [INCL_cong] @ ccl_mk_congs Fix.thy ["napply"];
    1.20 +
    1.21 +(*** Fixed Point Induction ***)
    1.22 +
    1.23 +val [base,step,incl] = goalw Fix.thy [INCL_def]
    1.24 +    "[| P(bot);  !!x.P(x) ==> P(f(x));  INCL(P) |] ==> P(fix(f))";
    1.25 +br (incl RS spec RS mp) 1;
    1.26 +by (rtac (Nat_ind RS ballI) 1 THEN atac 1);
    1.27 +by (ALLGOALS (SIMP_TAC term_ss));
    1.28 +by (REPEAT (ares_tac [base,step] 1));
    1.29 +val fix_ind = result();
    1.30 +
    1.31 +(*** Inclusive Predicates ***)
    1.32 +
    1.33 +val prems = goalw Fix.thy [INCL_def]
    1.34 +     "INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))";
    1.35 +br iff_refl 1;
    1.36 +val inclXH = result();
    1.37 +
    1.38 +val prems = goal Fix.thy
    1.39 +     "[| !!f.ALL n:Nat.P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x.P(x))";
    1.40 +by (fast_tac (term_cs addIs (prems @ [XH_to_I inclXH])) 1);
    1.41 +val inclI = result();
    1.42 +
    1.43 +val incl::prems = goal Fix.thy
    1.44 +     "[| INCL(P);  !!n.n:Nat ==> P(f^n`bot) |] ==> P(fix(f))";
    1.45 +by (fast_tac (term_cs addIs ([ballI RS (incl RS (XH_to_D inclXH) RS spec RS mp)] 
    1.46 +                       @ prems)) 1);
    1.47 +val inclD = result();
    1.48 +
    1.49 +val incl::prems = goal Fix.thy
    1.50 +     "[| INCL(P);  (ALL n:Nat.P(f^n`bot))-->P(fix(f)) ==> R |] ==> R";
    1.51 +by (fast_tac (term_cs addIs ([incl RS inclD] @ prems)) 1);
    1.52 +val inclE = result();
    1.53 +
    1.54 +val fix_ss = term_ss addcongs fix_congs;
    1.55 +
    1.56 +(*** Lemmas for Inclusive Predicates ***)
    1.57 +
    1.58 +goal Fix.thy "INCL(%x.~ a(x) [= t)";
    1.59 +br inclI 1;
    1.60 +bd bspec 1;
    1.61 +br zeroT 1;
    1.62 +be contrapos 1;
    1.63 +br po_trans 1;
    1.64 +ba 2;
    1.65 +br (napplyBzero RS ssubst) 1;
    1.66 +by (rtac po_cong 1 THEN rtac po_bot 1);
    1.67 +val npo_INCL = result();
    1.68 +
    1.69 +val prems = goal Fix.thy "[| INCL(P);  INCL(Q) |] ==> INCL(%x.P(x) & Q(x))";
    1.70 +by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
    1.71 +val conj_INCL = result();
    1.72 +
    1.73 +val prems = goal Fix.thy "[| !!a.INCL(P(a)) |] ==> INCL(%x.ALL a.P(a,x))";
    1.74 +by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
    1.75 +val all_INCL = result();
    1.76 +
    1.77 +val prems = goal Fix.thy "[| !!a.a:A ==> INCL(P(a)) |] ==> INCL(%x.ALL a:A.P(a,x))";
    1.78 +by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
    1.79 +val ball_INCL = result();
    1.80 +
    1.81 +goal Fix.thy "INCL(%x.a(x) = b(x)::'a::prog)";
    1.82 +by (SIMP_TAC (fix_ss addrews [eq_iff]) 1);
    1.83 +by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1));
    1.84 +val eq_INCL = result();
    1.85 +
    1.86 +(*** Derivation of Reachability Condition ***)
    1.87 +
    1.88 +(* Fixed points of idgen *)
    1.89 +
    1.90 +goal Fix.thy "idgen(fix(idgen)) = fix(idgen)";
    1.91 +br (fixB RS sym) 1;
    1.92 +val fix_idgenfp = result();
    1.93 +
    1.94 +goalw Fix.thy [idgen_def] "idgen(lam x.x) = lam x.x";
    1.95 +by (SIMP_TAC term_ss 1);
    1.96 +br (term_case RS allI) 1;
    1.97 +by (ALLGOALS (SIMP_TAC term_ss));
    1.98 +val id_idgenfp = result();
    1.99 +
   1.100 +(* All fixed points are lam-expressions *)
   1.101 +
   1.102 +val [prem] = goal Fix.thy "idgen(d) = d ==> d = lam x.?f(x)";
   1.103 +br (prem RS subst) 1;
   1.104 +bw idgen_def;
   1.105 +br refl 1;
   1.106 +val idgenfp_lam = result();
   1.107 +
   1.108 +(* Lemmas for rewriting fixed points of idgen *)
   1.109 +
   1.110 +val prems = goalw Fix.thy [idgen_def] 
   1.111 +    "[| a = b;  a ` t = u |] ==> b ` t = u";
   1.112 +by (SIMP_TAC (term_ss addrews (prems RL [sym])) 1);
   1.113 +val l_lemma= result();
   1.114 +
   1.115 +val idgen_lemmas =
   1.116 +    let fun mk_thm s = prove_goalw Fix.thy [idgen_def] s
   1.117 +           (fn [prem] => [rtac (prem RS l_lemma) 1,SIMP_TAC term_ss 1])
   1.118 +    in map mk_thm
   1.119 +          [    "idgen(d) = d ==> d ` bot = bot",
   1.120 +               "idgen(d) = d ==> d ` true = true",
   1.121 +               "idgen(d) = d ==> d ` false = false",
   1.122 +               "idgen(d) = d ==> d ` <a,b> = <d ` a,d ` b>",
   1.123 +               "idgen(d) = d ==> d ` (lam x.f(x)) = lam x.d ` f(x)"]
   1.124 +    end;
   1.125 +
   1.126 +(* Proof of Reachability law - show that fix and lam x.x both give LEAST fixed points 
   1.127 +                               of idgen and hence are they same *)
   1.128 +
   1.129 +val [p1,p2,p3] = goal CCL.thy
   1.130 +    "[| ALL x.t ` x [= u ` x;  EX f.t=lam x.f(x);  EX f.u=lam x.f(x) |] ==> t [= u";
   1.131 +br (p2 RS cond_eta RS ssubst) 1;
   1.132 +br (p3 RS cond_eta RS ssubst) 1;
   1.133 +br (p1 RS (po_lam RS iffD2)) 1;
   1.134 +val po_eta = result();
   1.135 +
   1.136 +val [prem] = goalw Fix.thy [idgen_def] "idgen(d) = d ==> d = lam x.?f(x)";
   1.137 +br (prem RS subst) 1;
   1.138 +br refl 1;
   1.139 +val po_eta_lemma = result();
   1.140 +
   1.141 +val [prem] = goal Fix.thy
   1.142 +    "idgen(d) = d ==> \
   1.143 +\      {p.EX a b.p=<a,b> & (EX t.a=fix(idgen) ` t & b = d ` t)} <=   \
   1.144 +\      POgen({p.EX a b.p=<a,b> & (EX t.a=fix(idgen) ` t  & b = d ` t)})";
   1.145 +by (REPEAT (step_tac term_cs 1));
   1.146 +by (term_case_tac "t" 1);
   1.147 +by (ALLGOALS (SIMP_TAC (term_ss addrews (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas)))));
   1.148 +by (ALLGOALS (fast_tac set_cs));
   1.149 +val lemma1 = result();
   1.150 +
   1.151 +val [prem] = goal Fix.thy
   1.152 +    "idgen(d) = d ==> fix(idgen) [= d";
   1.153 +br (allI RS po_eta) 1;
   1.154 +br (lemma1 RSN(2,po_coinduct)) 1;
   1.155 +by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
   1.156 +val fix_least_idgen = result();
   1.157 +
   1.158 +val [prem] = goal Fix.thy
   1.159 +    "idgen(d) = d ==> \
   1.160 +\      {p.EX a b.p=<a,b> & b = d ` a} <= POgen({p.EX a b.p=<a,b> & b = d ` a})";
   1.161 +by (REPEAT (step_tac term_cs 1));
   1.162 +by (term_case_tac "a" 1);
   1.163 +by (ALLGOALS (SIMP_TAC (term_ss addrews (POgenXH::([prem] RL idgen_lemmas)))));
   1.164 +by (ALLGOALS (fast_tac set_cs));
   1.165 +val lemma2 = result();
   1.166 +
   1.167 +val [prem] = goal Fix.thy
   1.168 +    "idgen(d) = d ==> lam x.x [= d";
   1.169 +br (allI RS po_eta) 1;
   1.170 +br (lemma2 RSN(2,po_coinduct)) 1;
   1.171 +by (SIMP_TAC term_ss 1);
   1.172 +by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
   1.173 +val id_least_idgen = result();
   1.174 +
   1.175 +goal Fix.thy  "fix(idgen) = lam x.x";
   1.176 +by (fast_tac (term_cs addIs [eq_iff RS iffD2,
   1.177 +                             id_idgenfp RS fix_least_idgen,
   1.178 +                             fix_idgenfp RS id_least_idgen]) 1);
   1.179 +val reachability = result();
   1.180 +
   1.181 +(********)
   1.182 +
   1.183 +val [prem] = goal Fix.thy "f = lam x.x ==> f`t = t";
   1.184 +br (prem RS sym RS subst) 1;
   1.185 +br applyB 1;
   1.186 +val id_apply = result();
   1.187 +
   1.188 +val prems = goal Fix.thy
   1.189 +     "[| P(bot);  P(true);  P(false);  \
   1.190 +\        !!x y.[| P(x);  P(y) |] ==> P(<x,y>);  \
   1.191 +\        !!u.(!!x.P(u(x))) ==> P(lam x.u(x));  INCL(P) |] ==> \
   1.192 +\     P(t)";
   1.193 +br (reachability RS id_apply RS subst) 1;
   1.194 +by (res_inst_tac [("x","t")] spec 1);
   1.195 +br fix_ind 1;
   1.196 +bw idgen_def;
   1.197 +by (REPEAT_SOME (ares_tac [allI]));
   1.198 +br (applyBbot RS ssubst) 1;
   1.199 +brs prems 1;
   1.200 +br (applyB RS ssubst )1;
   1.201 +by (res_inst_tac [("t","xa")] term_case 1);
   1.202 +by (ALLGOALS (SIMP_TAC term_ss));
   1.203 +by (ALLGOALS (fast_tac (term_cs addIs ([all_INCL,INCL_subst] @ prems))));
   1.204 +val term_ind = result();
   1.205 +