src/CCL/Hered.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5062 fbdb0b541314
child 17456 bcf7544875b2
permissions -rw-r--r--
tidying
clasohm@1459
     1
(*  Title:      CCL/hered
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
For hered.thy.
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open Hered;
clasohm@0
    10
clasohm@0
    11
fun type_of_terms (Const("Trueprop",_) $ (Const("op =",(Type ("fun", [t,_])))$_$_)) = t;
clasohm@0
    12
clasohm@0
    13
(*** Hereditary Termination ***)
clasohm@0
    14
wenzelm@5062
    15
Goalw [HTTgen_def]  "mono(%X. HTTgen(X))";
lcp@642
    16
by (rtac monoI 1);
clasohm@0
    17
by (fast_tac set_cs 1);
clasohm@757
    18
qed "HTTgen_mono";
clasohm@0
    19
wenzelm@5062
    20
Goalw [HTTgen_def]
wenzelm@3837
    21
  "t : HTTgen(A) <-> t=true | t=false | (EX a b. t=<a,b> & a : A & b : A) | \
wenzelm@3837
    22
\                                       (EX f. t=lam x. f(x) & (ALL x. f(x) : A))";
clasohm@0
    23
by (fast_tac set_cs 1);
clasohm@757
    24
qed "HTTgenXH";
clasohm@0
    25
wenzelm@5062
    26
Goal
wenzelm@3837
    27
  "t : HTT <-> t=true | t=false | (EX a b. t=<a,b> & a : HTT & b : HTT) | \
wenzelm@3837
    28
\                                  (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))";
wenzelm@4423
    29
