equal
deleted
inserted
replaced
81 monos listall_def |
81 monos listall_def |
82 |
82 |
83 lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n" |
83 lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n" |
84 apply (induct m) |
84 apply (induct m) |
85 apply (case_tac n) |
85 apply (case_tac n) |
86 apply (case_tac [3] na) |
86 apply (case_tac [3] n) |
87 apply (simp only: nat.simps, rules?)+ |
87 apply (simp only: nat.simps, rules?)+ |
88 done |
88 done |
89 |
89 |
90 lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)" |
90 lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)" |
91 apply (induct m) |
91 apply (induct m) |
92 apply (case_tac n) |
92 apply (case_tac n) |
93 apply (case_tac [3] na) |
93 apply (case_tac [3] n) |
94 apply (simp del: simp_thms, rules?)+ |
94 apply (simp del: simp_thms, rules?)+ |
95 done |
95 done |
96 |
96 |
97 lemma App_NF_D: assumes NF: "Var n \<degree>\<degree> ts \<in> NF" |
97 lemma App_NF_D: assumes NF: "Var n \<degree>\<degree> ts \<in> NF" |
98 shows "listall (\<lambda>t. t \<in> NF) ts" using NF |
98 shows "listall (\<lambda>t. t \<in> NF) ts" using NF |