diff options
| author | Josh Chen | 2018-08-17 13:58:26 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-17 13:58:26 +0200 |
| commit | 6608e0a3d48aae26f84087da5e4d60da8341bca5 (patch) | |
| tree | 7e1127d9c5080042521c716095c4eb6475c30c67 | |
| parent | a7806604105ebf09af4237fe338c0cfcf6ebb463 (diff) | |
Axiomatizations should be definitions
| -rw-r--r-- | EqualProps.thy | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index 5eea920..81f038f 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -15,8 +15,7 @@ begin section \<open>Symmetry / Path inverse\<close> -axiomatization inv :: "Term \<Rightarrow> Term" ("_\<inverse>" [1000] 1000) - where inv_def: "inv \<equiv> \<lambda>p. ind\<^sub>= (\<lambda>x. refl(x)) p" +definition inv :: "Term \<Rightarrow> Term" ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. refl(x)) p" text " In the proof below we begin by using path induction on \<open>p\<close> with the application of \<open>rule Equal_elim\<close>, telling Isabelle the specific substitutions to use. @@ -48,8 +47,7 @@ text " Raw composition function, of type \<open>\<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close> polymorphic over the type \<open>A\<close>. " -axiomatization rpathcomp :: Term where - rpathcomp_def: "rpathcomp \<equiv> \<^bold>\<lambda>x y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= (\<lambda>x. refl(x)) q) p" +definition rpathcomp :: Term where "rpathcomp \<equiv> \<^bold>\<lambda>x y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= (\<lambda>x. refl(x)) q) p" text " More complicated proofs---the nested path inductions require more explicit step-by-step rule applications: |