src/CCL/Type.thy
author wenzelm
Tue Aug 12 21:29:50 2014 +0200 (2014-08-12)
changeset 57920 c1953856cfca
parent 56199 8e8d28ed7529
child 58889 5b7a9633cfa8
permissions -rw-r--r--
clarified focus and key handling -- more like SideKick;
avoid resetting input map with its potentially confusion propagation of key events to unrelated components, e.g. main text area or tree scrollbar;
wenzelm@17456
     1
(*  Title:      CCL/Type.thy
clasohm@0
     2
    Author:     Martin Coen
clasohm@0
     3
    Copyright   1993  University of Cambridge
clasohm@0
     4
*)
clasohm@0
     5
wenzelm@17456
     6
header {* Types in CCL are defined as sets of terms *}
wenzelm@17456
     7
wenzelm@17456
     8
theory Type
wenzelm@17456
     9
imports Term
wenzelm@17456
    10
begin
clasohm@0
    11
clasohm@0
    12
consts
clasohm@0
    13
clasohm@0
    14
  Subtype       :: "['a set, 'a => o] => 'a set"
clasohm@0
    15
  Bool          :: "i set"
clasohm@0
    16
  Unit          :: "i set"
wenzelm@24825
    17
  Plus           :: "[i set, i set] => i set"        (infixr "+" 55)
clasohm@0
    18
  Pi            :: "[i set, i => i set] => i set"
clasohm@0
    19
  Sigma         :: "[i set, i => i set] => i set"
clasohm@0
    20
  Nat           :: "i set"
clasohm@0
    21
  List          :: "i set => i set"
clasohm@0
    22
  Lists         :: "i set => i set"
clasohm@0
    23
  ILists        :: "i set => i set"
lcp@999
    24
  TAll          :: "(i set => i set) => i set"       (binder "TALL " 55)
lcp@999
    25
  TEx           :: "(i set => i set) => i set"       (binder "TEX " 55)
lcp@999
    26
  Lift          :: "i set => i set"                  ("(3[_])")
clasohm@0
    27
clasohm@0
    28
  SPLIT         :: "[i, [i, i] => i set] => i set"
clasohm@0
    29
wenzelm@14765
    30
syntax
wenzelm@35113
    31
  "_Pi"         :: "[idt, i set, i set] => i set"    ("(3PROD _:_./ _)"
clasohm@1474
    32
                                [0,0,60] 60)
lcp@999
    33
wenzelm@35113
    34
  "_Sigma"      :: "[idt, i set, i set] => i set"    ("(3SUM _:_./ _)"
clasohm@1474
    35
                                [0,0,60] 60)
wenzelm@17456
    36
wenzelm@35113
    37
  "_arrow"      :: "[i set, i set] => i set"         ("(_ ->/ _)"  [54, 53] 53)
wenzelm@35113
    38
  "_star"       :: "[i set, i set] => i set"         ("(_ */ _)" [56, 55] 55)
wenzelm@35113
    39
  "_Subtype"    :: "[idt, 'a set, o] => 'a set"      ("(1{_: _ ./ _})")
clasohm@0
    40
clasohm@0
    41
translations
wenzelm@35054
    42
  "PROD x:A. B" => "CONST Pi(A, %x. B)"
wenzelm@35054
    43
  "A -> B"      => "CONST Pi(A, %_. B)"
wenzelm@35054
    44
  "SUM x:A. B"  => "CONST Sigma(A, %x. B)"
wenzelm@35054
    45
  "A * B"       => "CONST Sigma(A, %_. B)"
wenzelm@35054
    46
  "{x: A. B}"   == "CONST Subtype(A, %x. B)"
clasohm@0
    47
wenzelm@17456
    48
