src/CCL/Wfd.thy
author wenzelm
Sat Jun 14 23:19:51 2008 +0200 (2008-06-14)
changeset 27208 5fe899199f85
parent 27146 443c19953137
child 27221 31328dc30196
permissions -rw-r--r--
proper context for tactics derived from res_inst_tac;
wenzelm@17456
     1
(*  Title:      CCL/Wfd.thy
clasohm@0
     2
    ID:         $Id$
clasohm@1474
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
*)
clasohm@0
     6
wenzelm@17456
     7
header {* Well-founded relations in CCL *}
wenzelm@17456
     8
wenzelm@17456
     9
theory Wfd
wenzelm@17456
    10
imports Trancl Type Hered
wenzelm@17456
    11
begin
clasohm@0
    12
clasohm@0
    13
consts
clasohm@0
    14
      (*** Predicates ***)
clasohm@0
    15
  Wfd        ::       "[i set] => o"
clasohm@0
    16
      (*** Relations ***)
clasohm@0
    17
  wf         ::       "[i set] => i set"
clasohm@0
    18
  wmap       ::       "[i=>i,i set] => i set"
wenzelm@24825
    19
  lex        ::       "[i set,i set] => i set"      (infixl "**" 70)
clasohm@0
    20
  NatPR      ::       "i set"
clasohm@0
    21
  ListPR     ::       "i set => i set"
clasohm@0
    22
wenzelm@24825
    23
defs
clasohm@0
    24
wenzelm@17456
    25
  Wfd_def:
wenzelm@3837
    26
  "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a. a:P)"
clasohm@0
    27
wenzelm@17456
    28
  wf_def:         "wf(R) == {x. x:R & Wfd(R)}"
clasohm@0
    29
wenzelm@17456
    30
  wmap_def:       "wmap(f,R) == {p. EX x y. p=<x,y>  &  <f(x),f(y)> : R}"
wenzelm@17456
    31
  lex_def:
wenzelm@3837
    32
  "ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
clasohm@0
    33
wenzelm@17456
    34
  NatPR_def:      "NatPR == {p. EX x:Nat. p=<x,succ(x)>}"
wenzelm@17456
    35
  ListPR_def:     "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}"
wenzelm@17456
    36
wenzelm@20140
    37
wenzelm@20140
    38
lemma wfd_induct:
wenzelm@20140
    39
  assumes 1: "Wfd(R)"
wenzelm@20140
    40
    and 2: "!!x.[| ALL y. <y,x>: R --> P(y) |] ==> P(x)"
wenzelm@20140
    41
  shows "P(a)"
wenzelm@20140
    42
  apply (rule 1 [unfolded Wfd_def, rule_format, THEN CollectD])
wenzelm@20140
    43
  using 2 apply blast
wenzelm@20140
    44
  done
wenzelm@20140
    45
wenzelm@20140
    46
lemma wfd_strengthen_lemma:
wenzelm@20140
    47
  assumes 1: "!!x y.<x,y> : R ==> Q(x)"
wenzelm@20140
    48
    and 2: "ALL x. (ALL y. <y,x> : R --> y : P) --> x : P"
wenzelm@20140
    49
    and 3: "!!x. Q(x) ==> x:P"
wenzelm@20140
    50
  shows "a:P"
wenzelm@20140
    51
  apply (rule 2 [rule_format])
wenzelm@20140
    52
  using 1 3
wenzelm@20140
    53
  apply blast
wenzelm@20140
    54
  done
wenzelm@20140
    55
wenzelm@20140
    56
ML {*
wenzelm@27208
    57
  fun wfd_strengthen_tac ctxt s i =
wenzelm@27208
    58
    RuleInsts.res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
wenzelm@20140
    59
*}
wenzelm@20140
    60
wenzelm@20140
    61
