diff options
| author | Josh Chen | 2019-02-05 18:32:43 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-02-05 18:32:43 +0100 |
| commit | 64d2a5c60acce40113362c9d7eca8cd633362d23 (patch) | |
| tree | 29e953d8b4d423c881050a430e36f1f13dbe4543 | |
| parent | 9d21e7e4ca3f22055acf72f15f19d4c9248882ca (diff) | |
Add cong named theorem for congruence rules
| -rw-r--r-- | HoTT_Base.thy | 9 | ||||
| -rw-r--r-- | Prod.thy | 5 |
2 files changed, 9 insertions, 5 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 88cf986..e74ef31 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -68,16 +68,19 @@ text \<open>We use the notation @{prop "B: A \<leadsto> U i"} to abbreviate type section \<open>Named theorems\<close> -named_theorems comp named_theorems form +named_theorems comp +named_theorems cong text \<open> The named theorems above will be used by proof methods defined in @{file HoTT_Methods.thy}. -@{attribute comp} declares computation rules, which are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting. - @{attribute form} declares type formation rules. These are mainly used by the \<open>cumulativity\<close> method, which lifts types into higher universes. + +@{attribute comp} declares computation rules, which are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting. + +@{attribute cong} declares congruence rules, the definitional equality rules of the type theory. \<close> (* Todo: Set up the Simplifier! *) @@ -66,6 +66,7 @@ Note that this is a separate rule from function extensionality. lemmas Prod_form [form] lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim lemmas Prod_comp [comp] = Prod_cmp Prod_uniq +lemmas Prod_cong [cong] = Prod_form_eq Prod_intro_eq section \<open>Function composition\<close> @@ -98,12 +99,12 @@ end lemma compose_assoc: assumes "A: U i" "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: TT x: C. D x" shows "compose A (compose B h g) f \<equiv> compose A h (compose A g f)" -by (derive lems: assms Prod_intro_eq) +by (derive lems: assms cong) lemma compose_comp: assumes "A: U i" and "\<And>x. x: A \<Longrightarrow> b x: B" and "\<And>x. x: B \<Longrightarrow> c x: C x" shows "(,\\x: B. c x) o (,\\x: A. b x) \<equiv> ,\\x: A. c (b x)" -by (derive lems: assms Prod_intro_eq) +by (derive lems: assms cong) abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> ,\\x: A. x" |