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