src/CCL/CCL.ML
changeset 3837 d7f033c74b38
parent 1963 a4abf41134e2
child 3935 52c14fe8f16b
equal deleted inserted replaced
3836:f1a1817659e6 3837:d7f033c74b38
    20 
    20 
    21 (*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
    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)"
    22 qed_goal "arg_cong" CCL.thy "x=y ==> f(x)=f(y)"
    23  (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
    23  (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
    24 
    24 
    25 goal CCL.thy  "(ALL x. f(x) = g(x)) --> (%x.f(x)) = (%x.g(x))";
    25 goal CCL.thy  "(ALL x. f(x) = g(x)) --> (%x. f(x)) = (%x. g(x))";
    26 by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
    26 by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
    27 by (fast_tac (set_cs addIs [po_abstractn]) 1);
    27 by (fast_tac (set_cs addIs [po_abstractn]) 1);
    28 bind_thm("abstractn", standard (allI RS (result() RS mp)));
    28 bind_thm("abstractn", standard (allI RS (result() RS mp)));
    29 
    29 
    30 fun type_of_terms (Const("Trueprop",_) $ 
    30 fun type_of_terms (Const("Trueprop",_) $ 
    66       in prove_goal thy s (fn _ => [tac])
    66       in prove_goal thy s (fn _ => [tac])
    67       end;
    67       end;
    68 
    68 
    69 val ccl_injs = map (mk_inj_rl CCL.thy caseBs)
    69 val ccl_injs = map (mk_inj_rl CCL.thy caseBs)
    70                ["<a,b> = <a',b'> <-> (a=a' & b=b')",
    70                ["<a,b> = <a',b'> <-> (a=a' & b=b')",
    71                 "(lam x.b(x) = lam x.b'(x)) <-> ((ALL z.b(z)=b'(z)))"];
    71                 "(lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"];
    72 
    72 
    73 val pair_inject = ((hd ccl_injs) RS iffD1) RS conjE;
    73 val pair_inject = ((hd ccl_injs) RS iffD1) RS conjE;
    74 
    74 
    75 (*** Constructors are distinct ***)
    75 (*** Constructors are distinct ***)
    76 
    76 
   138 
   138 
   139 val major::prems = goal Set.thy "[| A=B;  a:B <-> P |] ==> a:A <-> P";
   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);
   140 by (resolve_tac (prems RL [major RS ssubst]) 1);
   141 qed "XHlemma1";
   141 qed "XHlemma1";
   142 
   142 
   143 goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p.EX t t'.p=<t,t'> &  P(t,t')} <-> Q)";
   143 goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p. EX t t'. p=<t,t'> &  P(t,t')} <-> Q)";
   144 by (fast_tac ccl_cs 1);
   144 by (fast_tac ccl_cs 1);
   145 bind_thm("XHlemma2", result() RS mp);
   145 bind_thm("XHlemma2", result() RS mp);
   146 
   146 
   147 (*** Pre-Order ***)
   147 (*** Pre-Order ***)
   148 
   148 
   149 goalw CCL.thy [POgen_def,SIM_def]  "mono(%X.POgen(X))";
   149 goalw CCL.thy [POgen_def,SIM_def]  "mono(%X. POgen(X))";
   150 by (rtac monoI 1);
   150 by (rtac monoI 1);
   151 by (safe_tac ccl_cs);
   151 by (safe_tac ccl_cs);
   152 by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
   152 by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
   153 by (ALLGOALS (simp_tac ccl_ss));
   153 by (ALLGOALS (simp_tac ccl_ss));
   154 by (ALLGOALS (fast_tac set_cs));
   154 by (ALLGOALS (fast_tac set_cs));
   155 qed "POgen_mono";
   155 qed "POgen_mono";
   156 
   156 
   157 goalw CCL.thy [POgen_def,SIM_def]
   157 goalw CCL.thy [POgen_def,SIM_def]
   158   "<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true)  | (t=false & t'=false) | \
   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) | \
   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))";
   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);
   161 by (rtac (iff_refl RS XHlemma2) 1);
   162 qed "POgenXH";
   162 qed "POgenXH";
   163 
   163 
   164 goal CCL.thy
   164 goal CCL.thy
   165   "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
   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') | \
   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)))";
   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]) 1);
   168 by (simp_tac (ccl_ss addsimps [PO_iff]) 1);
   169 br (rewrite_rule [POgen_def,SIM_def] 
   169 br (rewrite_rule [POgen_def,SIM_def] 
   170                  (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
   170                  (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
   171 by (rtac (iff_refl RS XHlemma2) 1);
   171 by (rtac (iff_refl RS XHlemma2) 1);
   172 qed "poXH";
   172 qed "poXH";
   187 by (rtac (poXH RS iff_trans) 1);
   187 by (rtac (poXH RS iff_trans) 1);
   188 by (simp_tac ccl_ss 1);
   188 by (simp_tac ccl_ss 1);
   189 by (fast_tac ccl_cs 1);
   189 by (fast_tac ccl_cs 1);
   190 qed "po_pair";
   190 qed "po_pair";
   191 
   191 
   192 goal CCL.thy "lam x.f(x) [= lam x.f'(x) <-> (ALL x. f(x) [= f'(x))";
   192 goal CCL.thy "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))";
   193 by (rtac (poXH RS iff_trans) 1);
   193 by (rtac (poXH RS iff_trans) 1);
   194 by (simp_tac ccl_ss 1);
   194 by (simp_tac ccl_ss 1);
   195 by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1));
   195 by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1));
   196 by (asm_simp_tac ccl_ss 1);
   196 by (asm_simp_tac ccl_ss 1);
   197 by (fast_tac ccl_cs 1);
   197 by (fast_tac ccl_cs 1);
   198 qed "po_lam";
   198 qed "po_lam";
   199 
   199 
   200 val ccl_porews = [po_bot,po_pair,po_lam];
   200 val ccl_porews = [po_bot,po_pair,po_lam];
   201 
   201 
   202 val [p1,p2,p3,p4,p5] = goal CCL.thy
   202 val [p1,p2,p3,p4,p5] = goal CCL.thy
   203     "[| t [= t';  a [= a';  b [= b';  !!x y.c(x,y) [= c'(x,y); \
   203     "[| t [= t';  a [= a';  b [= b';  !!x y. c(x,y) [= c'(x,y); \
   204 \       !!u.d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')";
   204 \       !!u. d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')";
   205 by (rtac (p1 RS po_cong RS po_trans) 1);
   205 by (rtac (p1 RS po_cong RS po_trans) 1);
   206 by (rtac (p2 RS po_cong RS po_trans) 1);
   206 by (rtac (p2 RS po_cong RS po_trans) 1);
   207 by (rtac (p3 RS po_cong RS po_trans) 1);
   207 by (rtac (p3 RS po_cong RS po_trans) 1);
   208 by (rtac (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1);
   208 by (rtac (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1);
   209 by (res_inst_tac [("f1","%d.case(t',a',b',c',d)")] 
   209 by (res_inst_tac [("f1","%d. case(t',a',b',c',d)")] 
   210                (p5 RS po_abstractn RS po_cong RS po_trans) 1);
   210                (p5 RS po_abstractn RS po_cong RS po_trans) 1);
   211 by (rtac po_refl 1);
   211 by (rtac po_refl 1);
   212 qed "case_pocong";
   212 qed "case_pocong";
   213 
   213 
   214 val [p1,p2] = goalw CCL.thy ccl_data_defs
   214 val [p1,p2] = goalw CCL.thy ccl_data_defs
   215     "[| f [= f';  a [= a' |] ==> f ` a [= f' ` a'";
   215     "[| f [= f';  a [= a' |] ==> f ` a [= f' ` a'";
   216 by (REPEAT (ares_tac [po_refl,case_pocong,p1,p2 RS po_cong] 1));
   216 by (REPEAT (ares_tac [po_refl,case_pocong,p1,p2 RS po_cong] 1));
   217 qed "apply_pocong";
   217 qed "apply_pocong";
   218 
   218 
   219 
   219 
   220 val prems = goal CCL.thy "~ lam x.b(x) [= bot";
   220 val prems = goal CCL.thy "~ lam x. b(x) [= bot";
   221 by (rtac notI 1);
   221 by (rtac notI 1);
   222 by (dtac bot_poleast 1);
   222 by (dtac bot_poleast 1);
   223 by (etac (distinctness RS notE) 1);
   223 by (etac (distinctness RS notE) 1);
   224 qed "npo_lam_bot";
   224 qed "npo_lam_bot";
   225 
   225 
   228 by (rtac (eq1 RS subst) 1);
   228 by (rtac (eq1 RS subst) 1);
   229 by (rtac (eq2 RS subst) 1);
   229 by (rtac (eq2 RS subst) 1);
   230 by (resolve_tac prems 1);
   230 by (resolve_tac prems 1);
   231 qed "po_lemma";
   231 qed "po_lemma";
   232 
   232 
   233 goal CCL.thy "~ <a,b> [= lam x.f(x)";
   233 goal CCL.thy "~ <a,b> [= lam x. f(x)";
   234 by (rtac notI 1);
   234 by (rtac notI 1);
   235 by (rtac (npo_lam_bot RS notE) 1);
   235 by (rtac (npo_lam_bot RS notE) 1);
   236 by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1);
   236 by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1);
   237 by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
   237 by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
   238 qed "npo_pair_lam";
   238 qed "npo_pair_lam";
   239 
   239 
   240 goal CCL.thy "~ lam x.f(x) [= <a,b>";
   240 goal CCL.thy "~ lam x. f(x) [= <a,b>";
   241 by (rtac notI 1);
   241 by (rtac notI 1);
   242 by (rtac (npo_lam_bot RS notE) 1);
   242 by (rtac (npo_lam_bot RS notE) 1);
   243 by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1);
   243 by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1);
   244 by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
   244 by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
   245 qed "npo_lam_pair";
   245 qed "npo_lam_pair";
   250                            REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)]);
   250                            REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)]);
   251 
   251 
   252 val npo_rls = [npo_pair_lam,npo_lam_pair] @ map mk_thm
   252 val npo_rls = [npo_pair_lam,npo_lam_pair] @ map mk_thm
   253             ["~ true [= false",          "~ false [= true",
   253             ["~ true [= false",          "~ false [= true",
   254              "~ true [= <a,b>",          "~ <a,b> [= true",
   254              "~ true [= <a,b>",          "~ <a,b> [= true",
   255              "~ true [= lam x.f(x)","~ lam x.f(x) [= true",
   255              "~ true [= lam x. f(x)","~ lam x. f(x) [= true",
   256             "~ false [= <a,b>",          "~ <a,b> [= false",
   256             "~ false [= <a,b>",          "~ <a,b> [= false",
   257             "~ false [= lam x.f(x)","~ lam x.f(x) [= false"];
   257             "~ false [= lam x. f(x)","~ lam x. f(x) [= false"];
   258 
   258 
   259 (* Coinduction for [= *)
   259 (* Coinduction for [= *)
   260 
   260 
   261 val prems = goal CCL.thy "[|  <t,u> : R;  R <= POgen(R) |] ==> t [= u";
   261 val prems = goal CCL.thy "[|  <t,u> : R;  R <= POgen(R) |] ==> t [= u";
   262 by (rtac (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1);
   262 by (rtac (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1);
   265 
   265 
   266 fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i;
   266 fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i;
   267 
   267 
   268 (*************** EQUALITY *******************)
   268 (*************** EQUALITY *******************)
   269 
   269 
   270 goalw CCL.thy [EQgen_def,SIM_def]  "mono(%X.EQgen(X))";
   270 goalw CCL.thy [EQgen_def,SIM_def]  "mono(%X. EQgen(X))";
   271 by (rtac monoI 1);
   271 by (rtac monoI 1);
   272 by (safe_tac set_cs);
   272 by (safe_tac set_cs);
   273 by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
   273 by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
   274 by (ALLGOALS (simp_tac ccl_ss));
   274 by (ALLGOALS (simp_tac ccl_ss));
   275 by (ALLGOALS (fast_tac set_cs));
   275 by (ALLGOALS (fast_tac set_cs));
   276 qed "EQgen_mono";
   276 qed "EQgen_mono";
   277 
   277 
   278 goalw CCL.thy [EQgen_def,SIM_def]
   278 goalw CCL.thy [EQgen_def,SIM_def]
   279   "<t,t'> : EQgen(R) <-> (t=bot & t'=bot)  | (t=true & t'=true)  | \
   279   "<t,t'> : EQgen(R) <-> (t=bot & t'=bot)  | (t=true & t'=true)  | \
   280 \                                            (t=false & t'=false) | \
   280 \                                            (t=false & t'=false) | \
   281 \                (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
   281 \                (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
   282 \                (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
   282 \                (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))";
   283 by (rtac (iff_refl RS XHlemma2) 1);
   283 by (rtac (iff_refl RS XHlemma2) 1);
   284 qed "EQgenXH";
   284 qed "EQgenXH";
   285 
   285 
   286 goal CCL.thy
   286 goal CCL.thy
   287   "t=t' <-> (t=bot & t'=bot)  | (t=true & t'=true)  | (t=false & t'=false) | \
   287   "t=t' <-> (t=bot & t'=bot)  | (t=true & t'=true)  | (t=false & t'=false) | \
   288 \                    (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & a=a' & b=b') | \
   288 \                    (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & a=a' & b=b') | \
   289 \                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.f(x)=f'(x)))";
   289 \                    (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. f(x)=f'(x)))";
   290 by (subgoal_tac
   290 by (subgoal_tac
   291   "<t,t'> : EQ <-> (t=bot & t'=bot)  | (t=true & t'=true) | (t=false & t'=false) | \
   291   "<t,t'> : EQ <-> (t=bot & t'=bot)  | (t=true & t'=true) | (t=false & t'=false) | \
   292 \             (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : EQ & <b,b'> : EQ) | \
   292 \             (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : EQ & <b,b'> : EQ) | \
   293 \             (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : EQ))" 1);
   293 \             (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : EQ))" 1);
   294 by (etac rev_mp 1);
   294 by (etac rev_mp 1);
   295 by (simp_tac (CCL_ss addsimps [EQ_iff RS iff_sym]) 1);
   295 by (simp_tac (CCL_ss addsimps [EQ_iff RS iff_sym]) 1);
   296 br (rewrite_rule [EQgen_def,SIM_def]
   296 br (rewrite_rule [EQgen_def,SIM_def]
   297                  (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1;
   297                  (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1;
   298 by (rtac (iff_refl RS XHlemma2) 1);
   298 by (rtac (iff_refl RS XHlemma2) 1);
   302 by (rtac (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1);
   302 by (rtac (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1);
   303 by (REPEAT (ares_tac prems 1));
   303 by (REPEAT (ares_tac prems 1));
   304 qed "eq_coinduct";
   304 qed "eq_coinduct";
   305 
   305 
   306 val prems = goal CCL.thy 
   306 val prems = goal CCL.thy 
   307     "[|  <t,u> : R;  R <= EQgen(lfp(%x.EQgen(x) Un R Un EQ)) |] ==> t = u";
   307     "[|  <t,u> : R;  R <= EQgen(lfp(%x. EQgen(x) Un R Un EQ)) |] ==> t = u";
   308 by (rtac (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1);
   308 by (rtac (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1);
   309 by (REPEAT (ares_tac (EQgen_mono::prems) 1));
   309 by (REPEAT (ares_tac (EQgen_mono::prems) 1));
   310 qed "eq_coinduct3";
   310 qed "eq_coinduct3";
   311 
   311 
   312 fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i;
   312 fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i;
   313 fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i;
   313 fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i;
   314 
   314 
   315 (*** Untyped Case Analysis and Other Facts ***)
   315 (*** Untyped Case Analysis and Other Facts ***)
   316 
   316 
   317 goalw CCL.thy [apply_def]  "(EX f.t=lam x.f(x)) --> t = lam x.(t ` x)";
   317 goalw CCL.thy [apply_def]  "(EX f. t=lam x. f(x)) --> t = lam x.(t ` x)";
   318 by (safe_tac ccl_cs);
   318 by (safe_tac ccl_cs);
   319 by (simp_tac ccl_ss 1);
   319 by (simp_tac ccl_ss 1);
   320 bind_thm("cond_eta", result() RS mp);
   320 bind_thm("cond_eta", result() RS mp);
   321 
   321 
   322 goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b.t=<a,b>) | (EX f.t=lam x.f(x))";
   322 goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b. t=<a,b>) | (EX f. t=lam x. f(x))";
   323 by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1);
   323 by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1);
   324 by (fast_tac set_cs 1);
   324 by (fast_tac set_cs 1);
   325 qed "exhaustion";
   325 qed "exhaustion";
   326 
   326 
   327 val prems = goal CCL.thy 
   327 val prems = goal CCL.thy 
   328     "[| P(bot);  P(true);  P(false);  !!x y.P(<x,y>);  !!b.P(lam x.b(x)) |] ==> P(t)";
   328     "[| P(bot);  P(true);  P(false);  !!x y. P(<x,y>);  !!b. P(lam x. b(x)) |] ==> P(t)";
   329 by (cut_facts_tac [exhaustion] 1);
   329 by (cut_facts_tac [exhaustion] 1);
   330 by (REPEAT_SOME (ares_tac prems ORELSE' eresolve_tac [disjE,exE,ssubst]));
   330 by (REPEAT_SOME (ares_tac prems ORELSE' eresolve_tac [disjE,exE,ssubst]));
   331 qed "term_case";
   331 qed "term_case";
   332 
   332 
   333 fun term_case_tac a i = res_inst_tac [("t",a)] term_case i;
   333 fun term_case_tac a i = res_inst_tac [("t",a)] term_case i;