diff options
| author | Josh Chen | 2018-06-30 07:07:42 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-06-30 07:07:42 +0200 |
| commit | 352a6e40a5bdf193b8f9690e76aede4e0650a445 (patch) | |
| tree | 01904cf0570b28389cfcb02d4bb4b26ef086f067 /HoTT_Methods.thy | |
| parent | 0dfe6d34967faaf366ed4ac7b5718b64b7f5a721 (diff) | |
Equality
Diffstat (limited to 'HoTT_Methods.thy')
| -rw-r--r-- | HoTT_Methods.thy | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index aa6fca2..7886c1a 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -11,6 +11,7 @@ theory HoTT_Methods "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools" HoTT_Base + Equal Prod Sum begin @@ -27,16 +28,25 @@ method wellformed uses jdgmt = ( "A : U" for A \<Rightarrow> \<open> match (A) in "\<Prod>x:?A. ?B x" \<Rightarrow> \<open> - rule Prod.Prod_form_cond1[OF jdgmt] | + print_term "\<Pi>", + (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> + 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> \<bar> + "?a =[?A] ?b" \<Rightarrow> \<open> + rule Equal.Equal_form_cond1[OF jdgmt] | + rule Equal.Equal_form_cond2[OF jdgmt] | + rule Equal.Equal_form_cond3[OF jdgmt] | + catch \<open>wellformed jdgmt: Equal.Equal_form_cond1[OF jdgmt]\<close> \<open>fail\<close> | + catch \<open>wellformed jdgmt: Equal.Equal_form_cond2[OF jdgmt]\<close> \<open>fail\<close> | + catch \<open>wellformed jdgmt: Equal.Equal_form_cond3[OF jdgmt]\<close> \<open>fail\<close> \<close> \<close> \<bar> "PROP ?P \<Longrightarrow> PROP Q" for Q \<Rightarrow> \<open> |