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