lemma wf_anti_sym: "[| Wfd(r);  <a,x>:r;  <x,a>:r |] ==> P"
wenzelm@20140
    62
  apply (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P")
wenzelm@20140
    63
   apply blast
wenzelm@20140
    64
  apply (erule wfd_induct)
wenzelm@20140
    65
  apply blast
wenzelm@20140
    66
  done
wenzelm@20140
    67
wenzelm@20140
    68
lemma wf_anti_refl: "[| Wfd(r);  <a,a>: r |] ==> P"
wenzelm@20140
    69
  apply (rule wf_anti_sym)
wenzelm@20140
    70
  apply assumption+
wenzelm@20140
    71
  done
wenzelm@20140
    72
wenzelm@20140
    73
wenzelm@20140
    74
subsection {* Irreflexive transitive closure *}
wenzelm@20140
    75
wenzelm@20140
    76
lemma trancl_wf:
wenzelm@20140
    77
  assumes 1: "Wfd(R)"
wenzelm@20140
    78
  shows "Wfd(R^+)"
wenzelm@20140
    79
  apply (unfold Wfd_def)
wenzelm@20140
    80
  apply (rule allI ballI impI)+
wenzelm@20140
    81
(*must retain the universal formula for later use!*)
wenzelm@20140
    82
  apply (rule allE, assumption)
wenzelm@20140
    83
  apply (erule mp)
wenzelm@20140
    84
  apply (rule 1 [THEN wfd_induct])
wenzelm@20140
    85
  apply (rule impI [THEN allI])
wenzelm@20140
    86
  apply (erule tranclE)
wenzelm@20140
    87
   apply blast
wenzelm@20140
    88
  apply (erule spec [THEN mp, THEN spec, THEN mp])
wenzelm@20140
    89
   apply assumption+
wenzelm@20140
    90
  done
wenzelm@20140
    91
wenzelm@20140
    92
wenzelm@20140
    93
subsection {* Lexicographic Ordering *}
wenzelm@20140
    94
wenzelm@20140
    95
lemma lexXH:
wenzelm@20140
    96
  "p : ra**rb <-> (EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))"
wenzelm@20140
    97
  unfolding lex_def by blast
wenzelm@20140
    98
wenzelm@20140
    99
lemma lexI1: "<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb"
wenzelm@20140
   100
  by (blast intro!: lexXH [THEN iffD2])
wenzelm@20140
   101
wenzelm@20140
   102
lemma lexI2: "<b,b'> : rb ==> <<a,b>,<a,b'>> : ra**rb"
wenzelm@20140
   103
  by (blast intro!: lexXH [THEN iffD2])
wenzelm@20140
   104
wenzelm@20140
   105
lemma lexE:
wenzelm@20140
   106
  assumes 1: "p : ra**rb"
wenzelm@20140
   107
    and 2: "!!a a' b b'.[| <a,a'> : ra; p=<<a,b>,<a',b'>> |] ==> R"
wenzelm@20140
   108
    and 3: "!!a b b'.[| <b,b'> : rb;  p = <<a,b>,<a,b'>> |] ==> R"
wenzelm@20140
   109
  shows R
wenzelm@20140
   110
  apply (rule 1 [THEN lexXH [THEN iffD1], THEN exE])
wenzelm@20140
   111
  using 2 3
wenzelm@20140
   112
  apply blast
wenzelm@20140
   113
  done
wenzelm@20140
   114
wenzelm@20140
   115
lemma lex_pair: "[| p : r**s;  !!a a' b b'. p = <<a,b>,<a',b'>> ==> P |] ==>P"
wenzelm@20140
   116
  apply (erule lexE)
wenzelm@20140
   117
   apply blast+
wenzelm@20140
   118
  done
wenzelm@20140
   119
wenzelm@20140
   120
lemma lex_wf:
wenzelm@20140
   121
  assumes 1: "Wfd(R)"
wenzelm@20140
   122
    and 2: "Wfd(S)"
wenzelm@20140
   123
  shows "Wfd(R**S)"
wenzelm@20140
   124
  apply (unfold Wfd_def)
wenzelm@20140
   125
  apply safe
wenzelm@27208
   126
  apply (tactic {* wfd_strengthen_tac @{context} "%x. EX a b. x=<a,b>" 1 *})
wenzelm@20140
   127
   apply (blast elim!: lex_pair)
wenzelm@20140
   128
  apply (subgoal_tac "ALL a b.<a,b>:P")
wenzelm@20140
   129
   apply blast
wenzelm@20140
   130
  apply (rule 1 [THEN wfd_induct, THEN allI])
wenzelm@20140
   131
  apply (rule 2 [THEN wfd_induct, THEN allI]) back
wenzelm@20140
   132
  apply (fast elim!: lexE)
wenzelm@20140
   133
  done
wenzelm@20140
   134
wenzelm@20140
   135
wenzelm@20140
   136
subsection {* Mapping *}
wenzelm@20140
   137
wenzelm@20140
   138
lemma wmapXH: "p : wmap(f,r) <-> (EX x y. p=<x,y>  &  <f(x),f(y)> : r)"
wenzelm@20140
   139
  unfolding wmap_def by blast
wenzelm@20140
   140
wenzelm@20140
   141
lemma wmapI: "<f(a),f(b)> : r ==> <a,b> : wmap(f,r)"
wenzelm@20140
   142
  by (blast intro!: wmapXH [THEN iffD2])
wenzelm@20140
   143
wenzelm@20140
   144
lemma wmapE: "[| p : wmap(f,r);  !!a b.[| <f(a),f(b)> : r;  p=<a,b> |] ==> R |] ==> R"
wenzelm@20140
   145
  by (blast dest!: wmapXH [THEN iffD1])
wenzelm@20140
   146
wenzelm@20140
   147
lemma wmap_wf:
wenzelm@20140
   148
  assumes 1: "Wfd(r)"
wenzelm@20140
   149
  shows "Wfd(wmap(f,r))"
wenzelm@20140
   150
  apply (unfold Wfd_def)
wenzelm@20140
   151
  apply clarify
wenzelm@20140
   152
  apply (subgoal_tac "ALL b. ALL a. f (a) =b-->a:P")
wenzelm@20140
   153
   apply blast
wenzelm@20140
   154
  apply (rule 1 [THEN wfd_induct, THEN allI])
wenzelm@20140
   155
  apply clarify
wenzelm@20140
   156
  apply (erule spec [THEN mp])
wenzelm@20140
   157
  apply (safe elim!: wmapE)
wenzelm@20140
   158
  apply (erule spec [THEN mp, THEN spec, THEN mp])
wenzelm@20140
   159
   apply assumption
wenzelm@20140
   160
   apply (rule refl)
wenzelm@20140
   161
  done
wenzelm@20140
   162
wenzelm@20140
   163
wenzelm@20140
   164
subsection {* Projections *}
wenzelm@20140
   165
wenzelm@20140
   166
lemma wfstI: "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)"
wenzelm@20140
   167
  apply (rule wmapI)
wenzelm@20140
   168
  apply simp
wenzelm@20140
   169
  done
wenzelm@20140
   170
wenzelm@20140
   171
lemma wsndI: "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)"
wenzelm@20140
   172
  apply (rule wmapI)
wenzelm@20140
   173
  apply simp
wenzelm@20140
   174
  done
wenzelm@20140
   175
wenzelm@20140
   176
lemma wthdI: "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)"
wenzelm@20140
   177
  apply (rule wmapI)
wenzelm@20140
   178
  apply simp
wenzelm@20140
   179
  done
wenzelm@20140
   180
wenzelm@20140
   181
wenzelm@20140
   182
subsection {* Ground well-founded relations *}
wenzelm@20140
   183
wenzelm@20140
   184
lemma wfI: "[| Wfd(r);  a : r |] ==> a : wf(r)"
wenzelm@20140
   185
  unfolding wf_def by blast
wenzelm@20140
   186
wenzelm@20140
   187
lemma Empty_wf: "Wfd({})"
wenzelm@20140
   188
  unfolding Wfd_def by (blast elim: EmptyXH [THEN iffD1, THEN FalseE])
wenzelm@20140
   189
wenzelm@20140
   190
lemma wf_wf: "Wfd(wf(R))"
wenzelm@20140
   191
  unfolding wf_def
wenzelm@20140
   192
  apply (rule_tac Q = "Wfd(R)" in excluded_middle [THEN disjE])
wenzelm@20140
   193
   apply simp_all
wenzelm@20140
   194
  apply (rule Empty_wf)
wenzelm@20140
   195
  done
wenzelm@20140
   196
wenzelm@20140
   197
lemma NatPRXH: "p : NatPR <-> (EX x:Nat. p=<x,succ(x)>)"
wenzelm@20140
   198
  unfolding NatPR_def by blast
wenzelm@20140
   199
wenzelm@20140
   200
lemma ListPRXH: "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=<t,h$t>)"
wenzelm@20140
   201
  unfolding ListPR_def by blast
wenzelm@20140
   202
wenzelm@20140
   203
lemma NatPRI: "x : Nat ==> <x,succ(x)> : NatPR"
wenzelm@20140
   204
  by (auto simp: NatPRXH)
wenzelm@20140
   205
wenzelm@20140
   206
lemma ListPRI: "[| t : List(A); h : A |] ==> <t,h $ t> : ListPR(A)"
wenzelm@20140
   207
  by (auto simp: ListPRXH)
wenzelm@20140
   208
wenzelm@20140
   209
lemma NatPR_wf: "Wfd(NatPR)"
wenzelm@20140
   210
  apply (unfold Wfd_def)
wenzelm@20140
   211
  apply clarify
wenzelm@27208
   212
  apply (tactic {* wfd_strengthen_tac @{context} "%x. x:Nat" 1 *})
wenzelm@20140
   213
   apply (fastsimp iff: NatPRXH)
wenzelm@20140
   214
  apply (erule Nat_ind)
wenzelm@20140
   215
   apply (fastsimp iff: NatPRXH)+
wenzelm@20140
   216
  done
wenzelm@20140
   217
wenzelm@20140
   218
lemma ListPR_wf: "Wfd(ListPR(A))"
wenzelm@20140
   219
  apply (unfold Wfd_def)
wenzelm@20140
   220
  apply clarify
wenzelm@27208
   221
  apply (tactic {* wfd_strengthen_tac @{context} "%x. x:List (A)" 1 *})
wenzelm@20140
   222
   apply (fastsimp iff: ListPRXH)
wenzelm@20140
   223
  apply (erule List_ind)
wenzelm@20140
   224
   apply (fastsimp iff: ListPRXH)+
wenzelm@20140
   225
  done
wenzelm@20140
   226
wenzelm@20140
   227
wenzelm@20140
   228
subsection {* General Recursive Functions *}
wenzelm@20140
   229
wenzelm@20140
   230
lemma letrecT:
wenzelm@20140
   231
  assumes 1: "a : A"
wenzelm@20140
   232
    and 2: "!!p g.[| p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x) |] ==> h(p,g) : D(p)"
wenzelm@20140
   233
  shows "letrec g x be h(x,g) in g(a) : D(a)"
wenzelm@20140
   234
  apply (rule 1 [THEN rev_mp])
wenzelm@20140
   235
  apply (rule wf_wf [THEN wfd_induct])
wenzelm@20140
   236
  apply (subst letrecB)
wenzelm@20140
   237
  apply (rule impI)
wenzelm@20140
   238
  apply (erule 2)
wenzelm@20140
   239
  apply blast
wenzelm@20140
   240
  done
wenzelm@20140
   241
wenzelm@20140
   242
lemma SPLITB: "SPLIT(<a,b>,B) = B(a,b)"
wenzelm@20140
   243
  unfolding SPLIT_def
wenzelm@20140
   244
  apply (rule set_ext)
wenzelm@20140
   245
  apply blast
wenzelm@20140
   246
  done
wenzelm@17456
   247
wenzelm@20140
   248
lemma letrec2T:
wenzelm@20140
   249
  assumes "a : A"
wenzelm@20140
   250
    and "b : B"
wenzelm@20140
   251
    and "!!p q g.[| p:A; q:B;
wenzelm@20140
   252
              ALL x:A. ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==> 
wenzelm@20140
   253
                h(p,q,g) : D(p,q)"
wenzelm@20140
   254
  shows "letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"
wenzelm@20140
   255
  apply (unfold letrec2_def)
wenzelm@20140
   256
  apply (rule SPLITB [THEN subst])
wenzelm@20140
   257
  apply (assumption | rule letrecT pairT splitT prems)+
wenzelm@20140
   258
  apply (subst SPLITB)
wenzelm@20140
   259
  apply (assumption | rule ballI SubtypeI prems)+
wenzelm@20140
   260
  apply (rule SPLITB [THEN subst])
wenzelm@20140
   261
  apply (assumption | rule letrecT SubtypeI pairT splitT prems |
wenzelm@20140
   262
    erule bspec SubtypeE sym [THEN subst])+
wenzelm@20140
   263
  done
wenzelm@20140
   264
wenzelm@20140
   265
lemma lem: "SPLIT(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)"
wenzelm@20140
   266
  by (simp add: SPLITB)
wenzelm@20140
   267
wenzelm@20140
   268
lemma letrec3T:
wenzelm@20140
   269
  assumes "a : A"
wenzelm@20140
   270
    and "b : B"
wenzelm@20140
   271
    and "c : C"
wenzelm@20140
   272
    and "!!p q r g.[| p:A; q:B; r:C;
wenzelm@20140
   273
       ALL x:A. ALL y:B. ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}.  
