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