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