aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--EqualProps.thy6
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: