Removed references to system generated names.
This commit is contained in:
parent
3b6e93906b
commit
93bb823f90
|
|
@ -143,7 +143,7 @@ lemma aux: "\<lbrakk>a \<in> c; a \<notin> d; c = d\<rbrakk> \<Longrightarrow> F
|
|||
by auto
|
||||
|
||||
lemma sets_distinct5: "(s::int) < g \<Longrightarrow> {(a::int, b::int). a = s} \<noteq> {(a::int, b::int). g < a}"
|
||||
apply (auto simp: sets_distinct3)
|
||||
apply (auto simp: sets_distinct3)[1]
|
||||
apply (subgoal_tac "(s,4) \<in> {(a::int,b::int). a = (s)}")
|
||||
apply (subgoal_tac "(s,4) \<notin> {(a::int,b::int). g < a}")
|
||||
apply (erule aux)
|
||||
|
|
|
|||
|
|
@ -351,7 +351,7 @@ fun qsort where
|
|||
|
||||
lemma qsort_permutes:
|
||||
"set (qsort xs l) = set xs"
|
||||
apply (induct xs l rule: qsort.induct)
|
||||
apply (induct "xs" "l" rule: qsort.induct)
|
||||
by (auto)
|
||||
|
||||
lemma set_qsort [simp]: "set (qsort xs l) = set xs"
|
||||
|
|
@ -451,7 +451,7 @@ fun rotatePolicy where
|
|||
| "rotatePolicy (a\<oplus>b) = (rotatePolicy b) \<oplus> (rotatePolicy a)"
|
||||
|
||||
lemma check: "rev (policy2list (rotatePolicy p)) = policy2list p"
|
||||
apply (induct p)
|
||||
apply (induct "p")
|
||||
by (simp_all)
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
(*****************************************************************************
|
||||
* Copyright (c) 2005-2010 ETH Zurich, Switzerland
|
||||
* 2008-2015 Achim D. Brucker, Germany
|
||||
* 2009-2016 Université Paris-Sud, France
|
||||
* 2015-2016 The University of Sheffield, UK
|
||||
* 2009-2017 Université Paris-Sud, France
|
||||
* 2015-2017 The University of Sheffield, UK
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
|
|
@ -56,31 +56,32 @@ lemma denyNMT: "deny_all \<noteq> \<emptyset>"
|
|||
|
||||
lemma wellformed_policy1_charn[rule_format]:
|
||||
"wellformed_policy1 p \<longrightarrow> DenyAll \<in> set p \<longrightarrow> (\<exists> p'. p = DenyAll # p' \<and> DenyAll \<notin> set p')"
|
||||
by(induct p,simp_all)
|
||||
by(induct "p",simp_all)
|
||||
|
||||
lemma singleCombinatorsConc: "singleCombinators (x#xs) \<Longrightarrow> singleCombinators xs"
|
||||
by (case_tac x,simp_all)
|
||||
|
||||
lemma aux0_0: "singleCombinators x \<Longrightarrow> \<not> (\<exists> a b. (a\<oplus>b) \<in> set x)"
|
||||
apply (induct x, simp_all)
|
||||
apply (rule allI)+
|
||||
by (case_tac a,simp_all)
|
||||
|
||||
apply (induct "x", simp_all)
|
||||
subgoal for a b
|
||||
by (case_tac "a",simp_all)
|
||||
done
|
||||
|
||||
lemma aux0_4: "(a \<in> set x \<or> a \<in> set y) = (a \<in> set (x@y))"
|
||||
by auto
|
||||
|
||||
lemma aux0_1: "\<lbrakk>singleCombinators xs; singleCombinators [x]\<rbrakk> \<Longrightarrow>
|
||||
singleCombinators (x#xs)"
|
||||
by (case_tac x,simp_all)
|
||||
by (case_tac "x",simp_all)
|
||||
|
||||
lemma aux0_6: "\<lbrakk>singleCombinators xs; \<not> (\<exists> a b. x = a \<oplus> b)\<rbrakk> \<Longrightarrow>
|
||||
singleCombinators(x#xs)"
|
||||
apply (rule aux0_1,simp_all)
|
||||
apply (case_tac x,simp_all)
|
||||
apply (case_tac "x",simp_all)
|
||||
by auto
|
||||
|
||||
lemma aux0_5: " \<not> (\<exists> a b. (a\<oplus>b) \<in> set x) \<Longrightarrow> singleCombinators x"
|
||||
apply (induct x)
|
||||
apply (induct "x")
|
||||
apply simp_all
|
||||
by (metis aux0_6)
|
||||
|
||||
|
|
@ -113,18 +114,24 @@ lemma aux10[rule_format]: "a \<in> set (net_list p) \<longrightarrow> a \<in> se
|
|||
|
||||
lemma srcInNetListaux[simp]:
|
||||
"\<lbrakk>x \<in> set p; singleCombinators[x]; x \<noteq> DenyAll\<rbrakk> \<Longrightarrow> srcNet x \<in> set (net_list_aux p)"
|
||||
apply (induct p)
|
||||
apply (induct "p")
|
||||
apply simp_all
|
||||
apply (case_tac "x = a", simp_all)
|
||||
apply (case_tac a, simp_all)+
|
||||
subgoal for a p
|
||||
apply (case_tac "x = a", simp_all)
|
||||
apply (case_tac a, simp_all)
|
||||
apply (case_tac a, simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma destInNetListaux[simp]:
|
||||
"\<lbrakk>x \<in> set p; singleCombinators[x]; x \<noteq> DenyAll\<rbrakk> \<Longrightarrow> destNet x \<in> set (net_list_aux p)"
|
||||
apply (induct p)
|
||||
apply simp_all
|
||||
apply (case_tac "x = a", simp_all)
|
||||
apply (case_tac a, simp_all)+
|
||||
subgoal for a p
|
||||
apply (case_tac "x = a", simp_all)
|
||||
apply (case_tac "a", simp_all)
|
||||
apply (case_tac "a", simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma tND1: "\<lbrakk>allNetsDistinct p; x \<in> set p; y \<in> set p; a = srcNet x;
|
||||
|
|
@ -198,11 +205,13 @@ lemma aNDSubsetaux[rule_format]: "singleCombinators a \<longrightarrow> set a \
|
|||
apply simp_all
|
||||
apply clarify
|
||||
apply (drule mp, erule singleCombinatorsConc)
|
||||
apply (case_tac "a1")
|
||||
apply (simp_all add: contra_subsetD)
|
||||
apply (metis contra_subsetD)
|
||||
apply (metis ND0aux1 ND0aux2 contra_subsetD)
|
||||
apply (metis ND0aux3 ND0aux4 contra_subsetD)
|
||||
subgoal for a a' x
|
||||
apply (case_tac "a")
|
||||
apply (simp_all add: contra_subsetD)
|
||||
apply (metis contra_subsetD)
|
||||
apply (metis ND0aux1 ND0aux2 contra_subsetD)
|
||||
apply (metis ND0aux3 ND0aux4 contra_subsetD)
|
||||
done
|
||||
done
|
||||
|
||||
lemma aNDSetsEqaux[rule_format]: "singleCombinators a \<longrightarrow> singleCombinators b \<longrightarrow>
|
||||
|
|
@ -217,16 +226,20 @@ lemma aNDSubset: "\<lbrakk>singleCombinators a;set a \<subseteq> set b; allNetsD
|
|||
apply (simp add: allNetsDistinct_def)
|
||||
apply (rule allI)+
|
||||
apply (rule impI)+
|
||||
apply (drule_tac x = "aa" in spec, drule_tac x = "ba" in spec)
|
||||
using aNDSubsetaux by blast
|
||||
subgoal for x y
|
||||
apply (drule_tac x = "x" in spec, drule_tac x = "y" in spec)
|
||||
using aNDSubsetaux by blast
|
||||
done
|
||||
|
||||
lemma aNDSetsEq: "\<lbrakk>singleCombinators a; singleCombinators b; set a = set b;
|
||||
allNetsDistinct b\<rbrakk> \<Longrightarrow> allNetsDistinct a"
|
||||
apply (simp add: allNetsDistinct_def)
|
||||
apply (rule allI)+
|
||||
apply (rule impI)+
|
||||
apply (drule_tac x = "aa" in spec, drule_tac x = "ba" in spec)
|
||||
using aNDSetsEqaux by auto
|
||||
subgoal for x y
|
||||
apply (drule_tac x = "x" in spec, drule_tac x = "y" in spec)
|
||||
using aNDSetsEqaux by auto
|
||||
done
|
||||
|
||||
lemma SCConca: "\<lbrakk>singleCombinators p; singleCombinators [a]\<rbrakk> \<Longrightarrow>
|
||||
singleCombinators (a#p)"
|
||||
|
|
@ -285,7 +298,7 @@ lemma waux3[rule_format]: "\<lbrakk>x \<noteq> a; x \<notin> set p\<rbrakk> \<L
|
|||
by (metis aux79)
|
||||
|
||||
lemma wellformed1_sorted_aux[rule_format]: "wellformed_policy1 (x#p) \<Longrightarrow>
|
||||
wellformed_policy1 (insort x p l)" try
|
||||
wellformed_policy1 (insort x p l)"
|
||||
by (metis NormalisationGenericProofs.set_insort list.set(2) saux waux2 wellformed_eq
|
||||
wellformed_policy1_strong.simps(2))
|
||||
|
||||
|
|
@ -302,8 +315,11 @@ next
|
|||
|
||||
lemma SR1Subset: "set (removeShadowRules1 p) \<subseteq> set p"
|
||||
apply (induct_tac p, simp_all)
|
||||
apply (case_tac a, simp_all)
|
||||
by auto
|
||||
subgoal for x xs
|
||||
apply (case_tac "x", simp_all)
|
||||
apply(auto)
|
||||
done
|
||||
done
|
||||
|
||||
lemma SCSubset[rule_format]: " singleCombinators b \<longrightarrow> set a \<subseteq> set b \<longrightarrow>
|
||||
singleCombinators a"
|
||||
|
|
@ -324,8 +340,11 @@ lemma SC_RS1[rule_format,simp]: "singleCombinators p \<longrightarrow> allNetsDi
|
|||
using ANDConc singleCombinatorsConc by blast
|
||||
|
||||
lemma RS2Set[rule_format]: "set (removeShadowRules2 p) \<subseteq> set p"
|
||||
by (induct p, simp_all) (case_tac a, auto)
|
||||
|
||||
apply(induct p, simp_all)
|
||||
subgoal for a as
|
||||
apply(case_tac a)
|
||||
by(auto)
|
||||
done
|
||||
|
||||
lemma WP1: "a \<notin> set list \<Longrightarrow> a \<notin> set (removeShadowRules2 list)"
|
||||
using RS2Set [of list] by blast
|
||||
|
|
@ -338,7 +357,10 @@ lemma lCdom2: "(list2FWpolicy (a @ (b @ c))) = (list2FWpolicy ((a@b)@c))"
|
|||
by auto
|
||||
|
||||
lemma SCConcEnd: "singleCombinators (xs @ [xa]) \<Longrightarrow> singleCombinators xs"
|
||||
by (induct "xs", simp_all, case_tac a, simp_all)
|
||||
apply (induct "xs", simp_all)
|
||||
subgoal for a as
|
||||
by (case_tac "a" , simp_all)
|
||||
done
|
||||
|
||||
lemma list2FWpolicyconc[rule_format]: "a \<noteq> [] \<longrightarrow>
|
||||
(list2FWpolicy (xa # a)) = (xa) \<oplus> (list2FWpolicy a)"
|
||||
|
|
@ -358,7 +380,10 @@ lemma foo2: "a \<notin> set ps \<Longrightarrow>
|
|||
|
||||
|
||||
lemma SCnotConc[rule_format,simp]: "a\<oplus>b \<in> set p \<longrightarrow> singleCombinators p \<longrightarrow>False"
|
||||
by (induct p, simp_all, case_tac aa, simp_all)
|
||||
apply (induct p, simp_all)
|
||||
subgoal for p ps
|
||||
by(case_tac p, simp_all)
|
||||
done
|
||||
|
||||
lemma auxx8: "removeShadowRules1_alternative_rev [x] = [x]"
|
||||
by (case_tac "x", simp_all)
|
||||
|
|
@ -384,10 +409,14 @@ lemma RS1_DA[simp]: "removeShadowRules1 (xs @ [DenyAll]) = [DenyAll]"
|
|||
lemma rSR1_eq: "removeShadowRules1_alternative = removeShadowRules1"
|
||||
apply (rule ext)
|
||||
apply (simp add: removeShadowRules1_alternative_def)
|
||||
apply (rule_tac xs = x in rev_induct)
|
||||
apply simp_all
|
||||
apply (case_tac "xa = DenyAll", simp_all)
|
||||
apply (metis RS1End aux114 rev.simps(2))
|
||||
subgoal for x
|
||||
apply (rule_tac xs = x in rev_induct)
|
||||
apply simp_all
|
||||
subgoal for x xs
|
||||
apply (case_tac "x = DenyAll", simp_all)
|
||||
apply (metis RS1End aux114 rev.simps(2))
|
||||
done
|
||||
done
|
||||
done
|
||||
|
||||
lemma domInterMT[rule_format]: "\<lbrakk>dom a \<inter> dom b = {}; x \<in> dom a\<rbrakk> \<Longrightarrow> x \<notin> dom b"
|
||||
|
|
@ -520,8 +549,10 @@ lemma distinct_RS2[rule_format,simp]: "distinct p \<longrightarrow>
|
|||
apply (induct p)
|
||||
apply simp_all
|
||||
apply clarify
|
||||
apply (case_tac "a")
|
||||
by auto
|
||||
subgoal for a p
|
||||
apply (case_tac "a")
|
||||
by auto
|
||||
done
|
||||
|
||||
lemma setPaireq: " {x, y} = {a, b} \<Longrightarrow> x = a \<and> y = b \<or> x = b \<and> y = a"
|
||||
by (metis doubleton_eq_iff)
|
||||
|
|
@ -592,7 +623,9 @@ lemma sortedConcStart[rule_format]:
|
|||
apply simp
|
||||
apply (rule_tac y = "aa" in order_trans)
|
||||
apply simp_all
|
||||
apply (case_tac ab, simp_all)
|
||||
subgoal for p ps
|
||||
apply (case_tac "p", simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma singleCombinatorsStart[simp]: "singleCombinators (x#xs) \<Longrightarrow>
|
||||
|
|
@ -802,7 +835,12 @@ lemma distinct_sortQ[rule_format]:
|
|||
lemma singleCombinatorsAppend[rule_format]:
|
||||
"singleCombinators (xs) \<longrightarrow> singleCombinators (ys) \<longrightarrow> singleCombinators (xs @ ys)"
|
||||
apply (induct xs, auto)
|
||||
apply (case_tac a,simp_all)+
|
||||
subgoal for a as
|
||||
apply (case_tac a,simp_all)
|
||||
done
|
||||
subgoal for a as
|
||||
apply (case_tac a,simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma sorted_append1[rule_format]:
|
||||
|
|
@ -909,10 +947,12 @@ lemma RS1n_assoc:
|
|||
lemma RS1n_nMT[rule_format,simp]: "p \<noteq> []\<longrightarrow> removeShadowRules1_alternative p \<noteq> []"
|
||||
apply (simp add: removeShadowRules1_alternative_def)
|
||||
apply (rule_tac xs = p in rev_induct, simp_all)
|
||||
apply (case_tac "xs = []", simp_all)
|
||||
apply (case_tac x, simp_all)
|
||||
apply (rule_tac xs = "xs" in rev_induct, simp_all)
|
||||
apply (case_tac x, simp_all)+
|
||||
subgoal for x xs
|
||||
apply (case_tac "xs = []", simp_all)
|
||||
apply (case_tac x, simp_all)
|
||||
apply (rule_tac xs = "xs" in rev_induct, simp_all)
|
||||
apply (case_tac x, simp_all)+
|
||||
done
|
||||
done
|
||||
|
||||
lemma RS1N_DA[simp]: "removeShadowRules1_alternative (a@[DenyAll]) = [DenyAll]"
|
||||
|
|
@ -964,8 +1004,10 @@ lemma wp1n_RS2[rule_format]:
|
|||
|
||||
lemma RS2_NMT[rule_format]: "p \<noteq> [] \<longrightarrow> removeShadowRules2 p \<noteq> []"
|
||||
apply (induct p, simp_all)
|
||||
apply (case_tac "p \<noteq> []", simp_all)
|
||||
apply (case_tac "a", simp_all)+
|
||||
subgoal for a p
|
||||
apply (case_tac "p \<noteq> []", simp_all)
|
||||
apply (case_tac "a", simp_all)+
|
||||
done
|
||||
done
|
||||
|
||||
lemma wp1_alternative_not_mt[simp]: "wellformed_policy1_strong p \<Longrightarrow> p \<noteq> []"
|
||||
|
|
@ -976,7 +1018,11 @@ lemma AIL1[rule_format,simp]: "all_in_list p l \<longrightarrow>
|
|||
by (induct_tac p, simp_all)
|
||||
|
||||
lemma wp1ID: "wellformed_policy1_strong (insertDeny (removeShadowRules1 p))"
|
||||
by (induct p, simp_all, case_tac a, simp_all)
|
||||
apply (induct p, simp_all)
|
||||
subgoal for a p
|
||||
apply (case_tac a, simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma dRD[simp]: "distinct (remdups p)"
|
||||
by simp
|
||||
|
|
@ -987,19 +1033,24 @@ lemma AILrd[rule_format,simp]: "all_in_list p l \<longrightarrow> all_in_list (r
|
|||
lemma AILiD[rule_format,simp]: "all_in_list p l \<longrightarrow> all_in_list (insertDeny p) l"
|
||||
apply (induct p, simp_all)
|
||||
apply (rule impI, simp)
|
||||
apply (case_tac "a", simp_all)
|
||||
subgoal for a p
|
||||
apply (case_tac a, simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma SCrd[rule_format,simp]:"singleCombinators p\<longrightarrow> singleCombinators(remdups p)"
|
||||
apply (induct p, simp_all)
|
||||
apply (case_tac a)
|
||||
apply simp_all
|
||||
subgoal for a p
|
||||
apply (case_tac a, simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma SCRiD[rule_format,simp]: "singleCombinators p \<longrightarrow>
|
||||
singleCombinators(insertDeny p)"
|
||||
apply (induct p, simp_all)
|
||||
apply (case_tac "a", simp_all)
|
||||
subgoal for a p
|
||||
apply (case_tac a, simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma WP1rd[rule_format,simp]:
|
||||
|
|
@ -1018,7 +1069,9 @@ lemma ANDiD[rule_format,simp]:
|
|||
apply (induct p, simp_all)
|
||||
apply (simp add: allNetsDistinct_def)
|
||||
apply (auto intro: ANDConc)
|
||||
apply (case_tac "a",simp_all add: allNetsDistinct_def)
|
||||
subgoal for a p
|
||||
apply (case_tac "a",simp_all add: allNetsDistinct_def)
|
||||
done
|
||||
done
|
||||
|
||||
lemma mr_iD[rule_format]:
|
||||
|
|
@ -1030,14 +1083,22 @@ lemma WP1iD[rule_format,simp]: "wellformed_policy1_strong p \<longrightarrow>
|
|||
by (induct p, simp_all)
|
||||
|
||||
lemma DAiniD: "DenyAll \<in> set (insertDeny p)"
|
||||
by (induct p, simp_all, case_tac a, simp_all)
|
||||
apply (induct p, simp_all)
|
||||
subgoal for a p
|
||||
apply(case_tac a, simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma p2lNmt: "policy2list p \<noteq> []"
|
||||
by (rule policy2list.induct, simp_all)
|
||||
|
||||
lemma AIL2[rule_format,simp]:
|
||||
"all_in_list p l \<longrightarrow> all_in_list (removeShadowRules2 p) l"
|
||||
by (induct_tac p, simp_all, case_tac a, simp_all)
|
||||
apply (induct_tac p, simp_all)
|
||||
subgoal for a p
|
||||
apply(case_tac a, simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma SCConc: "singleCombinators x \<Longrightarrow> singleCombinators y \<Longrightarrow> singleCombinators (x@y)"
|
||||
apply (rule aux0_5)
|
||||
|
|
@ -1095,15 +1156,20 @@ lemma sortnMT: "p \<noteq> [] \<Longrightarrow> sort p l \<noteq> []"
|
|||
|
||||
lemma idNMT[rule_format]: "p \<noteq> [] \<longrightarrow> insertDenies p \<noteq> []"
|
||||
apply (induct p, simp_all)
|
||||
apply (case_tac a, simp_all)
|
||||
subgoal for a p
|
||||
apply(case_tac a, simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma OTNoTN[rule_format]: " OnlyTwoNets p \<longrightarrow> x \<noteq> DenyAll \<longrightarrow> x \<in> set p \<longrightarrow> onlyTwoNets x"
|
||||
apply (induct p, simp_all, rename_tac a p)
|
||||
apply (intro impI conjI, simp)
|
||||
apply (case_tac a, simp_all)
|
||||
apply (drule mp, simp_all)
|
||||
apply (case_tac a, simp_all)
|
||||
subgoal for a p
|
||||
apply(case_tac a, simp_all)
|
||||
done
|
||||
subgoal for a p
|
||||
apply(case_tac a, simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma first_isIn[rule_format]: "\<not> member DenyAll x \<longrightarrow> (first_srcNet x,first_destNet x) \<in> sdnets x"
|
||||
|
|
@ -1171,7 +1237,11 @@ lemma disjSD2aux:
|
|||
using first_isIn by blast
|
||||
|
||||
lemma noDA1eq[rule_format]: "noDenyAll p \<longrightarrow> noDenyAll1 p"
|
||||
by (induct p, simp,rename_tac a p, case_tac a, simp_all)
|
||||
apply (induct p, simp,rename_tac a p)
|
||||
subgoal for a p
|
||||
apply(case_tac a, simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma noDA1C[rule_format]: "noDenyAll1 (a#p) \<longrightarrow> noDenyAll1 p"
|
||||
by (case_tac a, simp_all,rule impI, rule noDA1eq, simp)+
|
||||
|
|
@ -1186,21 +1256,31 @@ lemma disjSD_2IDa:
|
|||
by(simp add:disjSD2aux)
|
||||
|
||||
lemma noDAID[rule_format]: "noDenyAll p \<longrightarrow> noDenyAll (insertDenies p)"
|
||||
by (induct p, simp_all,case_tac a, simp_all)
|
||||
apply (induct p, simp_all)
|
||||
subgoal for a p
|
||||
apply(case_tac a, simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma isInIDo[rule_format]:
|
||||
"noDenyAll p \<longrightarrow> s \<in> set (insertDenies p) \<longrightarrow>
|
||||
(\<exists>! a. s = (DenyAllFromTo (first_srcNet a) (first_destNet a)) \<oplus>
|
||||
(DenyAllFromTo (first_destNet a) (first_srcNet a)) \<oplus> a \<and> a \<in> set p)"
|
||||
apply (induct p, simp, rename_tac a p)
|
||||
apply (case_tac "a = DenyAll", simp)
|
||||
apply (case_tac a, auto)
|
||||
subgoal for a p
|
||||
apply (case_tac "a = DenyAll", simp)
|
||||
apply (case_tac a, auto)
|
||||
done
|
||||
done
|
||||
|
||||
lemma id_aux1[rule_format]: "DenyAllFromTo (first_srcNet s) (first_destNet s) \<oplus>
|
||||
DenyAllFromTo (first_destNet s) (first_srcNet s) \<oplus> s\<in> set (insertDenies p)
|
||||
\<longrightarrow> s \<in> set p"
|
||||
by (induct p, simp_all, rename_tac a p, case_tac a, simp_all)
|
||||
apply (induct p, simp_all, rename_tac a p)
|
||||
subgoal for a p
|
||||
apply(case_tac a, simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma id_aux2:
|
||||
"noDenyAll p \<Longrightarrow>
|
||||
|
|
@ -1216,7 +1296,7 @@ lemma id_aux4[rule_format]:
|
|||
"noDenyAll p \<Longrightarrow> \<forall>s. s \<in> set p \<longrightarrow> disjSD_2 a s \<Longrightarrow>
|
||||
s \<in> set (insertDenies p) \<Longrightarrow> \<not> member DenyAll a \<Longrightarrow>
|
||||
disjSD_2 a s"
|
||||
apply (subgoal_tac " \<exists>a. s =
|
||||
apply (subgoal_tac "\<exists>a. s =
|
||||
DenyAllFromTo (first_srcNet a) (first_destNet a) \<oplus>
|
||||
DenyAllFromTo (first_destNet a) (first_srcNet a) \<oplus> a \<and>
|
||||
a \<in> set p")
|
||||
|
|
@ -1228,10 +1308,12 @@ lemma sepNetsID[rule_format]:
|
|||
apply (induct p, simp)
|
||||
apply (rename_tac a p, auto)
|
||||
using noDA1C apply blast
|
||||
apply (case_tac "a = DenyAll", auto)
|
||||
apply (simp add: disjSD_2_def)
|
||||
apply (case_tac a,auto)
|
||||
apply (rule disjSD_2IDa, simp_all, rule id_aux4, simp_all, metis noDA noDAID)+
|
||||
subgoal for a p
|
||||
apply (case_tac "a = DenyAll", auto)
|
||||
apply (simp add: disjSD_2_def)
|
||||
apply (case_tac a,auto)
|
||||
apply (rule disjSD_2IDa, simp_all, rule id_aux4, simp_all, metis noDA noDAID)+
|
||||
done
|
||||
done
|
||||
|
||||
lemma aNDDA[rule_format]: "allNetsDistinct p \<longrightarrow> allNetsDistinct(DenyAll#p)"
|
||||
|
|
@ -1444,8 +1526,10 @@ lemma isInAlternativeListb:
|
|||
lemma ANDSepaux: "allNetsDistinct (x # y # z) \<Longrightarrow> allNetsDistinct (x \<oplus> y # z)"
|
||||
apply (simp add: allNetsDistinct_def)
|
||||
apply (intro allI impI, rename_tac a b)
|
||||
apply (drule_tac x = a in spec, drule_tac x = b in spec)
|
||||
by (meson isInAlternativeList)
|
||||
subgoal for a b
|
||||
apply (drule_tac x = a in spec, drule_tac x = b in spec)
|
||||
by (meson isInAlternativeList)
|
||||
done
|
||||
|
||||
lemma netlistalternativeSeparateaux:
|
||||
"net_list_aux [y] @ net_list_aux z = net_list_aux (y # z)"
|
||||
|
|
@ -1474,24 +1558,28 @@ lemma wp1_alternativesep[rule_format]:
|
|||
|
||||
lemma noDAsort[rule_format]: "noDenyAll1 p \<longrightarrow> noDenyAll1 (sort p l)"
|
||||
apply (case_tac "p",simp_all)
|
||||
apply (case_tac "a = DenyAll", auto)
|
||||
using NormalisationGenericProofs.set_sort nDAeqSet apply blast
|
||||
proof -
|
||||
fix a::"('a,'b)Combinators" fix list
|
||||
have * : "a \<noteq> DenyAll \<Longrightarrow> noDenyAll1 (a # list) \<Longrightarrow> noDenyAll (a#list)" by (case_tac a, simp_all)
|
||||
show "a \<noteq> DenyAll \<Longrightarrow> noDenyAll1 (a # list) \<Longrightarrow> noDenyAll1 (insort a (sort list l) l)"
|
||||
apply(cases "insort a (sort list l) l", simp_all)
|
||||
by (metis "*" NormalisationGenericProofs.set_insort NormalisationGenericProofs.set_sort
|
||||
list.simps(15) nDAeqSet noDA1eq)
|
||||
qed
|
||||
subgoal for a as
|
||||
apply (case_tac "a = DenyAll", auto)
|
||||
using NormalisationGenericProofs.set_sort nDAeqSet apply blast
|
||||
proof -
|
||||
fix a::"('a,'b)Combinators" fix list
|
||||
have * : "a \<noteq> DenyAll \<Longrightarrow> noDenyAll1 (a # list) \<Longrightarrow> noDenyAll (a#list)" by (case_tac a, simp_all)
|
||||
show "a \<noteq> DenyAll \<Longrightarrow> noDenyAll1 (a # list) \<Longrightarrow> noDenyAll1 (insort a (sort list l) l)"
|
||||
apply(cases "insort a (sort list l) l", simp_all)
|
||||
by (metis "*" NormalisationGenericProofs.set_insort NormalisationGenericProofs.set_sort
|
||||
list.simps(15) nDAeqSet noDA1eq)
|
||||
qed
|
||||
done
|
||||
|
||||
lemma OTNSC[rule_format]: "singleCombinators p \<longrightarrow> OnlyTwoNets p"
|
||||
apply (induct p,simp_all)
|
||||
apply (rename_tac a p)
|
||||
apply (rule impI,drule mp)
|
||||
apply (erule singleCombinatorsConc)
|
||||
apply (case_tac a, simp_all)
|
||||
apply (simp add: onlyTwoNets_def)+
|
||||
subgoal for a b
|
||||
apply (case_tac a, simp_all)
|
||||
apply (simp add: onlyTwoNets_def)+
|
||||
done
|
||||
done
|
||||
|
||||
lemma fMTaux: "\<not> member DenyAll x \<Longrightarrow> first_bothNet x \<noteq> {}"
|
||||
|
|
@ -1711,10 +1799,12 @@ next
|
|||
apply (rule_tac y = "position (first_bothNet aa) l" in basic_trans_rules(22))
|
||||
apply (simp_all split: if_splits)
|
||||
apply (case_tac aa, simp_all)
|
||||
apply (case_tac "a = x21 \<and> b = x22", simp_all)
|
||||
apply (case_tac "a = x21", simp_all)
|
||||
apply (simp add: order.not_eq_order_implies_strict posaux6)
|
||||
apply (simp add: order.not_eq_order_implies_strict posaux6)
|
||||
subgoal for x x'
|
||||
apply (case_tac "a = x \<and> b = x'", simp_all)
|
||||
apply (case_tac "a = x", simp_all)
|
||||
apply (simp add: order.not_eq_order_implies_strict posaux6)
|
||||
apply (simp add: order.not_eq_order_implies_strict posaux6)
|
||||
done
|
||||
apply (simp add: order.not_eq_order_implies_strict posaux6)
|
||||
apply (rule basic_trans_rules(18))
|
||||
apply (rule_tac a = "DenyAllFromTo a b" and b = aa in posaux4, simp_all)
|
||||
|
|
@ -2143,7 +2233,7 @@ lemma NCisSD2[rule_format]:
|
|||
lemma separatedNC[rule_format]:
|
||||
"OnlyTwoNets p \<longrightarrow> NetsCollected2 p \<longrightarrow> NetsCollected p \<longrightarrow> noDenyAll1 p \<longrightarrow>
|
||||
allNetsDistinct p \<longrightarrow> separated p"
|
||||
proof (induct p, simp_all, case_tac "a = DenyAll", simp_all, goal_cases)
|
||||
proof (induct p, simp_all, rename_tac a b, case_tac "a = DenyAll", simp_all, goal_cases)
|
||||
fix a fix p::"('a set set, 'b) Combinators list"
|
||||
show "OnlyTwoNets p \<longrightarrow> NetsCollected2 p \<longrightarrow> NetsCollected p \<longrightarrow> noDenyAll1 p \<longrightarrow>
|
||||
allNetsDistinct p \<longrightarrow> separated p \<Longrightarrow> a \<noteq> DenyAll \<Longrightarrow> OnlyTwoNets (a # p) \<longrightarrow>
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
(*****************************************************************************
|
||||
* Copyright (c) 2005-2010 ETH Zurich, Switzerland
|
||||
* 2008-2015 Achim D. Brucker, Germany
|
||||
* 2009-2016 Université Paris-Sud, France
|
||||
* 2015-2016 The University of Sheffield, UK
|
||||
* 2009-2017 Université Paris-Sud, France
|
||||
* 2015-2017 The University of Sheffield, UK
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
|
|
@ -55,8 +55,12 @@ lemma aux26[simp]:
|
|||
|
||||
lemma wp2_aux[rule_format]:
|
||||
"wellformed_policy2Pr (xs @ [x]) \<longrightarrow> wellformed_policy2Pr xs"
|
||||
by (induct xs, simp_all) (case_tac "a", simp_all)
|
||||
|
||||
apply(induct xs, simp_all)
|
||||
subgoal for a as
|
||||
apply(case_tac "a", simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma Cdom2: "x \<in> dom(Cp b) \<Longrightarrow> Cp (a \<oplus> b) x = (Cp b) x"
|
||||
by (auto simp: Cp.simps)
|
||||
|
||||
|
|
@ -123,7 +127,7 @@ lemma bar3:
|
|||
|
||||
lemma CeqEnd[rule_format,simp]:
|
||||
"a \<noteq> [] \<longrightarrow> x \<in> dom (Cp(list2FWpolicy a)) \<longrightarrow> Cp(list2FWpolicy(b@a)) x = (Cp(list2FWpolicy a)) x"
|
||||
proof (induct rule: rev_induct)print_cases
|
||||
proof (induct rule: rev_induct)
|
||||
case Nil show ?case by simp
|
||||
next
|
||||
case (snoc xa xs) show ?case
|
||||
|
|
@ -154,7 +158,7 @@ lemma C_eq_if_mr_eq2:
|
|||
|
||||
lemma nMRtoNone[rule_format]:
|
||||
"p \<noteq> [] \<longrightarrow> applied_rule_rev Cp x p = None \<longrightarrow> Cp (list2FWpolicy p) x = None"
|
||||
proof (induct rule: rev_induct) print_cases
|
||||
proof (induct rule: rev_induct)
|
||||
case Nil show ?case by simp
|
||||
next
|
||||
case (snoc xa xs) show ?case
|
||||
|
|
@ -228,7 +232,11 @@ lemma mrConcEnd[rule_format]:
|
|||
|
||||
|
||||
lemma wp3tl[rule_format]: "wellformed_policy3Pr p \<longrightarrow> wellformed_policy3Pr (tl p)"
|
||||
by (induct p, simp_all, case_tac a, simp_all)
|
||||
apply (induct p, simp_all)
|
||||
subgoal for a as
|
||||
apply(case_tac a, simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma wp3Conc[rule_format]: "wellformed_policy3Pr (a#p) \<longrightarrow> wellformed_policy3Pr p"
|
||||
by (induct p, simp_all, case_tac a, simp_all)
|
||||
|
|
@ -259,7 +267,11 @@ lemma mr_not_Conc: "singleCombinators p \<Longrightarrow> applied_rule_rev Cp x
|
|||
|
||||
|
||||
lemma foo25[rule_format]: "wellformed_policy3Pr (p@[x]) \<longrightarrow> wellformed_policy3Pr p"
|
||||
by (induct p, simp_all, case_tac a, simp_all)
|
||||
apply(induct p, simp_all)
|
||||
subgoal for a p
|
||||
apply(case_tac a, simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma mr_in_dom[rule_format]: "applied_rule_rev Cp x p = Some a \<longrightarrow> x \<in> dom (Cp a)"
|
||||
by (rule_tac xs = p in rev_induct) (auto simp: applied_rule_rev_def)
|
||||
|
|
@ -268,7 +280,7 @@ lemma mr_in_dom[rule_format]: "applied_rule_rev Cp x p = Some a \<longrightarrow
|
|||
lemma wp3EndMT[rule_format]:
|
||||
"wellformed_policy3Pr (p@[xs]) \<longrightarrow> AllowPortFromTo a b po \<in> set p \<longrightarrow>
|
||||
dom (Cp (AllowPortFromTo a b po)) \<inter> dom (Cp xs) = {}"
|
||||
apply (induct p,simp_all)
|
||||
apply (induct p, simp_all)
|
||||
by (metis NormalisationIPPProofs.wp3Conc aux0_4 inf_commute list.set_intros(1)
|
||||
wellformed_policy3Pr.simps(2))
|
||||
|
||||
|
|
@ -324,7 +336,6 @@ lemma DomInterAllowsMT_Ports:
|
|||
apply (simp add: twoNetsDistinct_def netsDistinct_def PLemmas)
|
||||
by (auto simp: prod_eqI)
|
||||
|
||||
|
||||
lemma wellformed_policy3_charn[rule_format]:
|
||||
"singleCombinators p \<longrightarrow> distinct p \<longrightarrow> allNetsDistinct p \<longrightarrow>
|
||||
wellformed_policy1 p \<longrightarrow> wellformed_policy2Pr p \<longrightarrow> wellformed_policy3Pr p"
|
||||
|
|
@ -334,10 +345,12 @@ next
|
|||
case (Cons a p) then show ?case
|
||||
apply (auto intro: singleCombinatorsConc ANDConc waux2 wp2Conc)
|
||||
apply (case_tac a,simp_all, clarify)
|
||||
apply (case_tac r,simp_all)
|
||||
apply (metis Int_commute)
|
||||
apply (metis DomInterAllowsMT aux7aa DomInterAllowsMT_Ports)
|
||||
apply (metis aux0_0 )
|
||||
subgoal for a b c d r
|
||||
apply (case_tac r,simp_all)
|
||||
apply (metis Int_commute)
|
||||
apply (metis DomInterAllowsMT aux7aa DomInterAllowsMT_Ports)
|
||||
apply (metis aux0_0 )
|
||||
done
|
||||
done
|
||||
qed
|
||||
|
||||
|
|
@ -417,13 +430,15 @@ next
|
|||
using Cons apply simp
|
||||
apply (intro impI conjI allI, rename_tac "aa" "b")
|
||||
apply (rule aux26)
|
||||
apply (rule_tac x = "AllowPortFromTo c d e" and y = "DenyAllFromTo aa b" in tND,
|
||||
assumption,simp_all)
|
||||
apply (subgoal_tac "smaller (AllowPortFromTo c d e) (DenyAllFromTo aa b) l")
|
||||
apply (simp split: if_splits)
|
||||
apply metis
|
||||
apply (erule sorted_is_smaller, simp_all)
|
||||
apply (metis bothNet.simps(2) in_list.simps(2) in_set_in_list)
|
||||
subgoal for aa b
|
||||
apply (rule_tac x = "AllowPortFromTo c d e" and y = "DenyAllFromTo aa b" in tND,
|
||||
assumption,simp_all)
|
||||
apply (subgoal_tac "smaller (AllowPortFromTo c d e) (DenyAllFromTo aa b) l")
|
||||
apply (simp split: if_splits)
|
||||
apply metis
|
||||
apply (erule sorted_is_smaller, simp_all)
|
||||
apply (metis bothNet.simps(2) in_list.simps(2) in_set_in_list)
|
||||
done
|
||||
by (auto intro: aux7 tNDComm ANDConc singleCombinatorsConc sortedConcEnd)
|
||||
next
|
||||
case (Conc a b) thus ?thesis using Cons by simp
|
||||
|
|
@ -464,7 +479,9 @@ next
|
|||
apply (rule_tac t = "removeShadowRules1_alternative (xs @ [x])" and
|
||||
s = "(removeShadowRules1_alternative xs)@[x]" in subst)
|
||||
apply (erule RS1n_assoc)
|
||||
apply (case_tac "xa \<in> dom (Cp x)", simp_all)
|
||||
subgoal for a
|
||||
apply (case_tac "a \<in> dom (Cp x)", simp_all)
|
||||
done
|
||||
done
|
||||
qed
|
||||
qed
|
||||
|
|
@ -881,7 +898,11 @@ lemma AILRS3[rule_format,simp]:
|
|||
|
||||
lemma SCRS3[rule_format,simp]:
|
||||
"singleCombinators p \<longrightarrow> singleCombinators(rm_MT_rules Cp p)"
|
||||
by (induct p, simp_all) (case_tac "a", simp_all)
|
||||
apply (induct p, simp_all)
|
||||
subgoal for a p
|
||||
apply(case_tac "a", simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma RS3subset: "set (rm_MT_rules Cp p) \<subseteq> set p "
|
||||
by (induct p, auto)
|
||||
|
|
@ -992,11 +1013,13 @@ lemma list2FWpolicy2list[rule_format]:
|
|||
"Cp (list2FWpolicy(policy2list p)) = (Cp p)"
|
||||
apply (rule ext)
|
||||
apply (induct_tac p, simp_all)
|
||||
apply (case_tac "x \<in> dom (Cp (x2))")
|
||||
apply (metis Cdom2 CeqEnd domIff p2lNmt)
|
||||
apply (metis CeqStart domIff p2lNmt nlpaux)
|
||||
subgoal for x x1 x2
|
||||
apply (case_tac "x \<in> dom (Cp (x2))")
|
||||
apply (metis Cdom2 CeqEnd domIff p2lNmt)
|
||||
apply (metis CeqStart domIff p2lNmt nlpaux)
|
||||
done
|
||||
done
|
||||
|
||||
|
||||
lemmas C_eq_Lemmas = none_MT_rulesRS2 none_MT_rulesrd SCp2l wp1n_RS2 wp1ID NMPiD waux2
|
||||
wp1alternative_RS1 p2lNmt list2FWpolicy2list wellformed_policy3_charn wp1_eq
|
||||
|
||||
|
|
@ -1044,8 +1067,12 @@ lemma C_eq_All_untilSorted_withSimpsQ:
|
|||
|
||||
lemma InDomConc[rule_format]: "p \<noteq> [] \<longrightarrow> x \<in> dom (Cp (list2FWpolicy (p))) \<longrightarrow>
|
||||
x \<in> dom (Cp (list2FWpolicy (a#p)))"
|
||||
by (induct p, simp_all) (case_tac "p = []",simp_all add: dom_def Cp.simps)
|
||||
|
||||
apply (induct p, simp_all)
|
||||
subgoal for a p
|
||||
apply(case_tac "p = []",simp_all add: dom_def Cp.simps)
|
||||
done
|
||||
done
|
||||
|
||||
lemma not_in_member[rule_format]: "member a b \<longrightarrow> x \<notin> dom (Cp b) \<longrightarrow> x \<notin> dom (Cp a)"
|
||||
by (induct b)(simp_all add: dom_def Cp.simps)
|
||||
|
||||
|
|
@ -1055,9 +1082,11 @@ lemma src_in_sdnets[rule_format]:
|
|||
apply (simp_all add: fst_set_def subnetsOfAdr_def PLemmas, rename_tac x1 x2)
|
||||
apply (intro impI)
|
||||
apply (simp add: fst_set_def)
|
||||
apply (case_tac "p \<in> dom (Cp x2)")
|
||||
apply (rule subnetAux)
|
||||
apply (auto simp: PLemmas)
|
||||
subgoal for x1 x2
|
||||
apply (case_tac "p \<in> dom (Cp x2)")
|
||||
apply (rule subnetAux)
|
||||
apply (auto simp: PLemmas)
|
||||
done
|
||||
done
|
||||
|
||||
lemma dest_in_sdnets[rule_format]:
|
||||
|
|
@ -1065,9 +1094,11 @@ lemma dest_in_sdnets[rule_format]:
|
|||
apply (induct rule: Combinators.induct)
|
||||
apply (simp_all add: snd_set_def subnetsOfAdr_def PLemmas, rename_tac x1 x2)
|
||||
apply (intro impI,simp add: snd_set_def)
|
||||
apply (case_tac "p \<in> dom (Cp x2)")
|
||||
apply (rule subnetAux)
|
||||
apply (auto simp: PLemmas)
|
||||
subgoal for x1 x2
|
||||
apply (case_tac "p \<in> dom (Cp x2)")
|
||||
apply (rule subnetAux)
|
||||
apply (auto simp: PLemmas)
|
||||
done
|
||||
done
|
||||
|
||||
lemma sdnets_in_subnets[rule_format]:
|
||||
|
|
@ -1076,8 +1107,10 @@ lemma sdnets_in_subnets[rule_format]:
|
|||
apply (rule Combinators.induct)
|
||||
apply (simp_all add: PLemmas subnetsOfAdr_def)
|
||||
apply (intro impI, simp)
|
||||
apply (case_tac "p \<in> dom (Cp (x2))")
|
||||
apply (auto simp: PLemmas subnetsOfAdr_def)
|
||||
subgoal for x1 x2
|
||||
apply (case_tac "p \<in> dom (Cp (x2))")
|
||||
apply (auto simp: PLemmas subnetsOfAdr_def)
|
||||
done
|
||||
done
|
||||
|
||||
lemma disjSD_no_p_in_both[rule_format]:
|
||||
|
|
@ -1400,13 +1433,15 @@ lemma isSepaux:
|
|||
apply (rule_tac A = "(DenyAllFromTo (first_srcNet a) (first_destNet a) \<oplus>
|
||||
DenyAllFromTo (first_destNet a) (first_srcNet a) \<oplus> a)" in domsdisj, simp_all)
|
||||
apply (rule notI)
|
||||
apply (rule_tac p = xa and x ="(DenyAllFromTo (first_srcNet a) (first_destNet a) \<oplus>
|
||||
subgoal for xa s
|
||||
apply (rule_tac p = xa and x ="(DenyAllFromTo (first_srcNet a) (first_destNet a) \<oplus>
|
||||
DenyAllFromTo (first_destNet a) (first_srcNet a) \<oplus> a)"
|
||||
and y = s in disjSD_no_p_in_both, simp_all)
|
||||
using disjSD2aux noDA apply blast
|
||||
using noDA
|
||||
by blast
|
||||
|
||||
and y = s in disjSD_no_p_in_both, simp_all)
|
||||
using disjSD2aux noDA apply blast
|
||||
using noDA
|
||||
by blast
|
||||
done
|
||||
|
||||
lemma none_MT_rulessep[rule_format]: "none_MT_rules Cp p \<longrightarrow> none_MT_rules Cp (separate p)"
|
||||
by (induct p rule: separate.induct) (simp_all add: Cp.simps map_add_le_mapE map_le_antisym)
|
||||
|
||||
|
|
@ -1700,20 +1735,22 @@ lemma list2FWpolicys_eq_el[rule_format]:
|
|||
"Filter \<noteq> [] \<longrightarrow> Cp (list2policyR Filter) p = Cp (list2FWpolicy (rev Filter)) p"
|
||||
apply (induct_tac Filter)
|
||||
apply simp_all
|
||||
apply (case_tac "list = []")
|
||||
apply simp_all
|
||||
apply (case_tac "p \<in> dom (Cp a)")
|
||||
apply simp_all
|
||||
apply (rule list2policyR_Start)
|
||||
apply simp_all
|
||||
apply (subgoal_tac "Cp (list2policyR (a # list)) p = Cp (list2policyR list) p")
|
||||
apply (subgoal_tac "Cp (list2FWpolicy (rev list @ [a])) p = Cp (list2FWpolicy (rev list)) p")
|
||||
apply simp
|
||||
apply (rule CConcStart2)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (case_tac list,simp_all)
|
||||
apply (simp_all add: Cp.simps dom_def map_add_def)
|
||||
subgoal for a list
|
||||
apply (case_tac "list = []")
|
||||
apply simp_all
|
||||
apply (case_tac "p \<in> dom (Cp a)")
|
||||
apply simp_all
|
||||
apply (rule list2policyR_Start)
|
||||
apply simp_all
|
||||
apply (subgoal_tac "Cp (list2policyR (a # list)) p = Cp (list2policyR list) p")
|
||||
apply (subgoal_tac "Cp (list2FWpolicy (rev list @ [a])) p = Cp (list2FWpolicy (rev list)) p")
|
||||
apply simp
|
||||
apply (rule CConcStart2)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (case_tac list,simp_all)
|
||||
apply (simp_all add: Cp.simps dom_def map_add_def)
|
||||
done
|
||||
done
|
||||
|
||||
lemma list2FWpolicys_eq:
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
(*****************************************************************************
|
||||
* Copyright (c) 2005-2010 ETH Zurich, Switzerland
|
||||
* 2008-2015 Achim D. Brucker, Germany
|
||||
* 2009-2016 Université Paris-Sud, France
|
||||
* 2015-2016 The University of Sheffield, UK
|
||||
* 2009-2017 Université Paris-Sud, France
|
||||
* 2015-2017 The University of Sheffield, UK
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
|
|
@ -56,7 +56,11 @@ lemma aux26[simp]: "twoNetsDistinct a b c d \<Longrightarrow>
|
|||
|
||||
lemma wp2_aux[rule_format]: "wellformed_policy2 (xs @ [x]) \<longrightarrow>
|
||||
wellformed_policy2 xs"
|
||||
by (induct xs, simp_all) (case_tac "a", simp_all)
|
||||
apply (induct xs, simp_all)
|
||||
subgoal for a xs
|
||||
apply (case_tac "a", simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma Cdom2: "x \<in> dom(C b) \<Longrightarrow> C (a \<oplus> b) x = (C b) x"
|
||||
by (auto simp: C.simps)
|
||||
|
|
@ -90,6 +94,7 @@ lemma CConcEnd[rule_format]:
|
|||
apply (rule_tac P = ?P in list2FWpolicy.induct)
|
||||
by (simp_all add:C.simps)
|
||||
|
||||
|
||||
lemma CConcStartaux: " C a x = None \<Longrightarrow> (C aa ++ C a) x = C aa x"
|
||||
by (simp add: PLemmas)
|
||||
|
||||
|
|
@ -132,13 +137,15 @@ lemma bar3:
|
|||
lemma CeqEnd[rule_format,simp]:
|
||||
"a \<noteq> [] \<longrightarrow> x \<in> dom (C (list2FWpolicy a)) \<longrightarrow> C (list2FWpolicy(b@a)) x = (C (list2FWpolicy a)) x"
|
||||
apply (rule rev_induct,simp_all)
|
||||
apply (case_tac "xs \<noteq> []", simp_all)
|
||||
apply (case_tac "x \<in> dom (C xa)")
|
||||
apply (metis CConcEnd2 MRList2 mr_is_C )
|
||||
apply (metis CConcEnd1 CConcStart2 Nil_is_append_conv bar3 )
|
||||
apply (metis MRList2 eq_Nil_appendI mr_is_C )
|
||||
subgoal for xa xs
|
||||
apply (case_tac "xs \<noteq> []", simp_all)
|
||||
apply (case_tac "x \<in> dom (C xa)")
|
||||
apply (metis CConcEnd2 MRList2 mr_is_C )
|
||||
apply (metis CConcEnd1 CConcStart2 Nil_is_append_conv bar3 )
|
||||
apply (metis MRList2 eq_Nil_appendI mr_is_C )
|
||||
done
|
||||
done
|
||||
|
||||
|
||||
lemma CConcStartA[rule_format,simp]:
|
||||
"x \<in> dom (C a) \<longrightarrow> x \<in> dom (C (list2FWpolicy (a # b)))" (is "?P b")
|
||||
apply (rule_tac P = ?P in list2FWpolicy.induct)
|
||||
|
|
@ -164,9 +171,11 @@ by (metis mr_is_C)
|
|||
lemma nMRtoNone[rule_format]:
|
||||
"p \<noteq> [] \<longrightarrow> applied_rule_rev C x p = None \<longrightarrow> C (list2FWpolicy p) x = None"
|
||||
apply (rule rev_induct, simp_all)
|
||||
apply (case_tac "xs = []", simp_all)
|
||||
by (simp_all add: applied_rule_rev_def dom_def)
|
||||
|
||||
subgoal for xa xs
|
||||
apply (case_tac "xs = []", simp_all)
|
||||
by (simp_all add: applied_rule_rev_def dom_def)
|
||||
done
|
||||
|
||||
lemma C_eq_if_mr_eq:
|
||||
"applied_rule_rev C x b = applied_rule_rev C x a \<Longrightarrow> a \<noteq> [] \<Longrightarrow> b \<noteq> [] \<Longrightarrow>
|
||||
C (list2FWpolicy a) x = C (list2FWpolicy b) x"
|
||||
|
|
@ -183,7 +192,9 @@ lemma foo3a[rule_format]:
|
|||
apply (rule rev_induct)
|
||||
apply simp_all
|
||||
apply (intro impI conjI, simp)
|
||||
apply (rule_tac p = "a @ b # xs" in notmatching_notdom,simp_all)
|
||||
subgoal for xa xs
|
||||
apply (rule_tac p = "a @ b # xs" in notmatching_notdom,simp_all)
|
||||
done
|
||||
by (metis MRList2 MRList3 append_Cons option.inject)
|
||||
|
||||
lemma foo3D:
|
||||
|
|
@ -225,20 +236,24 @@ lemma mrConcEnd[rule_format]:
|
|||
|
||||
|
||||
lemma wp3tl[rule_format]: "wellformed_policy3 p \<longrightarrow> wellformed_policy3 (tl p)"
|
||||
by (induct p, simp_all, case_tac a, simp_all)
|
||||
|
||||
apply (induct p, simp_all)
|
||||
subgoal for a p
|
||||
apply(case_tac a, simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma wp3Conc[rule_format]: "wellformed_policy3 (a#p) \<longrightarrow> wellformed_policy3 p"
|
||||
by (induct p, simp_all, case_tac a, simp_all)
|
||||
|
||||
|
||||
lemma foo98[rule_format]:
|
||||
"applied_rule_rev C x (aa # p) = Some a \<longrightarrow> x \<in> dom (C r) \<longrightarrow> r \<in> set p \<longrightarrow> a \<in> set p"
|
||||
unfolding applied_rule_rev_def
|
||||
apply (rule rev_induct, simp_all)
|
||||
apply (case_tac "r = xa", simp_all)
|
||||
subgoal for xa xs
|
||||
apply (case_tac "r = xa", simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
|
||||
lemma mrMTNone[simp]: "applied_rule_rev C x [] = None"
|
||||
by (simp add: applied_rule_rev_def)
|
||||
|
||||
|
|
@ -329,11 +344,10 @@ lemma wellformed_policy3_charn[rule_format]:
|
|||
apply (induct_tac p)
|
||||
apply simp_all
|
||||
apply (auto intro: singleCombinatorsConc ANDConc waux2 wp2Conc)
|
||||
apply (case_tac a, simp_all, clarify)
|
||||
apply (case_tac r, simp_all)
|
||||
apply (metis Int_commute)
|
||||
apply (metis DomInterAllowsMT aux7aa DomInterAllowsMT_Ports)
|
||||
apply (metis aux0_0 )
|
||||
subgoal for a list
|
||||
apply (case_tac a, simp_all, clarify)
|
||||
apply (metis C.elims DomInterAllowsMT DomInterAllowsMT_Ports aux0_0 aux7aa inf_commute) (* slow *)
|
||||
done
|
||||
done
|
||||
|
||||
lemma DistinctNetsDenyAllow:
|
||||
|
|
@ -452,12 +466,14 @@ next
|
|||
case (Cons x list) show ?thesis
|
||||
apply (rule rev_induct)
|
||||
apply (metis rSR1_eq removeShadowRules1.simps(2))
|
||||
apply (case_tac "xs = []", simp_all)
|
||||
unfolding removeShadowRules1_alternative_def
|
||||
apply (case_tac x, simp_all)
|
||||
by (metis (no_types, hide_lams) CConcEnd2 CConcStart C_DenyAll RS1n_nMT aux114
|
||||
domIff removeShadowRules1_alternative_def
|
||||
removeShadowRules1_alternative_rev.simps(2) rev.simps(2))
|
||||
subgoal for x xs
|
||||
apply (case_tac "xs = []", simp_all)
|
||||
unfolding removeShadowRules1_alternative_def
|
||||
apply (case_tac x, simp_all)
|
||||
by (metis (no_types, hide_lams) CConcEnd2 CConcStart C_DenyAll RS1n_nMT aux114
|
||||
domIff removeShadowRules1_alternative_def
|
||||
removeShadowRules1_alternative_rev.simps(2) rev.simps(2))
|
||||
done
|
||||
qed
|
||||
|
||||
lemma C_eq_RS1[simp]:
|
||||
|
|
@ -815,8 +831,10 @@ lemma C_eq_None[rule_format]:
|
|||
apply (simp add: applied_rule_rev_def)
|
||||
apply (rule rev_induct, simp_all)
|
||||
apply (intro impI, simp)
|
||||
apply (case_tac "xs \<noteq> []")
|
||||
apply (simp_all add: dom_def)
|
||||
subgoal for xa xs
|
||||
apply (case_tac "xs \<noteq> []")
|
||||
apply (simp_all add: dom_def)
|
||||
done
|
||||
done
|
||||
|
||||
lemma C_eq_None2:
|
||||
|
|
@ -865,7 +883,11 @@ lemma AILRS3[rule_format,simp]:
|
|||
|
||||
lemma SCRS3[rule_format,simp]:
|
||||
"singleCombinators p \<longrightarrow> singleCombinators(rm_MT_rules C p)"
|
||||
by (induct p, simp_all, case_tac "a", simp_all)
|
||||
apply (induct p, simp_all)
|
||||
subgoal for a p
|
||||
apply(case_tac "a", simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma RS3subset: "set (rm_MT_rules C p) \<subseteq> set p "
|
||||
by (induct p, auto)
|
||||
|
|
@ -1025,7 +1047,11 @@ lemma C_eq_All_untilSorted_withSimpsQ:
|
|||
|
||||
lemma InDomConc[rule_format]:
|
||||
"p \<noteq> [] \<longrightarrow> x \<in> dom (C (list2FWpolicy (p))) \<longrightarrow> x \<in> dom (C (list2FWpolicy (a#p)))"
|
||||
by (induct p, simp_all) (case_tac "p = []", simp_all add: dom_def C.simps)
|
||||
apply (induct p, simp_all)
|
||||
subgoal for a' p
|
||||
apply (case_tac "p = []", simp_all add: dom_def C.simps)
|
||||
done
|
||||
done
|
||||
|
||||
lemma not_in_member[rule_format]: "member a b \<longrightarrow> x \<notin> dom (C b) \<longrightarrow> x \<notin> dom (C a)"
|
||||
by (induct b) (simp_all add: dom_def C.simps)
|
||||
|
|
@ -1035,9 +1061,11 @@ lemma src_in_sdnets[rule_format]:
|
|||
apply (induct rule: Combinators.induct)
|
||||
apply (simp_all add: fst_set_def subnetsOfAdr_def PLemmas fst_set_def)
|
||||
apply (intro impI)
|
||||
apply (case_tac "p \<in> dom (C x2)")
|
||||
apply (rule subnetAux)
|
||||
apply (auto simp: PLemmas fst_set_def)
|
||||
subgoal for x1 x2
|
||||
apply (case_tac "p \<in> dom (C x2)")
|
||||
apply (rule subnetAux)
|
||||
apply (auto simp: PLemmas fst_set_def)
|
||||
done
|
||||
done
|
||||
|
||||
lemma dest_in_sdnets[rule_format]:
|
||||
|
|
@ -1046,9 +1074,11 @@ lemma dest_in_sdnets[rule_format]:
|
|||
apply (simp_all add: snd_set_def subnetsOfAdr_def PLemmas)
|
||||
apply (intro impI)
|
||||
apply (simp add: snd_set_def)
|
||||
apply (case_tac "p \<in> dom (C x2)")
|
||||
apply (rule subnetAux)
|
||||
apply (auto simp: PLemmas)
|
||||
subgoal for x1 x2
|
||||
apply (case_tac "p \<in> dom (C x2)")
|
||||
apply (rule subnetAux)
|
||||
apply (auto simp: PLemmas)
|
||||
done
|
||||
done
|
||||
|
||||
lemma sdnets_in_subnets[rule_format]:
|
||||
|
|
@ -1057,8 +1087,10 @@ lemma sdnets_in_subnets[rule_format]:
|
|||
apply (rule Combinators.induct)
|
||||
apply (simp_all add: PLemmas subnetsOfAdr_def)
|
||||
apply (intro impI, simp)
|
||||
apply (case_tac "p \<in> dom (C (x2))")
|
||||
apply (auto simp: PLemmas subnetsOfAdr_def)
|
||||
subgoal for x1 x2
|
||||
apply (case_tac "p \<in> dom (C (x2))")
|
||||
apply (auto simp: PLemmas subnetsOfAdr_def)
|
||||
done
|
||||
done
|
||||
|
||||
lemma disjSD_no_p_in_both[rule_format]:
|
||||
|
|
@ -1121,7 +1153,7 @@ lemma domdConcStart[rule_format]:
|
|||
|
||||
lemma sep_dom2_aux:
|
||||
" x \<in> dom (C (list2FWpolicy (a \<oplus> y # z))) \<Longrightarrow> x \<in> dom (C (a \<oplus> list2FWpolicy (y # z)))"
|
||||
by (auto) (metis list2FWpolicy_eq p2lNmt)
|
||||
by (auto)[1] (metis list2FWpolicy_eq p2lNmt)
|
||||
|
||||
lemma sep_dom2_aux2:
|
||||
"x \<in> dom (C (list2FWpolicy (separate (y # z)))) \<longrightarrow> x \<in> dom (C (list2FWpolicy (y # z))) \<Longrightarrow>
|
||||
|
|
@ -1138,7 +1170,7 @@ lemma sepDom: "dom (C (list2FWpolicy p)) = dom (C (list2FWpolicy (separate p)))"
|
|||
|
||||
lemma C_eq_s_ext[rule_format]:
|
||||
"p \<noteq> [] \<longrightarrow> C (list2FWpolicy (separate p)) a = C (list2FWpolicy p) a "
|
||||
proof (induct rule: separate.induct, goal_cases) print_cases
|
||||
proof (induct rule: separate.induct, goal_cases)
|
||||
case (1 x) thus ?case
|
||||
apply simp
|
||||
apply (cases "x = []")
|
||||
|
|
@ -1503,12 +1535,14 @@ lemma C_eq_iD:
|
|||
|
||||
lemma noDAsortQ[rule_format]: "noDenyAll1 p \<longrightarrow> noDenyAll1 (qsort p l)"
|
||||
apply (case_tac "p",simp_all, rename_tac a list)
|
||||
apply (case_tac "a = DenyAll",simp_all)
|
||||
using nDAeqSet set_sortQ apply blast
|
||||
apply (rule impI,rule noDA1eq)
|
||||
apply (subgoal_tac "noDenyAll (a#list)")
|
||||
apply (metis append_Cons append_Nil nDAeqSet qsort.simps(2) set_sortQ)
|
||||
by (case_tac a, simp_all)
|
||||
subgoal for a list
|
||||
apply (case_tac "a = DenyAll",simp_all)
|
||||
using nDAeqSet set_sortQ apply blast
|
||||
apply (rule impI,rule noDA1eq)
|
||||
apply (subgoal_tac "noDenyAll (a#list)")
|
||||
apply (metis append_Cons append_Nil nDAeqSet qsort.simps(2) set_sortQ)
|
||||
by (case_tac a, simp_all)
|
||||
done
|
||||
|
||||
lemma NetsCollectedSortQ:
|
||||
"distinct p \<Longrightarrow>noDenyAll1 p \<Longrightarrow> all_in_list p l \<Longrightarrow> singleCombinators p \<Longrightarrow>
|
||||
|
|
@ -1790,8 +1824,12 @@ lemma CRotate_eq_rotateC: "CRotate p = C (rotatePolicy p)"
|
|||
|
||||
lemma DAinRotate:
|
||||
"DenyAll \<in> set (policy2list p) \<Longrightarrow> DenyAll \<in> set (policy2list (rotatePolicy p))"
|
||||
by (induct p,simp_all) (case_tac "DenyAll \<in> set (policy2list p1)",simp_all)
|
||||
|
||||
apply (induct p,simp_all)
|
||||
subgoal for p1 p2
|
||||
apply (case_tac "DenyAll \<in> set (policy2list p1)",simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
lemma DAUniv: "dom (CRotate (P \<oplus> DenyAll)) = UNIV"
|
||||
by (metis CRotate.simps(1) CRotate.simps(4) CRotate_eq_rotateC DAAux PLemmas(4) UNIV_eq_I domSubset3)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
(*****************************************************************************
|
||||
* Copyright (c) 2005-2010 ETH Zurich, Switzerland
|
||||
* 2008-2015 Achim D. Brucker, Germany
|
||||
* 2009-2016 Université Paris-Sud, France
|
||||
* 2015-2016 The University of Sheffield, UK
|
||||
* 2009-2017 Université Paris-Sud, France
|
||||
* 2015-2017 The University of Sheffield, UK
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
|
|
@ -127,13 +127,13 @@ definition content :: "('\<alpha>::adr,'\<beta>) packet \<Rightarrow> '\<beta> c
|
|||
datatype protocol = tcp | udp
|
||||
|
||||
lemma either: "\<lbrakk>a \<noteq> tcp;a \<noteq> udp\<rbrakk> \<Longrightarrow> False"
|
||||
by (case_tac a,simp_all)
|
||||
by (case_tac "a",simp_all)
|
||||
|
||||
lemma either2[simp]: "(a \<noteq> tcp) = (a = udp)"
|
||||
by (case_tac a,simp_all)
|
||||
by (case_tac "a",simp_all)
|
||||
|
||||
lemma either3[simp]: "(a \<noteq> udp) = (a = tcp)"
|
||||
by (case_tac a,simp_all)
|
||||
by (case_tac "a",simp_all)
|
||||
|
||||
text{*
|
||||
The following two constants give the source and destination port number of a packet. Address
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
(*****************************************************************************
|
||||
* Copyright (c) 2005-2010 ETH Zurich, Switzerland
|
||||
* 2008-2015 Achim D. Brucker, Germany
|
||||
* 2009-2016 Université Paris-Sud, France
|
||||
* 2015-2016 The University of Sheffield, UK
|
||||
* 2009-2017 Université Paris-Sud, France
|
||||
* 2015-2017 The University of Sheffield, UK
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
|
|
@ -74,7 +74,7 @@ definition
|
|||
|
||||
|
||||
text{* All these combinators and the default rules are put into one
|
||||
single lemma called @{text PolicyCombinators} to faciliate proving
|
||||
single lemma called @{text PolicyCombinators} to facilitate proving
|
||||
over policies. *}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
(*****************************************************************************
|
||||
* Copyright (c) 2005-2010 ETH Zurich, Switzerland
|
||||
* 2008-2015 Achim D. Brucker, Germany
|
||||
* 2009-2016 Université Paris-Sud, France
|
||||
* 2015-2016 The University of Sheffield, UK
|
||||
* 2009-2017 Université Paris-Sud, France
|
||||
* 2015-2017 The University of Sheffield, UK
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
|
|
@ -35,7 +35,7 @@
|
|||
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
*****************************************************************************)
|
||||
|
||||
subsection {* The File Transfer Prototol (ftp) *}
|
||||
subsection {* The File Transfer Protocol (ftp) *}
|
||||
theory
|
||||
FTP
|
||||
imports
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
(*****************************************************************************
|
||||
* Copyright (c) 2005-2010 ETH Zurich, Switzerland
|
||||
* 2008-2015 Achim D. Brucker, Germany
|
||||
* 2009-2016 Université Paris-Sud, France
|
||||
* 2015-2016 The University of Sheffield, UK
|
||||
* 2009-2017 Université Paris-Sud, France
|
||||
* 2015-2017 The University of Sheffield, UK
|
||||
*
|
||||
* All rights reserved.
|
||||
*
|
||||
|
|
@ -63,7 +63,7 @@ where
|
|||
| "atom p (a # S) = (p a)"
|
||||
|
||||
lemma holds_mono : "\<guillemotleft>q\<guillemotright> s \<Longrightarrow> \<guillemotleft>q\<guillemotright> (s @ t)"
|
||||
by(cases s,simp_all)
|
||||
by(cases "s",simp_all)
|
||||
|
||||
|
||||
fun always :: "('\<alpha> list \<Rightarrow> bool) \<Rightarrow> '\<alpha> list \<Rightarrow> bool" ("\<box>")
|
||||
|
|
@ -76,7 +76,7 @@ text{*
|
|||
locally, this paves the way to a wealth of library lemmas.
|
||||
*}
|
||||
lemma always_is_listall : "(\<box> \<guillemotleft>p\<guillemotright>) (t) = list_all (p) (t)"
|
||||
by(induct t, simp_all)
|
||||
by(induct "t", simp_all)
|
||||
|
||||
fun eventually :: "('\<alpha> list \<Rightarrow> bool) \<Rightarrow> '\<alpha> list \<Rightarrow> bool" ("\<diamondsuit>")
|
||||
where
|
||||
|
|
@ -89,7 +89,7 @@ text{*
|
|||
locally, this paves the way to a wealth of library lemmas.
|
||||
*}
|
||||
lemma eventually_is_listex : "(\<diamondsuit> \<guillemotleft>p\<guillemotright>) (t) = list_ex (p) (t)"
|
||||
by(induct t, simp_all)
|
||||
by(induct "t", simp_all)
|
||||
|
||||
text{*
|
||||
The next two constants will help us later in defining the state transitions. The constant
|
||||
|
|
@ -113,11 +113,15 @@ where
|
|||
"not_before p q [] = False"
|
||||
| "not_before p q (a # S) = (q a \<or> (\<not> (p a) \<and> (not_before p q S)))"
|
||||
|
||||
|
||||
lemma not_before_superfluous:
|
||||
"not_before p q = before (Not o p) q"
|
||||
by(rule ext,induct_tac "x", simp_all)
|
||||
|
||||
"not_before p q = before (Not o p) q"
|
||||
apply(rule ext)
|
||||
subgoal for n
|
||||
apply(induct_tac "n")
|
||||
apply(simp_all)
|
||||
done
|
||||
done
|
||||
|
||||
text{*General "before":*}
|
||||
fun until :: "('\<alpha> list \<Rightarrow> bool) \<Rightarrow> ('\<alpha> list \<Rightarrow> bool) \<Rightarrow> '\<alpha> list \<Rightarrow> bool" (infixl "U" 66)
|
||||
where
|
||||
|
|
@ -139,7 +143,7 @@ proof -
|
|||
done
|
||||
have C:"\<And>a aa list.(q a \<or> p a \<and> (\<exists>s t. aa # list = s @ t \<and> \<box> \<guillemotleft>p\<guillemotright> s \<and> \<guillemotleft>q\<guillemotright> t))
|
||||
\<Longrightarrow> (\<exists>s t. a # aa # list = s @ t \<and> \<box> \<guillemotleft>p\<guillemotright> s \<and> \<guillemotleft>q\<guillemotright> t)"
|
||||
apply auto
|
||||
apply auto[1]
|
||||
apply(rule_tac x="[]" in exI)
|
||||
apply(rule_tac x="a # aa # list" in exI, simp)
|
||||
apply(rule_tac x="a # s" in exI)
|
||||
|
|
@ -147,16 +151,21 @@ proof -
|
|||
done
|
||||
have D:"\<And>a aa list.(\<exists>s t. a # aa # list = s @ t \<and> \<box> \<guillemotleft>p\<guillemotright> s \<and> \<guillemotleft>q\<guillemotright> t)
|
||||
\<Longrightarrow> (q a \<or> p a \<and> (\<exists>s t. aa # list = s @ t \<and> \<box> \<guillemotleft>p\<guillemotright> s \<and> \<guillemotleft>q\<guillemotright> t))"
|
||||
apply auto
|
||||
apply auto[1]
|
||||
apply(case_tac "s", auto simp:List.neq_Nil_conv)
|
||||
apply(case_tac "s", auto simp:List.neq_Nil_conv)
|
||||
done
|
||||
show ?thesis
|
||||
apply(rule ext,induct_tac "x", simp,
|
||||
case_tac "list",simp_all)
|
||||
apply(rule iffI,erule A, erule B)
|
||||
apply(rule iffI,erule C, erule D)
|
||||
done
|
||||
qed
|
||||
|
||||
apply(rule ext)
|
||||
subgoal for n
|
||||
apply(induct_tac "n")
|
||||
apply(simp)
|
||||
subgoal for x xs
|
||||
apply(case_tac "xs")
|
||||
apply(simp,rule iffI,erule A, erule B)
|
||||
apply(simp,rule iffI,erule C, erule D)
|
||||
done
|
||||
done
|
||||
done
|
||||
qed
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue