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