summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 11 Aug 2022 11:57:19 +0200 | |

changeset 75804 | dd04e81172a8 |

parent 75803 | 40e16228405e |

child 75805 | 3581dcee70db |

nlists is picked up automatically but conflicts with the RBT setup

src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Library/NList.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Thu Aug 11 10:11:21 2022 +0200 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Thu Aug 11 11:57:19 2022 +0200 @@ -29,6 +29,7 @@ Euclidean_Algorithm.Lcm "Gcd :: _ poly set \<Rightarrow> _" "Lcm :: _ poly set \<Rightarrow> _" + nlists ]] text \<open>

--- a/src/HOL/Library/NList.thy Thu Aug 11 10:11:21 2022 +0200 +++ b/src/HOL/Library/NList.thy Thu Aug 11 11:57:19 2022 +0200 @@ -14,11 +14,11 @@ lemma nlistsI: "\<lbrakk> size xs = n; set xs \<subseteq> A \<rbrakk> \<Longrightarrow> xs \<in> nlists n A" by (simp add: nlists_def) -lemma nlistsE_length [simp](*rm simp del*): "xs \<in> nlists n A \<Longrightarrow> size xs = n" +lemma nlistsE_length (*rm simp del*): "xs \<in> nlists n A \<Longrightarrow> size xs = n" by (simp add: nlists_def) lemma less_lengthI: "\<lbrakk> xs \<in> nlists n A; p < n \<rbrakk> \<Longrightarrow> p < size xs" -by (simp) +by (simp add: nlistsE_length) lemma nlistsE_set[simp](*rm simp del*): "xs \<in> nlists n A \<Longrightarrow> set xs \<subseteq> A" unfolding nlists_def by (simp) @@ -27,7 +27,7 @@ assumes "A \<subseteq> B" shows "nlists n A \<subseteq> nlists n B" proof fix xs assume "xs \<in> nlists n A" - then obtain size: "size xs = n" and inA: "set xs \<subseteq> A" by simp + then obtain size: "size xs = n" and inA: "set xs \<subseteq> A" by (simp add:nlistsE_length) with assms have "set xs \<subseteq> B" by simp with size show "xs \<in> nlists n B" by(clarsimp intro!: nlistsI) qed