src/CCL/CCL.ML
author wenzelm
Mon, 20 Oct 1997 10:48:22 +0200
changeset 3935 52c14fe8f16b
parent 3837 d7f033c74b38
child 4347 d683b7898c61
permissions -rw-r--r--
adapted to qualified names;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1459
d12da312eff4 expanded tabs
clasohm
parents: 1087
diff changeset
     1
(*  Title:      CCL/ccl
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1459
d12da312eff4 expanded tabs
clasohm
parents: 1087
diff changeset
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
For ccl.thy.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open CCL;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
val ccl_data_defs = [apply_def,fix_def];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
1963
a4abf41134e2 These simpsets must not use miniscoping
paulson
parents: 1459
diff changeset
    13
val CCL_ss = set_ss addsimps [po_refl RS P_iff_T];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
(*** Congruence Rules ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
(*similar to AP_THM in Gordon's HOL*)
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
    18
qed_goal "fun_cong" CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
    22
qed_goal "arg_cong" CCL.thy "x=y ==> f(x)=f(y)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
 (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
    25
goal CCL.thy  "(ALL x. f(x) = g(x)) --> (%x. f(x)) = (%x. g(x))";
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
    26
by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
by (fast_tac (set_cs addIs [po_abstractn]) 1);
1087
c1ccf6679a96 replaced store_thm by bind_thm
clasohm
parents: 757
diff changeset
    28
bind_thm("abstractn", standard (allI RS (result() RS mp)));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
fun type_of_terms (Const("Trueprop",_) $ 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
                   (Const("op =",(Type ("fun", [t,_]))) $ _ $ _)) = t;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
fun abs_prems thm = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
   let fun do_abs n thm (Type ("fun", [_,t])) = do_abs n (abstractn RSN (n,thm)) t
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
         | do_abs n thm _                     = thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
       fun do_prems n      [] thm = thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
         | do_prems n (x::xs) thm = do_prems (n+1) xs (do_abs n thm (type_of_terms x));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
   in do_prems 1 (prems_of thm) thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
   end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
val caseBs = [caseBtrue,caseBfalse,caseBpair,caseBlam,caseBbot];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
(*** Termination and Divergence ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
goalw CCL.thy [Trm_def,Dvg_def] "Trm(t) <-> ~ t = bot";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
    46
by (rtac iff_refl 1);
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
    47
qed "Trm_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
goalw CCL.thy [Trm_def,Dvg_def] "Dvg(t) <-> t = bot";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
    50
by (rtac iff_refl 1);
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
    51
qed "Dvg_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
(*** Constructors are injective ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
val prems = goal CCL.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
    "[| x=a;  y=b;  x=y |] ==> a=b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
by  (REPEAT (SOMEGOAL (ares_tac (prems@[box_equals]))));
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
    58
qed "eq_lemma";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
    60
fun mk_inj_rl thy rews s = 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
      let fun mk_inj_lemmas r = ([arg_cong] RL [(r RS (r RS eq_lemma))]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
          val inj_lemmas = flat (map mk_inj_lemmas rews);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
          val tac = REPEAT (ares_tac [iffI,allI,conjI] 1 ORELSE
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
                            eresolve_tac inj_lemmas 1 ORELSE
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
    65
                            asm_simp_tac (CCL_ss addsimps rews) 1)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
      in prove_goal thy s (fn _ => [tac])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
      end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
    69
val ccl_injs = map (mk_inj_rl CCL.thy caseBs)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
               ["<a,b> = <a',b'> <-> (a=a' & b=b')",
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
    71
                "(lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
val pair_inject = ((hd ccl_injs) RS iffD1) RS conjE;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
(*** Constructors are distinct ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
local
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
  fun pairs_of f x [] = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
    | pairs_of f x (y::ys) = (f x y) :: (f y x) :: (pairs_of f x ys);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
  fun mk_combs ff [] = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
    | mk_combs ff (x::xs) = (pairs_of ff x xs) @ mk_combs ff xs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
(* Doesn't handle binder types correctly *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
  fun saturate thy sy name = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
       let fun arg_str 0 a s = s
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
         | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
         | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
           val sg = sign_of thy;
3935
52c14fe8f16b adapted to qualified names;
wenzelm
parents: 3837
diff changeset
    90
           val T = case Sign.const_type sg (Sign.intern_const (sign_of thy) sy) of
1459
d12da312eff4 expanded tabs
clasohm
parents: 1087
diff changeset
    91
                            None => error(sy^" not declared") | Some(T) => T;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
           val arity = length (fst (strip_type T));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
       in sy ^ (arg_str arity name "") end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
  fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b");
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
  val lemma = prove_goal CCL.thy "t=t' --> case(t,b,c,d,e) = case(t',b,c,d,e)"
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
    98
                   (fn _ => [simp_tac CCL_ss 1]) RS mp;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
  fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
                           [distinctness RS notE,sym RS (distinctness RS notE)];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
  fun mk_lemmas rls = flat (map mk_lemma (mk_combs pair rls));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
  fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
val caseB_lemmas = mk_lemmas caseBs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
val ccl_dstncts = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
        let fun mk_raw_dstnct_thm rls s = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
                  prove_goal CCL.thy s (fn _=> [rtac notI 1,eresolve_tac rls 1])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
        in map (mk_raw_dstnct_thm caseB_lemmas) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
                (mk_dstnct_rls CCL.thy ["bot","true","false","pair","lambda"]) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
fun mk_dstnct_thms thy defs inj_rls xs = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
          let fun mk_dstnct_thm rls s = prove_goalw thy defs s 
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   117
                               (fn _ => [simp_tac (CCL_ss addsimps (rls@inj_rls)) 1])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
          in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
fun mkall_dstnct_thms thy defs i_rls xss = flat (map (mk_dstnct_thms thy defs i_rls) xss);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
(*** Rewriting and Proving ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
fun XH_to_I rl = rl RS iffD2;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
fun XH_to_D rl = rl RS iffD1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
val XH_to_E = make_elim o XH_to_D;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
val XH_to_Is = map XH_to_I;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
val XH_to_Ds = map XH_to_D;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
val XH_to_Es = map XH_to_E;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
val ccl_rews = caseBs @ ccl_injs @ ccl_dstncts;
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   132
val ccl_ss = CCL_ss addsimps ccl_rews;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
val ccl_cs = set_cs addSEs (pair_inject::(ccl_dstncts RL [notE])) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
                    addSDs (XH_to_Ds ccl_injs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
(****** Facts from gfp Definition of [= and = ******)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
val major::prems = goal Set.thy "[| A=B;  a:B <-> P |] ==> a:A <-> P";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   140
by (resolve_tac (prems RL [major RS ssubst]) 1);
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   141
qed "XHlemma1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   143
goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p. EX t t'. p=<t,t'> &  P(t,t')} <-> Q)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
by (fast_tac ccl_cs 1);
1087
c1ccf6679a96 replaced store_thm by bind_thm
clasohm
parents: 757
diff changeset
   145
bind_thm("XHlemma2", result() RS mp);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
(*** Pre-Order ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   149
goalw CCL.thy [POgen_def,SIM_def]  "mono(%X. POgen(X))";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   150
by (rtac monoI 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
by (safe_tac ccl_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   153
by (ALLGOALS (simp_tac ccl_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
by (ALLGOALS (fast_tac set_cs));
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   155
qed "POgen_mono";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
goalw CCL.thy [POgen_def,SIM_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
  "<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true)  | (t=false & t'=false) | \
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   159
\                    (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   160
\                    (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : R))";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   161
by (rtac (iff_refl RS XHlemma2) 1);
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   162
qed "POgenXH";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
goal CCL.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
  "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   166
\                    (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & a [= a' & b [= b') | \
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   167
\                    (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))";
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   168
by (simp_tac (ccl_ss addsimps [PO_iff]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
br (rewrite_rule [POgen_def,SIM_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
                 (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   171
by (rtac (iff_refl RS XHlemma2) 1);
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   172
qed "poXH";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
goal CCL.thy "bot [= b";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   175
by (rtac (poXH RS iffD2) 1);
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   176
by (simp_tac ccl_ss 1);
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   177
qed "po_bot";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
goal CCL.thy "a [= bot --> a=bot";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   180
by (rtac impI 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   181
by (dtac (poXH RS iffD1) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   182
by (etac rev_mp 1);
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   183
by (simp_tac ccl_ss 1);
1087
c1ccf6679a96 replaced store_thm by bind_thm
clasohm
parents: 757
diff changeset
   184
bind_thm("bot_poleast", result() RS mp);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
goal CCL.thy "<a,b> [= <a',b'> <->  a [= a' & b [= b'";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   187
by (rtac (poXH RS iff_trans) 1);
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   188
by (simp_tac ccl_ss 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
by (fast_tac ccl_cs 1);
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   190
qed "po_pair";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   192
goal CCL.thy "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   193
by (rtac (poXH RS iff_trans) 1);
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   194
by (simp_tac ccl_ss 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1));
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   196
by (asm_simp_tac ccl_ss 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
by (fast_tac ccl_cs 1);
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   198
qed "po_lam";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
val ccl_porews = [po_bot,po_pair,po_lam];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
val [p1,p2,p3,p4,p5] = goal CCL.thy
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   203
    "[| t [= t';  a [= a';  b [= b';  !!x y. c(x,y) [= c'(x,y); \
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   204
\       !!u. d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   205
by (rtac (p1 RS po_cong RS po_trans) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   206
by (rtac (p2 RS po_cong RS po_trans) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   207
by (rtac (p3 RS po_cong RS po_trans) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   208
by (rtac (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1);
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   209
by (res_inst_tac [("f1","%d. case(t',a',b',c',d)")] 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
               (p5 RS po_abstractn RS po_cong RS po_trans) 1);
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   211
by (rtac po_refl 1);
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   212
qed "case_pocong";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
val [p1,p2] = goalw CCL.thy ccl_data_defs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
    "[| f [= f';  a [= a' |] ==> f ` a [= f' ` a'";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
by (REPEAT (ares_tac [po_refl,case_pocong,p1,p2 RS po_cong] 1));
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   217
qed "apply_pocong";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   220
val prems = goal CCL.thy "~ lam x. b(x) [= bot";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   221
by (rtac notI 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   222
by (dtac bot_poleast 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   223
by (etac (distinctness RS notE) 1);
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   224
qed "npo_lam_bot";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
val eq1::eq2::prems = goal CCL.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
    "[| x=a;  y=b;  x[=y |] ==> a[=b";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   228
by (rtac (eq1 RS subst) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   229
by (rtac (eq2 RS subst) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   230
by (resolve_tac prems 1);
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   231
qed "po_lemma";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   233
goal CCL.thy "~ <a,b> [= lam x. f(x)";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   234
by (rtac notI 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   235
by (rtac (npo_lam_bot RS notE) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   236
by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   238
qed "npo_pair_lam";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   240
goal CCL.thy "~ lam x. f(x) [= <a,b>";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   241
by (rtac notI 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   242
by (rtac (npo_lam_bot RS notE) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   243
by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   245
qed "npo_lam_pair";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
fun mk_thm s = prove_goal CCL.thy s (fn _ => 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
                          [rtac notI 1,dtac case_pocong 1,etac rev_mp 5,
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   249
                           ALLGOALS (simp_tac ccl_ss),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
                           REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
val npo_rls = [npo_pair_lam,npo_lam_pair] @ map mk_thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
            ["~ true [= false",          "~ false [= true",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
             "~ true [= <a,b>",          "~ <a,b> [= true",
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   255
             "~ true [= lam x. f(x)","~ lam x. f(x) [= true",
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
            "~ false [= <a,b>",          "~ <a,b> [= false",
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   257
            "~ false [= lam x. f(x)","~ lam x. f(x) [= false"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
(* Coinduction for [= *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
val prems = goal CCL.thy "[|  <t,u> : R;  R <= POgen(R) |] ==> t [= u";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   262
by (rtac (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
by (REPEAT (ares_tac prems 1));
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   264
qed "po_coinduct";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
(*************** EQUALITY *******************)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   270
goalw CCL.thy [EQgen_def,SIM_def]  "mono(%X. EQgen(X))";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   271
by (rtac monoI 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
by (safe_tac set_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   274
by (ALLGOALS (simp_tac ccl_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
by (ALLGOALS (fast_tac set_cs));
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   276
qed "EQgen_mono";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
goalw CCL.thy [EQgen_def,SIM_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
  "<t,t'> : EQgen(R) <-> (t=bot & t'=bot)  | (t=true & t'=true)  | \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
\                                            (t=false & t'=false) | \
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   281
\                (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   282
\                (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   283
by (rtac (iff_refl RS XHlemma2) 1);
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   284
qed "EQgenXH";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
goal CCL.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
  "t=t' <-> (t=bot & t'=bot)  | (t=true & t'=true)  | (t=false & t'=false) | \
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   288
\                    (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & a=a' & b=b') | \
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   289
\                    (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. f(x)=f'(x)))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
by (subgoal_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
  "<t,t'> : EQ <-> (t=bot & t'=bot)  | (t=true & t'=true) | (t=false & t'=false) | \
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   292
\             (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : EQ & <b,b'> : EQ) | \
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   293
\             (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : EQ))" 1);
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   294
by (etac rev_mp 1);
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   295
by (simp_tac (CCL_ss addsimps [EQ_iff RS iff_sym]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
br (rewrite_rule [EQgen_def,SIM_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
                 (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1;
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   298
by (rtac (iff_refl RS XHlemma2) 1);
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   299
qed "eqXH";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
val prems = goal CCL.thy "[|  <t,u> : R;  R <= EQgen(R) |] ==> t = u";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   302
by (rtac (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
by (REPEAT (ares_tac prems 1));
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   304
qed "eq_coinduct";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
val prems = goal CCL.thy 
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   307
    "[|  <t,u> : R;  R <= EQgen(lfp(%x. EQgen(x) Un R Un EQ)) |] ==> t = u";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 611
diff changeset
   308
by (rtac (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
by (REPEAT (ares_tac (EQgen_mono::prems) 1));
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   310
qed "eq_coinduct3";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
(*** Untyped Case Analysis and Other Facts ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   317
goalw CCL.thy [apply_def]  "(EX f. t=lam x. f(x)) --> t = lam x.(t ` x)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
by (safe_tac ccl_cs);
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
   319
by (simp_tac ccl_ss 1);
1087
c1ccf6679a96 replaced store_thm by bind_thm
clasohm
parents: 757
diff changeset
   320
bind_thm("cond_eta", result() RS mp);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   322
goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b. t=<a,b>) | (EX f. t=lam x. f(x))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
by (fast_tac set_cs 1);
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   325
qed "exhaustion";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
val prems = goal CCL.thy 
3837
d7f033c74b38 fixed dots;
wenzelm
parents: 1963
diff changeset
   328
    "[| P(bot);  P(true);  P(false);  !!x y. P(<x,y>);  !!b. P(lam x. b(x)) |] ==> P(t)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
by (cut_facts_tac [exhaustion] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
by (REPEAT_SOME (ares_tac prems ORELSE' eresolve_tac [disjE,exE,ssubst]));
757
2ca12511676d added qed and qed_goal[w]
clasohm
parents: 642
diff changeset
   331
qed "term_case";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
fun term_case_tac a i = res_inst_tac [("t",a)] term_case i;