295 done |
295 done |
296 |
296 |
297 text{*This version handles an alternative form of the bounded quantifier |
297 text{*This version handles an alternative form of the bounded quantifier |
298 in the second argument of @{text REFLECTS}.*} |
298 in the second argument of @{text REFLECTS}.*} |
299 theorem Rex_reflection': |
299 theorem Rex_reflection': |
300 "REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] |
300 "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] |
301 ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[**Lset(a)]. Q(a,x,z)]" |
301 ==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[##Lset(a)]. Q(a,x,z)]" |
302 apply (unfold setclass_def rex_def) |
302 apply (unfold setclass_def rex_def) |
303 apply (erule Rex_reflection [unfolded rex_def Bex_def]) |
303 apply (erule Rex_reflection [unfolded rex_def Bex_def]) |
304 done |
304 done |
305 |
305 |
306 text{*As above.*} |
306 text{*As above.*} |
307 theorem Rall_reflection': |
307 theorem Rall_reflection': |
308 "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] |
308 "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] |
309 ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z[**Lset(a)]. Q(a,x,z)]" |
309 ==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z[##Lset(a)]. Q(a,x,z)]" |
310 apply (unfold setclass_def rall_def) |
310 apply (unfold setclass_def rall_def) |
311 apply (erule Rall_reflection [unfolded rall_def Ball_def]) |
311 apply (erule Rall_reflection [unfolded rall_def Ball_def]) |
312 done |
312 done |
313 |
313 |
314 lemmas FOL_reflections = |
314 lemmas FOL_reflections = |
367 "x \<in> nat ==> empty_fm(x) \<in> formula" |
367 "x \<in> nat ==> empty_fm(x) \<in> formula" |
368 by (simp add: empty_fm_def) |
368 by (simp add: empty_fm_def) |
369 |
369 |
370 lemma sats_empty_fm [simp]: |
370 lemma sats_empty_fm [simp]: |
371 "[| x \<in> nat; env \<in> list(A)|] |
371 "[| x \<in> nat; env \<in> list(A)|] |
372 ==> sats(A, empty_fm(x), env) <-> empty(**A, nth(x,env))" |
372 ==> sats(A, empty_fm(x), env) <-> empty(##A, nth(x,env))" |
373 by (simp add: empty_fm_def empty_def) |
373 by (simp add: empty_fm_def empty_def) |
374 |
374 |
375 lemma empty_iff_sats: |
375 lemma empty_iff_sats: |
376 "[| nth(i,env) = x; nth(j,env) = y; |
376 "[| nth(i,env) = x; nth(j,env) = y; |
377 i \<in> nat; env \<in> list(A)|] |
377 i \<in> nat; env \<in> list(A)|] |
378 ==> empty(**A, x) <-> sats(A, empty_fm(i), env)" |
378 ==> empty(##A, x) <-> sats(A, empty_fm(i), env)" |
379 by simp |
379 by simp |
380 |
380 |
381 theorem empty_reflection: |
381 theorem empty_reflection: |
382 "REFLECTS[\<lambda>x. empty(L,f(x)), |
382 "REFLECTS[\<lambda>x. empty(L,f(x)), |
383 \<lambda>i x. empty(**Lset(i),f(x))]" |
383 \<lambda>i x. empty(##Lset(i),f(x))]" |
384 apply (simp only: empty_def) |
384 apply (simp only: empty_def) |
385 apply (intro FOL_reflections) |
385 apply (intro FOL_reflections) |
386 done |
386 done |
387 |
387 |
388 text{*Not used. But maybe useful?*} |
388 text{*Not used. But maybe useful?*} |
410 by (simp add: upair_fm_def) |
410 by (simp add: upair_fm_def) |
411 |
411 |
412 lemma sats_upair_fm [simp]: |
412 lemma sats_upair_fm [simp]: |
413 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
413 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
414 ==> sats(A, upair_fm(x,y,z), env) <-> |
414 ==> sats(A, upair_fm(x,y,z), env) <-> |
415 upair(**A, nth(x,env), nth(y,env), nth(z,env))" |
415 upair(##A, nth(x,env), nth(y,env), nth(z,env))" |
416 by (simp add: upair_fm_def upair_def) |
416 by (simp add: upair_fm_def upair_def) |
417 |
417 |
418 lemma upair_iff_sats: |
418 lemma upair_iff_sats: |
419 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
419 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
420 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
420 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
421 ==> upair(**A, x, y, z) <-> sats(A, upair_fm(i,j,k), env)" |
421 ==> upair(##A, x, y, z) <-> sats(A, upair_fm(i,j,k), env)" |
422 by (simp add: sats_upair_fm) |
422 by (simp add: sats_upair_fm) |
423 |
423 |
424 text{*Useful? At least it refers to "real" unordered pairs*} |
424 text{*Useful? At least it refers to "real" unordered pairs*} |
425 lemma sats_upair_fm2 [simp]: |
425 lemma sats_upair_fm2 [simp]: |
426 "[| x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A); Transset(A)|] |
426 "[| x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A); Transset(A)|] |
431 apply (blast intro: nth_type) |
431 apply (blast intro: nth_type) |
432 done |
432 done |
433 |
433 |
434 theorem upair_reflection: |
434 theorem upair_reflection: |
435 "REFLECTS[\<lambda>x. upair(L,f(x),g(x),h(x)), |
435 "REFLECTS[\<lambda>x. upair(L,f(x),g(x),h(x)), |
436 \<lambda>i x. upair(**Lset(i),f(x),g(x),h(x))]" |
436 \<lambda>i x. upair(##Lset(i),f(x),g(x),h(x))]" |
437 apply (simp add: upair_def) |
437 apply (simp add: upair_def) |
438 apply (intro FOL_reflections) |
438 apply (intro FOL_reflections) |
439 done |
439 done |
440 |
440 |
441 subsubsection{*Ordered pairs, Internalized*} |
441 subsubsection{*Ordered pairs, Internalized*} |
451 by (simp add: pair_fm_def) |
451 by (simp add: pair_fm_def) |
452 |
452 |
453 lemma sats_pair_fm [simp]: |
453 lemma sats_pair_fm [simp]: |
454 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
454 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
455 ==> sats(A, pair_fm(x,y,z), env) <-> |
455 ==> sats(A, pair_fm(x,y,z), env) <-> |
456 pair(**A, nth(x,env), nth(y,env), nth(z,env))" |
456 pair(##A, nth(x,env), nth(y,env), nth(z,env))" |
457 by (simp add: pair_fm_def pair_def) |
457 by (simp add: pair_fm_def pair_def) |
458 |
458 |
459 lemma pair_iff_sats: |
459 lemma pair_iff_sats: |
460 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
460 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
461 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
461 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
462 ==> pair(**A, x, y, z) <-> sats(A, pair_fm(i,j,k), env)" |
462 ==> pair(##A, x, y, z) <-> sats(A, pair_fm(i,j,k), env)" |
463 by (simp add: sats_pair_fm) |
463 by (simp add: sats_pair_fm) |
464 |
464 |
465 theorem pair_reflection: |
465 theorem pair_reflection: |
466 "REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)), |
466 "REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)), |
467 \<lambda>i x. pair(**Lset(i),f(x),g(x),h(x))]" |
467 \<lambda>i x. pair(##Lset(i),f(x),g(x),h(x))]" |
468 apply (simp only: pair_def) |
468 apply (simp only: pair_def) |
469 apply (intro FOL_reflections upair_reflection) |
469 apply (intro FOL_reflections upair_reflection) |
470 done |
470 done |
471 |
471 |
472 |
472 |
482 by (simp add: union_fm_def) |
482 by (simp add: union_fm_def) |
483 |
483 |
484 lemma sats_union_fm [simp]: |
484 lemma sats_union_fm [simp]: |
485 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
485 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
486 ==> sats(A, union_fm(x,y,z), env) <-> |
486 ==> sats(A, union_fm(x,y,z), env) <-> |
487 union(**A, nth(x,env), nth(y,env), nth(z,env))" |
487 union(##A, nth(x,env), nth(y,env), nth(z,env))" |
488 by (simp add: union_fm_def union_def) |
488 by (simp add: union_fm_def union_def) |
489 |
489 |
490 lemma union_iff_sats: |
490 lemma union_iff_sats: |
491 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
491 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
492 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
492 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
493 ==> union(**A, x, y, z) <-> sats(A, union_fm(i,j,k), env)" |
493 ==> union(##A, x, y, z) <-> sats(A, union_fm(i,j,k), env)" |
494 by (simp add: sats_union_fm) |
494 by (simp add: sats_union_fm) |
495 |
495 |
496 theorem union_reflection: |
496 theorem union_reflection: |
497 "REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)), |
497 "REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)), |
498 \<lambda>i x. union(**Lset(i),f(x),g(x),h(x))]" |
498 \<lambda>i x. union(##Lset(i),f(x),g(x),h(x))]" |
499 apply (simp only: union_def) |
499 apply (simp only: union_def) |
500 apply (intro FOL_reflections) |
500 apply (intro FOL_reflections) |
501 done |
501 done |
502 |
502 |
503 |
503 |
514 by (simp add: cons_fm_def) |
514 by (simp add: cons_fm_def) |
515 |
515 |
516 lemma sats_cons_fm [simp]: |
516 lemma sats_cons_fm [simp]: |
517 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
517 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
518 ==> sats(A, cons_fm(x,y,z), env) <-> |
518 ==> sats(A, cons_fm(x,y,z), env) <-> |
519 is_cons(**A, nth(x,env), nth(y,env), nth(z,env))" |
519 is_cons(##A, nth(x,env), nth(y,env), nth(z,env))" |
520 by (simp add: cons_fm_def is_cons_def) |
520 by (simp add: cons_fm_def is_cons_def) |
521 |
521 |
522 lemma cons_iff_sats: |
522 lemma cons_iff_sats: |
523 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
523 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
524 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
524 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
525 ==> is_cons(**A, x, y, z) <-> sats(A, cons_fm(i,j,k), env)" |
525 ==> is_cons(##A, x, y, z) <-> sats(A, cons_fm(i,j,k), env)" |
526 by simp |
526 by simp |
527 |
527 |
528 theorem cons_reflection: |
528 theorem cons_reflection: |
529 "REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)), |
529 "REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)), |
530 \<lambda>i x. is_cons(**Lset(i),f(x),g(x),h(x))]" |
530 \<lambda>i x. is_cons(##Lset(i),f(x),g(x),h(x))]" |
531 apply (simp only: is_cons_def) |
531 apply (simp only: is_cons_def) |
532 apply (intro FOL_reflections upair_reflection union_reflection) |
532 apply (intro FOL_reflections upair_reflection union_reflection) |
533 done |
533 done |
534 |
534 |
535 |
535 |
543 by (simp add: succ_fm_def) |
543 by (simp add: succ_fm_def) |
544 |
544 |
545 lemma sats_succ_fm [simp]: |
545 lemma sats_succ_fm [simp]: |
546 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
546 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
547 ==> sats(A, succ_fm(x,y), env) <-> |
547 ==> sats(A, succ_fm(x,y), env) <-> |
548 successor(**A, nth(x,env), nth(y,env))" |
548 successor(##A, nth(x,env), nth(y,env))" |
549 by (simp add: succ_fm_def successor_def) |
549 by (simp add: succ_fm_def successor_def) |
550 |
550 |
551 lemma successor_iff_sats: |
551 lemma successor_iff_sats: |
552 "[| nth(i,env) = x; nth(j,env) = y; |
552 "[| nth(i,env) = x; nth(j,env) = y; |
553 i \<in> nat; j \<in> nat; env \<in> list(A)|] |
553 i \<in> nat; j \<in> nat; env \<in> list(A)|] |
554 ==> successor(**A, x, y) <-> sats(A, succ_fm(i,j), env)" |
554 ==> successor(##A, x, y) <-> sats(A, succ_fm(i,j), env)" |
555 by simp |
555 by simp |
556 |
556 |
557 theorem successor_reflection: |
557 theorem successor_reflection: |
558 "REFLECTS[\<lambda>x. successor(L,f(x),g(x)), |
558 "REFLECTS[\<lambda>x. successor(L,f(x),g(x)), |
559 \<lambda>i x. successor(**Lset(i),f(x),g(x))]" |
559 \<lambda>i x. successor(##Lset(i),f(x),g(x))]" |
560 apply (simp only: successor_def) |
560 apply (simp only: successor_def) |
561 apply (intro cons_reflection) |
561 apply (intro cons_reflection) |
562 done |
562 done |
563 |
563 |
564 |
564 |
572 "x \<in> nat ==> number1_fm(x) \<in> formula" |
572 "x \<in> nat ==> number1_fm(x) \<in> formula" |
573 by (simp add: number1_fm_def) |
573 by (simp add: number1_fm_def) |
574 |
574 |
575 lemma sats_number1_fm [simp]: |
575 lemma sats_number1_fm [simp]: |
576 "[| x \<in> nat; env \<in> list(A)|] |
576 "[| x \<in> nat; env \<in> list(A)|] |
577 ==> sats(A, number1_fm(x), env) <-> number1(**A, nth(x,env))" |
577 ==> sats(A, number1_fm(x), env) <-> number1(##A, nth(x,env))" |
578 by (simp add: number1_fm_def number1_def) |
578 by (simp add: number1_fm_def number1_def) |
579 |
579 |
580 lemma number1_iff_sats: |
580 lemma number1_iff_sats: |
581 "[| nth(i,env) = x; nth(j,env) = y; |
581 "[| nth(i,env) = x; nth(j,env) = y; |
582 i \<in> nat; env \<in> list(A)|] |
582 i \<in> nat; env \<in> list(A)|] |
583 ==> number1(**A, x) <-> sats(A, number1_fm(i), env)" |
583 ==> number1(##A, x) <-> sats(A, number1_fm(i), env)" |
584 by simp |
584 by simp |
585 |
585 |
586 theorem number1_reflection: |
586 theorem number1_reflection: |
587 "REFLECTS[\<lambda>x. number1(L,f(x)), |
587 "REFLECTS[\<lambda>x. number1(L,f(x)), |
588 \<lambda>i x. number1(**Lset(i),f(x))]" |
588 \<lambda>i x. number1(##Lset(i),f(x))]" |
589 apply (simp only: number1_def) |
589 apply (simp only: number1_def) |
590 apply (intro FOL_reflections empty_reflection successor_reflection) |
590 apply (intro FOL_reflections empty_reflection successor_reflection) |
591 done |
591 done |
592 |
592 |
593 |
593 |
604 by (simp add: big_union_fm_def) |
604 by (simp add: big_union_fm_def) |
605 |
605 |
606 lemma sats_big_union_fm [simp]: |
606 lemma sats_big_union_fm [simp]: |
607 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
607 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
608 ==> sats(A, big_union_fm(x,y), env) <-> |
608 ==> sats(A, big_union_fm(x,y), env) <-> |
609 big_union(**A, nth(x,env), nth(y,env))" |
609 big_union(##A, nth(x,env), nth(y,env))" |
610 by (simp add: big_union_fm_def big_union_def) |
610 by (simp add: big_union_fm_def big_union_def) |
611 |
611 |
612 lemma big_union_iff_sats: |
612 lemma big_union_iff_sats: |
613 "[| nth(i,env) = x; nth(j,env) = y; |
613 "[| nth(i,env) = x; nth(j,env) = y; |
614 i \<in> nat; j \<in> nat; env \<in> list(A)|] |
614 i \<in> nat; j \<in> nat; env \<in> list(A)|] |
615 ==> big_union(**A, x, y) <-> sats(A, big_union_fm(i,j), env)" |
615 ==> big_union(##A, x, y) <-> sats(A, big_union_fm(i,j), env)" |
616 by simp |
616 by simp |
617 |
617 |
618 theorem big_union_reflection: |
618 theorem big_union_reflection: |
619 "REFLECTS[\<lambda>x. big_union(L,f(x),g(x)), |
619 "REFLECTS[\<lambda>x. big_union(L,f(x),g(x)), |
620 \<lambda>i x. big_union(**Lset(i),f(x),g(x))]" |
620 \<lambda>i x. big_union(##Lset(i),f(x),g(x))]" |
621 apply (simp only: big_union_def) |
621 apply (simp only: big_union_def) |
622 apply (intro FOL_reflections) |
622 apply (intro FOL_reflections) |
623 done |
623 done |
624 |
624 |
625 |
625 |
631 real concepts such as @{term Ord}. Now that we have instantiated the locale |
631 real concepts such as @{term Ord}. Now that we have instantiated the locale |
632 @{text M_trivial}, we no longer require the earlier versions.*} |
632 @{text M_trivial}, we no longer require the earlier versions.*} |
633 |
633 |
634 lemma sats_subset_fm': |
634 lemma sats_subset_fm': |
635 "[|x \<in> nat; y \<in> nat; env \<in> list(A)|] |
635 "[|x \<in> nat; y \<in> nat; env \<in> list(A)|] |
636 ==> sats(A, subset_fm(x,y), env) <-> subset(**A, nth(x,env), nth(y,env))" |
636 ==> sats(A, subset_fm(x,y), env) <-> subset(##A, nth(x,env), nth(y,env))" |
637 by (simp add: subset_fm_def Relative.subset_def) |
637 by (simp add: subset_fm_def Relative.subset_def) |
638 |
638 |
639 theorem subset_reflection: |
639 theorem subset_reflection: |
640 "REFLECTS[\<lambda>x. subset(L,f(x),g(x)), |
640 "REFLECTS[\<lambda>x. subset(L,f(x),g(x)), |
641 \<lambda>i x. subset(**Lset(i),f(x),g(x))]" |
641 \<lambda>i x. subset(##Lset(i),f(x),g(x))]" |
642 apply (simp only: Relative.subset_def) |
642 apply (simp only: Relative.subset_def) |
643 apply (intro FOL_reflections) |
643 apply (intro FOL_reflections) |
644 done |
644 done |
645 |
645 |
646 lemma sats_transset_fm': |
646 lemma sats_transset_fm': |
647 "[|x \<in> nat; env \<in> list(A)|] |
647 "[|x \<in> nat; env \<in> list(A)|] |
648 ==> sats(A, transset_fm(x), env) <-> transitive_set(**A, nth(x,env))" |
648 ==> sats(A, transset_fm(x), env) <-> transitive_set(##A, nth(x,env))" |
649 by (simp add: sats_subset_fm' transset_fm_def transitive_set_def) |
649 by (simp add: sats_subset_fm' transset_fm_def transitive_set_def) |
650 |
650 |
651 theorem transitive_set_reflection: |
651 theorem transitive_set_reflection: |
652 "REFLECTS[\<lambda>x. transitive_set(L,f(x)), |
652 "REFLECTS[\<lambda>x. transitive_set(L,f(x)), |
653 \<lambda>i x. transitive_set(**Lset(i),f(x))]" |
653 \<lambda>i x. transitive_set(##Lset(i),f(x))]" |
654 apply (simp only: transitive_set_def) |
654 apply (simp only: transitive_set_def) |
655 apply (intro FOL_reflections subset_reflection) |
655 apply (intro FOL_reflections subset_reflection) |
656 done |
656 done |
657 |
657 |
658 lemma sats_ordinal_fm': |
658 lemma sats_ordinal_fm': |
659 "[|x \<in> nat; env \<in> list(A)|] |
659 "[|x \<in> nat; env \<in> list(A)|] |
660 ==> sats(A, ordinal_fm(x), env) <-> ordinal(**A,nth(x,env))" |
660 ==> sats(A, ordinal_fm(x), env) <-> ordinal(##A,nth(x,env))" |
661 by (simp add: sats_transset_fm' ordinal_fm_def ordinal_def) |
661 by (simp add: sats_transset_fm' ordinal_fm_def ordinal_def) |
662 |
662 |
663 lemma ordinal_iff_sats: |
663 lemma ordinal_iff_sats: |
664 "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|] |
664 "[| nth(i,env) = x; i \<in> nat; env \<in> list(A)|] |
665 ==> ordinal(**A, x) <-> sats(A, ordinal_fm(i), env)" |
665 ==> ordinal(##A, x) <-> sats(A, ordinal_fm(i), env)" |
666 by (simp add: sats_ordinal_fm') |
666 by (simp add: sats_ordinal_fm') |
667 |
667 |
668 theorem ordinal_reflection: |
668 theorem ordinal_reflection: |
669 "REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(**Lset(i),f(x))]" |
669 "REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(##Lset(i),f(x))]" |
670 apply (simp only: ordinal_def) |
670 apply (simp only: ordinal_def) |
671 apply (intro FOL_reflections transitive_set_reflection) |
671 apply (intro FOL_reflections transitive_set_reflection) |
672 done |
672 done |
673 |
673 |
674 |
674 |
687 by (simp add: Memrel_fm_def) |
687 by (simp add: Memrel_fm_def) |
688 |
688 |
689 lemma sats_Memrel_fm [simp]: |
689 lemma sats_Memrel_fm [simp]: |
690 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
690 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
691 ==> sats(A, Memrel_fm(x,y), env) <-> |
691 ==> sats(A, Memrel_fm(x,y), env) <-> |
692 membership(**A, nth(x,env), nth(y,env))" |
692 membership(##A, nth(x,env), nth(y,env))" |
693 by (simp add: Memrel_fm_def membership_def) |
693 by (simp add: Memrel_fm_def membership_def) |
694 |
694 |
695 lemma Memrel_iff_sats: |
695 lemma Memrel_iff_sats: |
696 "[| nth(i,env) = x; nth(j,env) = y; |
696 "[| nth(i,env) = x; nth(j,env) = y; |
697 i \<in> nat; j \<in> nat; env \<in> list(A)|] |
697 i \<in> nat; j \<in> nat; env \<in> list(A)|] |
698 ==> membership(**A, x, y) <-> sats(A, Memrel_fm(i,j), env)" |
698 ==> membership(##A, x, y) <-> sats(A, Memrel_fm(i,j), env)" |
699 by simp |
699 by simp |
700 |
700 |
701 theorem membership_reflection: |
701 theorem membership_reflection: |
702 "REFLECTS[\<lambda>x. membership(L,f(x),g(x)), |
702 "REFLECTS[\<lambda>x. membership(L,f(x),g(x)), |
703 \<lambda>i x. membership(**Lset(i),f(x),g(x))]" |
703 \<lambda>i x. membership(##Lset(i),f(x),g(x))]" |
704 apply (simp only: membership_def) |
704 apply (simp only: membership_def) |
705 apply (intro FOL_reflections pair_reflection) |
705 apply (intro FOL_reflections pair_reflection) |
706 done |
706 done |
707 |
707 |
708 subsubsection{*Predecessor Set, Internalized*} |
708 subsubsection{*Predecessor Set, Internalized*} |
721 by (simp add: pred_set_fm_def) |
721 by (simp add: pred_set_fm_def) |
722 |
722 |
723 lemma sats_pred_set_fm [simp]: |
723 lemma sats_pred_set_fm [simp]: |
724 "[| U \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat; env \<in> list(A)|] |
724 "[| U \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat; env \<in> list(A)|] |
725 ==> sats(A, pred_set_fm(U,x,r,B), env) <-> |
725 ==> sats(A, pred_set_fm(U,x,r,B), env) <-> |
726 pred_set(**A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))" |
726 pred_set(##A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))" |
727 by (simp add: pred_set_fm_def pred_set_def) |
727 by (simp add: pred_set_fm_def pred_set_def) |
728 |
728 |
729 lemma pred_set_iff_sats: |
729 lemma pred_set_iff_sats: |
730 "[| nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B; |
730 "[| nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B; |
731 i \<in> nat; j \<in> nat; k \<in> nat; l \<in> nat; env \<in> list(A)|] |
731 i \<in> nat; j \<in> nat; k \<in> nat; l \<in> nat; env \<in> list(A)|] |
732 ==> pred_set(**A,U,x,r,B) <-> sats(A, pred_set_fm(i,j,k,l), env)" |
732 ==> pred_set(##A,U,x,r,B) <-> sats(A, pred_set_fm(i,j,k,l), env)" |
733 by (simp add: sats_pred_set_fm) |
733 by (simp add: sats_pred_set_fm) |
734 |
734 |
735 theorem pred_set_reflection: |
735 theorem pred_set_reflection: |
736 "REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)), |
736 "REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)), |
737 \<lambda>i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]" |
737 \<lambda>i x. pred_set(##Lset(i),f(x),g(x),h(x),b(x))]" |
738 apply (simp only: pred_set_def) |
738 apply (simp only: pred_set_def) |
739 apply (intro FOL_reflections pair_reflection) |
739 apply (intro FOL_reflections pair_reflection) |
740 done |
740 done |
741 |
741 |
742 |
742 |
756 by (simp add: domain_fm_def) |
756 by (simp add: domain_fm_def) |
757 |
757 |
758 lemma sats_domain_fm [simp]: |
758 lemma sats_domain_fm [simp]: |
759 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
759 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
760 ==> sats(A, domain_fm(x,y), env) <-> |
760 ==> sats(A, domain_fm(x,y), env) <-> |
761 is_domain(**A, nth(x,env), nth(y,env))" |
761 is_domain(##A, nth(x,env), nth(y,env))" |
762 by (simp add: domain_fm_def is_domain_def) |
762 by (simp add: domain_fm_def is_domain_def) |
763 |
763 |
764 lemma domain_iff_sats: |
764 lemma domain_iff_sats: |
765 "[| nth(i,env) = x; nth(j,env) = y; |
765 "[| nth(i,env) = x; nth(j,env) = y; |
766 i \<in> nat; j \<in> nat; env \<in> list(A)|] |
766 i \<in> nat; j \<in> nat; env \<in> list(A)|] |
767 ==> is_domain(**A, x, y) <-> sats(A, domain_fm(i,j), env)" |
767 ==> is_domain(##A, x, y) <-> sats(A, domain_fm(i,j), env)" |
768 by simp |
768 by simp |
769 |
769 |
770 theorem domain_reflection: |
770 theorem domain_reflection: |
771 "REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)), |
771 "REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)), |
772 \<lambda>i x. is_domain(**Lset(i),f(x),g(x))]" |
772 \<lambda>i x. is_domain(##Lset(i),f(x),g(x))]" |
773 apply (simp only: is_domain_def) |
773 apply (simp only: is_domain_def) |
774 apply (intro FOL_reflections pair_reflection) |
774 apply (intro FOL_reflections pair_reflection) |
775 done |
775 done |
776 |
776 |
777 |
777 |
790 by (simp add: range_fm_def) |
790 by (simp add: range_fm_def) |
791 |
791 |
792 lemma sats_range_fm [simp]: |
792 lemma sats_range_fm [simp]: |
793 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
793 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
794 ==> sats(A, range_fm(x,y), env) <-> |
794 ==> sats(A, range_fm(x,y), env) <-> |
795 is_range(**A, nth(x,env), nth(y,env))" |
795 is_range(##A, nth(x,env), nth(y,env))" |
796 by (simp add: range_fm_def is_range_def) |
796 by (simp add: range_fm_def is_range_def) |
797 |
797 |
798 lemma range_iff_sats: |
798 lemma range_iff_sats: |
799 "[| nth(i,env) = x; nth(j,env) = y; |
799 "[| nth(i,env) = x; nth(j,env) = y; |
800 i \<in> nat; j \<in> nat; env \<in> list(A)|] |
800 i \<in> nat; j \<in> nat; env \<in> list(A)|] |
801 ==> is_range(**A, x, y) <-> sats(A, range_fm(i,j), env)" |
801 ==> is_range(##A, x, y) <-> sats(A, range_fm(i,j), env)" |
802 by simp |
802 by simp |
803 |
803 |
804 theorem range_reflection: |
804 theorem range_reflection: |
805 "REFLECTS[\<lambda>x. is_range(L,f(x),g(x)), |
805 "REFLECTS[\<lambda>x. is_range(L,f(x),g(x)), |
806 \<lambda>i x. is_range(**Lset(i),f(x),g(x))]" |
806 \<lambda>i x. is_range(##Lset(i),f(x),g(x))]" |
807 apply (simp only: is_range_def) |
807 apply (simp only: is_range_def) |
808 apply (intro FOL_reflections pair_reflection) |
808 apply (intro FOL_reflections pair_reflection) |
809 done |
809 done |
810 |
810 |
811 |
811 |
825 by (simp add: field_fm_def) |
825 by (simp add: field_fm_def) |
826 |
826 |
827 lemma sats_field_fm [simp]: |
827 lemma sats_field_fm [simp]: |
828 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
828 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
829 ==> sats(A, field_fm(x,y), env) <-> |
829 ==> sats(A, field_fm(x,y), env) <-> |
830 is_field(**A, nth(x,env), nth(y,env))" |
830 is_field(##A, nth(x,env), nth(y,env))" |
831 by (simp add: field_fm_def is_field_def) |
831 by (simp add: field_fm_def is_field_def) |
832 |
832 |
833 lemma field_iff_sats: |
833 lemma field_iff_sats: |
834 "[| nth(i,env) = x; nth(j,env) = y; |
834 "[| nth(i,env) = x; nth(j,env) = y; |
835 i \<in> nat; j \<in> nat; env \<in> list(A)|] |
835 i \<in> nat; j \<in> nat; env \<in> list(A)|] |
836 ==> is_field(**A, x, y) <-> sats(A, field_fm(i,j), env)" |
836 ==> is_field(##A, x, y) <-> sats(A, field_fm(i,j), env)" |
837 by simp |
837 by simp |
838 |
838 |
839 theorem field_reflection: |
839 theorem field_reflection: |
840 "REFLECTS[\<lambda>x. is_field(L,f(x),g(x)), |
840 "REFLECTS[\<lambda>x. is_field(L,f(x),g(x)), |
841 \<lambda>i x. is_field(**Lset(i),f(x),g(x))]" |
841 \<lambda>i x. is_field(##Lset(i),f(x),g(x))]" |
842 apply (simp only: is_field_def) |
842 apply (simp only: is_field_def) |
843 apply (intro FOL_reflections domain_reflection range_reflection |
843 apply (intro FOL_reflections domain_reflection range_reflection |
844 union_reflection) |
844 union_reflection) |
845 done |
845 done |
846 |
846 |
861 by (simp add: image_fm_def) |
861 by (simp add: image_fm_def) |
862 |
862 |
863 lemma sats_image_fm [simp]: |
863 lemma sats_image_fm [simp]: |
864 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
864 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
865 ==> sats(A, image_fm(x,y,z), env) <-> |
865 ==> sats(A, image_fm(x,y,z), env) <-> |
866 image(**A, nth(x,env), nth(y,env), nth(z,env))" |
866 image(##A, nth(x,env), nth(y,env), nth(z,env))" |
867 by (simp add: image_fm_def Relative.image_def) |
867 by (simp add: image_fm_def Relative.image_def) |
868 |
868 |
869 lemma image_iff_sats: |
869 lemma image_iff_sats: |
870 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
870 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
871 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
871 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
872 ==> image(**A, x, y, z) <-> sats(A, image_fm(i,j,k), env)" |
872 ==> image(##A, x, y, z) <-> sats(A, image_fm(i,j,k), env)" |
873 by (simp add: sats_image_fm) |
873 by (simp add: sats_image_fm) |
874 |
874 |
875 theorem image_reflection: |
875 theorem image_reflection: |
876 "REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)), |
876 "REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)), |
877 \<lambda>i x. image(**Lset(i),f(x),g(x),h(x))]" |
877 \<lambda>i x. image(##Lset(i),f(x),g(x),h(x))]" |
878 apply (simp only: Relative.image_def) |
878 apply (simp only: Relative.image_def) |
879 apply (intro FOL_reflections pair_reflection) |
879 apply (intro FOL_reflections pair_reflection) |
880 done |
880 done |
881 |
881 |
882 |
882 |
896 by (simp add: pre_image_fm_def) |
896 by (simp add: pre_image_fm_def) |
897 |
897 |
898 lemma sats_pre_image_fm [simp]: |
898 lemma sats_pre_image_fm [simp]: |
899 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
899 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
900 ==> sats(A, pre_image_fm(x,y,z), env) <-> |
900 ==> sats(A, pre_image_fm(x,y,z), env) <-> |
901 pre_image(**A, nth(x,env), nth(y,env), nth(z,env))" |
901 pre_image(##A, nth(x,env), nth(y,env), nth(z,env))" |
902 by (simp add: pre_image_fm_def Relative.pre_image_def) |
902 by (simp add: pre_image_fm_def Relative.pre_image_def) |
903 |
903 |
904 lemma pre_image_iff_sats: |
904 lemma pre_image_iff_sats: |
905 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
905 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
906 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
906 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
907 ==> pre_image(**A, x, y, z) <-> sats(A, pre_image_fm(i,j,k), env)" |
907 ==> pre_image(##A, x, y, z) <-> sats(A, pre_image_fm(i,j,k), env)" |
908 by (simp add: sats_pre_image_fm) |
908 by (simp add: sats_pre_image_fm) |
909 |
909 |
910 theorem pre_image_reflection: |
910 theorem pre_image_reflection: |
911 "REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)), |
911 "REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)), |
912 \<lambda>i x. pre_image(**Lset(i),f(x),g(x),h(x))]" |
912 \<lambda>i x. pre_image(##Lset(i),f(x),g(x),h(x))]" |
913 apply (simp only: Relative.pre_image_def) |
913 apply (simp only: Relative.pre_image_def) |
914 apply (intro FOL_reflections pair_reflection) |
914 apply (intro FOL_reflections pair_reflection) |
915 done |
915 done |
916 |
916 |
917 |
917 |
931 by (simp add: fun_apply_fm_def) |
931 by (simp add: fun_apply_fm_def) |
932 |
932 |
933 lemma sats_fun_apply_fm [simp]: |
933 lemma sats_fun_apply_fm [simp]: |
934 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
934 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
935 ==> sats(A, fun_apply_fm(x,y,z), env) <-> |
935 ==> sats(A, fun_apply_fm(x,y,z), env) <-> |
936 fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))" |
936 fun_apply(##A, nth(x,env), nth(y,env), nth(z,env))" |
937 by (simp add: fun_apply_fm_def fun_apply_def) |
937 by (simp add: fun_apply_fm_def fun_apply_def) |
938 |
938 |
939 lemma fun_apply_iff_sats: |
939 lemma fun_apply_iff_sats: |
940 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
940 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
941 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
941 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
942 ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)" |
942 ==> fun_apply(##A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)" |
943 by simp |
943 by simp |
944 |
944 |
945 theorem fun_apply_reflection: |
945 theorem fun_apply_reflection: |
946 "REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)), |
946 "REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)), |
947 \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]" |
947 \<lambda>i x. fun_apply(##Lset(i),f(x),g(x),h(x))]" |
948 apply (simp only: fun_apply_def) |
948 apply (simp only: fun_apply_def) |
949 apply (intro FOL_reflections upair_reflection image_reflection |
949 apply (intro FOL_reflections upair_reflection image_reflection |
950 big_union_reflection) |
950 big_union_reflection) |
951 done |
951 done |
952 |
952 |
963 "[| x \<in> nat |] ==> relation_fm(x) \<in> formula" |
963 "[| x \<in> nat |] ==> relation_fm(x) \<in> formula" |
964 by (simp add: relation_fm_def) |
964 by (simp add: relation_fm_def) |
965 |
965 |
966 lemma sats_relation_fm [simp]: |
966 lemma sats_relation_fm [simp]: |
967 "[| x \<in> nat; env \<in> list(A)|] |
967 "[| x \<in> nat; env \<in> list(A)|] |
968 ==> sats(A, relation_fm(x), env) <-> is_relation(**A, nth(x,env))" |
968 ==> sats(A, relation_fm(x), env) <-> is_relation(##A, nth(x,env))" |
969 by (simp add: relation_fm_def is_relation_def) |
969 by (simp add: relation_fm_def is_relation_def) |
970 |
970 |
971 lemma relation_iff_sats: |
971 lemma relation_iff_sats: |
972 "[| nth(i,env) = x; nth(j,env) = y; |
972 "[| nth(i,env) = x; nth(j,env) = y; |
973 i \<in> nat; env \<in> list(A)|] |
973 i \<in> nat; env \<in> list(A)|] |
974 ==> is_relation(**A, x) <-> sats(A, relation_fm(i), env)" |
974 ==> is_relation(##A, x) <-> sats(A, relation_fm(i), env)" |
975 by simp |
975 by simp |
976 |
976 |
977 theorem is_relation_reflection: |
977 theorem is_relation_reflection: |
978 "REFLECTS[\<lambda>x. is_relation(L,f(x)), |
978 "REFLECTS[\<lambda>x. is_relation(L,f(x)), |
979 \<lambda>i x. is_relation(**Lset(i),f(x))]" |
979 \<lambda>i x. is_relation(##Lset(i),f(x))]" |
980 apply (simp only: is_relation_def) |
980 apply (simp only: is_relation_def) |
981 apply (intro FOL_reflections pair_reflection) |
981 apply (intro FOL_reflections pair_reflection) |
982 done |
982 done |
983 |
983 |
984 |
984 |
999 "[| x \<in> nat |] ==> function_fm(x) \<in> formula" |
999 "[| x \<in> nat |] ==> function_fm(x) \<in> formula" |
1000 by (simp add: function_fm_def) |
1000 by (simp add: function_fm_def) |
1001 |
1001 |
1002 lemma sats_function_fm [simp]: |
1002 lemma sats_function_fm [simp]: |
1003 "[| x \<in> nat; env \<in> list(A)|] |
1003 "[| x \<in> nat; env \<in> list(A)|] |
1004 ==> sats(A, function_fm(x), env) <-> is_function(**A, nth(x,env))" |
1004 ==> sats(A, function_fm(x), env) <-> is_function(##A, nth(x,env))" |
1005 by (simp add: function_fm_def is_function_def) |
1005 by (simp add: function_fm_def is_function_def) |
1006 |
1006 |
1007 lemma is_function_iff_sats: |
1007 lemma is_function_iff_sats: |
1008 "[| nth(i,env) = x; nth(j,env) = y; |
1008 "[| nth(i,env) = x; nth(j,env) = y; |
1009 i \<in> nat; env \<in> list(A)|] |
1009 i \<in> nat; env \<in> list(A)|] |
1010 ==> is_function(**A, x) <-> sats(A, function_fm(i), env)" |
1010 ==> is_function(##A, x) <-> sats(A, function_fm(i), env)" |
1011 by simp |
1011 by simp |
1012 |
1012 |
1013 theorem is_function_reflection: |
1013 theorem is_function_reflection: |
1014 "REFLECTS[\<lambda>x. is_function(L,f(x)), |
1014 "REFLECTS[\<lambda>x. is_function(L,f(x)), |
1015 \<lambda>i x. is_function(**Lset(i),f(x))]" |
1015 \<lambda>i x. is_function(##Lset(i),f(x))]" |
1016 apply (simp only: is_function_def) |
1016 apply (simp only: is_function_def) |
1017 apply (intro FOL_reflections pair_reflection) |
1017 apply (intro FOL_reflections pair_reflection) |
1018 done |
1018 done |
1019 |
1019 |
1020 |
1020 |
1037 by (simp add: typed_function_fm_def) |
1037 by (simp add: typed_function_fm_def) |
1038 |
1038 |
1039 lemma sats_typed_function_fm [simp]: |
1039 lemma sats_typed_function_fm [simp]: |
1040 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
1040 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
1041 ==> sats(A, typed_function_fm(x,y,z), env) <-> |
1041 ==> sats(A, typed_function_fm(x,y,z), env) <-> |
1042 typed_function(**A, nth(x,env), nth(y,env), nth(z,env))" |
1042 typed_function(##A, nth(x,env), nth(y,env), nth(z,env))" |
1043 by (simp add: typed_function_fm_def typed_function_def) |
1043 by (simp add: typed_function_fm_def typed_function_def) |
1044 |
1044 |
1045 lemma typed_function_iff_sats: |
1045 lemma typed_function_iff_sats: |
1046 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
1046 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
1047 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
1047 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
1048 ==> typed_function(**A, x, y, z) <-> sats(A, typed_function_fm(i,j,k), env)" |
1048 ==> typed_function(##A, x, y, z) <-> sats(A, typed_function_fm(i,j,k), env)" |
1049 by simp |
1049 by simp |
1050 |
1050 |
1051 lemmas function_reflections = |
1051 lemmas function_reflections = |
1052 empty_reflection number1_reflection |
1052 empty_reflection number1_reflection |
1053 upair_reflection pair_reflection union_reflection |
1053 upair_reflection pair_reflection union_reflection |
1097 by (simp add: composition_fm_def) |
1097 by (simp add: composition_fm_def) |
1098 |
1098 |
1099 lemma sats_composition_fm [simp]: |
1099 lemma sats_composition_fm [simp]: |
1100 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
1100 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
1101 ==> sats(A, composition_fm(x,y,z), env) <-> |
1101 ==> sats(A, composition_fm(x,y,z), env) <-> |
1102 composition(**A, nth(x,env), nth(y,env), nth(z,env))" |
1102 composition(##A, nth(x,env), nth(y,env), nth(z,env))" |
1103 by (simp add: composition_fm_def composition_def) |
1103 by (simp add: composition_fm_def composition_def) |
1104 |
1104 |
1105 lemma composition_iff_sats: |
1105 lemma composition_iff_sats: |
1106 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
1106 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
1107 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
1107 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
1108 ==> composition(**A, x, y, z) <-> sats(A, composition_fm(i,j,k), env)" |
1108 ==> composition(##A, x, y, z) <-> sats(A, composition_fm(i,j,k), env)" |
1109 by simp |
1109 by simp |
1110 |
1110 |
1111 theorem composition_reflection: |
1111 theorem composition_reflection: |
1112 "REFLECTS[\<lambda>x. composition(L,f(x),g(x),h(x)), |
1112 "REFLECTS[\<lambda>x. composition(L,f(x),g(x),h(x)), |
1113 \<lambda>i x. composition(**Lset(i),f(x),g(x),h(x))]" |
1113 \<lambda>i x. composition(##Lset(i),f(x),g(x),h(x))]" |
1114 apply (simp only: composition_def) |
1114 apply (simp only: composition_def) |
1115 apply (intro FOL_reflections pair_reflection) |
1115 apply (intro FOL_reflections pair_reflection) |
1116 done |
1116 done |
1117 |
1117 |
1118 |
1118 |
1137 by (simp add: injection_fm_def) |
1137 by (simp add: injection_fm_def) |
1138 |
1138 |
1139 lemma sats_injection_fm [simp]: |
1139 lemma sats_injection_fm [simp]: |
1140 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
1140 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
1141 ==> sats(A, injection_fm(x,y,z), env) <-> |
1141 ==> sats(A, injection_fm(x,y,z), env) <-> |
1142 injection(**A, nth(x,env), nth(y,env), nth(z,env))" |
1142 injection(##A, nth(x,env), nth(y,env), nth(z,env))" |
1143 by (simp add: injection_fm_def injection_def) |
1143 by (simp add: injection_fm_def injection_def) |
1144 |
1144 |
1145 lemma injection_iff_sats: |
1145 lemma injection_iff_sats: |
1146 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
1146 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
1147 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
1147 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
1148 ==> injection(**A, x, y, z) <-> sats(A, injection_fm(i,j,k), env)" |
1148 ==> injection(##A, x, y, z) <-> sats(A, injection_fm(i,j,k), env)" |
1149 by simp |
1149 by simp |
1150 |
1150 |
1151 theorem injection_reflection: |
1151 theorem injection_reflection: |
1152 "REFLECTS[\<lambda>x. injection(L,f(x),g(x),h(x)), |
1152 "REFLECTS[\<lambda>x. injection(L,f(x),g(x),h(x)), |
1153 \<lambda>i x. injection(**Lset(i),f(x),g(x),h(x))]" |
1153 \<lambda>i x. injection(##Lset(i),f(x),g(x),h(x))]" |
1154 apply (simp only: injection_def) |
1154 apply (simp only: injection_def) |
1155 apply (intro FOL_reflections function_reflections typed_function_reflection) |
1155 apply (intro FOL_reflections function_reflections typed_function_reflection) |
1156 done |
1156 done |
1157 |
1157 |
1158 |
1158 |
1174 by (simp add: surjection_fm_def) |
1174 by (simp add: surjection_fm_def) |
1175 |
1175 |
1176 lemma sats_surjection_fm [simp]: |
1176 lemma sats_surjection_fm [simp]: |
1177 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
1177 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
1178 ==> sats(A, surjection_fm(x,y,z), env) <-> |
1178 ==> sats(A, surjection_fm(x,y,z), env) <-> |
1179 surjection(**A, nth(x,env), nth(y,env), nth(z,env))" |
1179 surjection(##A, nth(x,env), nth(y,env), nth(z,env))" |
1180 by (simp add: surjection_fm_def surjection_def) |
1180 by (simp add: surjection_fm_def surjection_def) |
1181 |
1181 |
1182 lemma surjection_iff_sats: |
1182 lemma surjection_iff_sats: |
1183 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
1183 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
1184 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
1184 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
1185 ==> surjection(**A, x, y, z) <-> sats(A, surjection_fm(i,j,k), env)" |
1185 ==> surjection(##A, x, y, z) <-> sats(A, surjection_fm(i,j,k), env)" |
1186 by simp |
1186 by simp |
1187 |
1187 |
1188 theorem surjection_reflection: |
1188 theorem surjection_reflection: |
1189 "REFLECTS[\<lambda>x. surjection(L,f(x),g(x),h(x)), |
1189 "REFLECTS[\<lambda>x. surjection(L,f(x),g(x),h(x)), |
1190 \<lambda>i x. surjection(**Lset(i),f(x),g(x),h(x))]" |
1190 \<lambda>i x. surjection(##Lset(i),f(x),g(x),h(x))]" |
1191 apply (simp only: surjection_def) |
1191 apply (simp only: surjection_def) |
1192 apply (intro FOL_reflections function_reflections typed_function_reflection) |
1192 apply (intro FOL_reflections function_reflections typed_function_reflection) |
1193 done |
1193 done |
1194 |
1194 |
1195 |
1195 |
1206 by (simp add: bijection_fm_def) |
1206 by (simp add: bijection_fm_def) |
1207 |
1207 |
1208 lemma sats_bijection_fm [simp]: |
1208 lemma sats_bijection_fm [simp]: |
1209 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
1209 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
1210 ==> sats(A, bijection_fm(x,y,z), env) <-> |
1210 ==> sats(A, bijection_fm(x,y,z), env) <-> |
1211 bijection(**A, nth(x,env), nth(y,env), nth(z,env))" |
1211 bijection(##A, nth(x,env), nth(y,env), nth(z,env))" |
1212 by (simp add: bijection_fm_def bijection_def) |
1212 by (simp add: bijection_fm_def bijection_def) |
1213 |
1213 |
1214 lemma bijection_iff_sats: |
1214 lemma bijection_iff_sats: |
1215 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
1215 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
1216 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
1216 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
1217 ==> bijection(**A, x, y, z) <-> sats(A, bijection_fm(i,j,k), env)" |
1217 ==> bijection(##A, x, y, z) <-> sats(A, bijection_fm(i,j,k), env)" |
1218 by simp |
1218 by simp |
1219 |
1219 |
1220 theorem bijection_reflection: |
1220 theorem bijection_reflection: |
1221 "REFLECTS[\<lambda>x. bijection(L,f(x),g(x),h(x)), |
1221 "REFLECTS[\<lambda>x. bijection(L,f(x),g(x),h(x)), |
1222 \<lambda>i x. bijection(**Lset(i),f(x),g(x),h(x))]" |
1222 \<lambda>i x. bijection(##Lset(i),f(x),g(x),h(x))]" |
1223 apply (simp only: bijection_def) |
1223 apply (simp only: bijection_def) |
1224 apply (intro And_reflection injection_reflection surjection_reflection) |
1224 apply (intro And_reflection injection_reflection surjection_reflection) |
1225 done |
1225 done |
1226 |
1226 |
1227 |
1227 |
1242 by (simp add: restriction_fm_def) |
1242 by (simp add: restriction_fm_def) |
1243 |
1243 |
1244 lemma sats_restriction_fm [simp]: |
1244 lemma sats_restriction_fm [simp]: |
1245 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
1245 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
1246 ==> sats(A, restriction_fm(x,y,z), env) <-> |
1246 ==> sats(A, restriction_fm(x,y,z), env) <-> |
1247 restriction(**A, nth(x,env), nth(y,env), nth(z,env))" |
1247 restriction(##A, nth(x,env), nth(y,env), nth(z,env))" |
1248 by (simp add: restriction_fm_def restriction_def) |
1248 by (simp add: restriction_fm_def restriction_def) |
1249 |
1249 |
1250 lemma restriction_iff_sats: |
1250 lemma restriction_iff_sats: |
1251 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
1251 "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; |
1252 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
1252 i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|] |
1253 ==> restriction(**A, x, y, z) <-> sats(A, restriction_fm(i,j,k), env)" |
1253 ==> restriction(##A, x, y, z) <-> sats(A, restriction_fm(i,j,k), env)" |
1254 by simp |
1254 by simp |
1255 |
1255 |
1256 theorem restriction_reflection: |
1256 theorem restriction_reflection: |
1257 "REFLECTS[\<lambda>x. restriction(L,f(x),g(x),h(x)), |
1257 "REFLECTS[\<lambda>x. restriction(L,f(x),g(x),h(x)), |
1258 \<lambda>i x. restriction(**Lset(i),f(x),g(x),h(x))]" |
1258 \<lambda>i x. restriction(##Lset(i),f(x),g(x),h(x))]" |
1259 apply (simp only: restriction_def) |
1259 apply (simp only: restriction_def) |
1260 apply (intro FOL_reflections pair_reflection) |
1260 apply (intro FOL_reflections pair_reflection) |
1261 done |
1261 done |
1262 |
1262 |
1263 subsubsection{*Order-Isomorphisms, Internalized*} |
1263 subsubsection{*Order-Isomorphisms, Internalized*} |
1289 by (simp add: order_isomorphism_fm_def) |
1289 by (simp add: order_isomorphism_fm_def) |
1290 |
1290 |
1291 lemma sats_order_isomorphism_fm [simp]: |
1291 lemma sats_order_isomorphism_fm [simp]: |
1292 "[| U \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat; env \<in> list(A)|] |
1292 "[| U \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat; env \<in> list(A)|] |
1293 ==> sats(A, order_isomorphism_fm(U,r,B,s,f), env) <-> |
1293 ==> sats(A, order_isomorphism_fm(U,r,B,s,f), env) <-> |
1294 order_isomorphism(**A, nth(U,env), nth(r,env), nth(B,env), |
1294 order_isomorphism(##A, nth(U,env), nth(r,env), nth(B,env), |
1295 nth(s,env), nth(f,env))" |
1295 nth(s,env), nth(f,env))" |
1296 by (simp add: order_isomorphism_fm_def order_isomorphism_def) |
1296 by (simp add: order_isomorphism_fm_def order_isomorphism_def) |
1297 |
1297 |
1298 lemma order_isomorphism_iff_sats: |
1298 lemma order_isomorphism_iff_sats: |
1299 "[| nth(i,env) = U; nth(j,env) = r; nth(k,env) = B; nth(j',env) = s; |
1299 "[| nth(i,env) = U; nth(j,env) = r; nth(k,env) = B; nth(j',env) = s; |
1300 nth(k',env) = f; |
1300 nth(k',env) = f; |
1301 i \<in> nat; j \<in> nat; k \<in> nat; j' \<in> nat; k' \<in> nat; env \<in> list(A)|] |
1301 i \<in> nat; j \<in> nat; k \<in> nat; j' \<in> nat; k' \<in> nat; env \<in> list(A)|] |
1302 ==> order_isomorphism(**A,U,r,B,s,f) <-> |
1302 ==> order_isomorphism(##A,U,r,B,s,f) <-> |
1303 sats(A, order_isomorphism_fm(i,j,k,j',k'), env)" |
1303 sats(A, order_isomorphism_fm(i,j,k,j',k'), env)" |
1304 by simp |
1304 by simp |
1305 |
1305 |
1306 theorem order_isomorphism_reflection: |
1306 theorem order_isomorphism_reflection: |
1307 "REFLECTS[\<lambda>x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)), |
1307 "REFLECTS[\<lambda>x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)), |
1308 \<lambda>i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]" |
1308 \<lambda>i x. order_isomorphism(##Lset(i),f(x),g(x),h(x),g'(x),h'(x))]" |
1309 apply (simp only: order_isomorphism_def) |
1309 apply (simp only: order_isomorphism_def) |
1310 apply (intro FOL_reflections function_reflections bijection_reflection) |
1310 apply (intro FOL_reflections function_reflections bijection_reflection) |
1311 done |
1311 done |
1312 |
1312 |
1313 subsubsection{*Limit Ordinals, Internalized*} |
1313 subsubsection{*Limit Ordinals, Internalized*} |
1330 "x \<in> nat ==> limit_ordinal_fm(x) \<in> formula" |
1330 "x \<in> nat ==> limit_ordinal_fm(x) \<in> formula" |
1331 by (simp add: limit_ordinal_fm_def) |
1331 by (simp add: limit_ordinal_fm_def) |
1332 |
1332 |
1333 lemma sats_limit_ordinal_fm [simp]: |
1333 lemma sats_limit_ordinal_fm [simp]: |
1334 "[| x \<in> nat; env \<in> list(A)|] |
1334 "[| x \<in> nat; env \<in> list(A)|] |
1335 ==> sats(A, limit_ordinal_fm(x), env) <-> limit_ordinal(**A, nth(x,env))" |
1335 ==> sats(A, limit_ordinal_fm(x), env) <-> limit_ordinal(##A, nth(x,env))" |
1336 by (simp add: limit_ordinal_fm_def limit_ordinal_def sats_ordinal_fm') |
1336 by (simp add: limit_ordinal_fm_def limit_ordinal_def sats_ordinal_fm') |
1337 |
1337 |
1338 lemma limit_ordinal_iff_sats: |
1338 lemma limit_ordinal_iff_sats: |
1339 "[| nth(i,env) = x; nth(j,env) = y; |
1339 "[| nth(i,env) = x; nth(j,env) = y; |
1340 i \<in> nat; env \<in> list(A)|] |
1340 i \<in> nat; env \<in> list(A)|] |
1341 ==> limit_ordinal(**A, x) <-> sats(A, limit_ordinal_fm(i), env)" |
1341 ==> limit_ordinal(##A, x) <-> sats(A, limit_ordinal_fm(i), env)" |
1342 by simp |
1342 by simp |
1343 |
1343 |
1344 theorem limit_ordinal_reflection: |
1344 theorem limit_ordinal_reflection: |
1345 "REFLECTS[\<lambda>x. limit_ordinal(L,f(x)), |
1345 "REFLECTS[\<lambda>x. limit_ordinal(L,f(x)), |
1346 \<lambda>i x. limit_ordinal(**Lset(i),f(x))]" |
1346 \<lambda>i x. limit_ordinal(##Lset(i),f(x))]" |
1347 apply (simp only: limit_ordinal_def) |
1347 apply (simp only: limit_ordinal_def) |
1348 apply (intro FOL_reflections ordinal_reflection |
1348 apply (intro FOL_reflections ordinal_reflection |
1349 empty_reflection successor_reflection) |
1349 empty_reflection successor_reflection) |
1350 done |
1350 done |
1351 |
1351 |
1365 "x \<in> nat ==> finite_ordinal_fm(x) \<in> formula" |
1365 "x \<in> nat ==> finite_ordinal_fm(x) \<in> formula" |
1366 by (simp add: finite_ordinal_fm_def) |
1366 by (simp add: finite_ordinal_fm_def) |
1367 |
1367 |
1368 lemma sats_finite_ordinal_fm [simp]: |
1368 lemma sats_finite_ordinal_fm [simp]: |
1369 "[| x \<in> nat; env \<in> list(A)|] |
1369 "[| x \<in> nat; env \<in> list(A)|] |
1370 ==> sats(A, finite_ordinal_fm(x), env) <-> finite_ordinal(**A, nth(x,env))" |
1370 ==> sats(A, finite_ordinal_fm(x), env) <-> finite_ordinal(##A, nth(x,env))" |
1371 by (simp add: finite_ordinal_fm_def sats_ordinal_fm' finite_ordinal_def) |
1371 by (simp add: finite_ordinal_fm_def sats_ordinal_fm' finite_ordinal_def) |
1372 |
1372 |
1373 lemma finite_ordinal_iff_sats: |
1373 lemma finite_ordinal_iff_sats: |
1374 "[| nth(i,env) = x; nth(j,env) = y; |
1374 "[| nth(i,env) = x; nth(j,env) = y; |
1375 i \<in> nat; env \<in> list(A)|] |
1375 i \<in> nat; env \<in> list(A)|] |
1376 ==> finite_ordinal(**A, x) <-> sats(A, finite_ordinal_fm(i), env)" |
1376 ==> finite_ordinal(##A, x) <-> sats(A, finite_ordinal_fm(i), env)" |
1377 by simp |
1377 by simp |
1378 |
1378 |
1379 theorem finite_ordinal_reflection: |
1379 theorem finite_ordinal_reflection: |
1380 "REFLECTS[\<lambda>x. finite_ordinal(L,f(x)), |
1380 "REFLECTS[\<lambda>x. finite_ordinal(L,f(x)), |
1381 \<lambda>i x. finite_ordinal(**Lset(i),f(x))]" |
1381 \<lambda>i x. finite_ordinal(##Lset(i),f(x))]" |
1382 apply (simp only: finite_ordinal_def) |
1382 apply (simp only: finite_ordinal_def) |
1383 apply (intro FOL_reflections ordinal_reflection limit_ordinal_reflection) |
1383 apply (intro FOL_reflections ordinal_reflection limit_ordinal_reflection) |
1384 done |
1384 done |
1385 |
1385 |
1386 |
1386 |
1397 "x \<in> nat ==> omega_fm(x) \<in> formula" |
1397 "x \<in> nat ==> omega_fm(x) \<in> formula" |
1398 by (simp add: omega_fm_def) |
1398 by (simp add: omega_fm_def) |
1399 |
1399 |
1400 lemma sats_omega_fm [simp]: |
1400 lemma sats_omega_fm [simp]: |
1401 "[| x \<in> nat; env \<in> list(A)|] |
1401 "[| x \<in> nat; env \<in> list(A)|] |
1402 ==> sats(A, omega_fm(x), env) <-> omega(**A, nth(x,env))" |
1402 ==> sats(A, omega_fm(x), env) <-> omega(##A, nth(x,env))" |
1403 by (simp add: omega_fm_def omega_def) |
1403 by (simp add: omega_fm_def omega_def) |
1404 |
1404 |
1405 lemma omega_iff_sats: |
1405 lemma omega_iff_sats: |
1406 "[| nth(i,env) = x; nth(j,env) = y; |
1406 "[| nth(i,env) = x; nth(j,env) = y; |
1407 i \<in> nat; env \<in> list(A)|] |
1407 i \<in> nat; env \<in> list(A)|] |
1408 ==> omega(**A, x) <-> sats(A, omega_fm(i), env)" |
1408 ==> omega(##A, x) <-> sats(A, omega_fm(i), env)" |
1409 by simp |
1409 by simp |
1410 |
1410 |
1411 theorem omega_reflection: |
1411 theorem omega_reflection: |
1412 "REFLECTS[\<lambda>x. omega(L,f(x)), |
1412 "REFLECTS[\<lambda>x. omega(L,f(x)), |
1413 \<lambda>i x. omega(**Lset(i),f(x))]" |
1413 \<lambda>i x. omega(##Lset(i),f(x))]" |
1414 apply (simp only: omega_def) |
1414 apply (simp only: omega_def) |
1415 apply (intro FOL_reflections limit_ordinal_reflection) |
1415 apply (intro FOL_reflections limit_ordinal_reflection) |
1416 done |
1416 done |
1417 |
1417 |
1418 |
1418 |