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