by (rtac (rewrite_rule [HTTgen_def] 
wenzelm@4423
    30
                 (HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1);
clasohm@0
    31
by (fast_tac set_cs 1);
clasohm@757
    32
qed "HTTXH";
clasohm@0
    33
clasohm@0
    34
(*** Introduction Rules for HTT ***)
clasohm@0
    35
wenzelm@5062
    36
Goal "~ bot : HTT";
clasohm@0
    37
by (fast_tac (term_cs addDs [XH_to_D HTTXH]) 1);
clasohm@757
    38
qed "HTT_bot";
clasohm@0
    39
wenzelm@5062
    40
Goal "true : HTT";
clasohm@0
    41
by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
clasohm@757
    42
qed "HTT_true";
clasohm@0
    43
wenzelm@5062
    44
Goal "false : HTT";
clasohm@0
    45
by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
clasohm@757
    46
qed "HTT_false";
clasohm@0
    47
wenzelm@5062
    48
Goal "<a,b> : HTT <->  a : HTT  & b : HTT";
lcp@642
    49
by (rtac (HTTXH RS iff_trans) 1);
clasohm@0
    50
by (fast_tac term_cs 1);
clasohm@757
    51
qed "HTT_pair";
clasohm@0
    52
wenzelm@5062
    53
Goal "lam x. f(x) : HTT <-> (ALL x. f(x) : HTT)";
lcp@642
    54
by (rtac (HTTXH RS iff_trans) 1);
lcp@8
    55
by (simp_tac term_ss 1);
clasohm@0
    56
by (safe_tac term_cs);
lcp@8
    57
by (asm_simp_tac term_ss 1);
clasohm@0
    58
by (fast_tac term_cs 1);
clasohm@757
    59
qed "HTT_lam";
clasohm@0
    60
clasohm@0
    61
local
clasohm@0
    62
  val raw_HTTrews = [HTT_bot,HTT_true,HTT_false,HTT_pair,HTT_lam];
clasohm@0
    63
  fun mk_thm s = prove_goalw Hered.thy data_defs s (fn _ => 
lcp@8
    64
                  [simp_tac (term_ss addsimps raw_HTTrews) 1]);
clasohm@0
    65
in
clasohm@0
    66
  val HTT_rews = raw_HTTrews @
clasohm@0
    67
               map mk_thm ["one : HTT",
clasohm@0
    68
                           "inl(a) : HTT <-> a : HTT",
clasohm@0
    69
                           "inr(b) : HTT <-> b : HTT",
clasohm@0
    70
                           "zero : HTT",
clasohm@0
    71
                           "succ(n) : HTT <-> n : HTT",
clasohm@0
    72
                           "[] : HTT",
clasohm@289
    73
                           "x$xs : HTT <-> x : HTT & xs : HTT"];
clasohm@0
    74
end;
clasohm@0
    75
clasohm@0
    76
val HTT_Is = HTT_rews @ (HTT_rews RL [iffD2]);
clasohm@0
    77
clasohm@0
    78
(*** Coinduction for HTT ***)
clasohm@0
    79
clasohm@0
    80
val prems = goal Hered.thy "[|  t : R;  R <= HTTgen(R) |] ==> t : HTT";
lcp@642
    81
by (rtac (HTT_def RS def_coinduct) 1);
clasohm@0
    82
by (REPEAT (ares_tac prems 1));
clasohm@757
    83
qed "HTT_coinduct";
clasohm@0
    84
clasohm@0
    85
fun HTT_coinduct_tac s i = res_inst_tac [("R",s)] HTT_coinduct i;
clasohm@0
    86
clasohm@0
    87
val prems = goal Hered.thy 
clasohm@0
    88
    "[|  t : R;   R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT";
lcp@642
    89
by (rtac (HTTgen_mono RSN(3,HTT_def RS def_coinduct3)) 1);
clasohm@0
    90
by (REPEAT (ares_tac prems 1));
clasohm@757
    91
qed "HTT_coinduct3";
clasohm@0
    92
val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3;
clasohm@0
    93
clasohm@0
    94
fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] HTT_coinduct3 i;
clasohm@0
    95
clasohm@0
    96
val HTTgenIs = map (mk_genIs Hered.thy data_defs HTTgenXH HTTgen_mono)
clasohm@0
    97
       ["true : HTTgen(R)",
clasohm@0
    98
        "false : HTTgen(R)",
clasohm@0
    99
        "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)",
wenzelm@3837
   100
        "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)",
clasohm@0
   101
        "one : HTTgen(R)",
clasohm@0
   102
        "a : lfp(%x. HTTgen(x) Un R Un HTT) ==> \
clasohm@0
   103
\                         inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
clasohm@0
   104
        "b : lfp(%x. HTTgen(x) Un R Un HTT) ==> \
clasohm@0
   105
\                         inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
clasohm@0
   106
        "zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
clasohm@0
   107
        "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> \
clasohm@0
   108
\                         succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
clasohm@0
   109
        "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
clasohm@0
   110
        "[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==>\
clasohm@289
   111
\                         h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))"];
clasohm@0
   112
clasohm@0
   113
(*** Formation Rules for Types ***)
clasohm@0
   114
wenzelm@5062
   115
Goal "Unit <= HTT";
lcp@8
   116
by (simp_tac (CCL_ss addsimps ([subsetXH,UnitXH] @ HTT_rews)) 1);
clasohm@757
   117
qed "UnitF";
clasohm@0
   118
wenzelm@5062
   119
Goal "Bool <= HTT";
lcp@8
   120
by (simp_tac (CCL_ss addsimps ([subsetXH,BoolXH] @ HTT_rews)) 1);
clasohm@0
   121
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
clasohm@757
   122
qed "BoolF";
clasohm@0
   123
clasohm@0
   124
val prems = goal Hered.thy "[| A <= HTT;  B <= HTT |] ==> A + B  <= HTT";
lcp@8
   125
by (simp_tac (CCL_ss addsimps ([subsetXH,PlusXH] @ HTT_rews)) 1);
clasohm@0
   126
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
clasohm@757
   127
qed "PlusF";
clasohm@0
   128
clasohm@0
   129
val prems = goal Hered.thy 
wenzelm@3837
   130
     "[| A <= HTT;  !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT";
lcp@8
   131
by (simp_tac (CCL_ss addsimps ([subsetXH,SgXH] @ HTT_rews)) 1);
clasohm@0
   132
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
clasohm@757
   133
qed "SigmaF";
clasohm@0
   134
clasohm@0
   135
(*** Formation Rules for Recursive types - using coinduction these only need ***)
clasohm@0
   136
