From a7806604105ebf09af4237fe338c0cfcf6ebb463 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 17 Aug 2018 13:57:36 +0200
Subject: Make function composition a definition instead of an axiomatization
 (should not need to worry about preconditions)

---
 Prod.thy | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

(limited to 'Prod.thy')

diff --git a/Prod.thy b/Prod.thy
index 120fc59..8c94ec6 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -75,19 +75,11 @@ lemmas Prod_comps [comp] = Prod_comp Prod_uniq Prod_eq
 
 section \<open>Function composition\<close>
 
-axiomatization compose :: "[Term, Term] \<Rightarrow> Term"  (infixr "o" 70)
+definition compose :: "[Term, Term] \<Rightarrow> Term"  (infixr "o" 70) where "g o f \<equiv> \<^bold>\<lambda>x. g`(f`x)"
 
 syntax "_COMPOSE" :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<circ>" 70)
 translations "g \<circ> f" \<rightleftharpoons> "g o f"
 
-axiomatization where
-  compose_def: "\<lbrakk>
-    f: A \<rightarrow> B;
-    g: \<Prod>x:B. C(x);
-    A \<rightarrow> B: U(i);
-    (\<Prod>x:B. C(x)): U(i)
-  \<rbrakk> \<Longrightarrow> g \<circ> f \<equiv> \<^bold>\<lambda>x. g`(f`x)"
-
 
 section \<open>Unit type\<close>
 
-- 
cgit v1.2.3