print_translation {*
wenzelm@42284
    49
 [(@{const_syntax Pi},
wenzelm@52143
    50
    fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
wenzelm@42284
    51
  (@{const_syntax Sigma},
wenzelm@52143
    52
    fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
wenzelm@35113
    53
*}
clasohm@0
    54
wenzelm@42156
    55
defs
wenzelm@17456
    56
  Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}"
wenzelm@17456
    57
  Unit_def:          "Unit == {x. x=one}"
wenzelm@17456
    58
  Bool_def:          "Bool == {x. x=true | x=false}"
wenzelm@17456
    59
  Plus_def:           "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}"
wenzelm@17456
    60
  Pi_def:         "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}"
wenzelm@17456
    61
  Sigma_def:   "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
wenzelm@17456
    62
  Nat_def:            "Nat == lfp(% X. Unit + X)"
wenzelm@17456
    63
  List_def:       "List(A) == lfp(% X. Unit + A*X)"
clasohm@0
    64
wenzelm@17456
    65
  Lists_def:     "Lists(A) == gfp(% X. Unit + A*X)"
wenzelm@17456
    66
  ILists_def:   "ILists(A) == gfp(% X.{} + A*X)"
clasohm@0
    67
wenzelm@17456
    68
  Tall_def:   "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})"
wenzelm@17456
    69
  Tex_def:     "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"
wenzelm@17456
    70
  Lift_def:           "[A] == A Un {bot}"
clasohm@0
    71
wenzelm@17456
    72
  SPLIT_def:   "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})"
wenzelm@17456
    73
wenzelm@20140
    74
wenzelm@20140
    75
lemmas simp_type_defs =
wenzelm@20140
    76
    Subtype_def Unit_def Bool_def Plus_def Sigma_def Pi_def Lift_def Tall_def Tex_def
wenzelm@20140
    77
  and ind_type_defs = Nat_def List_def
wenzelm@20140
    78
  and simp_data_defs = one_def inl_def inr_def
wenzelm@20140
    79
  and ind_data_defs = zero_def succ_def nil_def cons_def
wenzelm@20140
    80
wenzelm@20140
    81
lemma subsetXH: "A <= B <-> (ALL x. x:A --> x:B)"
wenzelm@20140
    82
  by blast
wenzelm@20140
    83
wenzelm@20140
    84
wenzelm@20140
    85
subsection {* Exhaustion Rules *}
wenzelm@20140
    86
wenzelm@20140
    87
lemma EmptyXH: "!!a. a : {} <-> False"
wenzelm@20140
    88
  and SubtypeXH: "!!a A P. a : {x:A. P(x)} <-> (a:A & P(a))"
wenzelm@20140
    89
  and UnitXH: "!!a. a : Unit          <-> a=one"
wenzelm@20140
    90
  and BoolXH: "!!a. a : Bool          <-> a=true | a=false"
wenzelm@20140
    91
  and PlusXH: "!!a A B. a : A+B           <-> (EX x:A. a=inl(x)) | (EX x:B. a=inr(x))"
wenzelm@20140
    92
  and PiXH: "!!a A B. a : PROD x:A. B(x) <-> (EX b. a=lam x. b(x) & (ALL x:A. b(x):B(x)))"
wenzelm@20140
    93
  and SgXH: "!!a A B. a : SUM x:A. B(x)  <-> (EX x:A. EX y:B(x).a=<x,y>)"
wenzelm@20140
    94
  unfolding simp_type_defs by blast+
wenzelm@20140
    95
wenzelm@20140
    96
lemmas XHs = EmptyXH SubtypeXH UnitXH BoolXH PlusXH PiXH SgXH
wenzelm@20140
    97
wenzelm@20140
    98
lemma LiftXH: "a : [A] <-> (a=bot | a:A)"
wenzelm@20140
    99
  and TallXH: "a : TALL X. B(X) <-> (ALL X. a:B(X))"
wenzelm@20140
   100
  and TexXH: "a : TEX X. B(X) <-> (EX X. a:B(X))"
wenzelm@20140
   101
  unfolding simp_type_defs by blast+
wenzelm@20140
   102
wenzelm@20140
   103
ML {*
wenzelm@56199
   104
ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs});
wenzelm@20140
   105
*}
wenzelm@20140
   106
wenzelm@20140
   107
wenzelm@20140
   108
subsection {* Canonical Type Rules *}
wenzelm@20140
   109
wenzelm@20140
   110
lemma oneT: "one : Unit"
wenzelm@20140
   111
  and trueT: "true : Bool"
wenzelm@20140
   112
  and falseT: "false : Bool"
wenzelm@20140
   113
  and lamT: "!!b B. [| !!x. x:A ==> b(x):B(x) |] ==> lam x. b(x) : Pi(A,B)"
wenzelm@20140
   114
  and pairT: "!!b B. [| a:A; b:B(a) |] ==> <a,b>:Sigma(A,B)"
wenzelm@20140
   115
  and inlT: "a:A ==> inl(a) : A+B"
wenzelm@20140
   116
  and inrT: "b:B ==> inr(b) : A+B"
wenzelm@20140
   117
  by (blast intro: XHs [THEN iffD2])+
wenzelm@20140
   118
wenzelm@20140
   119
lemmas canTs = oneT trueT falseT pairT lamT inlT inrT
wenzelm@20140
   120
