diff options
| -rw-r--r-- | HoTT_Methods.thy | 76 |
1 files changed, 76 insertions, 0 deletions
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 |