From f46df86db9308dde29e0e5f97f54546ea1dc34bf Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 18 Jan 2021 23:49:13 +0000 Subject: Swapped notation for metas (now ?) and holes (now {}), other notation and name changes. --- hott/Equivalence.thy | 35 +++++++++++------- hott/Identity.thy | 92 +++++++++++++++++++++++----------------------- hott/List+.thy | 18 --------- hott/List_HoTT.thy | 18 +++++++++ hott/Nat.thy | 14 +++---- spartan/core/Spartan.thy | 85 +++++++++++++++++++----------------------- spartan/core/calc.ML | 87 +++++++++++++++++++++++++++++++++++++++++++ spartan/core/congruence.ML | 82 ----------------------------------------- spartan/core/rewrite.ML | 4 +- spartan/lib/List.thy | 14 +++---- spartan/lib/Maybe.thy | 4 +- spartan/lib/Prelude.thy | 2 +- 12 files changed, 229 insertions(+), 226 deletions(-) delete mode 100644 hott/List+.thy create mode 100644 hott/List_HoTT.thy create mode 100644 spartan/core/calc.ML delete mode 100644 spartan/core/congruence.ML diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index 99300a0..379dc81 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -8,7 +8,7 @@ section \Homotopy\ definition "homotopy A B f g \ \x: A. f `x =\<^bsub>B x\<^esub> g `x" definition homotopy_i (infix "~" 100) - where [implicit]: "f ~ g \ homotopy ? ? f g" + where [implicit]: "f ~ g \ homotopy {} {} f g" translations "f ~ g" \ "CONST homotopy A B f g" @@ -79,7 +79,7 @@ Lemma (def) htrans: section \Rewriting homotopies\ -congruence "f ~ g" rhs g +calc "f ~ g" rhs g lemmas homotopy_sym [sym] = hsym[rotated 4] and @@ -129,7 +129,6 @@ Lemma funcomp_right_htpy: method lhtpy = rule funcomp_left_htpy[rotated 6] method rhtpy = rule funcomp_right_htpy[rotated 6] - Lemma (def) commute_homotopy: assumes "A: U i" "B: U i" @@ -152,8 +151,16 @@ Corollary (def) commute_homotopy': "H: f ~ (id A)" shows "H (f x) = f [H x]" proof - - (*FIXME: Bug; if the following type declaration isn't made then bad things - happen on the next lines.*) + (* Rewrite the below proof + have *: "H (f x) \ (id A)[H x] = f[H x] \ H x" + using \H:_\ unfolding homotopy_def by (rule commute_homotopy) + + thus "H (f x) = f[H x]" + apply (pathcomp_cancelr) + ... + *) + (*FUTURE: Because we don't have very good normalization integrated into + things yet, we need to manually unfold the type of H.*) from \H: f ~ id A\ have [type]: "H: \x: A. f x = x" by (reduce add: homotopy_def) @@ -161,7 +168,7 @@ Corollary (def) commute_homotopy': by (rule left_whisker, transport eq: ap_id, refl) also have [simplified id_comp]: "H (f x) \ (id A)[H x] = f[H x] \ H x" by (rule commute_homotopy) - finally have "{}" by this + finally have "?" by this thus "H (f x) = f [H x]" by pathcomp_cancelr (fact, typechk+) qed @@ -181,7 +188,7 @@ Lemma is_qinv_type [type]: by typechk definition is_qinv_i ("is'_qinv") - where [implicit]: "is_qinv f \ Equivalence.is_qinv ? ? f" + where [implicit]: "is_qinv f \ Equivalence.is_qinv {} {} f" no_translations "is_qinv f" \ "CONST Equivalence.is_qinv A B f" @@ -241,7 +248,7 @@ Lemma (def) funcomp_is_qinv: have "(finv \ ginv) \ g \ f ~ finv \ (ginv \ g) \ f" by reduce refl also have ".. ~ finv \ id B \ f" by (rhtpy, lhtpy) fact also have ".. ~ id A" by reduce fact - finally show "{}" by this + finally show "?" by this qed show "(g \ f) \ finv \ ginv ~ id C" @@ -249,7 +256,7 @@ Lemma (def) funcomp_is_qinv: have "(g \ f) \ finv \ ginv ~ g \ (f \ finv) \ ginv" by reduce refl also have ".. ~ g \ id B \ ginv" by (rhtpy, lhtpy) fact also have ".. ~ id C" by reduce fact - finally show "{}" by this + finally show "?" by this qed qed done @@ -267,7 +274,7 @@ Lemma is_biinv_type [type]: unfolding is_biinv_def by typechk definition is_biinv_i ("is'_biinv") - where [implicit]: "is_biinv f \ Equivalence.is_biinv ? ? f" + where [implicit]: "is_biinv f \ Equivalence.is_biinv {} {} f" translations "is_biinv f" \ "CONST Equivalence.is_biinv A B f" @@ -279,8 +286,8 @@ Lemma is_biinvI: shows "is_biinv f" unfolding is_biinv_def proof intro - show ": {}" by typechk - show ": {}" by typechk + show ": \g: B \ A. g \ f ~ id A" by typechk + show ": \g: B \ A. f \ g ~ id B" by typechk qed Lemma is_biinv_components [type]: @@ -408,7 +415,7 @@ text \ Lemma (def) equiv_if_equal: assumes "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B" - shows ": A \ B" + shows ": A \ B" unfolding equivalence_def apply intro defer \<^item> apply (eq p) @@ -422,7 +429,7 @@ Lemma (def) equiv_if_equal: using [[solve_side_conds=1]] apply (rewrite transport_comp) \ by (rule Ui_in_USi) - \ by reduce (rule in_USi_if_in_Ui) + \ by reduce (rule U_lift) \ by reduce (rule id_is_biinv) done done diff --git a/hott/Identity.thy b/hott/Identity.thy index dc27ee8..0a31dc7 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -20,7 +20,7 @@ syntax "_Id" :: \o \ o \ o \ o\ translations "a =\<^bsub>A\<^esub> b" \ "CONST Id A a b" axiomatization where - \ \Here `A: U i` comes last because A is often implicit\ + \ \Here \A: U i\ comes last because A is often implicit\ IdF: "\a: A; b: A; A: U i\ \ a =\<^bsub>A\<^esub> b: U i" and IdI: "a: A \ refl a: a =\<^bsub>A\<^esub> a" and @@ -49,8 +49,8 @@ lemmas section \Path induction\ -\ \With `p: x = y` in the context the invokation `eq p` is essentially - `elim p x y`, with some extra bits before and after.\ +\ \With \p: x = y\ in the context the invokation \eq p\ is essentially + \elim p x y\, with some extra bits before and after.\ method_setup eq = \Args.term >> (fn tm => K (CONTEXT_METHOD ( @@ -109,13 +109,13 @@ method pathcomp for p q :: o = rule pathcomp[where ?p=p and ?q=q] section \Notation\ definition Id_i (infix "=" 110) - where [implicit]: "Id_i x y \ x =\<^bsub>?\<^esub> y" + where [implicit]: "Id_i x y \ x =\<^bsub>{}\<^esub> y" definition pathinv_i ("_\" [1000]) - where [implicit]: "pathinv_i p \ pathinv ? ? ? p" + where [implicit]: "pathinv_i p \ pathinv {} {} {} p" definition pathcomp_i (infixl "\" 121) - where [implicit]: "pathcomp_i p q \ pathcomp ? ? ? ? p q" + where [implicit]: "pathcomp_i p q \ pathcomp {} {} {} {} p q" translations "x = y" \ "x =\<^bsub>A\<^esub> y" @@ -125,7 +125,7 @@ translations section \Calculational reasoning\ -congruence "x = y" rhs y +calc "x = y" rhs y lemmas [sym] = pathinv[rotated 3] and @@ -144,8 +144,8 @@ Lemma (def) pathcomp_refl: shows "p \ (refl y) = p" by (eq p) (reduce, refl) -definition [implicit]: "lu p \ refl_pathcomp ? ? ? p" -definition [implicit]: "ru p \ pathcomp_refl ? ? ? p" +definition [implicit]: "lu p \ refl_pathcomp {} {} {} p" +definition [implicit]: "ru p \ pathcomp_refl {} {} {} p" translations "CONST lu p" \ "CONST refl_pathcomp A x y p" @@ -204,7 +204,7 @@ Lemma (def) ap: by (eq p) intro definition ap_i ("_[_]" [1000, 0]) - where [implicit]: "ap_i f p \ ap ? ? ? ? f p" + where [implicit]: "ap_i f p \ ap {} {} {} {} f p" translations "f[p]" \ "CONST ap A B x y f p" @@ -265,17 +265,17 @@ Lemma (def) transport: shows "P x \ P y" by (eq p) intro -definition transport_i ("trans") - where [implicit]: "trans P p \ transport ? P ? ? p" +definition transport_i ("transp") + where [implicit]: "transp P p \ transport {} P {} {} p" -translations "trans P p" \ "CONST transport A P x y p" +translations "transp P p" \ "CONST transport A P x y p" Lemma transport_comp [comp]: assumes "a: A" "A: U i" "\x. x: A \ P x: U i" - shows "trans P (refl a) \ id (P a)" + shows "transp P (refl a) \ id (P a)" unfolding transport_def by reduce Lemma apply_transport: @@ -284,7 +284,7 @@ Lemma apply_transport: "x: A" "y: A" "p: y =\<^bsub>A\<^esub> x" "u: P x" - shows "trans P p\ u: P y" + shows "transp P p\ u: P y" by typechk method transport uses eq = (rule apply_transport[OF _ _ _ _ eq]) @@ -304,7 +304,7 @@ Lemma (def) pathcomp_cancel_left: by (transport eq: pathcomp_assoc, transport eq: inv_pathcomp, transport eq: refl_pathcomp) refl - finally show "{}" by this + finally show "?" by this qed Lemma (def) pathcomp_cancel_right: @@ -323,7 +323,7 @@ Lemma (def) pathcomp_cancel_right: transport eq: pathcomp_assoc[symmetric], transport eq: pathcomp_inv, transport eq: pathcomp_refl) refl - finally show "{}" by this + finally show "?" by this qed method pathcomp_cancell = rule pathcomp_cancel_left[rotated 7] @@ -335,7 +335,7 @@ Lemma (def) transport_left_inv: "\x. x: A \ P x: U i" "x: A" "y: A" "p: x = y" - shows "(trans P p\) \ (trans P p) = id (P x)" + shows "(transp P p\) \ (transp P p) = id (P x)" by (eq p) (reduce, refl) Lemma (def) transport_right_inv: @@ -344,7 +344,7 @@ Lemma (def) transport_right_inv: "\x. x: A \ P x: U i" "x: A" "y: A" "p: x = y" - shows "(trans P p) \ (trans P p\) = id (P y)" + shows "(transp P p) \ (transp P p\) = id (P y)" by (eq p) (reduce, refl) Lemma (def) transport_pathcomp: @@ -354,11 +354,11 @@ Lemma (def) transport_pathcomp: "x: A" "y: A" "z: A" "u: P x" "p: x = y" "q: y = z" - shows "trans P q (trans P p u) = trans P (p \ q) u" + shows "transp P q (transp P p u) = transp P (p \ q) u" proof (eq p) fix x q u assuming "x: A" "q: x = z" "u: P x" - show "trans P q (trans P (refl x) u) = trans P ((refl x) \ q) u" + show "transp P q (transp P (refl x) u) = transp P ((refl x) \ q) u" by (eq q) (reduce, refl) qed @@ -370,7 +370,7 @@ Lemma (def) transport_compose_typefam: "x: A" "y: A" "p: x = y" "u: P (f x)" - shows "trans (fn x. P (f x)) p u = trans P f[p] u" + shows "transp (fn x. P (f x)) p u = transp P f[p] u" by (eq p) (reduce, refl) Lemma (def) transport_function_family: @@ -382,7 +382,7 @@ Lemma (def) transport_function_family: "x: A" "y: A" "u: P x" "p: x = y" - shows "trans Q p ((f x) u) = (f y) (trans P p u)" + shows "transp Q p ((f x) u) = (f y) (transp P p u)" by (eq p) (reduce, refl) Lemma (def) transport_const: @@ -390,19 +390,19 @@ Lemma (def) transport_const: "A: U i" "B: U i" "x: A" "y: A" "p: x = y" - shows "\b: B. trans (fn _. B) p b = b" + shows "\b: B. transp (fn _. B) p b = b" by intro (eq p, reduce, refl) -definition transport_const_i ("trans'_const") - where [implicit]: "trans_const B p \ transport_const ? B ? ? p" +definition transport_const_i ("transp'_c") + where [implicit]: "transp_c B p \ transport_const {} B {} {} p" -translations "trans_const B p" \ "CONST transport_const A B x y p" +translations "transp_c B p" \ "CONST transport_const A B x y p" Lemma transport_const_comp [comp]: assumes "x: A" "b: B" "A: U i" "B: U i" - shows "trans_const B (refl x) b \ refl b" + shows "transp_c B (refl x) b \ refl b" unfolding transport_const_def by reduce Lemma (def) pathlift: @@ -412,11 +412,11 @@ Lemma (def) pathlift: "x: A" "y: A" "p: x = y" "u: P x" - shows " = " + shows " = " by (eq p) (reduce, refl) definition pathlift_i ("lift") - where [implicit]: "lift P p u \ pathlift ? P ? ? p u" + where [implicit]: "lift P p u \ pathlift {} P {} {} p u" translations "lift P p u" \ "CONST pathlift A P x y p u" @@ -449,11 +449,11 @@ Lemma (def) apd: "f: \x: A. P x" "x: A" "y: A" "p: x = y" - shows "trans P p (f x) = f y" + shows "transp P p (f x) = f y" by (eq p) (reduce, refl) definition apd_i ("apd") - where [implicit]: "apd f p \ Identity.apd ? ? f ? ? p" + where [implicit]: "apd f p \ Identity.apd {} {} f {} {} p" translations "apd f p" \ "CONST Identity.apd A P f x y p" @@ -472,7 +472,7 @@ Lemma (def) apd_ap: "f: A \ B" "x: A" "y: A" "p: x = y" - shows "apd f p = trans_const B p (f x) \ f[p]" + shows "apd f p = transp_c B p (f x) \ f[p]" by (eq p) (reduce, refl) @@ -488,7 +488,7 @@ Lemma (def) right_whisker: have "s \ refl x = s" by (rule pathcomp_refl) also have ".. = t" by fact also have ".. = t \ refl x" by (rule pathcomp_refl[symmetric]) - finally show "{}" by this + finally show "?" by this qed done @@ -502,15 +502,15 @@ Lemma (def) left_whisker: have "refl x \ s = s" by (rule refl_pathcomp) also have ".. = t" by fact also have ".. = refl x \ t" by (rule refl_pathcomp[symmetric]) - finally show "{}" by this + finally show "?" by this qed done definition right_whisker_i (infix "\\<^sub>r" 121) - where [implicit]: "\ \\<^sub>r r \ right_whisker ? ? ? ? ? ? r \" + where [implicit]: "\ \\<^sub>r r \ right_whisker {} {} {} {} {} {} r \" definition left_whisker_i (infix "\\<^sub>l" 121) - where [implicit]: "r \\<^sub>l \ \ left_whisker ? ? ? ? ? ? r \" + where [implicit]: "r \\<^sub>l \ \ left_whisker {} {} {} {} {} {} r \" translations "\ \\<^sub>r r" \ "CONST right_whisker A a b c p q r \" @@ -532,8 +532,8 @@ method right_whisker = (rule right_whisker) section \Horizontal path-composition\ -text \Conditions under which horizontal path-composition is defined.\ locale horiz_pathcomposable = +\ \Conditions under which horizontal path-composition is defined.\ fixes i A a b c p q r s assumes [type]: @@ -615,17 +615,17 @@ Lemma (def) pathcomp_eq_horiz_pathcomp: have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) - finally have eq\: "{} = \" by this + finally have eq\: "? = \" by this have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) - finally have eq\: "{} = \" by this + finally have eq\: "? = \" by this have "refl (refl a) \ \ \ refl (refl a) \ (refl (refl a) \ \ \ refl (refl a)) - = \ \ {}" by right_whisker (fact eq\) + = \ \ ?" by right_whisker (fact eq\) also have ".. = \ \ \" by left_whisker (fact eq\) - finally show "{} = \ \ \" by this + finally show "? = \ \ \" by this qed Lemma (def) pathcomp_eq_horiz_pathcomp': @@ -637,17 +637,17 @@ Lemma (def) pathcomp_eq_horiz_pathcomp': have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) - finally have eq\: "{} = \" by this + finally have eq\: "? = \" by this have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) - finally have eq\: "{} = \" by this + finally have eq\: "? = \" by this have "refl (refl a) \ \ \ refl (refl a) \ (refl (refl a) \ \ \ refl (refl a)) - = \ \ {}" by right_whisker (fact eq\) + = \ \ ?" by right_whisker (fact eq\) also have ".. = \ \ \" by left_whisker (fact eq\) - finally show "{} = \ \ \" by this + finally show "? = \ \ \" by this qed Lemma (def) eckmann_hilton: diff --git a/hott/List+.thy b/hott/List+.thy deleted file mode 100644 index 869d667..0000000 --- a/hott/List+.thy +++ /dev/null @@ -1,18 +0,0 @@ -theory "List+" -imports - Spartan.List - Nat - -begin - -section \Length\ - -definition [implicit]: "len \ ListRec ? Nat 0 (fn _ _ rec. suc rec)" - -experiment begin - Lemma "len [] \ ?n" by (subst comp; typechk?) - Lemma "len [0, suc 0, suc (suc 0)] \ ?n" by (subst comp; typechk?)+ -end - - -end diff --git a/hott/List_HoTT.thy b/hott/List_HoTT.thy new file mode 100644 index 0000000..9bd1517 --- /dev/null +++ b/hott/List_HoTT.thy @@ -0,0 +1,18 @@ +theory List_HoTT +imports + Spartan.List + Nat + +begin + +section \Length\ + +definition [implicit]: "len \ ListRec {} Nat 0 (fn _ _ rec. suc rec)" + +experiment begin + Lemma "len [] \ ?n" by (subst comp; typechk?) + Lemma "len [0, suc 0, suc (suc 0)] \ ?n" by (subst comp; typechk?)+ +end + + +end diff --git a/hott/Nat.thy b/hott/Nat.thy index f45387c..1aa7932 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -115,7 +115,7 @@ Lemma (def) add_comm: proof reduce have "suc (m + n) = suc (n + m)" by (eq ih) refl also have ".. = suc n + m" by (transport eq: suc_add) refl - finally show "{}" by this + finally show "?" by this qed done @@ -152,7 +152,7 @@ Lemma (def) zero_mul: proof reduce have "0 + 0 * n = 0 + 0 " by (eq ih) refl also have ".. = 0" by reduce refl - finally show "{}" by this + finally show "?" by this qed done @@ -163,9 +163,9 @@ Lemma (def) suc_mul: \<^item> by reduce refl \<^item> vars n ih proof (reduce, transport eq: \ih:_\) - have "suc m + (m * n + n) = suc (m + {})" by (rule suc_add) + have "suc m + (m * n + n) = suc (m + ?)" by (rule suc_add) also have ".. = suc (m + m * n + n)" by (transport eq: add_assoc) refl - finally show "{}" by this + finally show "?" by this qed done @@ -180,7 +180,7 @@ Lemma (def) mul_dist_add: also have ".. = l + l * m + l * n" by (rule add_assoc) also have ".. = l * m + l + l * n" by (transport eq: add_comm) refl also have ".. = l * m + (l + l * n)" by (transport eq: add_assoc) refl - finally show "{}" by this + finally show "?" by this qed done @@ -193,7 +193,7 @@ Lemma (def) mul_assoc: proof reduce have "l * (m + m * n) = l * m + l * (m * n)" by (rule mul_dist_add) also have ".. = l * m + l * m * n" by (transport eq: \ih:_\) refl - finally show "{}" by this + finally show "?" by this qed done @@ -207,7 +207,7 @@ Lemma (def) mul_comm: have "suc n * m = n * m + m" by (rule suc_mul) also have ".. = m + m * n" by (transport eq: \ih:_\, transport eq: add_comm) refl - finally show "{}" by this + finally show "?" by this qed done diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index 6b2ed58..ffe3778 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -9,23 +9,18 @@ keywords "Theorem" "Lemma" "Corollary" "Proposition" "Definition" :: thy_goal_stmt and "assuming" :: prf_asm % "proof" and "focus" "\<^item>" "\<^enum>" "\" "\" "~" :: prf_script_goal % "proof" and - "congruence" "print_coercions" :: thy_decl and + "calc" "print_coercions" :: thy_decl and "rhs" "def" "vars" :: quasi_command begin - -section \Prelude\ - -paragraph \Set up the meta-logic just so.\ - -paragraph \Notation.\ +section \Notation\ declare [[eta_contract=false]] text \ - Rebind notation for meta-lambdas since we want to use `\` for the object - lambdas. Meta-functions now use the binder `fn`. +Rebind notation for meta-lambdas since we want to use \\\ for the object +lambdas. Metafunctions now use the binder \fn\. \ setup \ let @@ -41,34 +36,31 @@ in end \ -syntax "_dollar" :: \logic \ logic \ logic\ (infixr "$" 3) +syntax "_app" :: \logic \ logic \ logic\ (infixr "$" 3) translations "a $ b" \ "a (b)" abbreviation (input) K where "K x \ fn _. x" -paragraph \ - Deeply embed dependent type theory: meta-type of expressions, and typing - judgment. + +section \Metalogic\ + +text \ +HOAS embedding of dependent type theory: metatype of expressions, and typing +judgment. \ typedecl o consts has_type :: \o \ o \ prop\ ("(2_:/ _)" 999) -text \Type annotations for type-checking and inference.\ - -definition anno :: \o \ o \ o\ ("'(_ : _')") - where "(a : A) \ a" if "a: A" - -lemma anno: "a: A \ (a : A): A" - by (unfold anno_def) - section \Axioms\ subsection \Universes\ -typedecl lvl \ \Universe levels\ +text \\-many cumulative Russell universes.\ + +typedecl lvl axiomatization O :: \lvl\ and @@ -81,16 +73,15 @@ axiomatization axiomatization U :: \lvl \ o\ where Ui_in_Uj: "i < j \ U i: U j" and - in_Uj_if_in_Ui: "A: U i \ i < j \ A: U j" + U_cumul: "A: U i \ i < j \ A: U j" lemma Ui_in_USi: "U i: U (S i)" by (rule Ui_in_Uj, rule lt_S) -lemma in_USi_if_in_Ui: +lemma U_lift: "A: U i \ A: U (S i)" - by (erule in_Uj_if_in_Ui, rule lt_S) - + by (erule U_cumul, rule lt_S) subsection \\-type\ @@ -134,7 +125,6 @@ axiomatization where lam_cong: "\\x. x: A \ b x \ c x; A: U i\ \ \x: A. b x \ \x: A. c x" - subsection \\-type\ axiomatization @@ -207,7 +197,7 @@ lemma sub: shows "a: A'" using assms by simp -\ \Basic substitution of definitional equalities\ +\ \Basic rewriting of computational equality\ ML_file \~~/src/Tools/misc_legacy.ML\ ML_file \~~/src/Tools/IsaPlanner/isand.ML\ ML_file \~~/src/Tools/IsaPlanner/rw_inst.ML\ @@ -305,7 +295,7 @@ method_setup this = subsection \Rewriting\ -consts rewrite_HOLE :: "'a::{}" ("\") +consts rewrite_hole :: "'a::{}" ("\") lemma eta_expand: fixes f :: "'a::{} \ 'b::{}" @@ -331,28 +321,28 @@ lemma imp_cong_eq: ML_file \~~/src/HOL/Library/cconv.ML\ ML_file \rewrite.ML\ -\ \\reduce\ computes terms via judgmental equalities\ +\ \\reduce\ simplifies terms via computational equalities\ method reduce uses add = changed \repeat_new \(simp add: comp add | subst comp); typechk?\\ -subsection \Congruence relations\ +subsection \Calculational reasoning\ consts "rhs" :: \'a\ ("..") -ML_file \congruence.ML\ +ML_file \calc.ML\ section \Implicits\ text \ - \?\ is used to mark implicit arguments in definitions, while \{}\ is expanded + \{}\ is used to mark implicit arguments in definitions, while \?\ is expanded immediately for elaboration in statements. \ consts - iarg :: \'a\ ("?") - hole :: \'b\ ("{}") + iarg :: \'a\ ("{}") + hole :: \'b\ ("?") ML_file \implicits.ML\ @@ -363,11 +353,12 @@ ML \val _ = Context.>> (Syntax_Phases.term_check 1 "" Implicits.make_holes text \Automatically insert inhabitation judgments where needed:\ syntax inhabited :: \o \ prop\ ("(_)") -translations "inhabited A" \ "CONST has_type {} A" +translations "inhabited A" \ "CONST has_type ? A" + -text \Implicit lambdas\ +subsection \Implicit lambdas\ -definition lam_i where [implicit]: "lam_i f \ lam ? f" +definition lam_i where [implicit]: "lam_i f \ lam {} f" syntax "_lam_i" :: \idts \ o \ o\ ("(2\_./ _)" 30) @@ -410,7 +401,7 @@ Lemma refine_codomain: Lemma lift_universe_codomain: assumes "A: U i" "f: A \ U j" shows "f: A \ U (S j)" - using in_USi_if_in_Ui[of "f {}"] + using U_lift by (rule refine_codomain) subsection \Function composition\ @@ -460,10 +451,10 @@ Lemma funcomp_apply_comp [comp]: shows "(g \\<^bsub>A\<^esub> f) x \ g (f x)" unfolding funcomp_def by reduce -text \Notation:\ +subsection \Notation\ definition funcomp_i (infixr "\" 120) - where [implicit]: "funcomp_i g f \ g \\<^bsub>?\<^esub> f" + where [implicit]: "funcomp_i g f \ g \\<^bsub>{}\<^esub> f" translations "g \ f" \ "g \\<^bsub>A\<^esub> f" @@ -520,10 +511,10 @@ Lemma snd_comp [comp]: subsection \Notation\ definition fst_i ("fst") - where [implicit]: "fst \ Spartan.fst ? ?" + where [implicit]: "fst \ Spartan.fst {} {}" definition snd_i ("snd") - where [implicit]: "snd \ Spartan.snd ? ?" + where [implicit]: "snd \ Spartan.snd {} {}" translations "fst" \ "CONST Spartan.fst A B" @@ -550,10 +541,10 @@ method snd for p::o = rule snd[where ?p=p] text \Double projections:\ -definition [implicit]: "p\<^sub>1\<^sub>1 p \ Spartan.fst ? ? (Spartan.fst ? ? p)" -definition [implicit]: "p\<^sub>1\<^sub>2 p \ Spartan.snd ? ? (Spartan.fst ? ? p)" -definition [implicit]: "p\<^sub>2\<^sub>1 p \ Spartan.fst ? ? (Spartan.snd ? ? p)" -definition [implicit]: "p\<^sub>2\<^sub>2 p \ Spartan.snd ? ? (Spartan.snd ? ? p)" +definition [implicit]: "p\<^sub>1\<^sub>1 p \ Spartan.fst {} {} (Spartan.fst {} {} p)" +definition [implicit]: "p\<^sub>1\<^sub>2 p \ Spartan.snd {} {} (Spartan.fst {} {} p)" +definition [implicit]: "p\<^sub>2\<^sub>1 p \ Spartan.fst {} {} (Spartan.snd {} {} p)" +definition [implicit]: "p\<^sub>2\<^sub>2 p \ Spartan.snd {} {} (Spartan.snd {} {} p)" translations "CONST p\<^sub>1\<^sub>1 p" \ "fst (fst p)" diff --git a/spartan/core/calc.ML b/spartan/core/calc.ML new file mode 100644 index 0000000..67dc7fc --- /dev/null +++ b/spartan/core/calc.ML @@ -0,0 +1,87 @@ +structure Calc = struct + +(* Calculational type context data + +A "calculational" type is a type expressing some congruence relation. In +particular, it has a notion of composition of terms that is often used to derive +proofs equationally. +*) + +structure RHS = Generic_Data ( + type T = (term * indexname) Termtab.table + val empty = Termtab.empty + val extend = I + val merge = Termtab.merge (Term.aconv o apply2 #1) +) + +fun register_rhs t var = + let + val key = Term.head_of t + val idxname = #1 (dest_Var var) + in + RHS.map (Termtab.update (key, (t, idxname))) + end + +fun lookup_calc ctxt t = + Termtab.lookup (RHS.get (Context.Proof ctxt)) (Term.head_of t) + + +(* Declaration *) + +local val Frees_to_Vars = + map_aterms (fn tm => + case tm of + Free (name, T) => Var (("*!"^name, 0), T) (*FIXME: Hacky naming!*) + | _ => tm) +in + +(*Declare the "right-hand side" of calculational types. Does not handle bound + variables, so no dependent RHS in declarations!*) +val _ = Outer_Syntax.local_theory \<^command_keyword>\calc\ + "declare right hand side of calculational type" + (Parse.term -- (\<^keyword>\rhs\ |-- Parse.term) >> + (fn (t_str, rhs_str) => fn lthy => + let + val (t, rhs) = apply2 (Frees_to_Vars o Syntax.read_term lthy) + (t_str, rhs_str) + in lthy |> + Local_Theory.background_theory ( + Context.theory_map (register_rhs t rhs)) + end)) + +end + + +(* Ditto "''" setup *) + +fun last_rhs ctxt = map_aterms (fn t => + case t of + Const (\<^const_name>\rhs\, _) => + let + val this_name = Name_Space.full_name (Proof_Context.naming_of ctxt) + (Binding.name Auto_Bind.thisN) + val this = #thms (the (Proof_Context.lookup_fact ctxt this_name)) + handle Option => [] + val rhs = + (case map Thm.prop_of this of + [prop] => + (let + val typ = Lib.type_of_typing (Logic.strip_assums_concl prop) + val (cong_pttrn, varname) = the (lookup_calc ctxt typ) + val unif_res = Pattern.unify (Context.Proof ctxt) + (cong_pttrn, typ) Envir.init + val rhs = #2 (the + (Vartab.lookup (Envir.term_env unif_res) varname)) + in + rhs + end handle Option => + error (".. can't match right-hand side of calculational type")) + | _ => Term.dummy) + in rhs end + | _ => t) + +val _ = Context.>> + (Syntax_Phases.term_check 5 "" (fn ctxt => map (last_rhs ctxt))) + + +end diff --git a/spartan/core/congruence.ML b/spartan/core/congruence.ML deleted file mode 100644 index d9f4ffa..0000000 --- a/spartan/core/congruence.ML +++ /dev/null @@ -1,82 +0,0 @@ -structure Congruence = struct - -(* Congruence context data *) - -structure RHS = Generic_Data ( - type T = (term * indexname) Termtab.table - val empty = Termtab.empty - val extend = I - val merge = Termtab.merge (Term.aconv o apply2 #1) -) - -fun register_rhs t var = - let - val key = Term.head_of t - val idxname = #1 (dest_Var var) - in - RHS.map (Termtab.update (key, (t, idxname))) - end - -fun lookup_congruence ctxt t = - Termtab.lookup (RHS.get (Context.Proof ctxt)) (Term.head_of t) - - -(* Congruence declarations *) - -local val Frees_to_Vars = - map_aterms (fn tm => - case tm of - Free (name, T) => Var (("*!"^name, 0), T) (*Hacky naming!*) - | _ => tm) -in - -(*Declare the "right-hand side" of types that are congruences. - Does not handle bound variables, so no dependent RHS in declarations!*) -val _ = Outer_Syntax.local_theory \<^command_keyword>\congruence\ - "declare right hand side of congruence" - (Parse.term -- (\<^keyword>\rhs\ |-- Parse.term) >> - (fn (t_str, rhs_str) => fn lthy => - let - val (t, rhs) = apply2 (Frees_to_Vars o Syntax.read_term lthy) - (t_str, rhs_str) - in lthy |> - Local_Theory.background_theory ( - Context.theory_map (register_rhs t rhs)) - end)) - -end - - -(* Calculational reasoning: ".." setup *) - -fun last_rhs ctxt = map_aterms (fn t => - case t of - Const (\<^const_name>\rhs\, _) => - let - val this_name = Name_Space.full_name (Proof_Context.naming_of ctxt) - (Binding.name Auto_Bind.thisN) - val this = #thms (the (Proof_Context.lookup_fact ctxt this_name)) - handle Option => [] - val rhs = - (case map Thm.prop_of this of - [prop] => - (let - val typ = Lib.type_of_typing (Logic.strip_assums_concl prop) - val (cong_pttrn, varname) = the (lookup_congruence ctxt typ) - val unif_res = Pattern.unify (Context.Proof ctxt) - (cong_pttrn, typ) Envir.init - val rhs = #2 (the - (Vartab.lookup (Envir.term_env unif_res) varname)) - in - rhs - end handle Option => - error (".. can't match right-hand side of congruence")) - | _ => Term.dummy) - in rhs end - | _ => t) - -val _ = Context.>> - (Syntax_Phases.term_check 5 "" (fn ctxt => map (last_rhs ctxt))) - - -end diff --git a/spartan/core/rewrite.ML b/spartan/core/rewrite.ML index 99c21b5..af70cfc 100644 --- a/spartan/core/rewrite.ML +++ b/spartan/core/rewrite.ML @@ -72,13 +72,13 @@ fun mk_hole i T = Var ((holeN, i), T) fun is_hole (Var ((name, _), _)) = (name = holeN) | is_hole _ = false -fun is_hole_const (Const (\<^const_name>\rewrite_HOLE\, _)) = true +fun is_hole_const (Const (\<^const_name>\rewrite_hole\, _)) = true | is_hole_const _ = false val hole_syntax = let (* Modified variant of Term.replace_hole *) - fun replace_hole Ts (Const (\<^const_name>\rewrite_HOLE\, T)) i = + fun replace_hole Ts (Const (\<^const_name>\rewrite_hole\, T)) i = (list_comb (mk_hole i (Ts ---> T), map_range Bound (length Ts)), i + 1) | replace_hole Ts (Abs (x, T, t)) i = let val (t', i') = replace_hole (T :: Ts) t i diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy index 83e5149..1501221 100644 --- a/spartan/lib/List.thy +++ b/spartan/lib/List.thy @@ -64,10 +64,10 @@ Lemma list_cases [cases]: section \Notation\ definition nil_i ("[]") - where [implicit]: "[] \ nil ?" + where [implicit]: "[] \ nil {}" definition cons_i (infixr "#" 120) - where [implicit]: "x # xs \ cons ? x xs" + where [implicit]: "x # xs \ cons {} x xs" translations "[]" \ "CONST List.nil A" @@ -99,8 +99,8 @@ proof (cases xs) show "\xs. xs: List A \ xs: List A" . qed -definition head_i ("head") where [implicit]: "head xs \ List.head ? xs" -definition tail_i ("tail") where [implicit]: "tail xs \ List.tail ? xs" +definition head_i ("head") where [implicit]: "head xs \ List.head {} xs" +definition tail_i ("tail") where [implicit]: "tail xs \ List.tail {} xs" translations "head" \ "CONST List.head A" @@ -137,7 +137,7 @@ Definition app: proof - show "x # rec: List A" by typechk qed done -definition app_i ("app") where [implicit]: "app xs ys \ List.app ? xs ys" +definition app_i ("app") where [implicit]: "app xs ys \ List.app {} xs ys" translations "app" \ "CONST List.app A" @@ -153,7 +153,7 @@ proof (elim xs) show "f x # ys: List B" by typechk qed -definition map_i ("map") where [implicit]: "map \ List.map ? ?" +definition map_i ("map") where [implicit]: "map \ List.map {} {}" translations "map" \ "CONST List.map A B" @@ -173,7 +173,7 @@ Definition rev: \<^item> vars x _ rec proof - show "app rec [x]: List A" by typechk qed done -definition rev_i ("rev") where [implicit]: "rev \ List.rev ?" +definition rev_i ("rev") where [implicit]: "rev \ List.rev {}" translations "rev" \ "CONST List.rev A" diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy index da22a4e..e06a07b 100644 --- a/spartan/lib/Maybe.thy +++ b/spartan/lib/Maybe.thy @@ -64,8 +64,8 @@ lemmas abbreviation "MaybeRec A C \ MaybeInd A (K C)" -definition none_i ("none") where [implicit]: "none \ Maybe.none ?" -definition some_i ("some") where [implicit]: "some a \ Maybe.some ? a" +definition none_i ("none") where [implicit]: "none \ Maybe.none {}" +definition some_i ("some") where [implicit]: "some a \ Maybe.some {} a" translations "none" \ "CONST Maybe.none A" diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy index c0abf31..0043c1e 100644 --- a/spartan/lib/Prelude.thy +++ b/spartan/lib/Prelude.thy @@ -139,7 +139,7 @@ lemmas subsection \Notation\ definition ifelse_i ("if _ then _ else _") - where [implicit]: "if x then a else b \ ifelse ? x a b" + where [implicit]: "if x then a else b \ ifelse {} x a b" translations "if x then a else b" \ "CONST ifelse C x a b" -- cgit v1.2.3