equal
deleted
inserted
replaced
1068 |
1068 |
1069 lemma fsubset_finsert: |
1069 lemma fsubset_finsert: |
1070 "(finsert x xs |\<subseteq>| ys) = (x |\<in>| ys \<and> xs |\<subseteq>| ys)" |
1070 "(finsert x xs |\<subseteq>| ys) = (x |\<in>| ys \<and> xs |\<subseteq>| ys)" |
1071 by (lifting sub_list_cons) |
1071 by (lifting sub_list_cons) |
1072 |
1072 |
1073 thm sub_list_def[simplified memb_def[symmetric], quot_lifted, no_vars] |
1073 lemma "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys" |
|
1074 by (lifting sub_list_def[simplified memb_def[symmetric]]) |
1074 |
1075 |
1075 lemma fsubset_fin: "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)" |
1076 lemma fsubset_fin: "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)" |
1076 by (rule meta_eq_to_obj_eq) |
1077 by (rule meta_eq_to_obj_eq) |
1077 (lifting sub_list_def[simplified memb_def[symmetric]]) |
1078 (lifting sub_list_def[simplified memb_def[symmetric]]) |
1078 |
1079 |