wenzelm@20140
   274
                                                        g(x,y,z) : D(x,y,z) |] ==> 
wenzelm@20140
   275
                h(p,q,r,g) : D(p,q,r)"
wenzelm@20140
   276
  shows "letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"
wenzelm@20140
   277
  apply (unfold letrec3_def)
wenzelm@20140
   278
  apply (rule lem [THEN subst])
wenzelm@20140
   279
  apply (assumption | rule letrecT pairT splitT prems)+
wenzelm@20140
   280
  apply (simp add: SPLITB)
wenzelm@20140
   281
  apply (assumption | rule ballI SubtypeI prems)+
wenzelm@20140
   282
  apply (rule lem [THEN subst])
wenzelm@20140
   283
  apply (assumption | rule letrecT SubtypeI pairT splitT prems |
wenzelm@20140
   284
    erule bspec SubtypeE sym [THEN subst])+
wenzelm@20140
   285
  done
wenzelm@20140
   286
wenzelm@20140
   287
lemmas letrecTs = letrecT letrec2T letrec3T
wenzelm@20140
   288
wenzelm@20140
   289
wenzelm@20140
   290
subsection {* Type Checking for Recursive Calls *}
wenzelm@20140
   291
wenzelm@20140
   292
lemma rcallT:
wenzelm@20140
   293
  "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);  
