src/CCL/coinduction.ML
author paulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 1511 09354d37a5ab
parent 1459 d12da312eff4
child 2035 e329b36d9136
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:      92/CCL/coinduction
     2     ID:         $Id$
     3     Author:     Martin Coen, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Lemmas and tactics for using the rule coinduct3 on [= and =.
     7 *)
     8 
     9 val [mono,prem] = goal Lfp.thy "[| mono(f);  a : f(lfp(f)) |] ==> a : lfp(f)";
    10 by (rtac ((mono RS lfp_Tarski) RS ssubst) 1);
    11 by (rtac prem 1);
    12 qed "lfpI";
    13 
    14 val prems = goal CCL.thy "[| a=a';  a' : A |] ==> a : A";
    15 by (simp_tac (term_ss addsimps prems) 1);
    16 qed "ssubst_single";
    17 
    18 val prems = goal CCL.thy "[| a=a';  b=b';  <a',b'> : A |] ==> <a,b> : A";
    19 by (simp_tac (term_ss addsimps prems) 1);
    20 qed "ssubst_pair";
    21 
    22 (***)
    23 
    24 local 
    25 fun mk_thm s = prove_goal Term.thy s (fn mono::prems => 
    26        [fast_tac (term_cs addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1]);
    27 in
    28 val ci3_RI    = mk_thm "[|  mono(Agen);  a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)";
    29 val ci3_AgenI = mk_thm "[|  mono(Agen);  a : Agen(lfp(%x. Agen(x) Un R Un A)) |] ==> \
    30 \                       a : lfp(%x. Agen(x) Un R Un A)";
    31 val ci3_AI    = mk_thm "[|  mono(Agen);  a : A |] ==> a : lfp(%x. Agen(x) Un R Un A)";
    32 end;
    33 
    34 fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s 
    35       (fn prems => [rtac (genXH RS iffD2) 1,
    36                     (simp_tac term_ss 1),
    37                     TRY (fast_tac (term_cs addIs 
    38                             ([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI]
    39                              @ prems)) 1)]);
    40 
    41 (** POgen **)
    42 
    43 goal Term.thy "<a,a> : PO";
    44 by (rtac (po_refl RS (XH_to_D PO_iff)) 1);
    45 qed "PO_refl";
    46 
    47 val POgenIs = map (mk_genIs Term.thy data_defs POgenXH POgen_mono)
    48       ["<true,true> : POgen(R)",
    49        "<false,false> : POgen(R)",
    50        "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)",
    51        "[|!!x. <b(x),b'(x)> : R |] ==><lam x.b(x),lam x.b'(x)> : POgen(R)",
    52        "<one,one> : POgen(R)",
    53        "<a,a'> : lfp(%x. POgen(x) Un R Un PO) ==> \
    54 \                         <inl(a),inl(a')> : POgen(lfp(%x. POgen(x) Un R Un PO))",
    55        "<b,b'> : lfp(%x. POgen(x) Un R Un PO) ==> \
    56 \                         <inr(b),inr(b')> : POgen(lfp(%x. POgen(x) Un R Un PO))",
    57        "<zero,zero> : POgen(lfp(%x. POgen(x) Un R Un PO))",
    58        "<n,n'> : lfp(%x. POgen(x) Un R Un PO) ==> \
    59 \                         <succ(n),succ(n')> : POgen(lfp(%x. POgen(x) Un R Un PO))",
    60        "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))",
    61        "[| <h,h'> : lfp(%x. POgen(x) Un R Un PO); \
    62 \          <t,t'> : lfp(%x. POgen(x) Un R Un PO) |] ==> \
    63 \       <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"];
    64 
    65 fun POgen_tac (rla,rlb) i =
    66        SELECT_GOAL (safe_tac ccl_cs) i THEN
    67        rtac (rlb RS (rla RS ssubst_pair)) i THEN
    68        (REPEAT (resolve_tac (POgenIs @ [PO_refl RS (POgen_mono RS ci3_AI)] @ 
    69                    (POgenIs RL [POgen_mono RS ci3_AgenI]) @ [POgen_mono RS ci3_RI]) i));
    70 
    71 (** EQgen **)
    72 
    73 goal Term.thy "<a,a> : EQ";
    74 by (rtac (refl RS (EQ_iff RS iffD1)) 1);
    75 qed "EQ_refl";
    76 
    77 val EQgenIs = map (mk_genIs Term.thy data_defs EQgenXH EQgen_mono)
    78 ["<true,true> : EQgen(R)",
    79  "<false,false> : EQgen(R)",
    80  "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)",
    81  "[|!!x. <b(x),b'(x)> : R |] ==> <lam x.b(x),lam x.b'(x)> : EQgen(R)",
    82  "<one,one> : EQgen(R)",
    83  "<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==> \
    84 \                   <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
    85  "<b,b'> : lfp(%x. EQgen(x) Un R Un EQ) ==> \
    86 \                   <inr(b),inr(b')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
    87  "<zero,zero> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
    88  "<n,n'> : lfp(%x. EQgen(x) Un R Un EQ) ==> \
    89 \                   <succ(n),succ(n')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
    90  "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
    91  "[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); \
    92 \          <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) |] ==> \
    93 \       <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"];
    94 
    95 fun EQgen_raw_tac i =
    96        (REPEAT (resolve_tac (EQgenIs @ [EQ_refl RS (EQgen_mono RS ci3_AI)] @ 
    97                    (EQgenIs RL [EQgen_mono RS ci3_AgenI]) @ [EQgen_mono RS ci3_RI]) i));
    98 
    99 (* Goals of the form R <= EQgen(R) - rewrite elements <a,b> : EQgen(R) using rews and *)
   100 (* then reduce this to a goal <a',b'> : R (hopefully?)                                *)
   101 (*      rews are rewrite rules that would cause looping in the simpifier              *)
   102 
   103 fun EQgen_tac simp_set rews i = 
   104  SELECT_GOAL 
   105    (TRY (safe_tac ccl_cs) THEN
   106     resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [ssubst_pair])) i THEN
   107     ALLGOALS (simp_tac simp_set) THEN
   108     ALLGOALS EQgen_raw_tac) i;