equal
deleted
inserted
replaced
521 |
521 |
522 subsection{*Internalized formulas for basic concepts*} |
522 subsection{*Internalized formulas for basic concepts*} |
523 |
523 |
524 subsubsection{*The subset relation*} |
524 subsubsection{*The subset relation*} |
525 |
525 |
526 lemma lt_length_in_nat: |
|
527 "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat" |
|
528 apply (frule lt_nat_in_nat, typecheck) |
|
529 done |
|
530 |
|
531 constdefs subset_fm :: "[i,i]=>i" |
526 constdefs subset_fm :: "[i,i]=>i" |
532 "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))" |
527 "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))" |
533 |
528 |
534 lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula" |
529 lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula" |
535 by (simp add: subset_fm_def) |
530 by (simp add: subset_fm_def) |