wenzelm@20140
   294
      g(a) : D(a) ==> g(a) : E;  a:A;  <a,p>:wf(R) |] ==>  
wenzelm@20140
   295
  g(a) : E"
wenzelm@20140
   296
  by blast
wenzelm@20140
   297
wenzelm@20140
   298
lemma rcall2T:
wenzelm@20140
   299
  "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y);  
wenzelm@20140
   300
      g(a,b) : D(a,b) ==> g(a,b) : E;  a:A;  b:B;  <<a,b>,<p,q>>:wf(R) |] ==>  
wenzelm@20140
   301
  g(a,b) : E"
wenzelm@20140
   302
  by blast
wenzelm@20140
   303
wenzelm@20140
   304
lemma rcall3T:
wenzelm@20140
   305
  "[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z);  
wenzelm@20140
   306
      g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E;   
wenzelm@20140
   307
      a:A;  b:B;  c:C;  <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==>  
wenzelm@20140
   308
  g(a,b,c) : E"
wenzelm@20140
   309
  by blast
wenzelm@20140
   310
wenzelm@20140
   311
lemmas rcallTs = rcallT rcall2T rcall3T
wenzelm@20140
   312
wenzelm@20140
   313
wenzelm@20140
   314
subsection {* Instantiating an induction hypothesis with an equality assumption *}
wenzelm@20140
   315
