equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header {* Library for Bounded Natural Functors *} |
8 header {* Library for Bounded Natural Functors *} |
9 |
9 |
10 theory BNF_Library |
10 theory BNF_Library |
11 imports "../Ordinals_and_Cardinals/Cardinal_Arithmetic" "~~/src/HOL/Library/List_Prefix" |
11 imports "../Ordinals_and_Cardinals/Cardinal_Arithmetic" "~~/src/HOL/Library/Sublist" |
12 Equiv_Relations_More |
12 Equiv_Relations_More |
13 begin |
13 begin |
14 |
14 |
15 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)" |
15 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)" |
16 by blast |
16 by blast |
632 lemma meta_spec2: |
632 lemma meta_spec2: |
633 assumes "(\<And>x y. PROP P x y)" |
633 assumes "(\<And>x y. PROP P x y)" |
634 shows "PROP P x y" |
634 shows "PROP P x y" |
635 by (rule `(\<And>x y. PROP P x y)`) |
635 by (rule `(\<And>x y. PROP P x y)`) |
636 |
636 |
637 (*Extended List_Prefix*) |
637 (*Extended Sublist*) |
638 |
638 |
639 definition prefCl where |
639 definition prefCl where |
640 "prefCl Kl = (\<forall> kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)" |
640 "prefCl Kl = (\<forall> kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)" |
641 definition PrefCl where |
641 definition PrefCl where |
642 "PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> kl' \<le> kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))" |
642 "PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> kl' \<le> kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))" |