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