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