Rename to distinguish function and path composition; function composition proofs, which have issues...

1 files changed, 18 insertions, 8 deletions

diff --git a/Prod.thy b/Prod.thy
index 496bf3e..cb455ac 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -68,21 +68,31 @@ lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq
 lemmas Prod_wellform [wellform] = Prod_form_cond1 Prod_form_cond2
 lemmas Prod_comps [comp] = Prod_comp Prod_uniq
 
-subsection \<open>Composition\<close>
 
-axiomatization fncompose :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<circ>" 70) where
-  fncompose_type: "\<lbrakk>
+section \<open>Function composition\<close>
+
+axiomatization compose :: "[Term, Term] \<Rightarrow> Term"  (infixr "o" 70)
+
+syntax "_COMPOSE" :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<circ>" 70)
+translations "g \<circ> f" \<rightleftharpoons> "g o f"
+
+axiomatization where
+  compose_type: "\<lbrakk>
     g: \<Prod>x:B. C(x);
     f: A \<rightarrow> B;
     (\<Prod>x:B. C(x)): U(i);
     A \<rightarrow> B: U(i)
   \<rbrakk> \<Longrightarrow> g \<circ> f: \<Prod>x:A. C(f`x)"
 and
-  fncompose_comp: "\<lbrakk>
-    A: U(i);
-    \<And>x. x: A \<Longrightarrow> b(x): B;
-    \<And>x. x: A \<Longrightarrow> c(x): C(x)
-  \<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))"
+  compose_comp: "\<lbrakk>
+    g: \<Prod>x:B. C(x);
+    f: A \<rightarrow> B;
+    (\<Prod>x:B. C(x)): U(i);
+    A \<rightarrow> B: U(i)
+  \<rbrakk> \<Longrightarrow> g \<circ> f \<equiv> \<^bold>\<lambda>x. g`(f`x)"
+
+lemmas compose_rules [intro] = compose_type
+lemmas compose_comps [comp] = compose_comp
 
 
 section \<open>Unit type\<close>