121 lemma lem: "[| a:B(u); u=v |] ==> a : B(v)" |
121 lemma lem: "[| a:B(u); u=v |] ==> a : B(v)" |
122 by blast |
122 by blast |
123 |
123 |
124 |
124 |
125 ML {* |
125 ML {* |
126 local |
126 fun mk_ncanT_tac top_crls crls = |
127 val lemma = thm "lem" |
127 SUBPROOF (fn {context = ctxt, prems = major :: prems, ...} => |
128 val bspec = thm "bspec" |
128 resolve_tac ([major] RL top_crls) 1 THEN |
129 val bexE = thm "bexE" |
129 REPEAT_SOME (eresolve_tac (crls @ [exE, @{thm bexE}, conjE, disjE])) THEN |
130 in |
130 ALLGOALS (asm_simp_tac (simpset_of ctxt)) THEN |
131 |
131 ALLGOALS (ares_tac (prems RL [@{thm lem}]) ORELSE' etac @{thm bspec}) THEN |
132 fun mk_ncanT_tac ctxt defs top_crls crls s = prove_goalw (ProofContext.theory_of ctxt) defs s |
132 safe_tac (claset_of ctxt addSIs prems)) |
133 (fn major::prems => [(resolve_tac ([major] RL top_crls) 1), |
|
134 (REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))), |
|
135 (ALLGOALS (asm_simp_tac (simpset_of ctxt))), |
|
136 (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' |
|
137 etac bspec )), |
|
138 (safe_tac (claset_of ctxt addSIs prems))]) |
|
139 end |
|
140 *} |
133 *} |
141 |
134 |
142 ML {* |
135 method_setup ncanT = {* |
143 val ncanT_tac = mk_ncanT_tac @{context} [] @{thms case_rls} @{thms case_rls} |
136 Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms case_rls} @{thms case_rls}) |
144 *} |
137 *} "" |
145 |
138 |
146 ML {* |
139 lemma ifT: |
147 |
140 "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==> |
148 bind_thm ("ifT", ncanT_tac |
141 if b then t else u : A(b)" |
149 "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==> if b then t else u : A(b)"); |
142 by ncanT |
150 |
143 |
151 bind_thm ("applyT", ncanT_tac "[| f : Pi(A,B); a:A |] ==> f ` a : B(a)"); |
144 lemma applyT: "[| f : Pi(A,B); a:A |] ==> f ` a : B(a)" |
152 |
145 by ncanT |
153 bind_thm ("splitT", ncanT_tac |
146 |
154 "[| p:Sigma(A,B); !!x y. [| x:A; y:B(x); p=<x,y> |] ==> c(x,y):C(<x,y>) |] ==> split(p,c):C(p)"); |
147 lemma splitT: |
155 |
148 "[| p:Sigma(A,B); !!x y. [| x:A; y:B(x); p=<x,y> |] ==> c(x,y):C(<x,y>) |] |
156 bind_thm ("whenT", ncanT_tac |
149 ==> split(p,c):C(p)" |
157 "[| p:A+B; !!x.[| x:A; p=inl(x) |] ==> a(x):C(inl(x)); !!y.[| y:B; p=inr(y) |] ==> b(y):C(inr(y)) |] ==> when(p,a,b) : C(p)"); |
150 by ncanT |
158 *} |
151 |
|
152 lemma whenT: |
|
153 "[| p:A+B; !!x.[| x:A; p=inl(x) |] ==> a(x):C(inl(x)); !!y.[| y:B; p=inr(y) |] |
|
154 ==> b(y):C(inr(y)) |] ==> when(p,a,b) : C(p)" |
|
155 by ncanT |
159 |
156 |
160 lemmas ncanTs = ifT applyT splitT whenT |
157 lemmas ncanTs = ifT applyT splitT whenT |
161 |
158 |
162 |
159 |
163 subsection {* Subtypes *} |
160 subsection {* Subtypes *} |
390 |
390 |
391 lemma ssubst_pair: "[| a=a'; b=b'; <a',b'> : A |] ==> <a,b> : A" |
391 lemma ssubst_pair: "[| a=a'; b=b'; <a',b'> : A |] ==> <a,b> : A" |
392 by simp |
392 by simp |
393 |
393 |
394 |
394 |
395 (***) |
|
396 |
|
397 ML {* |
395 ML {* |
398 |
396 val coinduct3_tac = SUBPROOF (fn {context = ctxt, prems = mono :: prems, ...} => |
399 local |
397 (fast_tac (claset_of ctxt addIs |
400 val lfpI = thm "lfpI" |
398 (mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1)); |
401 val coinduct3_mono_lemma = thm "coinduct3_mono_lemma" |
|
402 fun mk_thm s = prove_goal (the_context ()) s (fn mono::prems => |
|
403 [fast_tac (@{claset} addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1]) |
|
404 in |
|
405 val ci3_RI = mk_thm "[| mono(Agen); a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)" |
|
406 val ci3_AgenI = mk_thm "[| mono(Agen); a : Agen(lfp(%x. Agen(x) Un R Un A)) |] ==> a : lfp(%x. Agen(x) Un R Un A)" |
|
407 val ci3_AI = mk_thm "[| mono(Agen); a : A |] ==> a : lfp(%x. Agen(x) Un R Un A)" |
|
408 |
|
409 fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s |
|
410 (fn prems => [rtac (genXH RS iffD2) 1, |
|
411 simp_tac (global_simpset_of thy) 1, |
|
412 TRY (fast_tac (@{claset} addIs |
|
413 ([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI] |
|
414 @ prems)) 1)]) |
|
415 end; |
|
416 |
|
417 bind_thm ("ci3_RI", ci3_RI); |
|
418 bind_thm ("ci3_AgenI", ci3_AgenI); |
|
419 bind_thm ("ci3_AI", ci3_AI); |
|
420 *} |
399 *} |
421 |
400 |
|
401 method_setup coinduct3 = {* |
|
402 Scan.succeed (SIMPLE_METHOD' o coinduct3_tac) |
|
403 *} "" |
|
404 |
|
405 lemma ci3_RI: "[| mono(Agen); a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)" |
|
406 by coinduct3 |
|
407 |
|
408 lemma ci3_AgenI: "[| mono(Agen); a : Agen(lfp(%x. Agen(x) Un R Un A)) |] ==> |
|
409 a : lfp(%x. Agen(x) Un R Un A)" |
|
410 by coinduct3 |
|
411 |
|
412 lemma ci3_AI: "[| mono(Agen); a : A |] ==> a : lfp(%x. Agen(x) Un R Un A)" |
|
413 by coinduct3 |
|
414 |
|
415 ML {* |
|
416 fun genIs_tac ctxt genXH gen_mono = |
|
417 rtac (genXH RS iffD2) THEN' |
|
418 simp_tac (simpset_of ctxt) THEN' |
|
419 TRY o fast_tac (claset_of ctxt addIs |
|
420 [genXH RS iffD2, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}]) |
|
421 *} |
|
422 |
|
423 method_setup genIs = {* |
|
424 Attrib.thm -- Attrib.thm >> (fn (genXH, gen_mono) => fn ctxt => |
|
425 SIMPLE_METHOD' (genIs_tac ctxt genXH gen_mono)) |
|
426 *} "" |
|
427 |
422 |
428 |
423 subsection {* POgen *} |
429 subsection {* POgen *} |
424 |
430 |
425 lemma PO_refl: "<a,a> : PO" |
431 lemma PO_refl: "<a,a> : PO" |
426 apply (rule po_refl [THEN PO_iff [THEN iffD1]]) |
432 by (rule po_refl [THEN PO_iff [THEN iffD1]]) |
427 done |
433 |
|
434 lemma POgenIs: |
|
435 "<true,true> : POgen(R)" |
|
436 "<false,false> : POgen(R)" |
|
437 "[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)" |
|
438 "!!b b'. [|!!x. <b(x),b'(x)> : R |] ==><lam x. b(x),lam x. b'(x)> : POgen(R)" |
|
439 "<one,one> : POgen(R)" |
|
440 "<a,a'> : lfp(%x. POgen(x) Un R Un PO) ==> |
|
441 <inl(a),inl(a')> : POgen(lfp(%x. POgen(x) Un R Un PO))" |
|
442 "<b,b'> : lfp(%x. POgen(x) Un R Un PO) ==> |
|
443 <inr(b),inr(b')> : POgen(lfp(%x. POgen(x) Un R Un PO))" |
|
444 "<zero,zero> : POgen(lfp(%x. POgen(x) Un R Un PO))" |
|
445 "<n,n'> : lfp(%x. POgen(x) Un R Un PO) ==> |
|
446 <succ(n),succ(n')> : POgen(lfp(%x. POgen(x) Un R Un PO))" |
|
447 "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))" |
|
448 "[| <h,h'> : lfp(%x. POgen(x) Un R Un PO); <t,t'> : lfp(%x. POgen(x) Un R Un PO) |] |
|
449 ==> <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))" |
|
450 unfolding data_defs by (genIs POgenXH POgen_mono)+ |
428 |
451 |
429 ML {* |
452 ML {* |
430 |
453 fun POgen_tac ctxt (rla, rlb) i = |
431 val POgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm POgenXH} @{thm POgen_mono}) |
|
432 ["<true,true> : POgen(R)", |
|
433 "<false,false> : POgen(R)", |
|
434 "[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)", |
|
435 "[|!!x. <b(x),b'(x)> : R |] ==><lam x. b(x),lam x. b'(x)> : POgen(R)", |
|
436 "<one,one> : POgen(R)", |
|
437 "<a,a'> : lfp(%x. POgen(x) Un R Un PO) ==> <inl(a),inl(a')> : POgen(lfp(%x. POgen(x) Un R Un PO))", |
|
438 "<b,b'> : lfp(%x. POgen(x) Un R Un PO) ==> <inr(b),inr(b')> : POgen(lfp(%x. POgen(x) Un R Un PO))", |
|
439 "<zero,zero> : POgen(lfp(%x. POgen(x) Un R Un PO))", |
|
440 "<n,n'> : lfp(%x. POgen(x) Un R Un PO) ==> <succ(n),succ(n')> : POgen(lfp(%x. POgen(x) Un R Un PO))", |
|
441 "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))", |
|
442 "[| <h,h'> : lfp(%x. POgen(x) Un R Un PO); <t,t'> : lfp(%x. POgen(x) Un R Un PO) |] ==> <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"]; |
|
443 |
|
444 fun POgen_tac ctxt (rla,rlb) i = |
|
445 SELECT_GOAL (safe_tac (claset_of ctxt)) i THEN |
454 SELECT_GOAL (safe_tac (claset_of ctxt)) i THEN |
446 rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN |
455 rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN |
447 (REPEAT (resolve_tac (POgenIs @ [@{thm PO_refl} RS (@{thm POgen_mono} RS ci3_AI)] @ |
456 (REPEAT (resolve_tac |
448 (POgenIs RL [@{thm POgen_mono} RS ci3_AgenI]) @ [@{thm POgen_mono} RS ci3_RI]) i)); |
457 (@{thms POgenIs} @ [@{thm PO_refl} RS (@{thm POgen_mono} RS @{thm ci3_AI})] @ |
449 |
458 (@{thms POgenIs} RL [@{thm POgen_mono} RS @{thm ci3_AgenI}]) @ |
|
459 [@{thm POgen_mono} RS @{thm ci3_RI}]) i)) |
450 *} |
460 *} |
451 |
461 |
452 |
462 |
453 subsection {* EQgen *} |
463 subsection {* EQgen *} |
454 |
464 |
455 lemma EQ_refl: "<a,a> : EQ" |
465 lemma EQ_refl: "<a,a> : EQ" |
456 apply (rule refl [THEN EQ_iff [THEN iffD1]]) |
466 by (rule refl [THEN EQ_iff [THEN iffD1]]) |
457 done |
467 |
|
468 lemma EQgenIs: |
|
469 "<true,true> : EQgen(R)" |
|
470 "<false,false> : EQgen(R)" |
|
471 "[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)" |
|
472 "!!b b'. [|!!x. <b(x),b'(x)> : R |] ==> <lam x. b(x),lam x. b'(x)> : EQgen(R)" |
|
473 "<one,one> : EQgen(R)" |
|
474 "<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==> |
|
475 <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" |
|
476 "<b,b'> : lfp(%x. EQgen(x) Un R Un EQ) ==> |
|
477 <inr(b),inr(b')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" |
|
478 "<zero,zero> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" |
|
479 "<n,n'> : lfp(%x. EQgen(x) Un R Un EQ) ==> |
|
480 <succ(n),succ(n')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" |
|
481 "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" |
|
482 "[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) |] |
|
483 ==> <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" |
|
484 unfolding data_defs by (genIs EQgenXH EQgen_mono)+ |
458 |
485 |
459 ML {* |
486 ML {* |
460 |
|
461 val EQgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm EQgenXH} @{thm EQgen_mono}) |
|
462 ["<true,true> : EQgen(R)", |
|
463 "<false,false> : EQgen(R)", |
|
464 "[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)", |
|
465 "[|!!x. <b(x),b'(x)> : R |] ==> <lam x. b(x),lam x. b'(x)> : EQgen(R)", |
|
466 "<one,one> : EQgen(R)", |
|
467 "<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==> <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", |
|
468 "<b,b'> : lfp(%x. EQgen(x) Un R Un EQ) ==> <inr(b),inr(b')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", |
|
469 "<zero,zero> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", |
|
470 "<n,n'> : lfp(%x. EQgen(x) Un R Un EQ) ==> <succ(n),succ(n')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", |
|
471 "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", |
|
472 "[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) |] ==> <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"]; |
|
473 |
|
474 fun EQgen_raw_tac i = |
487 fun EQgen_raw_tac i = |
475 (REPEAT (resolve_tac (EQgenIs @ [@{thm EQ_refl} RS (@{thm EQgen_mono} RS ci3_AI)] @ |
488 (REPEAT (resolve_tac (@{thms EQgenIs} @ |
476 (EQgenIs RL [@{thm EQgen_mono} RS ci3_AgenI]) @ [@{thm EQgen_mono} RS ci3_RI]) i)) |
489 [@{thm EQ_refl} RS (@{thm EQgen_mono} RS @{thm ci3_AI})] @ |
|
490 (@{thms EQgenIs} RL [@{thm EQgen_mono} RS @{thm ci3_AgenI}]) @ |
|
491 [@{thm EQgen_mono} RS @{thm ci3_RI}]) i)) |
477 |
492 |
478 (* Goals of the form R <= EQgen(R) - rewrite elements <a,b> : EQgen(R) using rews and *) |
493 (* Goals of the form R <= EQgen(R) - rewrite elements <a,b> : EQgen(R) using rews and *) |
479 (* then reduce this to a goal <a',b'> : R (hopefully?) *) |
494 (* then reduce this to a goal <a',b'> : R (hopefully?) *) |
480 (* rews are rewrite rules that would cause looping in the simpifier *) |
495 (* rews are rewrite rules that would cause looping in the simpifier *) |
481 |
496 |
482 fun EQgen_tac ctxt rews i = |
497 fun EQgen_tac ctxt rews i = |
483 SELECT_GOAL |
498 SELECT_GOAL |
484 (TRY (safe_tac (claset_of ctxt)) THEN |
499 (TRY (safe_tac (claset_of ctxt)) THEN |
485 resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [@{thm ssubst_pair}])) i THEN |
500 resolve_tac ((rews @ [refl]) RL ((rews @ [refl]) RL [@{thm ssubst_pair}])) i THEN |
486 ALLGOALS (simp_tac (simpset_of ctxt)) THEN |
501 ALLGOALS (simp_tac (simpset_of ctxt)) THEN |
487 ALLGOALS EQgen_raw_tac) i |
502 ALLGOALS EQgen_raw_tac) i |
488 *} |
503 *} |
489 |
504 |
490 end |
505 end |