src/CCL/Fix.thy
 author wenzelm Sat May 15 22:15:57 2010 +0200 (2010-05-15) changeset 36948 d2cdad45fd14 parent 36319 8feb2c4bef1a child 42156 df219e736a5d permissions -rw-r--r--
renamed Outer_Parse to Parse (in Scala);
```     1 (*  Title:      CCL/Fix.thy
```
```     2     Author:     Martin Coen
```
```     3     Copyright   1993  University of Cambridge
```
```     4 *)
```
```     5
```
```     6 header {* Tentative attempt at including fixed point induction; justified by Smith *}
```
```     7
```
```     8 theory Fix
```
```     9 imports Type
```
```    10 begin
```
```    11
```
```    12 consts
```
```    13   idgen      ::       "[i]=>i"
```
```    14   INCL      :: "[i=>o]=>o"
```
```    15
```
```    16 defs
```
```    17   idgen_def:
```
```    18   "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
```
```    19
```
```    20 axioms
```
```    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))"
```
```    23   INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
```
```    24
```
```    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 schematic_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 schematic_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 1: "P(bot)" and 2: "P(true)" and 3: "P(false)"
```
```   185     and 4: "!!x y.[| P(x);  P(y) |] ==> P(<x,y>)"
```
```   186     and 5: "!!u.(!!x. P(u(x))) ==> P(lam x. u(x))"
```
```   187     and 6: "INCL(P)"
```
```   188   shows "P(t)"
```
```   189   apply (rule reachability [THEN id_apply, THEN subst])
```
```   190   apply (rule_tac x = t in spec)
```
```   191   apply (rule fix_ind)
```
```   192     apply (unfold idgen_def)
```
```   193     apply (rule allI)
```
```   194     apply (subst applyBbot)
```
```   195     apply (rule 1)
```
```   196    apply (rule allI)
```
```   197    apply (rule applyB [THEN ssubst])
```
```   198     apply (rule_tac t = "xa" in term_case)
```
```   199        apply simp_all
```
```   200        apply (fast intro: assms INCL_subst all_INCL)+
```
```   201   done
```
```   202
```
```   203 end
```