aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-08-19 17:29:25 +0200
committerJosh Chen2018-08-19 17:29:25 +0200
commitae909b21905be847a2ce01388e34708c9d0246c0 (patch)
treeb6e95291938fee51d63b6e7e8e343a0d5fcace0e
parent746fab6476dc622a982d5ebaeb30a2e1426c3316 (diff)
Trying to atomize universal quantification
Diffstat (limited to '')
-rw-r--r--Prod.thy9
1 files changed, 9 insertions, 0 deletions
diff --git a/Prod.thy b/Prod.thy
index b0408b9..3b74531 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -81,4 +81,13 @@ syntax "_COMPOSE" :: "[Term, Term] \<Rightarrow> Term" (infixr "\<circ>" 70)
translations "g \<circ> f" \<rightleftharpoons> "g o f"
+section \<open>Atomization\<close>
+
+text "
+ Universal statements can be internalized within the theory; the following rule is admissible.
+" (* PROOF NEEDED *)
+
+axiomatization where Prod_atomize: "(\<^bold>\<lambda>x. b(x): \<Prod>x:A. B(x)) \<Longrightarrow> (\<And>x. x: A \<Longrightarrow> b(x): B(x))"
+
+
end