src/CCL/Fix.thy
author haftmann
Fri Jun 19 21:08:07 2009 +0200 (2009-06-19)
changeset 31726 ffd2dc631d88
parent 24825 c4f13ab78f9d
child 32153 a0e57fb1b930
permissions -rw-r--r--
merged
     1 (*  Title:      CCL/Fix.thy
     2     ID:         $Id$
     3     Author:     Martin Coen
     4     Copyright   1993  University of Cambridge
     5 *)
     6 
     7 header {* Tentative attempt at including fixed point induction; justified by Smith *}
     8 
     9 theory Fix
    10 imports Type
    11 begin
    12 
    13 consts
    14   idgen      ::       "[i]=>i"
    15   INCL      :: "[i=>o]=>o"
    16 
    17 defs
    18   idgen_def:
    19   "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
    20 
    21 axioms
    22   INCL_def:   "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
    23   po_INCL:    "INCL(%x. a(x) [= b(x))"
    24   INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
    25 
    26 
    27 subsection {* Fixed Point Induction *}
    28 
    29 lemma fix_ind:
    30   assumes base: "P(bot)"
    31     and step: "!!x. P(x) ==> P(f(x))"
    32     and incl: "INCL(P)"
    33   shows "P(fix(f))"
    34   apply (rule incl [unfolded INCL_def, rule_format])
    35   apply (rule Nat_ind [THEN ballI], assumption)
    36    apply simp_all
    37    apply (rule base)
    38   apply (erule step)
    39   done
    40 
    41 
    42 subsection {* Inclusive Predicates *}
    43 
    44 lemma inclXH: "INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))"
    45   by (simp add: INCL_def)
    46 
    47 lemma inclI: "[| !!f. ALL n:Nat. P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x. P(x))"
    48   unfolding inclXH by blast
    49 
    50 lemma inclD: "[| INCL(P);  !!n. n:Nat ==> P(f^n`bot) |] ==> P(fix(f))"
    51   unfolding inclXH by blast
    52 
    53 lemma inclE: "[| INCL(P);  (ALL n:Nat. P(f^n`bot))-->P(fix(f)) ==> R |] ==> R"
    54   by (blast dest: inclD)
    55 
    56 
    57 subsection {* Lemmas for Inclusive Predicates *}
    58 
    59 lemma npo_INCL: "INCL(%x.~ a(x) [= t)"
    60   apply (rule inclI)
    61   apply (drule bspec)
    62    apply (rule zeroT)
    63   apply (erule contrapos)
    64   apply (rule po_trans)
    65    prefer 2
    66    apply assumption
    67   apply (subst napplyBzero)
    68   apply (rule po_cong, rule po_bot)
    69   done
    70 
    71 lemma conj_INCL: "[| INCL(P);  INCL(Q) |] ==> INCL(%x. P(x) & Q(x))"
    72   by (blast intro!: inclI dest!: inclD)
    73 
    74 lemma all_INCL: "[| !!a. INCL(P(a)) |] ==> INCL(%x. ALL a. P(a,x))"
    75   by (blast intro!: inclI dest!: inclD)
    76 
    77 lemma ball_INCL: "[| !!a. a:A ==> INCL(P(a)) |] ==> INCL(%x. ALL a:A. P(a,x))"
    78   by (blast intro!: inclI dest!: inclD)
    79 
    80 lemma eq_INCL: "INCL(%x. a(x) = (b(x)::'a::prog))"
    81   apply (simp add: eq_iff)
    82   apply (rule conj_INCL po_INCL)+
    83   done
    84 
    85 
    86 subsection {* Derivation of Reachability Condition *}
    87 
    88 (* Fixed points of idgen *)
    89 
    90 lemma fix_idgenfp: "idgen(fix(idgen)) = fix(idgen)"
    91   apply (rule fixB [symmetric])
    92   done
    93 
    94 lemma id_idgenfp: "idgen(lam x. x) = lam x. x"
    95   apply (simp add: idgen_def)
    96   apply (rule term_case [THEN allI])
    97       apply simp_all
    98   done
    99 
   100 (* All fixed points are lam-expressions *)
   101 
   102 lemma idgenfp_lam: "idgen(d) = d ==> d = lam x. ?f(x)"
   103   apply (unfold idgen_def)
   104   apply (erule ssubst)
   105   apply (rule refl)
   106   done
   107 
   108 (* Lemmas for rewriting fixed points of idgen *)
   109 
   110 lemma l_lemma: "[| a = b;  a ` t = u |] ==> b ` t = u"
   111   by (simp add: idgen_def)
   112 
   113 lemma idgen_lemmas:
   114   "idgen(d) = d ==> d ` bot = bot"
   115   "idgen(d) = d ==> d ` true = true"
   116   "idgen(d) = d ==> d ` false = false"
   117   "idgen(d) = d ==> d ` <a,b> = <d ` a,d ` b>"
   118   "idgen(d) = d ==> d ` (lam x. f(x)) = lam x. d ` f(x)"
   119   by (erule l_lemma, simp add: idgen_def)+
   120 
   121 
   122 (* Proof of Reachability law - show that fix and lam x.x both give LEAST fixed points
   123   of idgen and hence are they same *)
   124 
   125 lemma po_eta:
   126   "[| ALL x. t ` x [= u ` x;  EX f. t=lam x. f(x);  EX f. u=lam x. f(x) |] ==> t [= u"
   127   apply (drule cond_eta)+
   128   apply (erule ssubst)
   129   apply (erule ssubst)
   130   apply (rule po_lam [THEN iffD2])
   131   apply simp
   132   done
   133 
   134 lemma po_eta_lemma: "idgen(d) = d ==> d = lam x. ?f(x)"
   135   apply (unfold idgen_def)
   136   apply (erule sym)
   137   done
   138 
   139 lemma lemma1:
   140   "idgen(d) = d ==>
   141     {p. EX a b. p=<a,b> & (EX t. a=fix(idgen) ` t & b = d ` t)} <=
   142       POgen({p. EX a b. p=<a,b> & (EX t. a=fix(idgen) ` t  & b = d ` t)})"
   143   apply clarify
   144   apply (rule_tac t = t in term_case)
   145       apply (simp_all add: POgenXH idgen_lemmas idgen_lemmas [OF fix_idgenfp])
   146    apply blast
   147   apply fast
   148   done
   149 
   150 lemma fix_least_idgen: "idgen(d) = d ==> fix(idgen) [= d"
   151   apply (rule allI [THEN po_eta])
   152     apply (rule lemma1 [THEN [2] po_coinduct])
   153      apply (blast intro: po_eta_lemma fix_idgenfp)+
   154   done
   155 
   156 lemma lemma2:
   157   "idgen(d) = d ==>
   158     {p. EX a b. p=<a,b> & b = d ` a} <= POgen({p. EX a b. p=<a,b> & b = d ` a})"
   159   apply clarify
   160   apply (rule_tac t = a in term_case)
   161       apply (simp_all add: POgenXH idgen_lemmas)
   162   apply fast
   163   done
   164 
   165 lemma id_least_idgen: "idgen(d) = d ==> lam x. x [= d"
   166   apply (rule allI [THEN po_eta])
   167     apply (rule lemma2 [THEN [2] po_coinduct])
   168      apply simp
   169     apply (fast intro: po_eta_lemma fix_idgenfp)+
   170   done
   171 
   172 lemma reachability: "fix(idgen) = lam x. x"
   173   apply (fast intro: eq_iff [THEN iffD2]
   174     id_idgenfp [THEN fix_least_idgen] fix_idgenfp [THEN id_least_idgen])
   175   done
   176 
   177 (********)
   178 
   179 lemma id_apply: "f = lam x. x ==> f`t = t"
   180   apply (erule ssubst)
   181   apply (rule applyB)
   182   done
   183 
   184 lemma term_ind:
   185   assumes 1: "P(bot)" and 2: "P(true)" and 3: "P(false)"
   186     and 4: "!!x y.[| P(x);  P(y) |] ==> P(<x,y>)"
   187     and 5: "!!u.(!!x. P(u(x))) ==> P(lam x. u(x))"
   188     and 6: "INCL(P)"
   189   shows "P(t)"
   190   apply (rule reachability [THEN id_apply, THEN subst])
   191   apply (rule_tac x = t in spec)
   192   apply (rule fix_ind)
   193     apply (unfold idgen_def)
   194     apply (rule allI)
   195     apply (subst applyBbot)
   196     apply (rule 1)
   197    apply (rule allI)
   198    apply (rule applyB [THEN ssubst])
   199     apply (rule_tac t = "xa" in term_case)
   200        apply simp_all
   201        apply (fast intro: assms INCL_subst all_INCL)+
   202   done
   203 
   204 end