diff options
author | Josh Chen | 2018-09-19 11:57:22 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-19 11:57:22 +0200 |
commit | 1305c6beca2448156b61649da1a719d055aaf7f7 (patch) | |
tree | 81f1ea81350a70cfa27269c41f59e8640f9fd65a | |
parent | f602cb54b39b3c1bb4f755db09bdeeb2f31a9559 (diff) |
Not sure what advantage is provided by having eta-expanded forms in the rules. Removing for now.
-rw-r--r-- | Coprod.thy | 6 | ||||
-rw-r--r-- | Equal.thy | 4 | ||||
-rw-r--r-- | Nat.thy | 6 | ||||
-rw-r--r-- | Prod.thy | 4 | ||||
-rw-r--r-- | Sum.thy | 4 |
5 files changed, 12 insertions, 12 deletions
@@ -28,19 +28,19 @@ where u: A + B; C: A + B \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> c x: C (inl x); - \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda> x. c x) (\<lambda>y. d y) u: C u" and + \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d u: C u" and Coprod_comp_inl: "\<lbrakk> a: A; C: A + B \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> c x: C (inl x); - \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda>x. c x) (\<lambda>y. d y) (inl a) \<equiv> c a" and + \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inl a) \<equiv> c a" and Coprod_comp_inr: "\<lbrakk> b: B; C: A + B \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> c x: C (inl x); - \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda>x. c x) (\<lambda>y. d y) (inr b) \<equiv> d b" + \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inr b) \<equiv> d b" lemmas Coprod_form [form] lemmas Coprod_routine [intro] = Coprod_form Coprod_intro_inl Coprod_intro_inr Coprod_elim @@ -37,12 +37,12 @@ axiomatization where x: A; y: A; \<And>x. x: A \<Longrightarrow> f x: C x x (refl x); - \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) p : C x y p" and + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= f p : C x y p" and Equal_comp: "\<lbrakk> a: A; \<And>x. x: A \<Longrightarrow> f x: C x x (refl x); - \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a" + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= f (refl a) \<equiv> f a" lemmas Equal_form [form] lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim @@ -28,18 +28,18 @@ where a: C 0; n: \<nat>; C: \<nat> \<longrightarrow> U i; - \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a n: C n" and + \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a n: C n" and Nat_comp_0: "\<lbrakk> a: C 0; C: \<nat> \<longrightarrow> U i; - \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a 0 \<equiv> a" and + \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a 0 \<equiv> a" and Nat_comp_succ: "\<lbrakk> a: C 0; n: \<nat>; C: \<nat> \<longrightarrow> U i; - \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)" + \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)" lemmas Nat_form [form] lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim @@ -20,8 +20,8 @@ axiomatization appl :: "[t, t] \<Rightarrow> t" ("(1_`/_)" [105, 106] 105) \<comment> \<open>Application binds tighter than abstraction.\<close> syntax - "_prod" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Prod>_:_./ _)" 30) - "_prod_ascii" :: "[idt, t, t] \<Rightarrow> t" ("(3II _:_./ _)" 30) + "_prod" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Prod>_: _./ _)" 30) + "_prod_ascii" :: "[idt, t, t] \<Rightarrow> t" ("(3II _: _./ _)" 30) text \<open>The translations below bind the variable @{term x} in the expressions @{term B} and @{term b}.\<close> @@ -38,14 +38,14 @@ axiomatization where Sum_elim: "\<lbrakk> p: \<Sum>x:A. B x; C: \<Sum>x:A. B x \<longrightarrow> U i; - \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> (\<lambda>x y. f x y) p: C p" and + \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> f p: C p" and Sum_comp: "\<lbrakk> a: A; b: B a; B: A \<longrightarrow> U i; C: \<Sum>x:A. B x \<longrightarrow> U i; - \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> (\<lambda>x y. f x y) <a,b> \<equiv> f a b" and + \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> f <a,b> \<equiv> f a b" and \<comment> \<open>Congruence rules\<close> |