src/CCL/ccl.ML
changeset 0 a5a9c433f639
child 8 c3d2c6dcf3f0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/ccl.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,362 @@
     1.4 +(*  Title: 	CCL/ccl
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Martin Coen, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +For ccl.thy.
    1.10 +*)
    1.11 +
    1.12 +open CCL;
    1.13 +
    1.14 +val ccl_data_defs = [apply_def,fix_def];
    1.15 +
    1.16 +(*** Simplifier for pre-order and equality ***)
    1.17 +
    1.18 +structure CCL_SimpData : SIMP_DATA =
    1.19 +  struct
    1.20 +  val refl_thms		= [refl, po_refl, iff_refl]
    1.21 +  val trans_thms	= [trans, iff_trans, po_trans]
    1.22 +  val red1		= iffD1
    1.23 +  val red2		= iffD2
    1.24 +  val mk_rew_rules	= mk_rew_rules
    1.25 +  val case_splits	= []         (*NO IF'S!*)
    1.26 +  val norm_thms		= norm_thms
    1.27 +  val subst_thms	= [subst];
    1.28 +  val dest_red		= dest_red
    1.29 +  end;
    1.30 +
    1.31 +structure CCL_Simp = SimpFun(CCL_SimpData);
    1.32 +open CCL_Simp;
    1.33 +
    1.34 +val auto_ss = empty_ss setauto (fn hyps => ares_tac (TrueI::hyps));
    1.35 +
    1.36 +val po_refl_iff_T = make_iff_T po_refl;
    1.37 +
    1.38 +val CCL_ss = auto_ss addcongs (FOL_congs @ set_congs)
    1.39 +                     addrews  ([po_refl_iff_T] @ FOL_rews @ mem_rews);
    1.40 +
    1.41 +(*** Congruence Rules ***)
    1.42 +
    1.43 +(*similar to AP_THM in Gordon's HOL*)
    1.44 +val fun_cong = prove_goal CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
    1.45 +  (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
    1.46 +
    1.47 +(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
    1.48 +val arg_cong = prove_goal CCL.thy "x=y ==> f(x)=f(y)"
    1.49 + (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
    1.50 +
    1.51 +goal CCL.thy  "(ALL x. f(x) = g(x)) --> (%x.f(x)) = (%x.g(x))";
    1.52 +by (SIMP_TAC (CCL_ss addrews [eq_iff]) 1);
    1.53 +by (fast_tac (set_cs addIs [po_abstractn]) 1);
    1.54 +val abstractn = standard (allI RS (result() RS mp));
    1.55 +
    1.56 +fun type_of_terms (Const("Trueprop",_) $ 
    1.57 +                   (Const("op =",(Type ("fun", [t,_]))) $ _ $ _)) = t;
    1.58 +
    1.59 +fun abs_prems thm = 
    1.60 +   let fun do_abs n thm (Type ("fun", [_,t])) = do_abs n (abstractn RSN (n,thm)) t
    1.61 +         | do_abs n thm _                     = thm
    1.62 +       fun do_prems n      [] thm = thm
    1.63 +         | do_prems n (x::xs) thm = do_prems (n+1) xs (do_abs n thm (type_of_terms x));
    1.64 +   in do_prems 1 (prems_of thm) thm
    1.65 +   end;
    1.66 +
    1.67 +fun ccl_mk_congs thy cs = map abs_prems (mk_congs thy cs); 
    1.68 +
    1.69 +val ccl_congs = ccl_mk_congs CCL.thy 
    1.70 + ["op [=","SIM","POgen","EQgen","pair","lambda","case","op `","fix"];
    1.71 +
    1.72 +val caseBs = [caseBtrue,caseBfalse,caseBpair,caseBlam,caseBbot];
    1.73 +
    1.74 +(*** Termination and Divergence ***)
    1.75 +
    1.76 +goalw CCL.thy [Trm_def,Dvg_def] "Trm(t) <-> ~ t = bot";
    1.77 +br iff_refl 1;
    1.78 +val Trm_iff = result();
    1.79 +
    1.80 +goalw CCL.thy [Trm_def,Dvg_def] "Dvg(t) <-> t = bot";
    1.81 +br iff_refl 1;
    1.82 +val Dvg_iff = result();
    1.83 +
    1.84 +(*** Constructors are injective ***)
    1.85 +
    1.86 +val prems = goal CCL.thy
    1.87 +    "[| x=a;  y=b;  x=y |] ==> a=b";
    1.88 +by  (REPEAT (SOMEGOAL (ares_tac (prems@[box_equals]))));
    1.89 +val eq_lemma = result();
    1.90 +
    1.91 +fun mk_inj_rl thy rews congs s = 
    1.92 +      let fun mk_inj_lemmas r = ([arg_cong] RL [(r RS (r RS eq_lemma))]);
    1.93 +          val inj_lemmas = flat (map mk_inj_lemmas rews);
    1.94 +          val tac = REPEAT (ares_tac [iffI,allI,conjI] 1 ORELSE
    1.95 +                            eresolve_tac inj_lemmas 1 ORELSE
    1.96 +                            ASM_SIMP_TAC (CCL_ss addrews rews 
    1.97 +                                                 addcongs congs) 1)
    1.98 +      in prove_goal thy s (fn _ => [tac])
    1.99 +      end;
   1.100 +
   1.101 +val ccl_injs = map (mk_inj_rl CCL.thy caseBs ccl_congs)
   1.102 +               ["<a,b> = <a',b'> <-> (a=a' & b=b')",
   1.103 +                "(lam x.b(x) = lam x.b'(x)) <-> ((ALL z.b(z)=b'(z)))"];
   1.104 +
   1.105 +val pair_inject = ((hd ccl_injs) RS iffD1) RS conjE;
   1.106 +
   1.107 +(*** Constructors are distinct ***)
   1.108 +
   1.109 +local
   1.110 +  fun pairs_of f x [] = []
   1.111 +    | pairs_of f x (y::ys) = (f x y) :: (f y x) :: (pairs_of f x ys);
   1.112 +
   1.113 +  fun mk_combs ff [] = []
   1.114 +    | mk_combs ff (x::xs) = (pairs_of ff x xs) @ mk_combs ff xs;
   1.115 +
   1.116 +(* Doesn't handle binder types correctly *)
   1.117 +  fun saturate thy sy name = 
   1.118 +       let fun arg_str 0 a s = s
   1.119 +         | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
   1.120 +         | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s);
   1.121 +           val sg = sign_of thy;
   1.122 +           val T = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),sy) of
   1.123 +  		            None => error(sy^" not declared") | Some(T) => T;
   1.124 +           val arity = length (fst (strip_type T));
   1.125 +       in sy ^ (arg_str arity name "") end;
   1.126 +
   1.127 +  fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b");
   1.128 +
   1.129 +  val lemma = prove_goal CCL.thy "t=t' --> case(t,b,c,d,e) = case(t',b,c,d,e)"
   1.130 +                   (fn _ => [SIMP_TAC (CCL_ss addcongs ccl_congs) 1]) RS mp;
   1.131 +  fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL 
   1.132 +                           [distinctness RS notE,sym RS (distinctness RS notE)];
   1.133 +in
   1.134 +  fun mk_lemmas rls = flat (map mk_lemma (mk_combs pair rls));
   1.135 +  fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs;
   1.136 +end;
   1.137 +
   1.138 +
   1.139 +val caseB_lemmas = mk_lemmas caseBs;
   1.140 +
   1.141 +val ccl_dstncts = 
   1.142 +        let fun mk_raw_dstnct_thm rls s = 
   1.143 +                  prove_goal CCL.thy s (fn _=> [rtac notI 1,eresolve_tac rls 1])
   1.144 +        in map (mk_raw_dstnct_thm caseB_lemmas) 
   1.145 +                (mk_dstnct_rls CCL.thy ["bot","true","false","pair","lambda"]) end;
   1.146 +
   1.147 +fun mk_dstnct_thms thy defs inj_rls xs = 
   1.148 +          let fun mk_dstnct_thm rls s = prove_goalw thy defs s 
   1.149 +                               (fn _ => [SIMP_TAC (CCL_ss addrews (rls@inj_rls)) 1])
   1.150 +          in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end;
   1.151 +
   1.152 +fun mkall_dstnct_thms thy defs i_rls xss = flat (map (mk_dstnct_thms thy defs i_rls) xss);
   1.153 +
   1.154 +(*** Rewriting and Proving ***)
   1.155 +
   1.156 +fun XH_to_I rl = rl RS iffD2;
   1.157 +fun XH_to_D rl = rl RS iffD1;
   1.158 +val XH_to_E = make_elim o XH_to_D;
   1.159 +val XH_to_Is = map XH_to_I;
   1.160 +val XH_to_Ds = map XH_to_D;
   1.161 +val XH_to_Es = map XH_to_E;
   1.162 +
   1.163 +val ccl_rews = caseBs @ ccl_injs @ ccl_dstncts;
   1.164 +val ccl_ss = CCL_ss addrews ccl_rews addcongs ccl_congs;
   1.165 +
   1.166 +val ccl_cs = set_cs addSEs (pair_inject::(ccl_dstncts RL [notE])) 
   1.167 +                    addSDs (XH_to_Ds ccl_injs);
   1.168 +
   1.169 +(****** Facts from gfp Definition of [= and = ******)
   1.170 +
   1.171 +val major::prems = goal Set.thy "[| A=B;  a:B <-> P |] ==> a:A <-> P";
   1.172 +brs (prems RL [major RS ssubst]) 1;
   1.173 +val XHlemma1 = result();
   1.174 +
   1.175 +goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p.EX t t'.p=<t,t'> &  P(t,t')} <-> Q)";
   1.176 +by (fast_tac ccl_cs 1);
   1.177 +val XHlemma2 = result() RS mp;
   1.178 +
   1.179 +(*** Pre-Order ***)
   1.180 +
   1.181 +goalw CCL.thy [POgen_def,SIM_def]  "mono(%X.POgen(X))";
   1.182 +br monoI 1;
   1.183 +by (safe_tac ccl_cs);
   1.184 +by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
   1.185 +by (ALLGOALS (SIMP_TAC ccl_ss));
   1.186 +by (ALLGOALS (fast_tac set_cs));
   1.187 +val POgen_mono = result();
   1.188 +
   1.189 +goalw CCL.thy [POgen_def,SIM_def]
   1.190 +  "<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true)  | (t=false & t'=false) | \
   1.191 +\                    (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
   1.192 +\                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
   1.193 +br (iff_refl RS XHlemma2) 1;
   1.194 +val POgenXH = result();
   1.195 +
   1.196 +goal CCL.thy
   1.197 +  "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
   1.198 +\                    (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & a [= a' & b [= b') | \
   1.199 +\                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.f(x) [= f'(x)))";
   1.200 +by (SIMP_TAC (ccl_ss addrews [PO_iff]) 1);
   1.201 +br (rewrite_rule [POgen_def,SIM_def] 
   1.202 +                 (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
   1.203 +br (iff_refl RS XHlemma2) 1;
   1.204 +val poXH = result();
   1.205 +
   1.206 +goal CCL.thy "bot [= b";
   1.207 +br (poXH RS iffD2) 1;
   1.208 +by (SIMP_TAC ccl_ss 1);
   1.209 +val po_bot = result();
   1.210 +
   1.211 +goal CCL.thy "a [= bot --> a=bot";
   1.212 +br impI 1;
   1.213 +bd (poXH RS iffD1) 1;
   1.214 +be rev_mp 1;
   1.215 +by (SIMP_TAC ccl_ss 1);
   1.216 +val bot_poleast = result() RS mp;
   1.217 +
   1.218 +goal CCL.thy "<a,b> [= <a',b'> <->  a [= a' & b [= b'";
   1.219 +br (poXH RS iff_trans) 1;
   1.220 +by (SIMP_TAC ccl_ss 1);
   1.221 +by (fast_tac ccl_cs 1);
   1.222 +val po_pair = result();
   1.223 +
   1.224 +goal CCL.thy "lam x.f(x) [= lam x.f'(x) <-> (ALL x. f(x) [= f'(x))";
   1.225 +br (poXH RS iff_trans) 1;
   1.226 +by (SIMP_TAC ccl_ss 1);
   1.227 +by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1));
   1.228 +by (ASM_SIMP_TAC ccl_ss 1);
   1.229 +by (fast_tac ccl_cs 1);
   1.230 +val po_lam = result();
   1.231 +
   1.232 +val ccl_porews = [po_bot,po_pair,po_lam];
   1.233 +
   1.234 +val [p1,p2,p3,p4,p5] = goal CCL.thy
   1.235 +    "[| t [= t';  a [= a';  b [= b';  !!x y.c(x,y) [= c'(x,y); \
   1.236 +\       !!u.d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')";
   1.237 +br (p1 RS po_cong RS po_trans) 1;
   1.238 +br (p2 RS po_cong RS po_trans) 1;
   1.239 +br (p3 RS po_cong RS po_trans) 1;
   1.240 +br (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1;
   1.241 +by (res_inst_tac [("f1","%d.case(t',a',b',c',d)")] 
   1.242 +               (p5 RS po_abstractn RS po_cong RS po_trans) 1);
   1.243 +br po_refl 1;
   1.244 +val case_pocong = result();
   1.245 +
   1.246 +val [p1,p2] = goalw CCL.thy ccl_data_defs
   1.247 +    "[| f [= f';  a [= a' |] ==> f ` a [= f' ` a'";
   1.248 +by (REPEAT (ares_tac [po_refl,case_pocong,p1,p2 RS po_cong] 1));
   1.249 +val apply_pocong = result();
   1.250 +
   1.251 +
   1.252 +val prems = goal CCL.thy "~ lam x.b(x) [= bot";
   1.253 +br notI 1;
   1.254 +bd bot_poleast 1;
   1.255 +be (distinctness RS notE) 1;
   1.256 +val npo_lam_bot = result();
   1.257 +
   1.258 +val eq1::eq2::prems = goal CCL.thy
   1.259 +    "[| x=a;  y=b;  x[=y |] ==> a[=b";
   1.260 +br (eq1 RS subst) 1;
   1.261 +br (eq2 RS subst) 1;
   1.262 +brs prems 1;
   1.263 +val po_lemma = result();
   1.264 +
   1.265 +goal CCL.thy "~ <a,b> [= lam x.f(x)";
   1.266 +br notI 1;
   1.267 +br (npo_lam_bot RS notE) 1;
   1.268 +be (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1;
   1.269 +by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
   1.270 +val npo_pair_lam = result();
   1.271 +
   1.272 +goal CCL.thy "~ lam x.f(x) [= <a,b>";
   1.273 +br notI 1;
   1.274 +br (npo_lam_bot RS notE) 1;
   1.275 +be (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1;
   1.276 +by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
   1.277 +val npo_lam_pair = result();
   1.278 +
   1.279 +fun mk_thm s = prove_goal CCL.thy s (fn _ => 
   1.280 +                          [rtac notI 1,dtac case_pocong 1,etac rev_mp 5,
   1.281 +                           ALLGOALS (SIMP_TAC ccl_ss),
   1.282 +                           REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)]);
   1.283 +
   1.284 +val npo_rls = [npo_pair_lam,npo_lam_pair] @ map mk_thm
   1.285 +            ["~ true [= false",          "~ false [= true",
   1.286 +             "~ true [= <a,b>",          "~ <a,b> [= true",
   1.287 +             "~ true [= lam x.f(x)","~ lam x.f(x) [= true",
   1.288 +            "~ false [= <a,b>",          "~ <a,b> [= false",
   1.289 +            "~ false [= lam x.f(x)","~ lam x.f(x) [= false"];
   1.290 +
   1.291 +(* Coinduction for [= *)
   1.292 +
   1.293 +val prems = goal CCL.thy "[|  <t,u> : R;  R <= POgen(R) |] ==> t [= u";
   1.294 +br (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1;
   1.295 +by (REPEAT (ares_tac prems 1));
   1.296 +val po_coinduct = result();
   1.297 +
   1.298 +fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i;
   1.299 +
   1.300 +(*************** EQUALITY *******************)
   1.301 +
   1.302 +goalw CCL.thy [EQgen_def,SIM_def]  "mono(%X.EQgen(X))";
   1.303 +br monoI 1;
   1.304 +by (safe_tac set_cs);
   1.305 +by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
   1.306 +by (ALLGOALS (SIMP_TAC ccl_ss));
   1.307 +by (ALLGOALS (fast_tac set_cs));
   1.308 +val EQgen_mono = result();
   1.309 +
   1.310 +goalw CCL.thy [EQgen_def,SIM_def]
   1.311 +  "<t,t'> : EQgen(R) <-> (t=bot & t'=bot)  | (t=true & t'=true)  | \
   1.312 +\                                            (t=false & t'=false) | \
   1.313 +\                (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
   1.314 +\                (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
   1.315 +br (iff_refl RS XHlemma2) 1;
   1.316 +val EQgenXH = result();
   1.317 +
   1.318 +goal CCL.thy
   1.319 +  "t=t' <-> (t=bot & t'=bot)  | (t=true & t'=true)  | (t=false & t'=false) | \
   1.320 +\                    (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & a=a' & b=b') | \
   1.321 +\                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.f(x)=f'(x)))";
   1.322 +by (subgoal_tac
   1.323 +  "<t,t'> : EQ <-> (t=bot & t'=bot)  | (t=true & t'=true) | (t=false & t'=false) | \
   1.324 +\             (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : EQ & <b,b'> : EQ) | \
   1.325 +\             (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : EQ))" 1);
   1.326 +be rev_mp 1;
   1.327 +by (SIMP_TAC (CCL_ss addrews [EQ_iff RS iff_sym]) 1);
   1.328 +br (rewrite_rule [EQgen_def,SIM_def]
   1.329 +                 (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1;
   1.330 +br (iff_refl RS XHlemma2) 1;
   1.331 +val eqXH = result();
   1.332 +
   1.333 +val prems = goal CCL.thy "[|  <t,u> : R;  R <= EQgen(R) |] ==> t = u";
   1.334 +br (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1;
   1.335 +by (REPEAT (ares_tac prems 1));
   1.336 +val eq_coinduct = result();
   1.337 +
   1.338 +val prems = goal CCL.thy 
   1.339 +    "[|  <t,u> : R;  R <= EQgen(lfp(%x.EQgen(x) Un R Un EQ)) |] ==> t = u";
   1.340 +br (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1;
   1.341 +by (REPEAT (ares_tac (EQgen_mono::prems) 1));
   1.342 +val eq_coinduct3 = result();
   1.343 +
   1.344 +fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i;
   1.345 +fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i;
   1.346 +
   1.347 +(*** Untyped Case Analysis and Other Facts ***)
   1.348 +
   1.349 +goalw CCL.thy [apply_def]  "(EX f.t=lam x.f(x)) --> t = lam x.(t ` x)";
   1.350 +by (safe_tac ccl_cs);
   1.351 +by (SIMP_TAC ccl_ss 1);
   1.352 +val cond_eta = result() RS mp;
   1.353 +
   1.354 +goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b.t=<a,b>) | (EX f.t=lam x.f(x))";
   1.355 +by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1);
   1.356 +by (fast_tac set_cs 1);
   1.357 +val exhaustion = result();
   1.358 +
   1.359 +val prems = goal CCL.thy 
   1.360 +    "[| P(bot);  P(true);  P(false);  !!x y.P(<x,y>);  !!b.P(lam x.b(x)) |] ==> P(t)";
   1.361 +by (cut_facts_tac [exhaustion] 1);
   1.362 +by (REPEAT_SOME (ares_tac prems ORELSE' eresolve_tac [disjE,exE,ssubst]));
   1.363 +val term_case = result();
   1.364 +
   1.365 +fun term_case_tac a i = res_inst_tac [("t",a)] term_case i;