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