wenzelm@20140
   121
wenzelm@20140
   122
subsection {* Non-Canonical Type Rules *}
wenzelm@20140
   123
wenzelm@20140
   124
lemma lem: "[| a:B(u);  u=v |] ==> a : B(v)"
wenzelm@20140
   125
  by blast
wenzelm@20140
   126
wenzelm@20140
   127
wenzelm@20140
   128
ML {*
wenzelm@32153
   129
fun mk_ncanT_tac top_crls crls =
wenzelm@32153
   130
  SUBPROOF (fn {context = ctxt, prems = major :: prems, ...} =>
wenzelm@32153
   131
    resolve_tac ([major] RL top_crls) 1 THEN
wenzelm@35409
   132
    REPEAT_SOME (eresolve_tac (crls @ [@{thm exE}, @{thm bexE}, @{thm conjE}, @{thm disjE}])) THEN
wenzelm@51717
   133
    ALLGOALS (asm_simp_tac ctxt) THEN
wenzelm@32153
   134
    ALLGOALS (ares_tac (prems RL [@{thm lem}]) ORELSE' etac @{thm bspec}) THEN
wenzelm@42793
   135
    safe_tac (ctxt addSIs prems))
wenzelm@28272
   136
*}
wenzelm@20140
   137
wenzelm@32153
   138
method_setup ncanT = {*
wenzelm@32153
   139
  Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms case_rls} @{thms case_rls})
wenzelm@42814
   140
*}
wenzelm@20140
   141
wenzelm@32153
   142
lemma ifT:
wenzelm@32153
   143
  "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==>
wenzelm@32153
   144
    if b then t else u : A(b)"
wenzelm@32153
   145
  by ncanT
wenzelm@20140
   146
wenzelm@32153
   147
lemma applyT: "[| f : Pi(A,B);  a:A |] ==> f ` a : B(a)"
wenzelm@32153
   148
  by ncanT
wenzelm@20140
   149
wenzelm@32153
   150
lemma splitT:
wenzelm@32153
   151
  "[| p:Sigma(A,B); !!x y. [| x:A;  y:B(x); p=<x,y> |] ==> c(x,y):C(<x,y>) |]
wenzelm@32153
   152
    ==> split(p,c):C(p)"
wenzelm@32153
   153
  by ncanT
wenzelm@20140
   154
wenzelm@32153
   155
lemma whenT:
wenzelm@32153
   156
  "[| p:A+B; !!x.[| x:A;  p=inl(x) |] ==> a(x):C(inl(x)); !!y.[| y:B;  p=inr(y) |]
wenzelm@32153
   157
    ==> b(y):C(inr(y)) |] ==> when(p,a,b) : C(p)"
wenzelm@32153
   158
  by ncanT
wenzelm@20140
   159
wenzelm@20140
   160
lemmas ncanTs = ifT applyT splitT whenT
wenzelm@20140
   161
wenzelm@20140
   162
wenzelm@20140
   163
subsection {* Subtypes *}
wenzelm@20140
   164
wenzelm@20140
   165
lemma SubtypeD1: "a : Subtype(A, P) ==> a : A"
wenzelm@20140
   166
  and SubtypeD2: "a : Subtype(A, P) ==> P(a)"
wenzelm@20140
   167
  by (simp_all add: SubtypeXH)
wenzelm@20140
   168
wenzelm@20140
   169
lemma SubtypeI: "[| a:A;  P(a) |] ==> a : {x:A. P(x)}"
wenzelm@20140
   170
  by (simp add: SubtypeXH)
wenzelm@20140
   171
wenzelm@20140
   172
lemma SubtypeE: "[| a : {x:A. P(x)};  [| a:A;  P(a) |] ==> Q |] ==> Q"
wenzelm@20140
   173
  by (simp add: SubtypeXH)
wenzelm@20140
   174
wenzelm@20140
   175
wenzelm@20140
   176
subsection {* Monotonicity *}
wenzelm@20140
   177
wenzelm@20140
   178
lemma idM: "mono (%X. X)"
wenzelm@20140
   179
  apply (rule monoI)
wenzelm@20140
   180
  apply assumption
wenzelm@20140
   181
  done
wenzelm@20140
   182
wenzelm@20140
   183
lemma constM: "mono(%X. A)"
wenzelm@20140
   184
  apply (rule monoI)
wenzelm@20140
   185
  apply (rule subset_refl)
wenzelm@20140
   186
  done
wenzelm@20140
   187
wenzelm@20140
   188
lemma "mono(%X. A(X)) ==> mono(%X.[A(X)])"
wenzelm@20140
   189
  apply (rule subsetI [THEN monoI])
wenzelm@20140
   190
  apply (drule LiftXH [THEN iffD1])
wenzelm@20140
   191
  apply (erule disjE)
wenzelm@20140
   192
   apply (erule disjI1 [THEN LiftXH [THEN iffD2]])
wenzelm@20140
   193
  apply (rule disjI2 [THEN LiftXH [THEN iffD2]])
wenzelm@20140
   194
  apply (drule (1) monoD)
wenzelm@20140
   195
  apply blast
wenzelm@20140
   196
  done
wenzelm@20140
   197
wenzelm@20140
   198
lemma SgM:
wenzelm@20140
   199
  "[| mono(%X. A(X)); !!x X. x:A(X) ==> mono(%X. B(X,x)) |] ==>
wenzelm@20140
   200
    mono(%X. Sigma(A(X),B(X)))"
wenzelm@20140
   201
  by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls
wenzelm@20140
   202
    dest!: monoD [THEN subsetD])
wenzelm@20140
   203
wenzelm@20140
   204
lemma PiM:
wenzelm@20140
   205
  "[| !!x. x:A ==> mono(%X. B(X,x)) |] ==> mono(%X. Pi(A,B(X)))"
wenzelm@20140
   206
  by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls
wenzelm@20140
   207
    dest!: monoD [THEN subsetD])
wenzelm@20140
   208
wenzelm@20140
   209
lemma PlusM:
wenzelm@20140
   210
    "[| mono(%X. A(X));  mono(%X. B(X)) |] ==> mono(%X. A(X)+B(X))"
wenzelm@20140
   211
  by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls
wenzelm@20140
   212
    dest!: monoD [THEN subsetD])
wenzelm@20140
   213
wenzelm@20140
   214
wenzelm@20140
   215
subsection {* Recursive types *}
wenzelm@20140
   216
wenzelm@20140
   217
subsubsection {* Conversion Rules for Fixed Points via monotonicity and Tarski *}
wenzelm@20140
   218
wenzelm@41526
   219
lemma NatM: "mono(%X. Unit+X)"
wenzelm@20140
   220
  apply (rule PlusM constM idM)+
wenzelm@20140
   221
  done
wenzelm@20140
   222
wenzelm@20140
   223
lemma def_NatB: "Nat = Unit + Nat"
wenzelm@20140
   224
  apply (rule def_lfp_Tarski [OF Nat_def])
wenzelm@20140
   225
  apply (rule NatM)
wenzelm@20140
   226
  done
wenzelm@20140
   227
wenzelm@20140
   228
lemma ListM: "mono(%X.(Unit+Sigma(A,%y. X)))"
wenzelm@20140
   229
  apply (rule PlusM SgM constM idM)+
wenzelm@20140
   230
  done
wenzelm@20140
   231
wenzelm@20140
   232
lemma def_ListB: "List(A) = Unit + A * List(A)"
wenzelm@20140
   233
  apply (rule def_lfp_Tarski [OF List_def])
wenzelm@20140
   234
  apply (rule ListM)
wenzelm@20140
   235
  done
wenzelm@20140
   236
wenzelm@20140
   237
lemma def_ListsB: "Lists(A) = Unit + A * Lists(A)"
wenzelm@20140
   238
  apply (rule def_gfp_Tarski [OF Lists_def])
wenzelm@20140
   239
  apply (rule ListM)
wenzelm@20140
   240
  done
wenzelm@20140
   241
wenzelm@20140
   242
lemma IListsM: "mono(%X.({} + Sigma(A,%y. X)))"
wenzelm@20140
   243
  apply (rule PlusM SgM constM idM)+
wenzelm@20140
   244
  done
wenzelm@20140
   245
wenzelm@20140
   246
lemma def_IListsB: "ILists(A) = {} + A * ILists(A)"
wenzelm@20140
   247
  apply (rule def_gfp_Tarski [OF ILists_def])
wenzelm@20140
   248
  apply (rule IListsM)
wenzelm@20140
   249
  done
wenzelm@20140
   250
wenzelm@20140
   251
lemmas ind_type_eqs = def_NatB def_ListB def_ListsB def_IListsB
wenzelm@20140
   252
wenzelm@20140
   253
wenzelm@20140
   254
subsection {* Exhaustion Rules *}
wenzelm@20140
   255
wenzelm@20140
   256
