diff options
| -rw-r--r-- | spartan/theories/Identity.thy | 2 | ||||
| -rw-r--r-- | spartan/theories/Spartan.thy | 12 |
2 files changed, 6 insertions, 8 deletions
diff --git a/spartan/theories/Identity.thy b/spartan/theories/Identity.thy index 0edf20e..19b8b7a 100644 --- a/spartan/theories/Identity.thy +++ b/spartan/theories/Identity.thy @@ -261,7 +261,7 @@ Lemma transport_comp [comps]: "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i" shows "trans P (refl a) \<equiv> id (P a)" - unfolding transport_def id_def by reduce + unfolding transport_def by reduce \<comment> \<open>TODO: Build transport automation!\<close> diff --git a/spartan/theories/Spartan.thy b/spartan/theories/Spartan.thy index ac12937..a79f209 100644 --- a/spartan/theories/Spartan.thy +++ b/spartan/theories/Spartan.thy @@ -242,7 +242,7 @@ setup \<open> ctxt addSolver (mk_solver "" typechk_tac)) \<close> -method reduce uses add = (simp add: comps add | subst comps, reduce add: add)+ +method reduce uses add = (simp add: comps add | subst comps)+ section \<open>Implicit notations\<close> @@ -355,23 +355,21 @@ translations "g \<circ> f" \<leftharpoondown> "g \<circ>\<^bsub>A\<^esub> f" subsection \<open>Identity function\<close> -definition id where "id A \<equiv> \<lambda>x: A. x" +abbreviation id where "id A \<equiv> \<lambda>x: A. x" lemma - idI [typechk]: "A: U i \<Longrightarrow> id A: A \<rightarrow> A" and - id_comp [comps]: "x: A \<Longrightarrow> (id A) x \<equiv> x" - unfolding id_def by reduce + id_type[typechk]: "A: U i \<Longrightarrow> id A: A \<rightarrow> A" and + id_comp [comps]: "x: A \<Longrightarrow> (id A) x \<equiv> x" \<comment> \<open>for the occasional manual rewrite\<close> + by reduce lemma id_left [comps]: assumes "f: A \<rightarrow> B" "A: U i" "B: U i" shows "(id B) \<circ>\<^bsub>A\<^esub> f \<equiv> f" - unfolding id_def by (subst eta_exp[of f]) (reduce, rule eta) lemma id_right [comps]: assumes "f: A \<rightarrow> B" "A: U i" "B: U i" shows "f \<circ>\<^bsub>A\<^esub> (id A) \<equiv> f" - unfolding id_def by (subst eta_exp[of f]) (reduce, rule eta) lemma id_U [typechk]: |