src/CCL/Fix.ML
author clasohm
Wed Nov 30 13:53:46 1994 +0100 (1994-11-30)
changeset 757 2ca12511676d
parent 642 0db578095e6a
child 1459 d12da312eff4
permissions -rw-r--r--
added qed and qed_goal[w]
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))";
lcp@642
    15
by (rtac (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@757
    19
qed "fix_ind";
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)))";
lcp@642
    25
by (rtac iff_refl 1);
clasohm@757
    26
qed "inclXH";
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@757
    31
qed "inclI";
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@757
    37
qed "inclD";
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@757
    42
qed "inclE";
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)";
lcp@642
    48
by (rtac inclI 1);
lcp@642
    49
by (dtac bspec 1);
lcp@642
    50
by (rtac zeroT 1);
lcp@642
    51
by (etac contrapos 1);
lcp@642
    52
by (rtac po_trans 1);
lcp@642
    53
by (assume_tac 2);
lcp@642
    54
by (rtac (napplyBzero RS ssubst) 1);
clasohm@0
    55
by (rtac po_cong 1 THEN rtac po_bot 1);
clasohm@757
    56
qed "npo_INCL";
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@757
    60
qed "conj_INCL";
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@757
    64
qed "all_INCL";
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@757
    68
qed "ball_INCL";
clasohm@0
    69
clasohm@442
    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@757
    73
qed "eq_INCL";
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)";
lcp@642
    80
by (rtac (fixB RS sym) 1);
clasohm@757
    81
qed "fix_idgenfp";
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);
lcp@642
    85
by (rtac (term_case RS allI) 1);
lcp@8
    86
by (ALLGOALS (simp_tac term_ss));
clasohm@757
    87
qed "id_idgenfp";
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)";
lcp@642
    92
by (rtac (prem RS subst) 1);
lcp@642
    93
by (rewtac idgen_def);
lcp@642
    94
by (rtac refl 1);
clasohm@757
    95
qed "idgenfp_lam";
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@757
   102
qed "l_lemma";
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";
lcp@642
   120
by (rtac (p2 RS cond_eta RS ssubst) 1);
lcp@642
   121
by (rtac (p3 RS cond_eta RS ssubst) 1);
lcp@642
   122
by (rtac (p1 RS (po_lam RS iffD2)) 1);
clasohm@757
   123
qed "po_eta";
clasohm@0
   124
clasohm@0
   125
val [prem] = goalw Fix.thy [idgen_def] "idgen(d) = d ==> d = lam x.?f(x)";
lcp@642
   126
by (rtac (prem RS subst) 1);
lcp@642
   127
by (rtac refl 1);
clasohm@757
   128
qed "po_eta_lemma";
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@757
   138
qed "lemma1";
clasohm@0
   139
clasohm@0
   140
val [prem] = goal Fix.thy
clasohm@0
   141
    "idgen(d) = d ==> fix(idgen) [= d";
lcp@642
   142
by (rtac (allI RS po_eta) 1);
lcp@642
   143
by (rtac (lemma1 RSN(2,po_coinduct)) 1);
clasohm@0
   144
by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
clasohm@757
   145
qed "fix_least_idgen";
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@757
   154
qed "lemma2";
clasohm@0
   155
clasohm@0
   156
val [prem] = goal Fix.thy
clasohm@0
   157
    "idgen(d) = d ==> lam x.x [= d";
lcp@642
   158
by (rtac (allI RS po_eta) 1);
lcp@642
   159
by (rtac (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@757
   162
qed "id_least_idgen";
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@757
   168
qed "reachability";
clasohm@0
   169
clasohm@0
   170
(********)
clasohm@0
   171
clasohm@0
   172
val [prem] = goal Fix.thy "f = lam x.x ==> f`t = t";
lcp@642
   173
by (rtac (prem RS sym RS subst) 1);
lcp@642
   174
by (rtac applyB 1);
clasohm@757
   175
qed "id_apply";
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)";
lcp@642
   182
by (rtac (reachability RS id_apply RS subst) 1);
clasohm@0
   183
by (res_inst_tac [("x","t")] spec 1);
lcp@642
   184
by (rtac fix_ind 1);
lcp@642
   185
by (rewtac idgen_def);
clasohm@0
   186
by (REPEAT_SOME (ares_tac [allI]));
lcp@642
   187
by (rtac (applyBbot RS ssubst) 1);
lcp@642
   188
by (resolve_tac 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@757
   193
qed "term_ind";
clasohm@0
   194