385 apply (rule sep_rules is_recfun_iff_sats | simp)+ |
437 apply (rule sep_rules is_recfun_iff_sats | simp)+ |
386 apply (simp_all add: succ_Un_distrib [symmetric]) |
438 apply (simp_all add: succ_Un_distrib [symmetric]) |
387 done |
439 done |
388 |
440 |
389 |
441 |
|
442 subsubsection{*Instantiating the locale @{text M_wfrank}*} |
|
443 ML |
|
444 {* |
|
445 val wfrank_separation = thm "wfrank_separation"; |
|
446 val wfrank_strong_replacement = thm "wfrank_strong_replacement"; |
|
447 val Ord_wfrank_separation = thm "Ord_wfrank_separation"; |
|
448 |
|
449 val m_wfrank = |
|
450 [wfrank_separation, wfrank_strong_replacement, Ord_wfrank_separation]; |
|
451 |
|
452 fun wfrank_L th = |
|
453 kill_flex_triv_prems (m_wfrank MRS (trancl_L th)); |
|
454 |
|
455 |
|
456 |
|
457 bind_thm ("iterates_closed", wfrank_L (thm "M_wfrank.iterates_closed")); |
|
458 bind_thm ("exists_wfrank", wfrank_L (thm "M_wfrank.exists_wfrank")); |
|
459 bind_thm ("M_wellfoundedrank", wfrank_L (thm "M_wfrank.M_wellfoundedrank")); |
|
460 bind_thm ("Ord_wfrank_range", wfrank_L (thm "M_wfrank.Ord_wfrank_range")); |
|
461 bind_thm ("Ord_range_wellfoundedrank", wfrank_L (thm "M_wfrank.Ord_range_wellfoundedrank")); |
|
462 bind_thm ("function_wellfoundedrank", wfrank_L (thm "M_wfrank.function_wellfoundedrank")); |
|
463 bind_thm ("domain_wellfoundedrank", wfrank_L (thm "M_wfrank.domain_wellfoundedrank")); |
|
464 bind_thm ("wellfoundedrank_type", wfrank_L (thm "M_wfrank.wellfoundedrank_type")); |
|
465 bind_thm ("Ord_wellfoundedrank", wfrank_L (thm "M_wfrank.Ord_wellfoundedrank")); |
|
466 bind_thm ("wellfoundedrank_eq", wfrank_L (thm "M_wfrank.wellfoundedrank_eq")); |
|
467 bind_thm ("wellfoundedrank_lt", wfrank_L (thm "M_wfrank.wellfoundedrank_lt")); |
|
468 bind_thm ("wellfounded_imp_subset_rvimage", wfrank_L (thm "M_wfrank.wellfounded_imp_subset_rvimage")); |
|
469 bind_thm ("wellfounded_imp_wf", wfrank_L (thm "M_wfrank.wellfounded_imp_wf")); |
|
470 bind_thm ("wellfounded_on_imp_wf_on", wfrank_L (thm "M_wfrank.wellfounded_on_imp_wf_on")); |
|
471 bind_thm ("wf_abs", wfrank_L (thm "M_wfrank.wf_abs")); |
|
472 bind_thm ("wf_on_abs", wfrank_L (thm "M_wfrank.wf_on_abs")); |
|
473 bind_thm ("wfrec_replacement_iff", wfrank_L (thm "M_wfrank.wfrec_replacement_iff")); |
|
474 bind_thm ("trans_wfrec_closed", wfrank_L (thm "M_wfrank.trans_wfrec_closed")); |
|
475 bind_thm ("wfrec_closed", wfrank_L (thm "M_wfrank.wfrec_closed")); |
|
476 *} |
|
477 |
|
478 declare iterates_closed [intro,simp] |
|
479 declare Ord_wfrank_range [rule_format] |
|
480 declare wf_abs [simp] |
|
481 declare wf_on_abs [simp] |
|
482 |
|
483 |
|
484 subsection{*For Datatypes*} |
|
485 |
|
486 subsubsection{*Binary Products, Internalized*} |
|
487 |
|
488 constdefs cartprod_fm :: "[i,i,i]=>i" |
|
489 (* "cartprod(M,A,B,z) == |
|
490 \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))" *) |
|
491 "cartprod_fm(A,B,z) == |
|
492 Forall(Iff(Member(0,succ(z)), |
|
493 Exists(And(Member(0,succ(succ(A))), |
|
494 Exists(And(Member(0,succ(succ(succ(B)))), |
|
495 pair_fm(1,0,2)))))))" |
|
496 |
|
497 lemma cartprod_type [TC]: |
|
498 "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> cartprod_fm(x,y,z) \<in> formula" |
|
499 by (simp add: cartprod_fm_def) |
|
500 |
|
501 lemma arity_cartprod_fm [simp]: |
|
502 "[| x \<in> nat; y \<in> nat; z \<in> nat |] |
|
503 ==> arity(cartprod_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" |
|
504 by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac) |
|
505 |
|
506 lemma sats_cartprod_fm [simp]: |
|
507 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
|
508 ==> sats(A, cartprod_fm(x,y,z), env) <-> |
|
509 cartprod(**A, nth(x,env), nth(y,env), nth(z,env))" |
|
510 by (simp add: cartprod_fm_def cartprod_def) |
|
511 |
|
512 lemma cartprod_iff_sats: |
|
513 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
|
514 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
|
515 ==> cartprod(**A, x, y, z) <-> sats(A, cartprod_fm(i,j,k), env)" |
|
516 by (simp add: sats_cartprod_fm) |
|
517 |
|
518 theorem cartprod_reflection: |
|
519 "REFLECTS[\<lambda>x. cartprod(L,f(x),g(x),h(x)), |
|
520 \<lambda>i x. cartprod(**Lset(i),f(x),g(x),h(x))]" |
|
521 apply (simp only: cartprod_def setclass_simps) |
|
522 apply (intro FOL_reflections pair_reflection) |
|
523 done |
|
524 |
|
525 |
|
526 subsubsection{*Binary Sums, Internalized*} |
|
527 |
|
528 (* "is_sum(M,A,B,Z) == |
|
529 \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M]. |
|
530 3 2 1 0 |
|
531 number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) & |
|
532 cartprod(M,s1,B,B1) & union(M,A0,B1,Z)" *) |
|
533 constdefs sum_fm :: "[i,i,i]=>i" |
|
534 "sum_fm(A,B,Z) == |
|
535 Exists(Exists(Exists(Exists( |
|
536 And(number1_fm(2), |
|
537 And(cartprod_fm(2,A#+4,3), |
|
538 And(upair_fm(2,2,1), |
|
539 And(cartprod_fm(1,B#+4,0), union_fm(3,0,Z#+4)))))))))" |
|
540 |
|
541 lemma sum_type [TC]: |
|
542 "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> sum_fm(x,y,z) \<in> formula" |
|
543 by (simp add: sum_fm_def) |
|
544 |
|
545 lemma arity_sum_fm [simp]: |
|
546 "[| x \<in> nat; y \<in> nat; z \<in> nat |] |
|
547 ==> arity(sum_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" |
|
548 by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac) |
|
549 |
|
550 lemma sats_sum_fm [simp]: |
|
551 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
|
552 ==> sats(A, sum_fm(x,y,z), env) <-> |
|
553 is_sum(**A, nth(x,env), nth(y,env), nth(z,env))" |
|
554 by (simp add: sum_fm_def is_sum_def) |
|
555 |
|
556 lemma sum_iff_sats: |
|
557 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
|
558 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
|
559 ==> is_sum(**A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)" |
|
560 by simp |
|
561 |
|
562 theorem sum_reflection: |
|
563 "REFLECTS[\<lambda>x. is_sum(L,f(x),g(x),h(x)), |
|
564 \<lambda>i x. is_sum(**Lset(i),f(x),g(x),h(x))]" |
|
565 apply (simp only: is_sum_def setclass_simps) |
|
566 apply (intro FOL_reflections function_reflections cartprod_reflection) |
|
567 done |
|
568 |
|
569 |
|
570 subsubsection{*The List Functor, Internalized*} |
|
571 |
|
572 constdefs list_functor_fm :: "[i,i,i]=>i" |
|
573 (* "is_list_functor(M,A,X,Z) == |
|
574 \<exists>n1[M]. \<exists>AX[M]. |
|
575 number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *) |
|
576 "list_functor_fm(A,X,Z) == |
|
577 Exists(Exists( |
|
578 And(number1_fm(1), |
|
579 And(cartprod_fm(A#+2,X#+2,0), sum_fm(1,0,Z#+2)))))" |
|
580 |
|
581 lemma list_functor_type [TC]: |
|
582 "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_functor_fm(x,y,z) \<in> formula" |
|
583 by (simp add: list_functor_fm_def) |
|
584 |
|
585 lemma arity_list_functor_fm [simp]: |
|
586 "[| x \<in> nat; y \<in> nat; z \<in> nat |] |
|
587 ==> arity(list_functor_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" |
|
588 by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac) |
|
589 |
|
590 lemma sats_list_functor_fm [simp]: |
|
591 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
|
592 ==> sats(A, list_functor_fm(x,y,z), env) <-> |
|
593 is_list_functor(**A, nth(x,env), nth(y,env), nth(z,env))" |
|
594 by (simp add: list_functor_fm_def is_list_functor_def) |
|
595 |
|
596 lemma list_functor_iff_sats: |
|
597 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
|
598 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
|
599 ==> is_list_functor(**A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)" |
|
600 by simp |
|
601 |
|
602 theorem list_functor_reflection: |
|
603 "REFLECTS[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)), |
|
604 \<lambda>i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]" |
|
605 apply (simp only: is_list_functor_def setclass_simps) |
|
606 apply (intro FOL_reflections number1_reflection |
|
607 cartprod_reflection sum_reflection) |
|
608 done |
|
609 |
|
610 subsubsection{*The Operator @{term quasinat}*} |
|
611 |
|
612 (* "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))" *) |
|
613 constdefs quasinat_fm :: "i=>i" |
|
614 "quasinat_fm(z) == Or(empty_fm(z), Exists(succ_fm(0,succ(z))))" |
|
615 |
|
616 lemma quasinat_type [TC]: |
|
617 "x \<in> nat ==> quasinat_fm(x) \<in> formula" |
|
618 by (simp add: quasinat_fm_def) |
|
619 |
|
620 lemma arity_quasinat_fm [simp]: |
|
621 "x \<in> nat ==> arity(quasinat_fm(x)) = succ(x)" |
|
622 by (simp add: quasinat_fm_def succ_Un_distrib [symmetric] Un_ac) |
|
623 |
|
624 lemma sats_quasinat_fm [simp]: |
|
625 "[| x \<in> nat; env \<in> list(A)|] |
|
626 ==> sats(A, quasinat_fm(x), env) <-> is_quasinat(**A, nth(x,env))" |
|
627 by (simp add: quasinat_fm_def is_quasinat_def) |
|
628 |
|
629 lemma quasinat_iff_sats: |
|
630 "[| nth(i,env) = x; nth(j,env) = y; |
|
631 i \<in> nat; env \<in> list(A)|] |
|
632 ==> is_quasinat(**A, x) <-> sats(A, quasinat_fm(i), env)" |
|
633 by simp |
|
634 |
|
635 theorem quasinat_reflection: |
|
636 "REFLECTS[\<lambda>x. is_quasinat(L,f(x)), |
|
637 \<lambda>i x. is_quasinat(**Lset(i),f(x))]" |
|
638 apply (simp only: is_quasinat_def setclass_simps) |
|
639 apply (intro FOL_reflections function_reflections) |
|
640 done |
|
641 |
|
642 |
|
643 subsubsection{*The Operator @{term is_nat_case}*} |
|
644 |
|
645 (* is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o" |
|
646 "is_nat_case(M, a, is_b, k, z) == |
|
647 (empty(M,k) --> z=a) & |
|
648 (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) & |
|
649 (is_quasinat(M,k) | empty(M,z))" *) |
|
650 text{*The formula @{term is_b} has free variables 1 and 0.*} |
|
651 constdefs is_nat_case_fm :: "[i, [i,i]=>i, i, i]=>i" |
|
652 "is_nat_case_fm(a,is_b,k,z) == |
|
653 And(Implies(empty_fm(k), Equal(z,a)), |
|
654 And(Forall(Implies(succ_fm(0,succ(k)), |
|
655 Forall(Implies(Equal(0,succ(succ(z))), is_b(1,0))))), |
|
656 Or(quasinat_fm(k), empty_fm(z))))" |
|
657 |
|
658 lemma is_nat_case_type [TC]: |
|
659 "[| is_b(1,0) \<in> formula; |
|
660 x \<in> nat; y \<in> nat; z \<in> nat |] |
|
661 ==> is_nat_case_fm(x,is_b,y,z) \<in> formula" |
|
662 by (simp add: is_nat_case_fm_def) |
|
663 |
|
664 lemma arity_is_nat_case_fm [simp]: |
|
665 "[| is_b(1,0) \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |] |
|
666 ==> arity(is_nat_case_fm(x,is_b,y,z)) = |
|
667 succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(is_b(1,0)) #- 2)" |
|
668 apply (subgoal_tac "arity(is_b(1,0)) \<in> nat") |
|
669 apply typecheck |
|
670 (*FIXME: could nat_diff_split work?*) |
|
671 apply (auto simp add: diff_def raw_diff_succ is_nat_case_fm_def nat_imp_quasinat |
|
672 succ_Un_distrib [symmetric] Un_ac |
|
673 split: split_nat_case) |
|
674 done |
|
675 |
|
676 lemma sats_is_nat_case_fm: |
|
677 assumes is_b_iff_sats: |
|
678 "!!a b. [| a \<in> A; b \<in> A|] |
|
679 ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env)))" |
|
680 shows |
|
681 "[|x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|] |
|
682 ==> sats(A, is_nat_case_fm(x,p,y,z), env) <-> |
|
683 is_nat_case(**A, nth(x,env), is_b, nth(y,env), nth(z,env))" |
|
684 apply (frule lt_length_in_nat, assumption) |
|
685 apply (simp add: is_nat_case_fm_def is_nat_case_def is_b_iff_sats [THEN iff_sym]) |
|
686 done |
|
687 |
|
688 lemma is_nat_case_iff_sats: |
|
689 "[| (!!a b. [| a \<in> A; b \<in> A|] |
|
690 ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env)))); |
|
691 nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
|
692 i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|] |
|
693 ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)" |
|
694 by (simp add: sats_is_nat_case_fm [of A is_b]) |
|
695 |
|
696 |
|
697 text{*The second argument of @{term is_b} gives it direct access to @{term x}, |
|
698 which is essential for handling free variable references. Without this |
|
699 argument, we cannot prove reflection for @{term iterates_MH}.*} |
|
700 theorem is_nat_case_reflection: |
|
701 assumes is_b_reflection: |
|
702 "!!h f g. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x)), |
|
703 \<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x))]" |
|
704 shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)), |
|
705 \<lambda>i x. is_nat_case(**Lset(i), f(x), is_b(**Lset(i), x), g(x), h(x))]" |
|
706 apply (simp (no_asm_use) only: is_nat_case_def setclass_simps) |
|
707 apply (intro FOL_reflections function_reflections |
|
708 restriction_reflection is_b_reflection quasinat_reflection) |
|
709 done |
|
710 |
|
711 |
|
712 |
|
713 subsection{*The Operator @{term iterates_MH}, Needed for Iteration*} |
|
714 |
|
715 (* iterates_MH :: "[i=>o, [i,i]=>o, i, i, i, i] => o" |
|
716 "iterates_MH(M,isF,v,n,g,z) == |
|
717 is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u), |
|
718 n, z)" *) |
|
719 constdefs iterates_MH_fm :: "[[i,i]=>i, i, i, i, i]=>i" |
|
720 "iterates_MH_fm(isF,v,n,g,z) == |
|
721 is_nat_case_fm(v, |
|
722 \<lambda>m u. Exists(And(fun_apply_fm(succ(succ(succ(g))),succ(m),0), |
|
723 Forall(Implies(Equal(0,succ(succ(u))), isF(1,0))))), |
|
724 n, z)" |
|
725 |
|
726 lemma iterates_MH_type [TC]: |
|
727 "[| p(1,0) \<in> formula; |
|
728 v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |] |
|
729 ==> iterates_MH_fm(p,v,x,y,z) \<in> formula" |
|
730 by (simp add: iterates_MH_fm_def) |
|
731 |
|
732 |
|
733 lemma arity_iterates_MH_fm [simp]: |
|
734 "[| p(1,0) \<in> formula; |
|
735 v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |] |
|
736 ==> arity(iterates_MH_fm(p,v,x,y,z)) = |
|
737 succ(v) \<union> succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(p(1,0)) #- 4)" |
|
738 apply (subgoal_tac "arity(p(1,0)) \<in> nat") |
|
739 apply typecheck |
|
740 apply (simp add: nat_imp_quasinat iterates_MH_fm_def Un_ac |
|
741 split: split_nat_case, clarify) |
|
742 apply (rename_tac i j) |
|
743 apply (drule eq_succ_imp_eq_m1, simp) |
|
744 apply (drule eq_succ_imp_eq_m1, simp) |
|
745 apply (simp add: diff_Un_distrib succ_Un_distrib Un_ac diff_diff_left) |
|
746 done |
|
747 |
|
748 lemma sats_iterates_MH_fm: |
|
749 assumes is_F_iff_sats: |
|
750 "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|] |
|
751 ==> is_F(a,b) <-> |
|
752 sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env)))))" |
|
753 shows |
|
754 "[|v \<in> nat; x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|] |
|
755 ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <-> |
|
756 iterates_MH(**A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))" |
|
757 by (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm |
|
758 is_F_iff_sats [symmetric]) |
|
759 |
|
760 lemma iterates_MH_iff_sats: |
|
761 "[| (!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|] |
|
762 ==> is_F(a,b) <-> |
|
763 sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env)))))); |
|
764 nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
|
765 i' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|] |
|
766 ==> iterates_MH(**A, is_F, v, x, y, z) <-> |
|
767 sats(A, iterates_MH_fm(p,i',i,j,k), env)" |
|
768 apply (rule iff_sym) |
|
769 apply (rule iff_trans) |
|
770 apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all) |
|
771 done |
|
772 |
|
773 theorem iterates_MH_reflection: |
|
774 assumes p_reflection: |
|
775 "!!f g h. REFLECTS[\<lambda>x. p(L, f(x), g(x)), |
|
776 \<lambda>i x. p(**Lset(i), f(x), g(x))]" |
|
777 shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L), e(x), f(x), g(x), h(x)), |
|
778 \<lambda>i x. iterates_MH(**Lset(i), p(**Lset(i)), e(x), f(x), g(x), h(x))]" |
|
779 apply (simp (no_asm_use) only: iterates_MH_def) |
|
780 txt{*Must be careful: simplifying with @{text setclass_simps} above would |
|
781 change @{text "\<exists>gm[**Lset(i)]"} into @{text "\<exists>gm \<in> Lset(i)"}, when |
|
782 it would no longer match rule @{text is_nat_case_reflection}. *} |
|
783 apply (rule is_nat_case_reflection) |
|
784 apply (simp (no_asm_use) only: setclass_simps) |
|
785 apply (intro FOL_reflections function_reflections is_nat_case_reflection |
|
786 restriction_reflection p_reflection) |
|
787 done |
|
788 |
|
789 |
|
790 |
|
791 subsection{*@{term L} is Closed Under the Operator @{term list}*} |
|
792 |
|
793 |
|
794 lemma list_replacement1_Reflects: |
|
795 "REFLECTS |
|
796 [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and> |
|
797 is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)), |
|
798 \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and> |
|
799 is_wfrec(**Lset(i), |
|
800 iterates_MH(**Lset(i), |
|
801 is_list_functor(**Lset(i), A), 0), memsn, u, y))]" |
|
802 by (intro FOL_reflections function_reflections is_wfrec_reflection |
|
803 iterates_MH_reflection list_functor_reflection) |
|
804 |
|
805 lemma list_replacement1: |
|
806 "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)" |
|
807 apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) |
|
808 apply (rule strong_replacementI) |
|
809 apply (rule rallI) |
|
810 apply (rename_tac B) |
|
811 apply (rule separation_CollectI) |
|
812 apply (insert nonempty) |
|
813 apply (subgoal_tac "L(Memrel(succ(n)))") |
|
814 apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast ) |
|
815 apply (rule ReflectsE [OF list_replacement1_Reflects], assumption) |
|
816 apply (drule subset_Lset_ltD, assumption) |
|
817 apply (erule reflection_imp_L_separation) |
|
818 apply (simp_all add: lt_Ord2) |
|
819 apply (rule DPowI2) |
|
820 apply (rename_tac v) |
|
821 apply (rule bex_iff_sats conj_iff_sats)+ |
|
822 apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats) |
|
823 apply (rule sep_rules | simp)+ |
|
824 txt{*Can't get sat rules to work for higher-order operators, so just expand them!*} |
|
825 apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def) |
|
826 apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+ |
|
827 apply (simp_all add: succ_Un_distrib [symmetric] Memrel_closed) |
|
828 done |
|
829 |
|
830 |
|
831 lemma list_replacement2_Reflects: |
|
832 "REFLECTS |
|
833 [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and> |
|
834 (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and> |
|
835 is_wfrec (L, iterates_MH (L, is_list_functor(L, A), 0), |
|
836 msn, u, x)), |
|
837 \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and> |
|
838 (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). |
|
839 successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and> |
|
840 is_wfrec (**Lset(i), |
|
841 iterates_MH (**Lset(i), is_list_functor(**Lset(i), A), 0), |
|
842 msn, u, x))]" |
|
843 by (intro FOL_reflections function_reflections is_wfrec_reflection |
|
844 iterates_MH_reflection list_functor_reflection) |
|
845 |
|
846 |
|
847 lemma list_replacement2: |
|
848 "L(A) ==> strong_replacement(L, |
|
849 \<lambda>n y. n\<in>nat & |
|
850 (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) & |
|
851 is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0), |
|
852 msn, n, y)))" |
|
853 apply (rule strong_replacementI) |
|
854 apply (rule rallI) |
|
855 apply (rename_tac B) |
|
856 apply (rule separation_CollectI) |
|
857 apply (insert nonempty) |
|
858 apply (rule_tac A="{A,B,z,0,nat}" in subset_LsetE) |
|
859 apply (blast intro: L_nat) |
|
860 apply (rule ReflectsE [OF list_replacement2_Reflects], assumption) |
|
861 apply (drule subset_Lset_ltD, assumption) |
|
862 apply (erule reflection_imp_L_separation) |
|
863 apply (simp_all add: lt_Ord2) |
|
864 apply (rule DPowI2) |
|
865 apply (rename_tac v) |
|
866 apply (rule bex_iff_sats conj_iff_sats)+ |
|
867 apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats) |
|
868 apply (rule sep_rules | simp)+ |
|
869 apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def) |
|
870 apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+ |
|
871 apply (simp_all add: succ_Un_distrib [symmetric] Memrel_closed) |
|
872 done |
|
873 |
|
874 |
|
875 |
390 end |
876 end |