From 5161a0356d8752f3b1b4f4385e799bca92718814 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 17 Jun 2018 00:48:01 +0200
Subject: Decided on a new proper scheme for type rules using the idea of
 implicit well-formed contexts and guaranteed conclusion well-formedness.
 Product type rules now follow this scheme.

---
 scratch.thy | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 scratch.thy

(limited to 'scratch.thy')

diff --git a/scratch.thy b/scratch.thy
new file mode 100644
index 0000000..331b607
--- /dev/null
+++ b/scratch.thy
@@ -0,0 +1,24 @@
+theory scratch
+  imports IFOL
+
+begin
+
+lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
+apply (erule disjE)  (* Compare with the less useful \<open>rule disjE\<close> *)
+  apply (rule disjI2)
+  apply assumption
+apply (rule disjI1)
+apply assumption
+done
+
+lemma imp_uncurry: "P \<longrightarrow> (Q \<longrightarrow> R) \<Longrightarrow> P \<and> Q \<longrightarrow> R"
+apply (rule impI)
+apply (erule conjE)
+apply (drule mp)
+apply assumption
+apply (drule mp)
+apply assumption
+apply assumption
+done
+
+end
\ No newline at end of file
-- 
cgit v1.2.3