lemma NatXH: "a : Nat <-> (a=zero | (EX x:Nat. a=succ(x)))"
wenzelm@20140
   257
  and ListXH: "a : List(A) <-> (a=[] | (EX x:A. EX xs:List(A).a=x$xs))"
wenzelm@20140
   258
  and ListsXH: "a : Lists(A) <-> (a=[] | (EX x:A. EX xs:Lists(A).a=x$xs))"
wenzelm@20140
   259
  and IListsXH: "a : ILists(A) <-> (EX x:A. EX xs:ILists(A).a=x$xs)"
wenzelm@20140
   260
  unfolding ind_data_defs
wenzelm@20140
   261
  by (rule ind_type_eqs [THEN XHlemma1], blast intro!: canTs elim!: case_rls)+
wenzelm@20140
   262
wenzelm@20140
   263
lemmas iXHs = NatXH ListXH
wenzelm@20140
   264
wenzelm@56199
   265
ML {* ML_Thms.bind_thms ("icase_rls", XH_to_Es @{thms iXHs}) *}
wenzelm@20140
   266
wenzelm@20140
   267
wenzelm@20140
   268
subsection {* Type Rules *}
wenzelm@20140
   269
wenzelm@20140
   270
lemma zeroT: "zero : Nat"
wenzelm@20140
   271
  and succT: "n:Nat ==> succ(n) : Nat"
wenzelm@20140
   272
  and nilT: "[] : List(A)"
wenzelm@20140
   273
  and consT: "[| h:A;  t:List(A) |] ==> h$t : List(A)"
wenzelm@20140
   274
  by (blast intro: iXHs [THEN iffD2])+
wenzelm@20140
   275
wenzelm@20140
   276
lemmas icanTs = zeroT succT nilT consT
wenzelm@20140
   277
wenzelm@32153
   278
wenzelm@32153
   279
method_setup incanT = {*
wenzelm@32153
   280
  Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms icase_rls} @{thms case_rls})
wenzelm@42814
   281
*}
wenzelm@20140
   282
wenzelm@32153
   283
lemma ncaseT:
wenzelm@32153
   284
  "[| n:Nat; n=zero ==> b:C(zero); !!x.[| x:Nat;  n=succ(x) |] ==> c(x):C(succ(x)) |]
wenzelm@32153
   285
    ==> ncase(n,b,c) : C(n)"
wenzelm@32153
   286
  by incanT
wenzelm@20140
   287
wenzelm@32153
   288
lemma lcaseT:
wenzelm@32153
   289
  "[| l:List(A); l=[] ==> b:C([]); !!h t.[| h:A;  t:List(A); l=h$t |] ==>
wenzelm@32153
   290
    c(h,t):C(h$t) |] ==> lcase(l,b,c) : C(l)"
wenzelm@32153
   291
  by incanT
wenzelm@20140
   292
wenzelm@20140
   293
lemmas incanTs = ncaseT lcaseT
wenzelm@20140
   294
wenzelm@20140
   295
wenzelm@20140
   296
subsection {* Induction Rules *}
wenzelm@20140
   297
wenzelm@20140
   298
lemmas ind_Ms = NatM ListM
wenzelm@20140
   299
wenzelm@20140
   300
lemma Nat_ind: "[| n:Nat; P(zero); !!x.[| x:Nat; P(x) |] ==> P(succ(x)) |] ==> P(n)"
wenzelm@20140
   301
  apply (unfold ind_data_defs)
wenzelm@20140
   302
  apply (erule def_induct [OF Nat_def _ NatM])
wenzelm@20140
   303
  apply (blast intro: canTs elim!: case_rls)
wenzelm@20140
   304
  done
wenzelm@20140
   305
wenzelm@20140
   306
lemma List_ind:
wenzelm@20140
   307
  "[| l:List(A); P([]); !!x xs.[| x:A;  xs:List(A); P(xs) |] ==> P(x$xs) |] ==> P(l)"
wenzelm@20140
   308
  apply (unfold ind_data_defs)
wenzelm@20140
   309
  apply (erule def_induct [OF List_def _ ListM])
wenzelm@20140
   310
  apply (blast intro: canTs elim!: case_rls)
wenzelm@20140
   311
  done
wenzelm@20140
   312
wenzelm@20140
   313
lemmas inds = Nat_ind List_ind
wenzelm@20140
   314
wenzelm@20140
   315
wenzelm@20140
   316
subsection {* Primitive Recursive Rules *}
wenzelm@20140
   317
wenzelm@20140
   318
lemma nrecT:
wenzelm@20140
   319
  "[| n:Nat; b:C(zero);
