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