wenzelm@20140
   316
lemma hyprcallT:
wenzelm@20140
   317
  assumes 1: "g(a) = b"
wenzelm@20140
   318
    and 2: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x)"
wenzelm@20140
   319
    and 3: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> b=g(a) ==> g(a) : D(a) ==> P"
wenzelm@20140
   320
    and 4: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> a:A"
wenzelm@20140
   321
    and 5: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> <a,p>:wf(R)"
wenzelm@20140
   322
  shows P
wenzelm@20140
   323
  apply (rule 3 [OF 2, OF 1 [symmetric]])
wenzelm@20140
   324
  apply (rule rcallT [OF 2])
wenzelm@20140
   325
    apply assumption
wenzelm@20140
   326
   apply (rule 4 [OF 2])
wenzelm@20140
   327
  apply (rule 5 [OF 2])
wenzelm@20140
   328
  done
wenzelm@20140
   329
wenzelm@20140
   330
lemma hyprcall2T:
wenzelm@20140
   331
  assumes 1: "g(a,b) = c"
wenzelm@20140
   332
    and 2: "ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y)"
wenzelm@20140
   333
    and 3: "[| c=g(a,b);  g(a,b) : D(a,b) |] ==> P"
wenzelm@20140
   334
    and 4: "a:A"
wenzelm@20140
   335
    and 5: "b:B"
wenzelm@20140
   336
    and 6: "<<a,b>,<p,q>>:wf(R)"
wenzelm@20140
   337
  shows P
wenzelm@20140
   338
  apply (rule 3)
wenzelm@20140
   339
    apply (rule 1 [symmetric])
wenzelm@20140
   340
  apply (rule rcall2T)
wenzelm@23467
   341
      apply (rule 2)
wenzelm@23467
   342
     apply assumption
wenzelm@23467
   343
    apply (rule 4)
wenzelm@23467
   344
   apply (rule 5)
wenzelm@23467
   345
  apply (rule 6)
wenzelm@20140
   346
  done
wenzelm@20140
   347
wenzelm@20140
   348
lemma hyprcall3T:
wenzelm@20140
   349
  assumes 1: "g(a,b,c) = d"
wenzelm@20140
   350
    and 2: "ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z)"
wenzelm@20140
   351
    and 3: "[| d=g(a,b,c);  g(a,b,c) : D(a,b,c) |] ==> P"
wenzelm@20140
   352
    and 4: "a:A"
wenzelm@20140
   353
    and 5: "b:B"
wenzelm@20140
   354
    and 6: "c:C"
wenzelm@20140
   355
    and 7: "<<a,<b,c>>,<p,<q,r>>> : wf(R)"
wenzelm@20140
   356
  shows P
wenzelm@20140
   357
  apply (rule 3)
wenzelm@20140
   358
   apply (rule 1 [symmetric])
wenzelm@20140
   359
  apply (rule rcall3T)
wenzelm@23467
   360
       apply (rule 2)
wenzelm@23467
   361
      apply assumption
wenzelm@23467
   362
     apply (rule 4)
wenzelm@23467
   363
    apply (rule 5)
wenzelm@23467
   364
   apply (rule 6)
wenzelm@23467
   365
  apply (rule 7)
wenzelm@20140
   366
  done
wenzelm@20140
   367
wenzelm@20140
   368
lemmas hyprcallTs = hyprcallT hyprcall2T hyprcall3T
wenzelm@20140
   369
wenzelm@20140
   370
wenzelm@20140
   371
subsection {* Rules to Remove Induction Hypotheses after Type Checking *}
wenzelm@20140
   372
wenzelm@20140
   373
lemma rmIH1: "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P |] ==> P" .
wenzelm@20140
   374
wenzelm@20140
   375
lemma rmIH2: "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> P" .
wenzelm@20140
   376
  
wenzelm@20140
   377
lemma rmIH3:
wenzelm@20140
   378
 "[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z);  
wenzelm@20140
   379
     P |] ==>  
wenzelm@20140
   380
     P" .
wenzelm@20140
   381
wenzelm@20140
   382
lemmas rmIHs = rmIH1 rmIH2 rmIH3
wenzelm@20140
   383
wenzelm@20140
   384
wenzelm@20140
   385
subsection {* Lemmas for constructors and subtypes *}
wenzelm@20140
   386
wenzelm@20140
   387
(* 0-ary constructors do not need additional rules as they are handled *)
wenzelm@20140
   388
(*                                      correctly by applying SubtypeI *)
wenzelm@20140
   389
wenzelm@20140
   390
lemma Subtype_canTs:
wenzelm@20140
   391
  "!!a b A B P. a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}"
wenzelm@20140
   392
  "!!a A B P. a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}"
wenzelm@20140
   393
  "!!b A B P. b : {x:B. P(inr(x))} ==> inr(b) : {x:A+B. P(x)}"