wenzelm@20140
   320
      !!x g.[| x:Nat; g:C(x) |] ==> c(x,g):C(succ(x)) |] ==>
wenzelm@20140
   321
      nrec(n,b,c) : C(n)"
wenzelm@20140
   322
  by (erule Nat_ind) auto
wenzelm@20140
   323
wenzelm@20140
   324
lemma lrecT:
wenzelm@20140
   325
  "[| l:List(A); b:C([]);
wenzelm@20140
   326
      !!x xs g.[| x:A;  xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x$xs) |] ==>
wenzelm@20140
   327
      lrec(l,b,c) : C(l)"
wenzelm@20140
   328
  by (erule List_ind) auto
wenzelm@20140
   329
wenzelm@20140
   330
lemmas precTs = nrecT lrecT
wenzelm@20140
   331
wenzelm@20140
   332
wenzelm@20140
   333
subsection {* Theorem proving *}
wenzelm@20140
   334
wenzelm@20140
   335
lemma SgE2:
wenzelm@20140
   336
  "[| <a,b> : Sigma(A,B);  [| a:A;  b:B(a) |] ==> P |] ==> P"
wenzelm@20140
   337
  unfolding SgXH by blast
wenzelm@20140
   338
wenzelm@20140
   339
(* General theorem proving ignores non-canonical term-formers,             *)
wenzelm@20140
   340
(*         - intro rules are type rules for canonical terms                *)
wenzelm@20140
   341
(*         - elim rules are case rules (no non-canonical terms appear)     *)
wenzelm@20140
   342
wenzelm@56199
   343
ML {* ML_Thms.bind_thms ("XHEs", XH_to_Es @{thms XHs}) *}
wenzelm@20140
   344
wenzelm@20140
   345
lemmas [intro!] = SubtypeI canTs icanTs
wenzelm@20140
   346
  and [elim!] = SubtypeE XHEs
wenzelm@20140
   347
wenzelm@20140
   348
wenzelm@20140
   349
subsection {* Infinite Data Types *}
wenzelm@20140
   350
wenzelm@20140
   351
lemma lfp_subset_gfp: "mono(f) ==> lfp(f) <= gfp(f)"
wenzelm@20140
   352
  apply (rule lfp_lowerbound [THEN subset_trans])
wenzelm@20140
   353
   apply (erule gfp_lemma3)
wenzelm@20140
   354
  apply (rule subset_refl)
wenzelm@20140
   355
  done
wenzelm@20140
   356
wenzelm@20140
   357
lemma gfpI:
wenzelm@20140
   358
  assumes "a:A"
wenzelm@20140
   359
    and "!!x X.[| x:A;  ALL y:A. t(y):X |] ==> t(x) : B(X)"
wenzelm@20140
   360
  shows "t(a) : gfp(B)"
wenzelm@20140
   361
  apply (rule coinduct)
wenzelm@20140
   362
   apply (rule_tac P = "%x. EX y:A. x=t (y)" in CollectI)
wenzelm@41526
   363
   apply (blast intro!: assms)+
wenzelm@20140
   364
  done
wenzelm@20140
   365
wenzelm@20140
   366
lemma def_gfpI:
wenzelm@20140
   367
  "[| C==gfp(B);  a:A;  !!x X.[| x:A;  ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==>
wenzelm@20140
   368
    t(a) : C"
wenzelm@20140
   369
  apply unfold
wenzelm@20140
   370
  apply (erule gfpI)
wenzelm@20140
   371
  apply blast
wenzelm@20140
   372
  done
wenzelm@20140
   373
wenzelm@20140
   374
(* EG *)
wenzelm@20140
   375
lemma "letrec g x be zero$g(x) in g(bot) : Lists(Nat)"
wenzelm@20140
   376
  apply (rule refl [THEN UnitXH [THEN iffD2], THEN Lists_def [THEN def_gfpI]])
wenzelm@20140
   377
  apply (subst letrecB)
wenzelm@20140
   378
  apply (unfold cons_def)
wenzelm@20140
   379
  apply blast
wenzelm@20140
   380
  done
wenzelm@20140
   381
wenzelm@20140
   382
wenzelm@20140
   383
subsection {* Lemmas and tactics for using the rule @{text
wenzelm@20140
   384
  "coinduct3"} on @{text "[="} and @{text "="} *}
wenzelm@20140
   385
wenzelm@20140
   386
lemma lfpI: "[| mono(f);  a : f(lfp(f)) |] ==> a : lfp(f)"
wenzelm@20140
   387
  apply (erule lfp_Tarski [THEN ssubst])
