From 93bb823f90876f0182b6ecc25d1605aa69f27df9 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 8 Jan 2017 19:52:08 +0000 Subject: [PATCH] Removed references to system generated names. --- .../Transformation/Transformation01.thy | 2 +- .../FWNormalisation/FWNormalisationCore.thy | 4 +- .../NormalisationGenericProofs.thy | 262 ++++++++++++------ .../NormalisationIPPProofs.thy | 151 ++++++---- .../NormalisationIntegerPortProof.thy | 140 ++++++---- UPF-Firewall/PacketFilter/NetworkCore.thy | 10 +- .../PacketFilter/PolicyCombinators.thy | 6 +- UPF-Firewall/StatefulFW/FTP.thy | 6 +- UPF-Firewall/StatefulFW/LTL_alike.thy | 45 +-- 9 files changed, 400 insertions(+), 226 deletions(-) diff --git a/UPF-Firewall/Examples/Transformation/Transformation01.thy b/UPF-Firewall/Examples/Transformation/Transformation01.thy index 224df2f..2b8cb8c 100644 --- a/UPF-Firewall/Examples/Transformation/Transformation01.thy +++ b/UPF-Firewall/Examples/Transformation/Transformation01.thy @@ -143,7 +143,7 @@ lemma aux: "\a \ c; a \ d; c = d\ \ F by auto lemma sets_distinct5: "(s::int) < g \ {(a::int, b::int). a = s} \ {(a::int, b::int). g < a}" - apply (auto simp: sets_distinct3) + apply (auto simp: sets_distinct3)[1] apply (subgoal_tac "(s,4) \ {(a::int,b::int). a = (s)}") apply (subgoal_tac "(s,4) \ {(a::int,b::int). g < a}") apply (erule aux) diff --git a/UPF-Firewall/FWNormalisation/FWNormalisationCore.thy b/UPF-Firewall/FWNormalisation/FWNormalisationCore.thy index 1d34ec6..04cfca2 100644 --- a/UPF-Firewall/FWNormalisation/FWNormalisationCore.thy +++ b/UPF-Firewall/FWNormalisation/FWNormalisationCore.thy @@ -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\b) = (rotatePolicy b) \ (rotatePolicy a)" lemma check: "rev (policy2list (rotatePolicy p)) = policy2list p" - apply (induct p) + apply (induct "p") by (simp_all) diff --git a/UPF-Firewall/FWNormalisation/NormalisationGenericProofs.thy b/UPF-Firewall/FWNormalisation/NormalisationGenericProofs.thy index 7cfe1f1..a3109af 100644 --- a/UPF-Firewall/FWNormalisation/NormalisationGenericProofs.thy +++ b/UPF-Firewall/FWNormalisation/NormalisationGenericProofs.thy @@ -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 \ \" lemma wellformed_policy1_charn[rule_format]: "wellformed_policy1 p \ DenyAll \ set p \ (\ p'. p = DenyAll # p' \ DenyAll \ set p')" - by(induct p,simp_all) + by(induct "p",simp_all) lemma singleCombinatorsConc: "singleCombinators (x#xs) \ singleCombinators xs" by (case_tac x,simp_all) lemma aux0_0: "singleCombinators x \ \ (\ a b. (a\b) \ 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 \ set x \ a \ set y) = (a \ set (x@y))" by auto lemma aux0_1: "\singleCombinators xs; singleCombinators [x]\ \ singleCombinators (x#xs)" - by (case_tac x,simp_all) + by (case_tac "x",simp_all) lemma aux0_6: "\singleCombinators xs; \ (\ a b. x = a \ b)\ \ 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: " \ (\ a b. (a\b) \ set x) \ singleCombinators x" - apply (induct x) + apply (induct "x") apply simp_all by (metis aux0_6) @@ -113,18 +114,24 @@ lemma aux10[rule_format]: "a \ set (net_list p) \ a \ se lemma srcInNetListaux[simp]: "\x \ set p; singleCombinators[x]; x \ DenyAll\ \ srcNet x \ 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]: "\x \ set p; singleCombinators[x]; x \ DenyAll\ \ destNet x \ 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: "\allNetsDistinct p; x \ set p; y \ set p; a = srcNet x; @@ -198,11 +205,13 @@ lemma aNDSubsetaux[rule_format]: "singleCombinators a \ 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 \ singleCombinators b \ @@ -217,16 +226,20 @@ lemma aNDSubset: "\singleCombinators a;set a \ 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: "\singleCombinators a; singleCombinators b; set a = set b; allNetsDistinct b\ \ 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: "\singleCombinators p; singleCombinators [a]\ \ singleCombinators (a#p)" @@ -285,7 +298,7 @@ lemma waux3[rule_format]: "\x \ a; x \ set p\ \ - 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) \ 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 \ set a \ set b \ singleCombinators a" @@ -324,8 +340,11 @@ lemma SC_RS1[rule_format,simp]: "singleCombinators p \ allNetsDi using ANDConc singleCombinatorsConc by blast lemma RS2Set[rule_format]: "set (removeShadowRules2 p) \ 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 \ set list \ a \ 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]) \ 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 \ [] \ (list2FWpolicy (xa # a)) = (xa) \ (list2FWpolicy a)" @@ -358,7 +380,10 @@ lemma foo2: "a \ set ps \ lemma SCnotConc[rule_format,simp]: "a\b \ set p \ singleCombinators p \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]: "\dom a \ dom b = {}; x \ dom a\ \ x \ dom b" @@ -520,8 +549,10 @@ lemma distinct_RS2[rule_format,simp]: "distinct p \ 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} \ x = a \ y = b \ x = b \ 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) \ @@ -802,7 +835,12 @@ lemma distinct_sortQ[rule_format]: lemma singleCombinatorsAppend[rule_format]: "singleCombinators (xs) \ singleCombinators (ys) \ 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 \ []\ removeShadowRules1_alternative p \ []" 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 \ [] \ removeShadowRules2 p \ []" apply (induct p, simp_all) - apply (case_tac "p \ []", simp_all) - apply (case_tac "a", simp_all)+ + subgoal for a p + apply (case_tac "p \ []", simp_all) + apply (case_tac "a", simp_all)+ + done done lemma wp1_alternative_not_mt[simp]: "wellformed_policy1_strong p \ p \ []" @@ -976,7 +1018,11 @@ lemma AIL1[rule_format,simp]: "all_in_list p l \ 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 \ all_in_list (r lemma AILiD[rule_format,simp]: "all_in_list p l \ 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\ 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 \ 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 \ by (induct p, simp_all) lemma DAiniD: "DenyAll \ 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 \ []" by (rule policy2list.induct, simp_all) lemma AIL2[rule_format,simp]: "all_in_list p l \ 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 \ singleCombinators y \ singleCombinators (x@y)" apply (rule aux0_5) @@ -1095,15 +1156,20 @@ lemma sortnMT: "p \ [] \ sort p l \ []" lemma idNMT[rule_format]: "p \ [] \ insertDenies 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 OTNoTN[rule_format]: " OnlyTwoNets p \ x \ DenyAll \ x \ set p \ 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]: "\ member DenyAll x \ (first_srcNet x,first_destNet x) \ sdnets x" @@ -1171,7 +1237,11 @@ lemma disjSD2aux: using first_isIn by blast lemma noDA1eq[rule_format]: "noDenyAll p \ 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) \ 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 \ 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 \ s \ set (insertDenies p) \ (\! a. s = (DenyAllFromTo (first_srcNet a) (first_destNet a)) \ (DenyAllFromTo (first_destNet a) (first_srcNet a)) \ a \ a \ 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) \ DenyAllFromTo (first_destNet s) (first_srcNet s) \ s\ set (insertDenies p) \ s \ 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 \ @@ -1216,7 +1296,7 @@ lemma id_aux4[rule_format]: "noDenyAll p \ \s. s \ set p \ disjSD_2 a s \ s \ set (insertDenies p) \ \ member DenyAll a \ disjSD_2 a s" - apply (subgoal_tac " \a. s = + apply (subgoal_tac "\a. s = DenyAllFromTo (first_srcNet a) (first_destNet a) \ DenyAllFromTo (first_destNet a) (first_srcNet a) \ a \ a \ 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 \ allNetsDistinct(DenyAll#p)" @@ -1444,8 +1526,10 @@ lemma isInAlternativeListb: lemma ANDSepaux: "allNetsDistinct (x # y # z) \ allNetsDistinct (x \ 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 \ 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 \ DenyAll \ noDenyAll1 (a # list) \ noDenyAll (a#list)" by (case_tac a, simp_all) - show "a \ DenyAll \ noDenyAll1 (a # list) \ 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 \ DenyAll \ noDenyAll1 (a # list) \ noDenyAll (a#list)" by (case_tac a, simp_all) + show "a \ DenyAll \ noDenyAll1 (a # list) \ 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 \ 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: "\ member DenyAll x \ first_bothNet x \ {}" @@ -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 \ 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 \ 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 \ NetsCollected2 p \ NetsCollected p \ noDenyAll1 p \ allNetsDistinct p \ 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 \ NetsCollected2 p \ NetsCollected p \ noDenyAll1 p \ allNetsDistinct p \ separated p \ a \ DenyAll \ OnlyTwoNets (a # p) \ diff --git a/UPF-Firewall/FWNormalisation/NormalisationIPPProofs.thy b/UPF-Firewall/FWNormalisation/NormalisationIPPProofs.thy index 5aed764..4359abc 100644 --- a/UPF-Firewall/FWNormalisation/NormalisationIPPProofs.thy +++ b/UPF-Firewall/FWNormalisation/NormalisationIPPProofs.thy @@ -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]) \ 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 \ dom(Cp b) \ Cp (a \ b) x = (Cp b) x" by (auto simp: Cp.simps) @@ -123,7 +127,7 @@ lemma bar3: lemma CeqEnd[rule_format,simp]: "a \ [] \ x \ dom (Cp(list2FWpolicy a)) \ 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 \ [] \ applied_rule_rev Cp x p = None \ 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 \ 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) \ wellformed_policy3Pr p" by (induct p, simp_all, case_tac a, simp_all) @@ -259,7 +267,11 @@ lemma mr_not_Conc: "singleCombinators p \ applied_rule_rev Cp x lemma foo25[rule_format]: "wellformed_policy3Pr (p@[x]) \ 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 \ x \ 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 \ AllowPortFromTo a b po \ set p \ dom (Cp (AllowPortFromTo a b po)) \ 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 \ distinct p \ allNetsDistinct p \ wellformed_policy1 p \ wellformed_policy2Pr p \ 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 \ dom (Cp x)", simp_all) + subgoal for a + apply (case_tac "a \ 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 \ 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) \ 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 \ dom (Cp (x2))") - apply (metis Cdom2 CeqEnd domIff p2lNmt) - apply (metis CeqStart domIff p2lNmt nlpaux) + subgoal for x x1 x2 + apply (case_tac "x \ 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 \ [] \ x \ dom (Cp (list2FWpolicy (p))) \ x \ 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 \ x \ dom (Cp b) \ x \ 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 \ dom (Cp x2)") - apply (rule subnetAux) - apply (auto simp: PLemmas) + subgoal for x1 x2 + apply (case_tac "p \ 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 \ dom (Cp x2)") - apply (rule subnetAux) - apply (auto simp: PLemmas) + subgoal for x1 x2 + apply (case_tac "p \ 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 \ dom (Cp (x2))") - apply (auto simp: PLemmas subnetsOfAdr_def) + subgoal for x1 x2 + apply (case_tac "p \ 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) \ DenyAllFromTo (first_destNet a) (first_srcNet a) \ a)" in domsdisj, simp_all) apply (rule notI) - apply (rule_tac p = xa and x ="(DenyAllFromTo (first_srcNet a) (first_destNet a) \ + subgoal for xa s + apply (rule_tac p = xa and x ="(DenyAllFromTo (first_srcNet a) (first_destNet a) \ DenyAllFromTo (first_destNet a) (first_srcNet a) \ 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 \ 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 \ [] \ 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 \ 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 \ 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: diff --git a/UPF-Firewall/FWNormalisation/NormalisationIntegerPortProof.thy b/UPF-Firewall/FWNormalisation/NormalisationIntegerPortProof.thy index b4675fc..868daac 100644 --- a/UPF-Firewall/FWNormalisation/NormalisationIntegerPortProof.thy +++ b/UPF-Firewall/FWNormalisation/NormalisationIntegerPortProof.thy @@ -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 \ lemma wp2_aux[rule_format]: "wellformed_policy2 (xs @ [x]) \ 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 \ dom(C b) \ C (a \ 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 \ (C aa ++ C a) x = C aa x" by (simp add: PLemmas) @@ -132,13 +137,15 @@ lemma bar3: lemma CeqEnd[rule_format,simp]: "a \ [] \ x \ dom (C (list2FWpolicy a)) \ C (list2FWpolicy(b@a)) x = (C (list2FWpolicy a)) x" apply (rule rev_induct,simp_all) - apply (case_tac "xs \ []", simp_all) - apply (case_tac "x \ 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 \ []", simp_all) + apply (case_tac "x \ 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 \ dom (C a) \ x \ 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 \ [] \ applied_rule_rev C x p = None \ 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 \ a \ [] \ b \ [] \ 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 \ 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) \ 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 \ x \ dom (C r) \ r \ set p \ a \ 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 \ []") - apply (simp_all add: dom_def) + subgoal for xa xs + apply (case_tac "xs \ []") + 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 \ 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) \ set p " by (induct p, auto) @@ -1025,7 +1047,11 @@ lemma C_eq_All_untilSorted_withSimpsQ: lemma InDomConc[rule_format]: "p \ [] \ x \ dom (C (list2FWpolicy (p))) \ x \ 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 \ x \ dom (C b) \ x \ 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 \ dom (C x2)") - apply (rule subnetAux) - apply (auto simp: PLemmas fst_set_def) + subgoal for x1 x2 + apply (case_tac "p \ 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 \ dom (C x2)") - apply (rule subnetAux) - apply (auto simp: PLemmas) + subgoal for x1 x2 + apply (case_tac "p \ 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 \ dom (C (x2))") - apply (auto simp: PLemmas subnetsOfAdr_def) + subgoal for x1 x2 + apply (case_tac "p \ 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 \ dom (C (list2FWpolicy (a \ y # z))) \ x \ dom (C (a \ list2FWpolicy (y # z)))" - by (auto) (metis list2FWpolicy_eq p2lNmt) + by (auto)[1] (metis list2FWpolicy_eq p2lNmt) lemma sep_dom2_aux2: "x \ dom (C (list2FWpolicy (separate (y # z)))) \ x \ dom (C (list2FWpolicy (y # z))) \ @@ -1138,7 +1170,7 @@ lemma sepDom: "dom (C (list2FWpolicy p)) = dom (C (list2FWpolicy (separate p)))" lemma C_eq_s_ext[rule_format]: "p \ [] \ 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 \ 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 \noDenyAll1 p \ all_in_list p l \ singleCombinators p \ @@ -1790,8 +1824,12 @@ lemma CRotate_eq_rotateC: "CRotate p = C (rotatePolicy p)" lemma DAinRotate: "DenyAll \ set (policy2list p) \ DenyAll \ set (policy2list (rotatePolicy p))" - by (induct p,simp_all) (case_tac "DenyAll \ set (policy2list p1)",simp_all) - + apply (induct p,simp_all) + subgoal for p1 p2 + apply (case_tac "DenyAll \ set (policy2list p1)",simp_all) + done + done + lemma DAUniv: "dom (CRotate (P \ DenyAll)) = UNIV" by (metis CRotate.simps(1) CRotate.simps(4) CRotate_eq_rotateC DAAux PLemmas(4) UNIV_eq_I domSubset3) diff --git a/UPF-Firewall/PacketFilter/NetworkCore.thy b/UPF-Firewall/PacketFilter/NetworkCore.thy index 8031497..ba6e261 100644 --- a/UPF-Firewall/PacketFilter/NetworkCore.thy +++ b/UPF-Firewall/PacketFilter/NetworkCore.thy @@ -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 :: "('\::adr,'\) packet \ '\ c datatype protocol = tcp | udp lemma either: "\a \ tcp;a \ udp\ \ False" - by (case_tac a,simp_all) + by (case_tac "a",simp_all) lemma either2[simp]: "(a \ tcp) = (a = udp)" - by (case_tac a,simp_all) + by (case_tac "a",simp_all) lemma either3[simp]: "(a \ 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 diff --git a/UPF-Firewall/PacketFilter/PolicyCombinators.thy b/UPF-Firewall/PacketFilter/PolicyCombinators.thy index 5691e38..3017476 100644 --- a/UPF-Firewall/PacketFilter/PolicyCombinators.thy +++ b/UPF-Firewall/PacketFilter/PolicyCombinators.thy @@ -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. *} diff --git a/UPF-Firewall/StatefulFW/FTP.thy b/UPF-Firewall/StatefulFW/FTP.thy index 83c19dc..881d9eb 100644 --- a/UPF-Firewall/StatefulFW/FTP.thy +++ b/UPF-Firewall/StatefulFW/FTP.thy @@ -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 diff --git a/UPF-Firewall/StatefulFW/LTL_alike.thy b/UPF-Firewall/StatefulFW/LTL_alike.thy index 20afe85..ace3a79 100644 --- a/UPF-Firewall/StatefulFW/LTL_alike.thy +++ b/UPF-Firewall/StatefulFW/LTL_alike.thy @@ -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 : "\q\ s \ \q\ (s @ t)" - by(cases s,simp_all) + by(cases "s",simp_all) fun always :: "('\ list \ bool) \ '\ list \ bool" ("\") @@ -76,7 +76,7 @@ text{* locally, this paves the way to a wealth of library lemmas. *} lemma always_is_listall : "(\ \p\) (t) = list_all (p) (t)" - by(induct t, simp_all) + by(induct "t", simp_all) fun eventually :: "('\ list \ bool) \ '\ list \ bool" ("\") where @@ -89,7 +89,7 @@ text{* locally, this paves the way to a wealth of library lemmas. *} lemma eventually_is_listex : "(\ \p\) (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 \ (\ (p a) \ (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 :: "('\ list \ bool) \ ('\ list \ bool) \ '\ list \ bool" (infixl "U" 66) where @@ -139,7 +143,7 @@ proof - done have C:"\a aa list.(q a \ p a \ (\s t. aa # list = s @ t \ \ \p\ s \ \q\ t)) \ (\s t. a # aa # list = s @ t \ \ \p\ s \ \q\ 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:"\a aa list.(\s t. a # aa # list = s @ t \ \ \p\ s \ \q\ t) \ (q a \ p a \ (\s t. aa # list = s @ t \ \ \p\ s \ \q\ 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