Equality inverse and composition done. Cleaned up methods and method example theory.

1 files changed, 12 insertions, 20 deletions

diff --git a/Proj.thy b/Proj.thy
index e90cd95..aa7e8ec 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -21,17 +21,14 @@ text "Typing judgments and computation rules for the dependent and non-dependent
 
 lemma fst_type:
   assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "fst(p): A"
-unfolding fst_def
-proof
-  show "A: U(i)" using assms(1) by (rule Sum_wellform)
-qed (fact assms | assumption)+
+unfolding fst_def by (derive lem: assms)
 
 
 lemma fst_comp:
   assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "fst(<a,b>) \<equiv> a"
 unfolding fst_def
 proof
-  show "\<And>x. x: A \<Longrightarrow> x: A" .
+  show "a: A" and "b: B(a)" by fact+
 qed (rule assms)+
 
 
@@ -39,20 +36,16 @@ lemma snd_type:
   assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "snd(p): B(fst p)"
 unfolding snd_def
 proof
-  show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)"
-  proof -
-    have "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> fst(p): A" using assms(1) by (rule fst_type)
-    with assms(1) show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)" by (rule Sum_wellform)
-  qed
-
+  show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)" by (derive lem: assms fst_type)
+  
   fix x y
   assume asm: "x: A" "y: B(x)"
   show "y: B(fst <x,y>)"
   proof (subst fst_comp)
-    show "A: U(i)" using assms(1) by (rule Sum_wellform)
-    show "\<And>x. x: A \<Longrightarrow> B(x): U(i)" using assms(1) by (rule Sum_wellform)
-  qed (rule asm)+
-qed (fact assms)
+    show "A: U(i)" by (wellformed lem: assms(1))
+    show "\<And>x. x: A \<Longrightarrow> B(x): U(i)" by (wellformed lem: assms(1))
+  qed fact+
+qed fact
 
 
 lemma snd_comp:
@@ -60,13 +53,12 @@ lemma snd_comp:
 unfolding snd_def
 proof
   show "\<And>x y. y: B(x) \<Longrightarrow> y: B(x)" .
-  show "a: A" by (fact assms)
-  show "b: B(a)" by (fact assms)
-  show *: "B(a): U(i)" using assms(3) by (rule assms(2))
-  show "B(a): U(i)" by (fact *)
-qed
+  show "a: A" by fact
+  show "b: B(a)" by fact
+qed (simple lem: assms)
 
 
+lemmas Proj_types [intro] = fst_type snd_type
 lemmas Proj_comps [intro] = fst_comp snd_comp