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