wenzelm@20140
   394
  "!!a P. a : {x:Nat. P(succ(x))} ==> succ(a) : {x:Nat. P(x)}"
wenzelm@20140
   395
  "!!h t A P. h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
wenzelm@20140
   396
  by (assumption | rule SubtypeI canTs icanTs | erule SubtypeE)+
wenzelm@20140
   397
wenzelm@20140
   398
lemma letT: "[| f(t):B;  ~t=bot  |] ==> let x be t in f(x) : B"
wenzelm@20140
   399
  apply (erule letB [THEN ssubst])
wenzelm@20140
   400
  apply assumption
wenzelm@20140
   401
  done
wenzelm@20140
   402
wenzelm@20140
   403
lemma applyT2: "[| a:A;  f : Pi(A,B)  |] ==> f ` a  : B(a)"
wenzelm@20140
   404
  apply (erule applyT)
wenzelm@20140
   405
  apply assumption
wenzelm@20140
   406
  done
wenzelm@20140
   407
wenzelm@20140
   408
lemma rcall_lemma1: "[| a:A;  a:A ==> P(a) |] ==> a : {x:A. P(x)}"
wenzelm@20140
   409
  by blast
wenzelm@20140
   410
wenzelm@20140
   411
lemma rcall_lemma2: "[| a:{x:A. Q(x)};  [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A. P(x)}"
wenzelm@20140
   412
  by blast
wenzelm@20140
   413
wenzelm@20140
   414
lemmas rcall_lemmas = asm_rl rcall_lemma1 SubtypeD1 rcall_lemma2
wenzelm@20140
   415
wenzelm@20140
   416
wenzelm@20140
   417
subsection {* Typechecking *}
wenzelm@20140
   418
wenzelm@20140
   419
ML {*
wenzelm@20140
   420
wenzelm@20140
   421
local
wenzelm@20140
   422
wenzelm@20140
   423
val type_rls =
wenzelm@20140
   424
  thms "canTs" @ thms "icanTs" @ thms "applyT2" @ thms "ncanTs" @ thms "incanTs" @
wenzelm@20140
   425
  thms "precTs" @ thms "letrecTs" @ thms "letT" @ thms "Subtype_canTs";
wenzelm@20140
   426
wenzelm@20140
   427
val rcallT = thm "rcallT";
wenzelm@20140
   428
val rcall2T = thm "rcall2T";
wenzelm@20140
   429
val rcall3T = thm "rcall3T";
wenzelm@20140
   430
val rcallTs = thms "rcallTs";
wenzelm@20140
   431
val rcall_lemmas = thms "rcall_lemmas";
wenzelm@20140
   432
val SubtypeE = thm "SubtypeE";
wenzelm@20140
   433
val SubtypeI = thm "SubtypeI";
wenzelm@20140
   434
val rmIHs = thms "rmIHs";
wenzelm@20140
   435
val hyprcallTs = thms "hyprcallTs";
wenzelm@20140
   436
wenzelm@20140
   437
fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l)
wenzelm@20140
   438
  | bvars _ l = l
wenzelm@20140
   439
wenzelm@20140
   440
fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t
wenzelm@20140
   441
  | get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t
wenzelm@20140
   442
  | get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
wenzelm@24825
   443
  | get_bno l n (Const("mem",_) $ t $ _) = get_bno l n t
wenzelm@20140
   444
  | get_bno l n (t $ s) = get_bno l n t
wenzelm@20140
   445
  | get_bno l n (Bound m) = (m-length(l),n)
wenzelm@20140
   446
wenzelm@20140
   447
(* Not a great way of identifying induction hypothesis! *)
wenzelm@20140
   448
fun could_IH x = could_unify(x,hd (prems_of rcallT)) orelse
wenzelm@20140
   449
                 could_unify(x,hd (prems_of rcall2T)) orelse
wenzelm@20140
   450
                 could_unify(x,hd (prems_of rcall3T))
wenzelm@20140
   451
wenzelm@20140
   452
fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
wenzelm@20140
   453
  let val bvs = bvars Bi []
wenzelm@20140
   454
      val ihs = List.filter could_IH (Logic.strip_assums_hyp Bi)
wenzelm@20140
   455
      val rnames = map (fn x=>
wenzelm@20140
   456
                    let val (a,b) = get_bno [] 0 x
wenzelm@20140
   457
                    in (List.nth(bvs,a),b) end) ihs
wenzelm@20140
   458
      fun try_IHs [] = no_tac
wenzelm@20140
   459
        | try_IHs ((x,y)::xs) = tac [("g",x)] (List.nth(rls,y-1)) i ORELSE (try_IHs xs)
wenzelm@20140
   460
  in try_IHs rnames end)
wenzelm@20140
   461
wenzelm@20140
   462
fun is_rigid_prog t =
wenzelm@20140
   463
     case (Logic.strip_assums_concl t) of
