Read about our upcoming Code of Conduct on this issue

Commit 0871f311 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

Fixed some looping proofs (though why they were looping isn't clear)

parent 74dd55b9ef33
......@@ -65,14 +65,14 @@ begin
apply(case_tac [!] "compress_pos_interfaces (getPos ifces)")
apply(simp_all)
apply(drule_tac p_i="p_iiface p" in compress_pos_interfaces_Some)
apply(simp split:if_split_asm)
using iface_is_wildcard_def iface_subset match_iface_case_nowildcard apply fastforce
using match_ifaceAny apply blast
apply(simp split:if_split_asm add: match_ifaceAny)
unfolding iface_is_wildcard_def using iface_subset match_iface_case_nowildcard
apply (metis (no_types, lifting) Collect_mono_iff iface.collapse list.distinct(1) list.set_cases list.set_intros(1) set_ConsD)
apply force
apply(drule_tac p_i="p_oiface p" in compress_pos_interfaces_Some)
apply(simp split:if_split_asm)
using iface_is_wildcard_def iface_subset match_iface_case_nowildcard apply fastforce
using match_ifaceAny apply blast
apply(simp split:if_split_asm add: match_ifaceAny)
unfolding iface_is_wildcard_def iface_subset using match_iface_case_nowildcard
apply (metis iface.collapse list.distinct(1) list.inject list.set_cases list.set_intros(1) mem_Collect_eq subsetI)
by force
......
......@@ -27,7 +27,8 @@ subsection\<open>Sanity checking for an @{typ "'i ipassignment"}.\<close>
ipassmt (Iface ifce2) = None \<Longrightarrow>
ipassmt ifce = Some a \<Longrightarrow>
\<not> match_iface ifce ifce2"
unfolding ipassmt_sanity_nowildcards_def using iface_is_wildcard_def match_iface_case_nowildcard by fastforce
unfolding ipassmt_sanity_nowildcards_def
by (metis domIff iface.exhaust iface.sel option.distinct(1) iface_is_wildcard_def match_iface_case_nowildcard)
(* use this in all exported code*)
......
......@@ -731,8 +731,6 @@ text\<open>Examples\<close>
match_simplematcher_SrcDst_not
primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher]
primitive_matcher_generic.Iface_single_not[OF primitive_matcher_generic_common_matcher])
apply(intro impI, thin_tac _)
apply eval
apply eval
done
......@@ -762,8 +760,6 @@ text\<open>Examples\<close>
apply(simp add: bunch_of_lemmata_about_matches
primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher]
primitive_matcher_generic.Iface_single_not[OF primitive_matcher_generic_common_matcher])
apply(intro impI, thin_tac _)
apply eval
apply eval
done
......
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