diff options
| author | Jakob L. Kreuze | 2023-12-21 14:30:43 -0500 |
|---|---|---|
| committer | Jakob L. Kreuze | 2023-12-21 14:30:43 -0500 |
| commit | 430f7f16fa8c6ae858b44a650324ab9958dfcd99 (patch) | |
| tree | ba5ad832d12eefec4e3e03ed332b01757f5c832d /xacml-proofs/lean | |
| parent | 9cda321fcfa57d14a5a960653369ff4ac5658168 (diff) | |
s/simp/rfl/ where necessary
Diffstat (limited to 'xacml-proofs/lean')
| -rw-r--r-- | xacml-proofs/lean/Xacml.lean | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean index 439b867..349b817 100644 --- a/xacml-proofs/lean/Xacml.lean +++ b/xacml-proofs/lean/Xacml.lean @@ -1813,11 +1813,11 @@ theorem pr₁ : ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) ∧ (ElementTree.eval req compiled_college100_element).fst == Decision'.permit := by have h₁ : bad_req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student")) := by - { simp } + { rfl } have h₂ : bad_req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Assign")) := by - { simp } + { rfl } have h₃ : bad_req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by - { simp } + { rfl } apply Exists.intro bad_req apply And.intro @@ -1870,11 +1870,11 @@ theorem pr₃ : { apply Exists.intro bad_req₀ have h₁ : bad_req₀.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student")) := by - { simp } + { rfl } have h₂ : bad_req₀.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Receive")) := by - { simp } - have h₃ : bad_req₀.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by - { simp } + { rfl } + -- have h₃ : bad_req₀.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by + -- { rfl } apply And.intro { rw_local @@ -1888,11 +1888,11 @@ theorem pr₃ : { apply Exists.intro bad_req₁ have h₁ : bad_req₁.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student")) := by - { simp } + { rfl } have h₂ : bad_req₁.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Assign")) := by - { simp } - have h₃ : bad_req₁.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by - { simp } + { rfl } + -- have h₃ : bad_req₁.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by + -- { rfl } apply And.intro { rw_local |