From ae909b21905be847a2ce01388e34708c9d0246c0 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 19 Aug 2018 17:29:25 +0200
Subject: Trying to atomize universal quantification

---
 Prod.thy | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'Prod.thy')

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
-- 
cgit v1.2.3