wenzelm@20140
   388
  apply assumption
wenzelm@20140
   389
  done
wenzelm@20140
   390
wenzelm@20140
   391
lemma ssubst_single: "[| a=a';  a' : A |] ==> a : A"
wenzelm@20140
   392
  by simp
wenzelm@20140
   393
wenzelm@20140
   394
lemma ssubst_pair: "[| a=a';  b=b';  <a',b'> : A |] ==> <a,b> : A"
wenzelm@20140
   395
  by simp
wenzelm@20140
   396
wenzelm@20140
   397
wenzelm@32153
   398
ML {*
wenzelm@32153
   399
  val coinduct3_tac = SUBPROOF (fn {context = ctxt, prems = mono :: prems, ...} =>
wenzelm@42793
   400
    fast_tac (ctxt addIs (mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1);
wenzelm@32153
   401
*}
wenzelm@32153
   402
wenzelm@42814
   403
method_setup coinduct3 = {* Scan.succeed (SIMPLE_METHOD' o coinduct3_tac) *}
wenzelm@32153
   404
wenzelm@32153
   405
lemma ci3_RI: "[| mono(Agen);  a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)"
wenzelm@32153
   406
  by coinduct3
wenzelm@32153
   407
wenzelm@32153
   408
lemma ci3_AgenI: "[| mono(Agen);  a : Agen(lfp(%x. Agen(x) Un R Un A)) |] ==>
wenzelm@32153
   409
    a : lfp(%x. Agen(x) Un R Un A)"
wenzelm@32153
   410
  by coinduct3
wenzelm@32153
   411
wenzelm@32153
   412
lemma ci3_AI: "[| mono(Agen);  a : A |] ==> a : lfp(%x. Agen(x) Un R Un A)"
wenzelm@32153
   413
  by coinduct3
wenzelm@20140
   414
wenzelm@20140
   415
ML {*
wenzelm@32153
   416
fun genIs_tac ctxt genXH gen_mono =
wenzelm@42480
   417
  rtac (genXH RS @{thm iffD2}) THEN'
wenzelm@51717
   418
  simp_tac ctxt THEN'
wenzelm@42793
   419
  TRY o fast_tac
wenzelm@42793
   420
    (ctxt addIs [genXH RS @{thm iffD2}, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}])
wenzelm@32153
   421
*}
wenzelm@20140
   422
wenzelm@32153
   423
method_setup genIs = {*
wenzelm@42814
   424
  Attrib.thm -- Attrib.thm >>
wenzelm@42814
   425
    (fn (genXH, gen_mono) => fn ctxt => SIMPLE_METHOD' (genIs_tac ctxt genXH gen_mono))
wenzelm@42814
   426
*}
wenzelm@20140
   427
wenzelm@20140
   428
wenzelm@20140
   429
subsection {* POgen *}
wenzelm@20140
   430
wenzelm@20140
   431
lemma PO_refl: "<a,a> : PO"
wenzelm@32153
   432
  by (rule po_refl [THEN PO_iff [THEN iffD1]])
wenzelm@32153
   433
wenzelm@32153
   434
lemma POgenIs:
wenzelm@32153
   435
  "<true,true> : POgen(R)"
wenzelm@32153
   436
  "<false,false> : POgen(R)"
wenzelm@32153
   437
  "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)"
wenzelm@32153
   438
  "!!b b'. [|!!x. <b(x),b'(x)> : R |] ==><lam x. b(x),lam x. b'(x)> : POgen(R)"
wenzelm@32153
   439
  "<one,one> : POgen(R)"
wenzelm@32153
   440
  "<a,a'> : lfp(%x. POgen(x) Un R Un PO) ==>
wenzelm@32153
   441
    <inl(a),inl(a')> : POgen(lfp(%x. POgen(x) Un R Un PO))"
wenzelm@32153
   442
  "<b,b'> : lfp(%x. POgen(x) Un R Un PO) ==>
wenzelm@32153
   443
    <inr(b),inr(b')> : POgen(lfp(%x. POgen(x) Un R Un PO))"
wenzelm@32153
   444
  "<zero,zero> : POgen(lfp(%x. POgen(x) Un R Un PO))"
wenzelm@32153
   445
  "<n,n'> : lfp(%x. POgen(x) Un R Un PO) ==>
wenzelm@32153
   446
    <succ(n),succ(n')> : POgen(lfp(%x. POgen(x) Un R Un PO))"
wenzelm@32153
   447
  "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))"
wenzelm@32153
   448
  "[| <h,h'> : lfp(%x. POgen(x) Un R Un PO);  <t,t'> : lfp(%x. POgen(x) Un R Un PO) |]
wenzelm@32153
   449
    ==> <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"
wenzelm@32153
   450
  unfolding data_defs by (genIs POgenXH POgen_mono)+
wenzelm@20140
   451
wenzelm@20140
   452
ML {*
wenzelm@32153
   453
fun POgen_tac ctxt (rla, rlb) i =
wenzelm@42793
   454
  SELECT_GOAL (safe_tac ctxt) i THEN
wenzelm@32010
   455
  rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN
wenzelm@32153
   456
  (REPEAT (resolve_tac
wenzelm@32153
   457
      (@{thms POgenIs} @ [@{thm PO_refl} RS (@{thm POgen_mono} RS @{thm ci3_AI})] @
wenzelm@32153
   458
        (@{thms POgenIs} RL [@{thm POgen_mono} RS @{thm ci3_AgenI}]) @
wenzelm@32153
   459
        [@{thm POgen_mono} RS @{thm ci3_RI}]) i))
wenzelm@20140
   460
*}
wenzelm@20140
   461
wenzelm@20140
   462
wenzelm@20140
   463
subsection {* EQgen *}
wenzelm@20140
   464
wenzelm@20140
   465
lemma EQ_refl: "<a,a> : EQ"
wenzelm@32153
   466
  by (rule refl [THEN EQ_iff [THEN iffD1]])
wenzelm@32153
   467
wenzelm@32153
   468
lemma EQgenIs:
wenzelm@32153
   469
  "<true,true> : EQgen(R)"
wenzelm@32153
   470
  "<false,false> : EQgen(R)"
wenzelm@32153
   471
  "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)"
wenzelm@32153
   472
  "!!b b'. [|!!x. <b(x),b'(x)> : R |] ==> <lam x. b(x),lam x. b'(x)> : EQgen(R)"
wenzelm@32153
   473
  "<one,one> : EQgen(R)"
wenzelm@32153
   474
  "<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==>
wenzelm@32153
   475
    <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
wenzelm@32153
   476
  "<b,b'> : lfp(%x. EQgen(x) Un R Un EQ) ==>
wenzelm@32153
   477
    <inr(b),inr(b')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
wenzelm@32153
   478
  "<zero,zero> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
wenzelm@32153
   479
  "<n,n'> : lfp(%x. EQgen(x) Un R Un EQ) ==>
wenzelm@32153
   480
    <succ(n),succ(n')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
wenzelm@32153
   481
  "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
wenzelm@32153
   482
  "[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) |]
wenzelm@32153
   483
    ==> <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
wenzelm@32153
   484
  unfolding data_defs by (genIs EQgenXH EQgen_mono)+
wenzelm@20140
   485
wenzelm@20140
   486
ML {*
wenzelm@20140
   487
fun EQgen_raw_tac i =
wenzelm@32153
   488
  (REPEAT (resolve_tac (@{thms EQgenIs} @
wenzelm@32153
   489
        [@{thm EQ_refl} RS (@{thm EQgen_mono} RS @{thm ci3_AI})] @
wenzelm@32153
   490
        (@{thms EQgenIs} RL [@{thm EQgen_mono} RS @{thm ci3_AgenI}]) @
wenzelm@32153
   491
        [@{thm EQgen_mono} RS @{thm ci3_RI}]) i))
wenzelm@20140
   492
wenzelm@20140
   493
(* Goals of the form R <= EQgen(R) - rewrite elements <a,b> : EQgen(R) using rews and *)
wenzelm@20140
   494
(* then reduce this to a goal <a',b'> : R (hopefully?)                                *)
wenzelm@20140
   495
(*      rews are rewrite rules that would cause looping in the simpifier              *)
wenzelm@20140
   496
wenzelm@23894
   497
fun EQgen_tac ctxt rews i =
wenzelm@20140
   498
 SELECT_GOAL
wenzelm@42793
   499
   (TRY (safe_tac ctxt) THEN
wenzelm@35409
   500
    resolve_tac ((rews @ [@{thm refl}]) RL ((rews @ [@{thm refl}]) RL [@{thm ssubst_pair}])) i THEN
wenzelm@51717
   501
    ALLGOALS (simp_tac ctxt) THEN
wenzelm@20140
   502
    ALLGOALS EQgen_raw_tac) i
wenzelm@20140
   503
*}
clasohm@0
   504
clasohm@0
   505
end