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