src/CCL/hered.ML
author paulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 1511 09354d37a5ab
parent 289 78541329ff35
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
clasohm@0
     1
(*  Title: 	CCL/hered
clasohm@0
     2
    ID:         $Id$
clasohm@0
     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
clasohm@0
    15
goalw Hered.thy [HTTgen_def]  "mono(%X.HTTgen(X))";
clasohm@0
    16
br monoI 1;
clasohm@0
    17
by (fast_tac set_cs 1);
clasohm@0
    18
val HTTgen_mono = result();
clasohm@0
    19
clasohm@0
    20
goalw Hered.thy [HTTgen_def]
clasohm@0
    21
  "t : HTTgen(A) <-> t=true | t=false | (EX a b.t=<a,b> & a : A & b : A) | \
clasohm@0
    22
\                                       (EX f.t=lam x.f(x) & (ALL x.f(x) : A))";
clasohm@0
    23
by (fast_tac set_cs 1);
clasohm@0
    24
val HTTgenXH = result();
clasohm@0
    25
clasohm@0
    26
goal Hered.thy
clasohm@0
    27
  "t : HTT <-> t=true | t=false | (EX a b.t=<a,b> & a : HTT & b : HTT) | \
clasohm@0
    28
\                                  (EX f.t=lam x.f(x) & (ALL x.f(x) : HTT))";
clasohm@0
    29
br (rewrite_rule [HTTgen_def] 
clasohm@0
    30
                 (HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1;
clasohm@0
    31
by (fast_tac set_cs 1);
clasohm@0
    32
val HTTXH = result();
clasohm@0
    33
clasohm@0
    34
(*** Introduction Rules for HTT ***)
clasohm@0
    35
clasohm@0
    36
goal Hered.thy "~ bot : HTT";
clasohm@0
    37
by (fast_tac (term_cs addDs [XH_to_D HTTXH]) 1);
clasohm@0
    38
val HTT_bot = result();
clasohm@0
    39
clasohm@0
    40
goal Hered.thy "true : HTT";
clasohm@0
    41
by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
clasohm@0
    42
val HTT_true = result();
clasohm@0
    43
clasohm@0
    44
goal Hered.thy "false : HTT";
clasohm@0
    45
by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
clasohm@0
    46
val HTT_false = result();
clasohm@0
    47
clasohm@0
    48
goal Hered.thy "<a,b> : HTT <->  a : HTT  & b : HTT";
clasohm@0
    49
br (HTTXH RS iff_trans) 1;
clasohm@0
    50
by (fast_tac term_cs 1);
clasohm@0
    51
val HTT_pair = result();
clasohm@0
    52
clasohm@0
    53
goal Hered.thy "lam x.f(x) : HTT <-> (ALL x. f(x) : HTT)";
clasohm@0
    54
br (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@0
    59
val HTT_lam = result();
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";
clasohm@0
    81
br (HTT_def RS def_coinduct) 1;
clasohm@0
    82
by (REPEAT (ares_tac prems 1));
clasohm@0
    83
val HTT_coinduct = result();
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";
clasohm@0
    89
br (HTTgen_mono RSN(3,HTT_def RS def_coinduct3)) 1;
clasohm@0
    90
by (REPEAT (ares_tac prems 1));
clasohm@0
    91
val HTT_coinduct3 = result();
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)",
clasohm@0
   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
clasohm@0
   115
goal Hered.thy "Unit <= HTT";
lcp@8
   116
by (simp_tac (CCL_ss addsimps ([subsetXH,UnitXH] @ HTT_rews)) 1);
clasohm@0
   117
val UnitF = result();
clasohm@0
   118
clasohm@0
   119
goal Hered.thy "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@0
   122
val BoolF = result();
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@0
   127
val PlusF = result();
clasohm@0
   128
clasohm@0
   129
val prems = goal Hered.thy 
clasohm@0
   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@0
   133
val SigmaF = result();
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*)
clasohm@0
   139
goal Hered.thy "Nat <= HTT";
lcp@8
   140
by (simp_tac (term_ss addsimps [subsetXH]) 1);
clasohm@0
   141
by (safe_tac set_cs);
clasohm@0
   142
be 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
clasohm@0
   146
goal Hered.thy "Nat <= HTT";
clasohm@0
   147
by (safe_tac set_cs);
clasohm@0
   148
be 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@0
   151
val NatF = result();
clasohm@0
   152
clasohm@0
   153
val [prem] = goal Hered.thy "A <= HTT ==> List(A) <= HTT";
clasohm@0
   154
by (safe_tac set_cs);
clasohm@0
   155
be 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@0
   159
val ListF = result();
clasohm@0
   160
clasohm@0
   161
val [prem] = goal Hered.thy "A <= HTT ==> Lists(A) <= HTT";
clasohm@0
   162
by (safe_tac set_cs);
clasohm@0
   163
be 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@0
   167
val ListsF = result();
clasohm@0
   168
clasohm@0
   169
val [prem] = goal Hered.thy "A <= HTT ==> ILists(A) <= HTT";
clasohm@0
   170
by (safe_tac set_cs);
clasohm@0
   171
be 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@0
   175
val IListsF = result();
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";
clasohm@0
   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);
clasohm@0
   184
bd (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@0
   189
val HTT_po_op = result();
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@0
   193
val HTT_po_eq = result();
clasohm@0
   194
*)