(***                                          exhaution rule for type-former ***)
clasohm@0
   137
clasohm@0
   138
(*Proof by induction - needs induction rule for type*)
wenzelm@5062
   139
Goal "Nat <= HTT";
lcp@8
   140
by (simp_tac (term_ss addsimps [subsetXH]) 1);
clasohm@0
   141
by (safe_tac set_cs);
lcp@642
   142
by (etac Nat_ind 1);
clasohm@0
   143
by (ALLGOALS (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD]))));
clasohm@0
   144
val NatF = result();
clasohm@0
   145
wenzelm@5062
   146
Goal "Nat <= HTT";
clasohm@0
   147
by (safe_tac set_cs);
lcp@642
   148
by (etac HTT_coinduct3 1);
clasohm@0
   149
by (fast_tac (set_cs addIs HTTgenIs 
clasohm@0
   150
                 addSEs [HTTgen_mono RS ci3_RI] addEs [XH_to_E NatXH]) 1);
clasohm@757
   151
qed "NatF";
clasohm@0
   152
clasohm@0
   153
val [prem] = goal Hered.thy "A <= HTT ==> List(A) <= HTT";
clasohm@0
   154
by (safe_tac set_cs);
lcp@642
   155
by (etac HTT_coinduct3 1);
clasohm@0
   156
by (fast_tac (set_cs addSIs HTTgenIs 
clasohm@0
   157
                 addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] 
clasohm@0
   158
                 addEs [XH_to_E ListXH]) 1);
clasohm@757
   159
qed "ListF";
clasohm@0
   160
clasohm@0
   161
val [prem] = goal Hered.thy "A <= HTT ==> Lists(A) <= HTT";
clasohm@0
   162
by (safe_tac set_cs);
lcp@642
   163
by (etac HTT_coinduct3 1);
clasohm@0
   164
by (fast_tac (set_cs addSIs HTTgenIs 
clasohm@0
   165
                 addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] 
clasohm@0
   166
                 addEs [XH_to_E ListsXH]) 1);
clasohm@757
   167
qed "ListsF";
clasohm@0
   168
clasohm@0
   169
val [prem] = goal Hered.thy "A <= HTT ==> ILists(A) <= HTT";
clasohm@0
   170
by (safe_tac set_cs);
lcp@642
   171
by (etac HTT_coinduct3 1);
clasohm@0
   172
by (fast_tac (set_cs addSIs HTTgenIs 
clasohm@0
   173
                 addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] 
clasohm@0
   174
                 addEs [XH_to_E IListsXH]) 1);
clasohm@757
   175
qed "IListsF";
clasohm@0
   176
clasohm@0
   177
(*** A possible use for this predicate is proving equality from pre-order       ***)
clasohm@0
   178
(*** but it seems as easy (and more general) to do this directly by coinduction ***)
clasohm@0
   179
(*
clasohm@0
   180
val prems = goal Hered.thy "[| t : HTT;  t [= u |] ==> u [= t";
wenzelm@3837
   181
by (po_coinduct_tac "{p. EX a b. p=<a,b> & b : HTT & b [= a}" 1);
clasohm@0
   182
by (fast_tac (ccl_cs addIs prems) 1);
clasohm@0
   183
by (safe_tac ccl_cs);
lcp@642
   184
by (dtac (poXH RS iffD1) 1);
clasohm@0
   185
by (safe_tac (set_cs addSEs [HTT_bot RS notE]));
clasohm@0
   186
by (REPEAT_SOME (rtac (POgenXH RS iffD2) ORELSE' etac rev_mp));
lcp@8
   187
by (ALLGOALS (simp_tac (term_ss addsimps HTT_rews)));
clasohm@0
   188
by (ALLGOALS (fast_tac ccl_cs));
clasohm@757
   189
qed "HTT_po_op";
clasohm@0
   190
clasohm@0
   191
val prems = goal Hered.thy "[| t : HTT;  t [= u |] ==> t = u";
clasohm@0
   192
by (REPEAT (ares_tac (prems @ [conjI RS (eq_iff RS iffD2),HTT_po_op]) 1));
clasohm@757
   193
qed "HTT_po_eq";
clasohm@0
   194
*)