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