wenzelm@24825
   464
        (Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => (term_vars a = [])
wenzelm@20140
   465
       | _ => false
wenzelm@20140
   466
in
wenzelm@20140
   467
wenzelm@27208
   468
fun rcall_tac i = let fun tac ps rl i = Tactic.res_inst_tac ps rl i THEN atac i
wenzelm@20140
   469
                       in IHinst tac rcallTs i end THEN
wenzelm@20140
   470
                  eresolve_tac rcall_lemmas i
wenzelm@20140
   471
wenzelm@20140
   472
fun raw_step_tac prems i = ares_tac (prems@type_rls) i ORELSE
wenzelm@20140
   473
                           rcall_tac i ORELSE
wenzelm@20140
   474
                           ematch_tac [SubtypeE] i ORELSE
wenzelm@20140
   475
                           match_tac [SubtypeI] i
wenzelm@20140
   476
wenzelm@20140
   477
fun tc_step_tac prems = SUBGOAL (fn (Bi,i) =>
wenzelm@20140
   478
          if is_rigid_prog Bi then raw_step_tac prems i else no_tac)
wenzelm@20140
   479
wenzelm@20140
   480
fun typechk_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls)) i
wenzelm@20140
   481
wenzelm@20140
   482
val tac = typechk_tac [] 1
wenzelm@20140
   483
wenzelm@20140
   484
(*** Clean up Correctness Condictions ***)
wenzelm@20140
   485
wenzelm@20140
   486
val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([SubtypeE]@rmIHs) ORELSE'
wenzelm@20140
   487
                                 hyp_subst_tac)
wenzelm@20140
   488
wenzelm@20140
   489
val clean_ccs_tac =
wenzelm@27208
   490
       let fun tac ps rl i = Tactic.eres_inst_tac ps rl i THEN atac i
wenzelm@20140
   491
       in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE'
wenzelm@20140
   492
                       eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE'
wenzelm@20140
   493
                       hyp_subst_tac)) end
wenzelm@20140
   494
wenzelm@20140
   495
fun gen_ccs_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls) THEN
wenzelm@20140
   496
                                     clean_ccs_tac) i
wenzelm@17456
   497
clasohm@0
   498
end
wenzelm@20140
   499
*}
wenzelm@20140
   500
wenzelm@20140
   501
wenzelm@20140
   502
subsection {* Evaluation *}
wenzelm@20140
   503
wenzelm@20140
   504
ML {*
wenzelm@20140
   505
wenzelm@20140
   506
local
wenzelm@24034
   507
  structure Data = NamedThmsFun(val name = "eval" val description = "evaluation rules");
wenzelm@20140
   508
in
wenzelm@20140
   509
wenzelm@20140
   510
fun eval_tac ctxt ths =
wenzelm@20140
   511
  METAHYPS (fn prems =>
wenzelm@24034
   512
    DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get ctxt) 1)) 1;
wenzelm@20140
   513
wenzelm@20140
   514
val eval_setup =
wenzelm@24034
   515
  Data.setup #>
wenzelm@20140
   516
  Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt =>
wenzelm@20140
   517
    Method.SIMPLE_METHOD (CHANGED (eval_tac ctxt ths))), "evaluation")];
wenzelm@20140
   518
wenzelm@20140
   519
end;
wenzelm@20140
   520
wenzelm@20140
   521
*}
wenzelm@20140
   522
wenzelm@20140
   523
setup eval_setup
wenzelm@20140
   524
wenzelm@20140
   525
lemmas eval_rls [eval] = trueV falseV pairV lamV caseVtrue caseVfalse caseVpair caseVlam
wenzelm@20140
   526
wenzelm@20140
   527
lemma applyV [eval]:
wenzelm@20140
   528
  assumes "f ---> lam x. b(x)"
wenzelm@20140
   529
    and "b(a) ---> c"
wenzelm@20140
   530
  shows "f ` a ---> c"
wenzelm@20140
   531
  unfolding apply_def by (eval prems)
wenzelm@20140
   532
wenzelm@20140
   533
lemma letV:
wenzelm@20140
   534
  assumes 1: "t ---> a"
wenzelm@20140
   535
    and 2: "f(a) ---> c"
wenzelm@20140
   536
  shows "let x be t in f(x) ---> c"
wenzelm@20140
   537
  apply (unfold let_def)
wenzelm@20140
   538
  apply (rule 1 [THEN canonical])
wenzelm@20140
   539
  apply (tactic {*
wenzelm@26391
   540
    REPEAT (DEPTH_SOLVE_1 (resolve_tac (@{thms assms} @ @{thms eval_rls}) 1 ORELSE
wenzelm@26391
   541
      etac @{thm substitute} 1)) *})
wenzelm@20140
   542
  done
wenzelm@20140
   543
wenzelm@20140
   544
lemma fixV: "f(fix(f)) ---> c ==> fix(f) ---> c"
wenzelm@20140
   545
  apply (unfold fix_def)
wenzelm@20140
   546
  apply (rule applyV)
wenzelm@20140
   547
   apply (rule lamV)
wenzelm@20140
   548
  apply assumption
wenzelm@20140
   549
  done
wenzelm@20140
   550
