From b3c466bf7f850e39a59ebc04580e385a48bfd655 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 27 Jun 2018 16:11:56 +0200
Subject: wellformed method to automatically prove wellformed judgments
 derivable from a wellformed judgment

---
 HoTT_Methods.thy | 76 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 76 insertions(+)
 create mode 100644 HoTT_Methods.thy

diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
new file mode 100644
index 0000000..8931c2b
--- /dev/null
+++ b/HoTT_Methods.thy
@@ -0,0 +1,76 @@
+(*  Title:  HoTT/HoTT_Methods.thy
+    Author: Josh Chen
+    Date:   Jun 2018
+
+Method setup for the HoTT library.
+Relies on Eisbach, which for the moment lives in HOL/Eisbach.
+*)
+
+theory HoTT_Methods
+  imports
+    "HOL-Eisbach.Eisbach"
+    "HOL-Eisbach.Eisbach_Tools"
+    HoTT_Base
+    Prod
+    Sum
+begin
+
+
+text "This method finds a proof of any valid typing judgment derivable from a given wellformed judgment."
+
+method wellformed uses jdgmt = (
+  match jdgmt in
+    "?a : ?A" \<Rightarrow> \<open>
+      rule HoTT_Base.inhabited_implies_type[OF jdgmt] |
+      wellformed jdgmt: HoTT_Base.inhabited_implies_type[OF jdgmt]
+      \<close> \<bar>
+    "A : U" for A \<Rightarrow> \<open>
+      print_term A,
+      match (A) in
+        "\<Prod>x:?A. ?B x" \<Rightarrow> \<open>
+          rule Prod.Prod_form_cond1[OF jdgmt] |
+          rule Prod.Prod_form_cond2[OF jdgmt] |
+          catch \<open>wellformed jdgmt: Prod.Prod_form_cond1[OF jdgmt]\<close> \<open>fail\<close> |
+          catch \<open>wellformed jdgmt: Prod.Prod_form_cond2[OF jdgmt]\<close> \<open>fail\<close>
+          \<close> \<bar>
+        "\<Sum>x:?A. ?B x" \<Rightarrow> \<open>
+          rule Sum.Sum_form_cond1[OF jdgmt] |
+          rule Sum.Sum_form_cond2[OF jdgmt] |
+          catch \<open>wellformed jdgmt: Sum.Sum_form_cond1[OF jdgmt]\<close> \<open>fail\<close> |
+          catch \<open>wellformed jdgmt: Sum.Sum_form_cond2[OF jdgmt]\<close> \<open>fail\<close>
+          \<close>
+      \<close> \<bar>
+    "PROP ?P \<Longrightarrow> PROP ?Q" \<Rightarrow> \<open>
+      (* Could probably direct the search here a bit more too. *)
+      catch \<open>rule Prod.Prod_form_cond1[OF jdgmt]\<close> \<open>fail\<close> |
+      catch \<open>rule Prod.Prod_form_cond2[OF jdgmt]\<close> \<open>fail\<close> |
+      catch \<open>rule Sum.Sum_form_cond1[OF jdgmt]\<close> \<open>fail\<close> |
+      catch \<open>rule Sum.Sum_form_cond2[OF jdgmt]\<close> \<open>fail\<close> |
+      catch \<open>wellformed jdgmt: Prod.Prod_form_cond1[OF jdgmt]\<close> \<open>fail\<close> |
+      catch \<open>wellformed jdgmt: Prod.Prod_form_cond2[OF jdgmt]\<close> \<open>fail\<close>
+    \<close>
+  )
+
+notepad  \<comment> \<open>Examples using \<open>wellformed\<close>\<close>
+begin
+
+assume 0: "f : \<Sum>x:A. B x"
+  have "\<Sum>x:A. B x : U" by (wellformed jdgmt: 0)
+  have "A : U" by (wellformed jdgmt: 0)
+  have "B: A \<rightarrow> U" by (wellformed jdgmt: 0)
+
+assume 1: "f : \<Prod>x:A. \<Prod>y: B x. C x y"
+  have "A : U" by (wellformed jdgmt: 1)
+  have "B: A \<rightarrow> U" by (wellformed jdgmt: 1)
+  have "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" by (wellformed jdgmt: 1)
+
+assume 2: "\<Sum>x:A. \<Prod>y: B x. \<Sum>z: C x y. D x y z : U"
+  have a: "A : U" by (wellformed jdgmt: 2)
+  have b: "B: A \<rightarrow> U" by (wellformed jdgmt: 2)
+  have c: "\<And>x. x : A \<Longrightarrow> C x : B x \<rightarrow> U" by (wellformed jdgmt: 2)
+  have d: "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y : C x y \<rightarrow> U" by (wellformed jdgmt: 2)
+
+end
+
+
+end
\ No newline at end of file
-- 
cgit v1.2.3