diff options
| author | Josh Chen | 2020-05-22 15:43:14 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-22 15:43:14 +0200 |
| commit | 720da0f918118388d114e09664b129d2b29be2b1 (patch) | |
| tree | e4411cceae3a790544e7bebb4eb7717c31e0fa63 /spartan/theories/Identity.thy | |
| parent | 1571e03b7dc5c7e6f2a46be57a12dd0d25fea452 (diff) | |
some tweaks and comments, in preparation for general inductive type elimination
Diffstat (limited to 'spartan/theories/Identity.thy')
| -rw-r--r-- | spartan/theories/Identity.thy | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/spartan/theories/Identity.thy b/spartan/theories/Identity.thy index 19b8b7a..4a4cc40 100644 --- a/spartan/theories/Identity.thy +++ b/spartan/theories/Identity.thy @@ -15,7 +15,7 @@ axiomatization refl :: \<open>o \<Rightarrow> o\<close> and IdInd :: \<open>o \<Rightarrow> (o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o) \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> -syntax "_Id" :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2_ =\<^bsub>_\<^esub>/ _)" [111, 0, 111] 110) +syntax "_Id" :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2_ =\<^bsub>_\<^esub>/ _)" [111, 0, 111] 110) translations "a =\<^bsub>A\<^esub> b" \<rightleftharpoons> "CONST Id A a b" @@ -71,7 +71,7 @@ Lemma (derive) pathcomp: shows "x =\<^bsub>A\<^esub> z" apply (equality \<open>p:_\<close>) - focus premises vars x p + focus prems vars x p apply (equality \<open>p:_\<close>) apply intro done @@ -158,9 +158,9 @@ Lemma (derive) pathcomp_assoc: "p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z" "r: z =\<^bsub>A\<^esub> w" shows "p \<bullet> (q \<bullet> r) = p \<bullet> q \<bullet> r" apply (equality \<open>p:_\<close>) - focus premises vars x p + focus prems vars x p apply (equality \<open>p:_\<close>) - focus premises vars x p + focus prems vars x p apply (equality \<open>p:_\<close>) apply (reduce; intros) done @@ -200,7 +200,7 @@ Lemma (derive) ap_pathcomp: shows "f[p \<bullet> q] = f[p] \<bullet> f[q]" apply (equality \<open>p:_\<close>) - focus premises vars x p + focus prems vars x p apply (equality \<open>p:_\<close>) apply (reduce; intro) done @@ -302,7 +302,7 @@ Lemma (derive) transport_pathcomp: "p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z" shows "trans P q (trans P p u) = trans P (p \<bullet> q) u" apply (equality \<open>p:_\<close>) - focus premises vars x p + focus prems vars x p apply (equality \<open>p:_\<close>) apply (reduce; intros) done @@ -430,4 +430,5 @@ Lemma (derive) apd_ap: shows "apd f p = trans_const B p (f x) \<bullet> f[p]" by (equality \<open>p:_\<close>) (reduce; intro) + end |