wenzelm@20140
   551
lemma letrecV:
wenzelm@20140
   552
  "h(t,%y. letrec g x be h(x,g) in g(y)) ---> c ==>  
wenzelm@20140
   553
                 letrec g x be h(x,g) in g(t) ---> c"
wenzelm@20140
   554
  apply (unfold letrec_def)
wenzelm@20140
   555
  apply (assumption | rule fixV applyV  lamV)+
wenzelm@20140
   556
  done
wenzelm@20140
   557
wenzelm@20140
   558
lemmas [eval] = letV letrecV fixV
wenzelm@20140
   559
wenzelm@20140
   560
lemma V_rls [eval]:
wenzelm@20140
   561
  "true ---> true"
wenzelm@20140
   562
  "false ---> false"
wenzelm@20140
   563
  "!!b c t u. [| b--->true;  t--->c |] ==> if b then t else u ---> c"
wenzelm@20140
   564
  "!!b c t u. [| b--->false;  u--->c |] ==> if b then t else u ---> c"
wenzelm@20140
   565
  "!!a b. <a,b> ---> <a,b>"
wenzelm@20140
   566
  "!!a b c t h. [| t ---> <a,b>;  h(a,b) ---> c |] ==> split(t,h) ---> c"
wenzelm@20140
   567
  "zero ---> zero"
wenzelm@20140
   568
  "!!n. succ(n) ---> succ(n)"
wenzelm@20140
   569
  "!!c n t u. [| n ---> zero; t ---> c |] ==> ncase(n,t,u) ---> c"
wenzelm@20140
   570
  "!!c n t u x. [| n ---> succ(x); u(x) ---> c |] ==> ncase(n,t,u) ---> c"
wenzelm@20140
   571
  "!!c n t u. [| n ---> zero; t ---> c |] ==> nrec(n,t,u) ---> c"
wenzelm@20140
   572
  "!!c n t u x. [| n--->succ(x); u(x,nrec(x,t,u))--->c |] ==> nrec(n,t,u)--->c"
wenzelm@20140
   573
  "[] ---> []"
wenzelm@20140
   574
  "!!h t. h$t ---> h$t"
wenzelm@20140
   575
  "!!c l t u. [| l ---> []; t ---> c |] ==> lcase(l,t,u) ---> c"
wenzelm@20140
   576
  "!!c l t u x xs. [| l ---> x$xs; u(x,xs) ---> c |] ==> lcase(l,t,u) ---> c"
wenzelm@20140
   577
  "!!c l t u. [| l ---> []; t ---> c |] ==> lrec(l,t,u) ---> c"
wenzelm@20140
   578
  "!!c l t u x xs. [| l--->x$xs; u(x,xs,lrec(xs,t,u))--->c |] ==> lrec(l,t,u)--->c"
wenzelm@20140
   579
  unfolding data_defs by eval+
wenzelm@20140
   580
wenzelm@20140
   581
wenzelm@20140
   582
subsection {* Factorial *}
wenzelm@20140
   583
wenzelm@20140
   584
lemma
wenzelm@20140
   585
  "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h))))  
wenzelm@20140
   586
   in f(succ(succ(zero))) ---> ?a"
wenzelm@20140
   587
  by eval
wenzelm@20140
   588
wenzelm@20140
   589
lemma
wenzelm@20140
   590
  "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h))))  
wenzelm@20140
   591
   in f(succ(succ(succ(zero)))) ---> ?a"
wenzelm@20140
   592
  by eval
wenzelm@20140
   593
wenzelm@20140
   594
subsection {* Less Than Or Equal *}
wenzelm@20140
   595
wenzelm@20140
   596
lemma
wenzelm@20140
   597
  "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
wenzelm@20140
   598
   in f(<succ(zero), succ(zero)>) ---> ?a"
wenzelm@20140
   599
  by eval
wenzelm@20140
   600
wenzelm@20140
   601
lemma
wenzelm@20140
   602
  "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
wenzelm@20140
   603
   in f(<succ(zero), succ(succ(succ(succ(zero))))>) ---> ?a"
wenzelm@20140
   604
  by eval
wenzelm@20140
   605
wenzelm@20140
   606
lemma
wenzelm@20140
   607
  "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
wenzelm@20140
   608
   in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) ---> ?a"
wenzelm@20140
   609
  by eval
wenzelm@20140
   610
wenzelm@20140
   611
wenzelm@20140
   612
subsection {* Reverse *}
wenzelm@20140
   613
wenzelm@20140
   614
lemma
wenzelm@20140
   615
  "letrec id l be lcase(l,[],%x xs. x$id(xs))  
wenzelm@20140
   616
   in id(zero$succ(zero)$[]) ---> ?a"
wenzelm@20140
   617
  by eval
wenzelm@20140
   618
wenzelm@20140
   619
lemma
wenzelm@20140
   620
  "letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g))  
wenzelm@20140
   621
   in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a"
wenzelm@20140
   622
  by eval
wenzelm@20140
   623
wenzelm@20140
   624
end