Read about our upcoming Code of Conduct on this issue

Commit d3cf9d67 authored by paulson's avatar paulson
Browse files

merged

......@@ -2399,9 +2399,7 @@ proof (intro equalityI subsetI)
apply (case_tac "c \<in> set(rev vs)")
apply (subgoal_tac "distinct(rev vs)") apply (simp only: in_set_conv_decomp) apply (elim exE) apply simp
apply (case_tac "zs") apply simp
apply (subgoal_tac "ys = as") apply(drule last_rev) apply (simp)
apply (rule dist_at1) apply (rule dist_f12) apply (rule sym) apply simp
apply simp
apply (metis dist_at2 dist_f12 last_rev last_snoc list.inject vertices_face.simps)
apply (simp add:rev_swap)
apply (subgoal_tac "ys = as")
apply (clarsimp simp add: Edges_def is_sublist_def)
......@@ -4957,10 +4955,6 @@ lemma pre_subdivFace'_Some1:
\<Longrightarrow> f21 = fst (snd (splitFace g v u f [countVertices g ..< countVertices g + n]))
\<Longrightarrow> g' = snd (snd (splitFace g v u f [countVertices g ..< countVertices g + n]))
\<Longrightarrow> pre_subdivFace' g' f21 v' u 0 vol"
apply (subgoal_tac "pre_splitFace g v u f [countVertices g ..< countVertices g + n]")
apply (rule pre_subdivFace'_Some1') apply assumption+
apply (simp)
apply (rule pre_subdivFace'_preFaceDiv)
by auto
by (meson pre_subdivFace'_Some1' pre_subdivFace'_preFaceDiv)
end
......@@ -12,8 +12,7 @@ begin
text \<open>Preliminaries\<close>
lemma last_rev' [simp]: "last (rev xs) = hd xs" \<comment> \<open>TODO define \<open>last []\<close> as \<open>hd []\<close>?\<close>
by (cases xs) (simp add: last_def hd_def, simp)
declare hd_Nil_eq_last [simp]
lemma nat_LEAST_True: "(LEAST _ :: nat. True) = 0"
by (rule Least_equality) simp_all
......
......@@ -157,7 +157,7 @@ begin
proof(induction eth rule: iface_name_is_wildcard.induct)
qed(simp_all)
private lemma iface_name_is_wildcard_alt': "iface_name_is_wildcard eth \<longleftrightarrow> eth \<noteq> [] \<and> hd (rev eth) = CHR ''+''"
unfolding iface_name_is_wildcard_alt using hd_rev by fastforce
unfolding iface_name_is_wildcard_alt by (simp add: hd_rev)
private lemma iface_name_is_wildcard_fst: "iface_name_is_wildcard (i # is) \<Longrightarrow> is \<noteq> [] \<Longrightarrow> iface_name_is_wildcard is"
by(simp add: iface_name_is_wildcard_alt)
......@@ -645,11 +645,6 @@ begin
apply (blast dest: iface_conjunct_None)
by (blast dest: iface_conjunct_Some)
qed
declare match_iface.simps[simp del]
declare iface_name_is_wildcard.simps[simp del]
end
end
......@@ -232,7 +232,7 @@ proof-
let ?zs = "v # xs' @ x # (rev ys')"
have "last ?zs\<rightarrow>hd ?zs"
using undirected walk_first_edge walk_first_edge' ys'(1) ys(1) last_rev by fastforce
using undirected walk_first_edge walk_first_edge' ys'(1) ys(1) by (fastforce simp: last_rev)
moreover have "path ?zs" proof
have "walk (x # rev ys')" proof(cases)
assume "ys' = Nil" thus ?thesis using \<open>last ?zs\<rightarrow>hd ?zs\<close> edges_are_in_V(1) by auto
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment