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