From aff3d43d9865e7b8d082f0c239d2c73eee1fb291 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 21 Jan 2021 00:52:13 +0000 Subject: renamings --- hott/Equivalence.thy | 58 +++--- hott/Identity.thy | 100 ++++----- hott/Nat.thy | 60 +++--- spartan/core/Spartan.thy | 26 +-- spartan/core/comp.ML | 468 ++++++++++++++++++++++++++++++++++++++++++ spartan/core/context_facts.ML | 1 + spartan/core/rewrite.ML | 465 ----------------------------------------- spartan/lib/List.thy | 6 +- spartan/lib/Maybe.thy | 4 +- spartan/lib/Prelude.thy | 6 +- 10 files changed, 595 insertions(+), 599 deletions(-) create mode 100644 spartan/core/comp.ML delete mode 100644 spartan/core/rewrite.ML diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index 379dc81..9fe11a7 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -88,12 +88,12 @@ lemmas Lemma id_funcomp_htpy: assumes "A: U i" "B: U i" "f: A \ B" shows "homotopy_refl A f: (id B) \ f ~ f" - by reduce + by compute Lemma funcomp_id_htpy: assumes "A: U i" "B: U i" "f: A \ B" shows "homotopy_refl A f: f \ (id A) ~ f" - by reduce + by compute Lemma funcomp_left_htpy: assumes @@ -105,7 +105,7 @@ Lemma funcomp_left_htpy: "H: g ~ g'" shows "(g \ f) ~ (g' \ f)" unfolding homotopy_def - apply (intro, reduce) + apply (intro, compute) apply (htpy H) done @@ -118,12 +118,12 @@ Lemma funcomp_right_htpy: "H: f ~ f'" shows "(g \ f) ~ (g \ f')" unfolding homotopy_def - proof (intro, reduce) + proof (intro, compute) fix x assuming "x: A" have *: "f x = f' x" by (htpy H) show "g (f x) = g (f' x)" - by (transport eq: *) refl + by (rewr eq: *) refl qed method lhtpy = rule funcomp_left_htpy[rotated 6] @@ -139,8 +139,8 @@ Lemma (def) commute_homotopy: shows "(H x) \ g[p] = f[p] \ (H y)" using \H:_\ unfolding homotopy_def - apply (eq p, reduce) - apply (transport eq: pathcomp_refl, transport eq: refl_pathcomp) + apply (eq p, compute) + apply (rewr eq: pathcomp_refl, rewr eq: refl_pathcomp) by refl Corollary (def) commute_homotopy': @@ -151,21 +151,13 @@ Corollary (def) commute_homotopy': "H: f ~ (id A)" shows "H (f x) = f [H x]" proof - - (* 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 + (*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) + by (compute add: homotopy_def) have "H (f x) \ H x = H (f x) \ (id A)[H x]" - by (rule left_whisker, transport eq: ap_id, refl) + by (rule left_whisker, rewr 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 @@ -198,7 +190,7 @@ Lemma (def) id_is_qinv: unfolding is_qinv_def proof intro show "id A: A \ A" by typechk - qed (reduce, intro; refl) + qed (compute, intro; refl) Lemma is_qinvI: assumes @@ -245,17 +237,17 @@ Lemma (def) funcomp_is_qinv: \<^item> proof intro show "(finv \ ginv) \ g \ f ~ id A" proof - - have "(finv \ ginv) \ g \ f ~ finv \ (ginv \ g) \ f" by reduce refl + have "(finv \ ginv) \ g \ f ~ finv \ (ginv \ g) \ f" by compute refl also have ".. ~ finv \ id B \ f" by (rhtpy, lhtpy) fact - also have ".. ~ id A" by reduce fact + also have ".. ~ id A" by compute fact finally show "?" by this qed show "(g \ f) \ finv \ ginv ~ id C" proof - - have "(g \ f) \ finv \ ginv ~ g \ (f \ finv) \ ginv" by reduce refl + have "(g \ f) \ finv \ ginv ~ g \ (f \ finv) \ ginv" by compute refl also have ".. ~ g \ id B \ ginv" by (rhtpy, lhtpy) fact - also have ".. ~ id C" by reduce fact + also have ".. ~ id C" by compute fact finally show "?" by this qed qed @@ -317,10 +309,10 @@ Lemma (def) is_qinv_if_is_biinv: \<^item> by (fact \g: _\) \<^item> by (fact \H1: _\) \<^item> proof - - have "g ~ g \ (id B)" by reduce refl + have "g ~ g \ (id B)" by compute refl also have ".. ~ g \ f \ h" by rhtpy (rule \H2:_\[symmetric]) - also have ".. ~ (id A) \ h" by (rewrite funcomp_assoc[symmetric]) (lhtpy, fact) - also have ".. ~ h" by reduce refl + also have ".. ~ (id A) \ h" by (comp funcomp_assoc[symmetric]) (lhtpy, fact) + also have ".. ~ h" by compute refl finally have "g ~ h" by this then have "f \ g ~ f \ h" by (rhtpy, this) also note \H2:_\ @@ -420,24 +412,24 @@ Lemma (def) equiv_if_equal: apply intro defer \<^item> apply (eq p) \<^enum> vars A B - apply (rewrite at A in "A \ B" id_comp[symmetric]) + apply (comp at A in "A \ B" id_comp[symmetric]) using [[solve_side_conds=1]] - apply (rewrite at B in "_ \ B" id_comp[symmetric]) + apply (comp at B in "_ \ B" id_comp[symmetric]) apply (rule transport, rule Ui_in_USi) by (rule lift_universe_codomain, rule Ui_in_USi) \<^enum> vars A using [[solve_side_conds=1]] - apply (rewrite transport_comp) + apply (comp transport_comp) \ by (rule Ui_in_USi) - \ by reduce (rule U_lift) - \ by reduce (rule id_is_biinv) + \ by compute (rule U_lift) + \ by compute (rule id_is_biinv) done done \<^item> \ \Similar proof as in the first subgoal above\ - apply (rewrite at A in "A \ B" id_comp[symmetric]) + apply (comp at A in "A \ B" id_comp[symmetric]) using [[solve_side_conds=1]] - apply (rewrite at B in "_ \ B" id_comp[symmetric]) + apply (comp at B in "_ \ B" id_comp[symmetric]) apply (rule transport, rule Ui_in_USi) by (rule lift_universe_codomain, rule Ui_in_USi) done diff --git a/hott/Identity.thy b/hott/Identity.thy index 0a31dc7..caab2e3 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -85,7 +85,7 @@ Lemma (def) pathinv: Lemma pathinv_comp [comp]: assumes "A: U i" "x: A" shows "pathinv A x x (refl x) \ refl x" - unfolding pathinv_def by reduce + unfolding pathinv_def by compute Lemma (def) pathcomp: assumes @@ -101,7 +101,7 @@ Lemma (def) pathcomp: Lemma pathcomp_comp [comp]: assumes "A: U i" "a: A" shows "pathcomp A a a a (refl a) (refl a) \ refl a" - unfolding pathcomp_def by reduce + unfolding pathcomp_def by compute method pathcomp for p q :: o = rule pathcomp[where ?p=p and ?q=q] @@ -137,12 +137,12 @@ section \Basic propositional equalities\ Lemma (def) refl_pathcomp: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "(refl x) \ p = p" - by (eq p) (reduce, refl) + by (eq p) (compute, refl) Lemma (def) pathcomp_refl: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p \ (refl y) = p" - by (eq p) (reduce, refl) + by (eq p) (compute, refl) definition [implicit]: "lu p \ refl_pathcomp {} {} {} p" definition [implicit]: "ru p \ pathcomp_refl {} {} {} p" @@ -154,27 +154,27 @@ translations Lemma lu_refl [comp]: assumes "A: U i" "x: A" shows "lu (refl x) \ refl (refl x)" - unfolding refl_pathcomp_def by reduce + unfolding refl_pathcomp_def by compute Lemma ru_refl [comp]: assumes "A: U i" "x: A" shows "ru (refl x) \ refl (refl x)" - unfolding pathcomp_refl_def by reduce + unfolding pathcomp_refl_def by compute Lemma (def) inv_pathcomp: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p\ \ p = refl y" - by (eq p) (reduce, refl) + by (eq p) (compute, refl) Lemma (def) pathcomp_inv: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p \ p\ = refl x" - by (eq p) (reduce, refl) + by (eq p) (compute, refl) Lemma (def) pathinv_pathinv: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p\\ = p" - by (eq p) (reduce, refl) + by (eq p) (compute, refl) Lemma (def) pathcomp_assoc: assumes @@ -187,7 +187,7 @@ Lemma (def) pathcomp_assoc: proof (eq q) fix x r assuming "x: A" "r: x = w" show "refl x \ (refl x \ r) = refl x \ refl x \ r" - by (eq r) (reduce, refl) + by (eq r) (compute, refl) qed qed @@ -211,7 +211,7 @@ translations "f[p]" \ "CONST ap A B x y f p" Lemma ap_refl [comp]: assumes "A: U i" "B: U i" "f: A \ B" "x: A" shows "f[refl x] \ refl (f x)" - unfolding ap_def by reduce + unfolding ap_def by compute Lemma (def) ap_pathcomp: assumes @@ -224,7 +224,7 @@ Lemma (def) ap_pathcomp: proof (eq p) fix x q assuming "x: A" "q: x = z" show "f[refl x \ q] = f[refl x] \ f[q]" - by (eq q) (reduce, refl) + by (eq q) (compute, refl) qed Lemma (def) ap_pathinv: @@ -234,7 +234,7 @@ Lemma (def) ap_pathinv: "f: A \ B" "p: x = y" shows "f[p\] = f[p]\" - by (eq p) (reduce, refl) + by (eq p) (compute, refl) Lemma (def) ap_funcomp: assumes @@ -244,14 +244,14 @@ Lemma (def) ap_funcomp: "p: x = y" shows "(g \ f)[p] = g[f[p]]" apply (eq p) - \<^item> by reduce - \<^item> by reduce refl + \<^item> by compute + \<^item> by compute refl done Lemma (def) ap_id: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "(id A)[p] = p" - by (eq p) (reduce, refl) + by (eq p) (compute, refl) section \Transport\ @@ -276,7 +276,7 @@ Lemma transport_comp [comp]: "A: U i" "\x. x: A \ P x: U i" shows "transp P (refl a) \ id (P a)" - unfolding transport_def by reduce + unfolding transport_def by compute Lemma apply_transport: assumes @@ -287,7 +287,7 @@ Lemma apply_transport: shows "transp P p\ u: P y" by typechk -method transport uses eq = (rule apply_transport[OF _ _ _ _ eq]) +method rewr uses eq = (rule apply_transport[OF _ _ _ _ eq]) Lemma (def) pathcomp_cancel_left: assumes @@ -297,13 +297,13 @@ Lemma (def) pathcomp_cancel_left: shows "q = r" proof - have "q = (p\ \ p) \ q" - by (transport eq: inv_pathcomp, transport eq: refl_pathcomp) refl + by (rewr eq: inv_pathcomp, rewr eq: refl_pathcomp) refl also have ".. = p\ \ (p \ r)" - by (transport eq: pathcomp_assoc[symmetric], transport eq: \\:_\) refl + by (rewr eq: pathcomp_assoc[symmetric], rewr eq: \\:_\) refl also have ".. = r" - by (transport eq: pathcomp_assoc, - transport eq: inv_pathcomp, - transport eq: refl_pathcomp) refl + by (rewr eq: pathcomp_assoc, + rewr eq: inv_pathcomp, + rewr eq: refl_pathcomp) refl finally show "?" by this qed @@ -315,14 +315,14 @@ Lemma (def) pathcomp_cancel_right: shows "p = q" proof - have "p = p \ r \ r\" - by (transport eq: pathcomp_assoc[symmetric], - transport eq: pathcomp_inv, - transport eq: pathcomp_refl) refl + by (rewr eq: pathcomp_assoc[symmetric], + rewr eq: pathcomp_inv, + rewr eq: pathcomp_refl) refl also have ".. = q" - by (transport eq: \\:_\, - transport eq: pathcomp_assoc[symmetric], - transport eq: pathcomp_inv, - transport eq: pathcomp_refl) refl + by (rewr eq: \\:_\, + rewr eq: pathcomp_assoc[symmetric], + rewr eq: pathcomp_inv, + rewr eq: pathcomp_refl) refl finally show "?" by this qed @@ -336,7 +336,7 @@ Lemma (def) transport_left_inv: "x: A" "y: A" "p: x = y" shows "(transp P p\) \ (transp P p) = id (P x)" - by (eq p) (reduce, refl) + by (eq p) (compute, refl) Lemma (def) transport_right_inv: assumes @@ -345,7 +345,7 @@ Lemma (def) transport_right_inv: "x: A" "y: A" "p: x = y" shows "(transp P p) \ (transp P p\) = id (P y)" - by (eq p) (reduce, refl) + by (eq p) (compute, refl) Lemma (def) transport_pathcomp: assumes @@ -359,7 +359,7 @@ proof (eq p) fix x q u assuming "x: A" "q: x = z" "u: P x" show "transp P q (transp P (refl x) u) = transp P ((refl x) \ q) u" - by (eq q) (reduce, refl) + by (eq q) (compute, refl) qed Lemma (def) transport_compose_typefam: @@ -371,7 +371,7 @@ Lemma (def) transport_compose_typefam: "p: x = y" "u: P (f x)" shows "transp (fn x. P (f x)) p u = transp P f[p] u" - by (eq p) (reduce, refl) + by (eq p) (compute, refl) Lemma (def) transport_function_family: assumes @@ -383,7 +383,7 @@ Lemma (def) transport_function_family: "u: P x" "p: x = y" shows "transp Q p ((f x) u) = (f y) (transp P p u)" - by (eq p) (reduce, refl) + by (eq p) (compute, refl) Lemma (def) transport_const: assumes @@ -391,7 +391,7 @@ Lemma (def) transport_const: "x: A" "y: A" "p: x = y" shows "\b: B. transp (fn _. B) p b = b" - by intro (eq p, reduce, refl) + by intro (eq p, compute, refl) definition transport_const_i ("transp'_c") where [implicit]: "transp_c B p \ transport_const {} B {} {} p" @@ -403,7 +403,7 @@ Lemma transport_const_comp [comp]: "x: A" "b: B" "A: U i" "B: U i" shows "transp_c B (refl x) b \ refl b" - unfolding transport_const_def by reduce + unfolding transport_const_def by compute Lemma (def) pathlift: assumes @@ -413,7 +413,7 @@ Lemma (def) pathlift: "p: x = y" "u: P x" shows " = " - by (eq p) (reduce, refl) + by (eq p) (compute, refl) definition pathlift_i ("lift") where [implicit]: "lift P p u \ pathlift {} P {} {} p u" @@ -427,7 +427,7 @@ Lemma pathlift_comp [comp]: "\x. x: A \ P x: U i" "A: U i" shows "lift P (refl x) u \ refl " - unfolding pathlift_def by reduce + unfolding pathlift_def by compute Lemma (def) pathlift_fst: assumes @@ -437,7 +437,7 @@ Lemma (def) pathlift_fst: "u: P x" "p: x = y" shows "fst[lift P p u] = p" - by (eq p) (reduce, refl) + by (eq p) (compute, refl) section \Dependent paths\ @@ -450,7 +450,7 @@ Lemma (def) apd: "x: A" "y: A" "p: x = y" shows "transp P p (f x) = f y" - by (eq p) (reduce, refl) + by (eq p) (compute, refl) definition apd_i ("apd") where [implicit]: "apd f p \ Identity.apd {} {} f {} {} p" @@ -464,7 +464,7 @@ Lemma dependent_map_comp [comp]: "A: U i" "\x. x: A \ P x: U i" shows "apd f (refl x) \ refl (f x)" - unfolding apd_def by reduce + unfolding apd_def by compute Lemma (def) apd_ap: assumes @@ -473,7 +473,7 @@ Lemma (def) apd_ap: "x: A" "y: A" "p: x = y" shows "apd f p = transp_c B p (f x) \ f[p]" - by (eq p) (reduce, refl) + by (eq p) (compute, refl) section \Whiskering\ @@ -519,12 +519,12 @@ translations Lemma whisker_refl [comp]: assumes "A: U i" "a: A" "b: A" "p: a = b" "q: a = b" "\: p = q" shows "\ \\<^sub>r (refl b) \ ru p \ \ \ (ru q)\" - unfolding right_whisker_def by reduce + unfolding right_whisker_def by compute Lemma refl_whisker [comp]: assumes "A: U i" "a: A" "b: A" "p: a = b" "q: a = b" "\: p = q" shows "(refl a) \\<^sub>l \ \ (lu p) \ \ \ (lu q)\" - unfolding left_whisker_def by reduce + unfolding left_whisker_def by compute method left_whisker = (rule left_whisker) method right_whisker = (rule right_whisker) @@ -569,7 +569,7 @@ Lemma (def) horiz_pathcomp_eq_horiz_pathcomp': unfolding horiz_pathcomp_def horiz_pathcomp'_def apply (eq \, eq \) focus vars p apply (eq p) - focus vars a _ _ _ r by (eq r) (reduce, refl) + focus vars a _ _ _ r by (eq r) (compute, refl) done done @@ -604,14 +604,14 @@ Lemma and horiz_pathcomp'_type [type]: "\ \' \: \2 A a" using assms unfolding \2.horiz_pathcomp_def \2.horiz_pathcomp'_def \2_def - by reduce+ + by compute+ Lemma (def) pathcomp_eq_horiz_pathcomp: assumes "\: \2 A a" "\: \2 A a" shows "\ \ \ = \ \ \" unfolding \2.horiz_pathcomp_def using assms[unfolded \2_def, type] (*TODO: A `noting` keyword that puts the noted theorem into [type]*) - proof (reduce, rule pathinv) + proof (compute, rule pathinv) have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) @@ -633,7 +633,7 @@ Lemma (def) pathcomp_eq_horiz_pathcomp': shows "\ \' \ = \ \ \" unfolding \2.horiz_pathcomp'_def using assms[unfolded \2_def, type] - proof reduce + proof compute have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) @@ -660,7 +660,7 @@ Lemma (def) eckmann_hilton: also have [simplified comp]: ".. = \ \' \" \ \Danger! Inferred implicit has an equivalent form but needs to be manually simplified.\ - by (transport eq: \2.horiz_pathcomp_eq_horiz_pathcomp') refl + by (rewr eq: \2.horiz_pathcomp_eq_horiz_pathcomp') refl also have ".. = \ \ \" by (rule pathcomp_eq_horiz_pathcomp') finally show "\ \ \ = \ \ \" diff --git a/hott/Nat.thy b/hott/Nat.thy index 1aa7932..33a5d0a 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -70,27 +70,27 @@ Lemma add_type [type]: Lemma add_zero [comp]: assumes "m: Nat" shows "m + 0 \ m" - unfolding add_def by reduce + unfolding add_def by compute Lemma add_suc [comp]: assumes "m: Nat" "n: Nat" shows "m + suc n \ suc (m + n)" - unfolding add_def by reduce + unfolding add_def by compute Lemma (def) zero_add: assumes "n: Nat" shows "0 + n = n" apply (elim n) - \<^item> by (reduce; intro) - \<^item> vars _ ih by reduce (eq ih; refl) + \<^item> by (compute; intro) + \<^item> vars _ ih by compute (eq ih; refl) done Lemma (def) suc_add: assumes "m: Nat" "n: Nat" shows "suc m + n = suc (m + n)" apply (elim n) - \<^item> by reduce refl - \<^item> vars _ ih by reduce (eq ih; refl) + \<^item> by compute refl + \<^item> vars _ ih by compute (eq ih; refl) done Lemma (def) suc_eq: @@ -102,19 +102,19 @@ Lemma (def) add_assoc: assumes "l: Nat" "m: Nat" "n: Nat" shows "l + (m + n) = l + m+ n" apply (elim n) - \<^item> by reduce intro - \<^item> vars _ ih by reduce (eq ih; refl) + \<^item> by compute intro + \<^item> vars _ ih by compute (eq ih; refl) done Lemma (def) add_comm: assumes "m: Nat" "n: Nat" shows "m + n = n + m" apply (elim n) - \<^item> by (reduce; rule zero_add[symmetric]) + \<^item> by (compute; rule zero_add[symmetric]) \<^item> vars n ih - proof reduce + proof compute have "suc (m + n) = suc (n + m)" by (eq ih) refl - also have ".. = suc n + m" by (transport eq: suc_add) refl + also have ".. = suc n + m" by (rewr eq: suc_add) refl finally show "?" by this qed done @@ -131,27 +131,27 @@ Lemma mul_type [type]: Lemma mul_zero [comp]: assumes "n: Nat" shows "n * 0 \ 0" - unfolding mul_def by reduce + unfolding mul_def by compute Lemma mul_one [comp]: assumes "n: Nat" shows "n * 1 \ n" - unfolding mul_def by reduce + unfolding mul_def by compute Lemma mul_suc [comp]: assumes "m: Nat" "n: Nat" shows "m * suc n \ m + m * n" - unfolding mul_def by reduce + unfolding mul_def by compute Lemma (def) zero_mul: assumes "n: Nat" shows "0 * n = 0" apply (elim n) - \<^item> by reduce refl + \<^item> by compute refl \<^item> vars n ih - proof reduce + proof compute have "0 + 0 * n = 0 + 0 " by (eq ih) refl - also have ".. = 0" by reduce refl + also have ".. = 0" by compute refl finally show "?" by this qed done @@ -160,11 +160,11 @@ Lemma (def) suc_mul: assumes "m: Nat" "n: Nat" shows "suc m * n = m * n + n" apply (elim n) - \<^item> by reduce refl + \<^item> by compute refl \<^item> vars n ih - proof (reduce, transport eq: \ih:_\) + proof (compute, rewr eq: \ih:_\) 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 + also have ".. = suc (m + m * n + n)" by (rewr eq: add_assoc) refl finally show "?" by this qed done @@ -173,13 +173,13 @@ Lemma (def) mul_dist_add: assumes "l: Nat" "m: Nat" "n: Nat" shows "l * (m + n) = l * m + l * n" apply (elim n) - \<^item> by reduce refl + \<^item> by compute refl \<^item> vars n ih - proof reduce + proof compute have "l + l * (m + n) = l + (l * m + l * n)" by (eq ih) refl 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 + also have ".. = l * m + l + l * n" by (rewr eq: add_comm) refl + also have ".. = l * m + (l + l * n)" by (rewr eq: add_assoc) refl finally show "?" by this qed done @@ -188,11 +188,11 @@ Lemma (def) mul_assoc: assumes "l: Nat" "m: Nat" "n: Nat" shows "l * (m * n) = l * m * n" apply (elim n) - \<^item> by reduce refl + \<^item> by compute refl \<^item> vars n ih - proof reduce + proof compute 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 + also have ".. = l * m + l * m * n" by (rewr eq: \ih:_\) refl finally show "?" by this qed done @@ -201,12 +201,12 @@ Lemma (def) mul_comm: assumes "m: Nat" "n: Nat" shows "m * n = n * m" apply (elim n) - \<^item> by reduce (transport eq: zero_mul, refl) + \<^item> by compute (rewr eq: zero_mul, refl) \<^item> vars n ih - proof (reduce, rule pathinv) + proof (compute, rule pathinv) 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 + by (rewr eq: \ih:_\, rewr eq: add_comm) refl finally show "?" by this qed done diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index ffe3778..5046b6a 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -295,7 +295,7 @@ method_setup this = subsection \Rewriting\ -consts rewrite_hole :: "'a::{}" ("\") +consts compute_hole :: "'a::{}" ("\") lemma eta_expand: fixes f :: "'a::{} \ 'b::{}" @@ -319,10 +319,10 @@ lemma imp_cong_eq: done ML_file \~~/src/HOL/Library/cconv.ML\ -ML_file \rewrite.ML\ +ML_file \comp.ML\ -\ \\reduce\ simplifies terms via computational equalities\ -method reduce uses add = +\ \\compute\ simplifies terms via computational equalities\ +method compute uses add = changed \repeat_new \(simp add: comp add | subst comp); typechk?\\ @@ -396,7 +396,7 @@ Lemma refine_codomain: "f: \x: A. B x" "\x. x: A \ f `x: C x" shows "f: \x: A. C x" - by (rewrite eta_exp) + by (comp eta_exp) Lemma lift_universe_codomain: assumes "A: U i" "f: A \ U j" @@ -432,7 +432,7 @@ Lemma funcomp_assoc [comp]: "h: \x: C. D x" shows "(h \\<^bsub>B\<^esub> g) \\<^bsub>A\<^esub> f \ h \\<^bsub>A\<^esub> g \\<^bsub>A\<^esub> f" - unfolding funcomp_def by reduce + unfolding funcomp_def by compute Lemma funcomp_lambda_comp [comp]: assumes @@ -441,7 +441,7 @@ Lemma funcomp_lambda_comp [comp]: "\x. x: B \ c x: C x" shows "(\x: B. c x) \\<^bsub>A\<^esub> (\x: A. b x) \ \x: A. c (b x)" - unfolding funcomp_def by reduce + unfolding funcomp_def by compute Lemma funcomp_apply_comp [comp]: assumes @@ -449,7 +449,7 @@ Lemma funcomp_apply_comp [comp]: "f: A \ B" "g: \x: B. C x" "x: A" shows "(g \\<^bsub>A\<^esub> f) x \ g (f x)" - unfolding funcomp_def by reduce + unfolding funcomp_def by compute subsection \Notation\ @@ -465,17 +465,17 @@ abbreviation id where "id A \ \x: A. x" lemma id_type [type]: "A: U i \ id A: A \ A" and id_comp [comp]: "x: A \ (id A) x \ x" \ \for the occasional manual rewrite\ - by reduce+ + by compute+ Lemma id_left [comp]: assumes "A: U i" "B: U i" "f: A \ B" shows "(id B) \\<^bsub>A\<^esub> f \ f" - by (rewrite eta_exp[of f]) (reduce, rule eta) + by (comp eta_exp[of f]) (compute, rule eta) Lemma id_right [comp]: assumes "A: U i" "B: U i" "f: A \ B" shows "f \\<^bsub>A\<^esub> (id A) \ f" - by (rewrite eta_exp[of f]) (reduce, rule eta) + by (comp eta_exp[of f]) (compute, rule eta) lemma id_U [type]: "id (U i): U i \ U i" @@ -496,7 +496,7 @@ Lemma fst_comp [comp]: assumes "A: U i" "\x. x: A \ B x: U i" "a: A" "b: B a" shows "fst A B \ a" - unfolding fst_def by reduce + unfolding fst_def by compute Lemma snd_type [type]: assumes "A: U i" "\x. x: A \ B x: U i" @@ -506,7 +506,7 @@ Lemma snd_type [type]: Lemma snd_comp [comp]: assumes "A: U i" "\x. x: A \ B x: U i" "a: A" "b: B a" shows "snd A B \ b" - unfolding snd_def by reduce + unfolding snd_def by compute subsection \Notation\ diff --git a/spartan/core/comp.ML b/spartan/core/comp.ML new file mode 100644 index 0000000..2e50753 --- /dev/null +++ b/spartan/core/comp.ML @@ -0,0 +1,468 @@ +(* Title: compute.ML + Author: Christoph Traut, Lars Noschinski, TU Muenchen + Modified: Joshua Chen, University of Innsbruck + +This is a method for rewriting computational equalities that supports subterm +selection based on patterns. + +This code has been slightly modified from the original at HOL/Library/compute.ML +to incorporate automatic discharge of type-theoretic side conditions. + +Comment from the original code follows: + +The patterns accepted by compute are of the following form: + ::= | "concl" | "asm" | "for" "(" ")" + ::= (in | at ) [] + ::= [] ("to" ) + +This syntax was clearly inspired by Gonthier's and Tassi's language of +patterns but has diverged significantly during its development. + +We also allow introduction of identifiers for bound variables, +which can then be used to match arbitrary subterms inside abstractions. +*) + +infix 1 then_pconv; +infix 0 else_pconv; + +signature COMPUTE = +sig + type patconv = Proof.context -> Type.tyenv * (string * term) list -> cconv + val then_pconv: patconv * patconv -> patconv + val else_pconv: patconv * patconv -> patconv + val abs_pconv: patconv -> string option * typ -> patconv (*XXX*) + val fun_pconv: patconv -> patconv + val arg_pconv: patconv -> patconv + val imp_pconv: patconv -> patconv + val params_pconv: patconv -> patconv + val forall_pconv: patconv -> string option * typ option -> patconv + val all_pconv: patconv + val for_pconv: patconv -> (string option * typ option) list -> patconv + val concl_pconv: patconv -> patconv + val asm_pconv: patconv -> patconv + val asms_pconv: patconv -> patconv + val judgment_pconv: patconv -> patconv + val in_pconv: patconv -> patconv + val match_pconv: patconv -> term * (string option * typ) list -> patconv + val comps_pconv: term option -> thm list -> patconv + + datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list + + val mk_hole: int -> typ -> term + + val compute_conv: Proof.context + -> (term * (string * typ) list, string * typ option) pattern list * term option + -> thm list + -> conv +end + +structure Compute : COMPUTE = +struct + +datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list + +exception NO_TO_MATCH + +val holeN = Name.internal "_hole" + +fun prep_meta_eq ctxt = Simplifier.mksimps ctxt #> map Drule.zero_var_indexes + + +(* holes *) + +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>\compute_hole\, _)) = true + | is_hole_const _ = false + +val hole_syntax = + let + (* Modified variant of Term.replace_hole *) + fun replace_hole Ts (Const (\<^const_name>\compute_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 + in (Abs (x, T, t'), i') end + | replace_hole Ts (t $ u) i = + let + val (t', i') = replace_hole Ts t i + val (u', i'') = replace_hole Ts u i' + in (t' $ u', i'') end + | replace_hole _ a i = (a, i) + fun prep_holes ts = #1 (fold_map (replace_hole []) ts 1) + in + Context.proof_map (Syntax_Phases.term_check 101 "hole_expansion" (K prep_holes)) + #> Proof_Context.set_mode Proof_Context.mode_pattern + end + + +(* pattern conversions *) + +type patconv = Proof.context -> Type.tyenv * (string * term) list -> cterm -> thm + +fun (cv1 then_pconv cv2) ctxt tytenv ct = (cv1 ctxt tytenv then_conv cv2 ctxt tytenv) ct + +fun (cv1 else_pconv cv2) ctxt tytenv ct = (cv1 ctxt tytenv else_conv cv2 ctxt tytenv) ct + +fun raw_abs_pconv cv ctxt tytenv ct = + case Thm.term_of ct of + Abs _ => CConv.abs_cconv (fn (x, ctxt') => cv x ctxt' tytenv) ctxt ct + | t => raise TERM ("raw_abs_pconv", [t]) + +fun raw_fun_pconv cv ctxt tytenv ct = + case Thm.term_of ct of + _ $ _ => CConv.fun_cconv (cv ctxt tytenv) ct + | t => raise TERM ("raw_fun_pconv", [t]) + +fun raw_arg_pconv cv ctxt tytenv ct = + case Thm.term_of ct of + _ $ _ => CConv.arg_cconv (cv ctxt tytenv) ct + | t => raise TERM ("raw_arg_pconv", [t]) + +fun abs_pconv cv (s,T) ctxt (tyenv, ts) ct = + let val u = Thm.term_of ct + in + case try (fastype_of #> dest_funT) u of + NONE => raise TERM ("abs_pconv: no function type", [u]) + | SOME (U, _) => + let + val tyenv' = + if T = dummyT then tyenv + else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv + val eta_expand_cconv = + case u of + Abs _=> Thm.reflexive + | _ => CConv.rewr_cconv @{thm eta_expand} + fun add_ident NONE _ l = l + | add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l + val abs_cv = CConv.abs_cconv (fn (ct, ctxt) => cv ctxt (tyenv', add_ident s ct ts)) ctxt + in (eta_expand_cconv then_conv abs_cv) ct end + handle Pattern.MATCH => raise TYPE ("abs_pconv: types don't match", [T,U], [u]) + end + +fun fun_pconv cv ctxt tytenv ct = + case Thm.term_of ct of + _ $ _ => CConv.fun_cconv (cv ctxt tytenv) ct + | Abs (_, T, _ $ Bound 0) => abs_pconv (fun_pconv cv) (NONE, T) ctxt tytenv ct + | t => raise TERM ("fun_pconv", [t]) + +local + +fun arg_pconv_gen cv0 cv ctxt tytenv ct = + case Thm.term_of ct of + _ $ _ => cv0 (cv ctxt tytenv) ct + | Abs (_, T, _ $ Bound 0) => abs_pconv (arg_pconv_gen cv0 cv) (NONE, T) ctxt tytenv ct + | t => raise TERM ("arg_pconv_gen", [t]) + +in + +fun arg_pconv ctxt = arg_pconv_gen CConv.arg_cconv ctxt +fun imp_pconv ctxt = arg_pconv_gen (CConv.concl_cconv 1) ctxt + +end + +(* Move to B in !!x_1 ... x_n. B. Do not eta-expand *) +fun params_pconv cv ctxt tytenv ct = + let val pconv = + case Thm.term_of ct of + Const (\<^const_name>\Pure.all\, _) $ Abs _ => (raw_arg_pconv o raw_abs_pconv) (fn _ => params_pconv cv) + | Const (\<^const_name>\Pure.all\, _) => raw_arg_pconv (params_pconv cv) + | _ => cv + in pconv ctxt tytenv ct end + +fun forall_pconv cv ident ctxt tytenv ct = + case Thm.term_of ct of + Const (\<^const_name>\Pure.all\, T) $ _ => + let + val def_U = T |> dest_funT |> fst |> dest_funT |> fst + val ident' = apsnd (the_default (def_U)) ident + in arg_pconv (abs_pconv cv ident') ctxt tytenv ct end + | t => raise TERM ("forall_pconv", [t]) + +fun all_pconv _ _ = Thm.reflexive + +fun for_pconv cv idents ctxt tytenv ct = + let + fun f rev_idents (Const (\<^const_name>\Pure.all\, _) $ t) = + let val (rev_idents', cv') = f rev_idents (case t of Abs (_,_,u) => u | _ => t) + in + case rev_idents' of + [] => ([], forall_pconv cv' (NONE, NONE)) + | (x :: xs) => (xs, forall_pconv cv' x) + end + | f rev_idents _ = (rev_idents, cv) + in + case f (rev idents) (Thm.term_of ct) of + ([], cv') => cv' ctxt tytenv ct + | _ => raise CTERM ("for_pconv", [ct]) + end + +fun concl_pconv cv ctxt tytenv ct = + case Thm.term_of ct of + (Const (\<^const_name>\Pure.imp\, _) $ _) $ _ => imp_pconv (concl_pconv cv) ctxt tytenv ct + | _ => cv ctxt tytenv ct + +fun asm_pconv cv ctxt tytenv ct = + case Thm.term_of ct of + (Const (\<^const_name>\Pure.imp\, _) $ _) $ _ => CConv.with_prems_cconv ~1 (cv ctxt tytenv) ct + | t => raise TERM ("asm_pconv", [t]) + +fun asms_pconv cv ctxt tytenv ct = + case Thm.term_of ct of + (Const (\<^const_name>\Pure.imp\, _) $ _) $ _ => + ((CConv.with_prems_cconv ~1 oo cv) else_pconv imp_pconv (asms_pconv cv)) ctxt tytenv ct + | t => raise TERM ("asms_pconv", [t]) + +fun judgment_pconv cv ctxt tytenv ct = + if Object_Logic.is_judgment ctxt (Thm.term_of ct) + then arg_pconv cv ctxt tytenv ct + else cv ctxt tytenv ct + +fun in_pconv cv ctxt tytenv ct = + (cv else_pconv + raw_fun_pconv (in_pconv cv) else_pconv + raw_arg_pconv (in_pconv cv) else_pconv + raw_abs_pconv (fn _ => in_pconv cv)) + ctxt tytenv ct + +fun replace_idents idents t = + let + fun subst ((n1, s)::ss) (t as Free (n2, _)) = if n1 = n2 then s else subst ss t + | subst _ t = t + in Term.map_aterms (subst idents) t end + +fun match_pconv cv (t,fixes) ctxt (tyenv, env_ts) ct = + let + val t' = replace_idents env_ts t + val thy = Proof_Context.theory_of ctxt + val u = Thm.term_of ct + + fun descend_hole fixes (Abs (_, _, t)) = + (case descend_hole fixes t of + NONE => NONE + | SOME (fix :: fixes', pos) => SOME (fixes', abs_pconv pos fix) + | SOME ([], _) => raise Match (* less fixes than abstractions on path to hole *)) + | descend_hole fixes (t as l $ r) = + let val (f, _) = strip_comb t + in + if is_hole f + then SOME (fixes, cv) + else + (case descend_hole fixes l of + SOME (fixes', pos) => SOME (fixes', fun_pconv pos) + | NONE => + (case descend_hole fixes r of + SOME (fixes', pos) => SOME (fixes', arg_pconv pos) + | NONE => NONE)) + end + | descend_hole fixes t = + if is_hole t then SOME (fixes, cv) else NONE + + val to_hole = descend_hole (rev fixes) #> the_default ([], cv) #> snd + in + case try (Pattern.match thy (apply2 Logic.mk_term (t',u))) (tyenv, Vartab.empty) of + NONE => raise TERM ("match_pconv: Does not match pattern", [t, t',u]) + | SOME (tyenv', _) => to_hole t ctxt (tyenv', env_ts) ct + end + +fun comps_pconv to thms ctxt (tyenv, env_ts) = + let + fun instantiate_normalize_env ctxt env thm = + let + val prop = Thm.prop_of thm + val norm_type = Envir.norm_type o Envir.type_env + val insts = Term.add_vars prop [] + |> map (fn x as (s, T) => + ((s, norm_type env T), Thm.cterm_of ctxt (Envir.norm_term env (Var x)))) + val tyinsts = Term.add_tvars prop [] + |> map (fn x => (x, Thm.ctyp_of ctxt (norm_type env (TVar x)))) + in Drule.instantiate_normalize (tyinsts, insts) thm end + + fun unify_with_rhs context to env thm = + let + val (_, rhs) = thm |> Thm.concl_of |> Logic.dest_equals + val env' = Pattern.unify context (Logic.mk_term to, Logic.mk_term rhs) env + handle Pattern.Unif => raise NO_TO_MATCH + in env' end + + fun inst_thm_to _ (NONE, _) thm = thm + | inst_thm_to (ctxt : Proof.context) (SOME to, env) thm = + instantiate_normalize_env ctxt (unify_with_rhs (Context.Proof ctxt) to env thm) thm + + fun inst_thm ctxt idents (to, tyenv) thm = + let + (* Replace any identifiers with their corresponding bound variables. *) + val maxidx = Term.maxidx_typs (map (snd o snd) (Vartab.dest tyenv)) 0 + val env = Envir.Envir {maxidx = maxidx, tenv = Vartab.empty, tyenv = tyenv} + val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (the_list to) + val thm' = Thm.incr_indexes (maxidx + 1) thm + in SOME (inst_thm_to ctxt (Option.map (replace_idents idents) to, env) thm') end + handle NO_TO_MATCH => NONE + + in CConv.rewrs_cconv (map_filter (inst_thm ctxt env_ts (to, tyenv)) thms) end + +fun compute_conv ctxt (pattern, to) thms ct = + let + fun apply_pat At = judgment_pconv + | apply_pat In = in_pconv + | apply_pat Asm = params_pconv o asms_pconv + | apply_pat Concl = params_pconv o concl_pconv + | apply_pat (For idents) = (fn cv => for_pconv cv (map (apfst SOME) idents)) + | apply_pat (Term x) = (fn cv => match_pconv cv (apsnd (map (apfst SOME)) x)) + + val cv = fold_rev apply_pat pattern + + fun distinct_prems th = + case Seq.pull (distinct_subgoals_tac th) of + NONE => th + | SOME (th', _) => th' + + val compute = comps_pconv to (maps (prep_meta_eq ctxt) thms) + in cv compute ctxt (Vartab.empty, []) ct |> distinct_prems end + +fun compute_export_tac ctxt (pat, pat_ctxt) thms = + let + val export = case pat_ctxt of + NONE => I + | SOME inner => singleton (Proof_Context.export inner ctxt) + in CCONVERSION (export o compute_conv ctxt pat thms) end + +val _ = + Theory.setup + let + fun mk_fix s = (Binding.name s, NONE, NoSyn) + + val raw_pattern : (string, binding * string option * mixfix) pattern list parser = + let + val sep = (Args.$$$ "at" >> K At) || (Args.$$$ "in" >> K In) + val atom = (Args.$$$ "asm" >> K Asm) || + (Args.$$$ "concl" >> K Concl) || + (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.vars []) >> For) || + (Parse.term >> Term) + val sep_atom = sep -- atom >> (fn (s,a) => [s,a]) + + fun append_default [] = [Concl, In] + | append_default (ps as Term _ :: _) = Concl :: In :: ps + | append_default [For x, In] = [For x, Concl, In] + | append_default (For x :: (ps as In :: Term _:: _)) = For x :: Concl :: ps + | append_default ps = ps + + in Scan.repeats sep_atom >> (rev #> append_default) end + + fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) => + let + val (r, toks') = scan toks + val (r', context') = Context.map_proof_result (fn ctxt => f ctxt r) context + in (r', (context', toks' : Token.T list)) end + + fun read_fixes fixes ctxt = + let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx) + in Proof_Context.add_fixes (map read_typ fixes) ctxt end + + fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) = + let + fun add_constrs ctxt n (Abs (x, T, t)) = + let + val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt + in + (case add_constrs ctxt' (n+1) t of + NONE => NONE + | SOME ((ctxt'', n', xs), t') => + let + val U = Type_Infer.mk_param n [] + val u = Type.constraint (U --> dummyT) (Abs (x, T, t')) + in SOME ((ctxt'', n', (x', U) :: xs), u) end) + end + | add_constrs ctxt n (l $ r) = + (case add_constrs ctxt n l of + SOME (c, l') => SOME (c, l' $ r) + | NONE => + (case add_constrs ctxt n r of + SOME (c, r') => SOME (c, l $ r') + | NONE => NONE)) + | add_constrs ctxt n t = + if is_hole_const t then SOME ((ctxt, n, []), t) else NONE + + fun prep (Term s) (n, ctxt) = + let + val t = Syntax.parse_term ctxt s + val ((ctxt', n', bs), t') = + the_default ((ctxt, n, []), t) (add_constrs ctxt (n+1) t) + in (Term (t', bs), (n', ctxt')) end + | prep (For ss) (n, ctxt) = + let val (ns, ctxt') = read_fixes ss ctxt + in (For ns, (n, ctxt')) end + | prep At (n,ctxt) = (At, (n, ctxt)) + | prep In (n,ctxt) = (In, (n, ctxt)) + | prep Concl (n,ctxt) = (Concl, (n, ctxt)) + | prep Asm (n,ctxt) = (Asm, (n, ctxt)) + + val (xs, (_, ctxt')) = fold_map prep ps (0, ctxt) + + in (xs, ctxt') end + + fun prep_args ctxt (((raw_pats, raw_to), raw_ths)) = + let + + fun check_terms ctxt ps to = + let + fun safe_chop (0: int) xs = ([], xs) + | safe_chop n (x :: xs) = chop (n - 1) xs |>> cons x + | safe_chop _ _ = raise Match + + fun reinsert_pat _ (Term (_, cs)) (t :: ts) = + let val (cs', ts') = safe_chop (length cs) ts + in (Term (t, map dest_Free cs'), ts') end + | reinsert_pat _ (Term _) [] = raise Match + | reinsert_pat ctxt (For ss) ts = + let val fixes = map (fn s => (s, Variable.default_type ctxt s)) ss + in (For fixes, ts) end + | reinsert_pat _ At ts = (At, ts) + | reinsert_pat _ In ts = (In, ts) + | reinsert_pat _ Concl ts = (Concl, ts) + | reinsert_pat _ Asm ts = (Asm, ts) + + fun free_constr (s,T) = Type.constraint T (Free (s, dummyT)) + fun mk_free_constrs (Term (t, cs)) = t :: map free_constr cs + | mk_free_constrs _ = [] + + val ts = maps mk_free_constrs ps @ the_list to + |> Syntax.check_terms (hole_syntax ctxt) + val ctxt' = fold Variable.declare_term ts ctxt + val (ps', (to', ts')) = fold_map (reinsert_pat ctxt') ps ts + ||> (fn xs => case to of NONE => (NONE, xs) | SOME _ => (SOME (hd xs), tl xs)) + val _ = case ts' of (_ :: _) => raise Match | [] => () + in ((ps', to'), ctxt') end + + val (pats, ctxt') = prep_pats ctxt raw_pats + + val ths = Attrib.eval_thms ctxt' raw_ths + val to = Option.map (Syntax.parse_term ctxt') raw_to + + val ((pats', to'), ctxt'') = check_terms ctxt' pats to + + in ((pats', ths, (to', ctxt)), ctxt'') end + + val to_parser = Scan.option ((Args.$$$ "to") |-- Parse.term) + + val subst_parser = + let val scan = raw_pattern -- to_parser -- Parse.thms1 + in context_lift scan prep_args end + + fun compute_export_ctac inputs inthms = + CONTEXT_TACTIC' (fn ctxt => compute_export_tac ctxt inputs inthms) + in + Method.setup \<^binding>\cmp\ (subst_parser >> + (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => SIMPLE_METHOD' + (compute_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms))) + "single-step rewriting, allowing subterm selection via patterns" #> + Method.setup \<^binding>\comp\ (subst_parser >> + (fn (pattern, inthms, (to, pat_ctxt)) => K (CONTEXT_METHOD ( + CHEADGOAL o SIDE_CONDS 0 + (compute_export_ctac ((pattern, to), SOME pat_ctxt) inthms))))) + "single-step rewriting with auto-typechecking" + end +end diff --git a/spartan/core/context_facts.ML b/spartan/core/context_facts.ML index c372ca7..5aa7c70 100644 --- a/spartan/core/context_facts.ML +++ b/spartan/core/context_facts.ML @@ -17,6 +17,7 @@ val eq: Proof.context -> thm list val eq_of: Proof.context -> term -> thm list val register_eq: thm -> Context.generic -> Context.generic val register_eqs: thm list -> Context.generic -> Context.generic + val register_facts: thm list -> Proof.context -> Proof.context end = struct diff --git a/spartan/core/rewrite.ML b/spartan/core/rewrite.ML deleted file mode 100644 index af70cfc..0000000 --- a/spartan/core/rewrite.ML +++ /dev/null @@ -1,465 +0,0 @@ -(* Title: rewrite.ML - Author: Christoph Traut, Lars Noschinski, TU Muenchen - Modified: Joshua Chen, University of Innsbruck - -This is a rewrite method that supports subterm-selection based on patterns. - -The patterns accepted by rewrite are of the following form: - ::= | "concl" | "asm" | "for" "(" ")" - ::= (in | at ) [] - ::= [] ("to" ) - -This syntax was clearly inspired by Gonthier's and Tassi's language of -patterns but has diverged significantly during its development. - -We also allow introduction of identifiers for bound variables, -which can then be used to match arbitrary subterms inside abstractions. - -This code has been slightly modified from the original at HOL/Library/rewrite.ML -to incorporate automatic discharge of type-theoretic side conditions. -*) - -infix 1 then_pconv; -infix 0 else_pconv; - -signature REWRITE = -sig - type patconv = Proof.context -> Type.tyenv * (string * term) list -> cconv - val then_pconv: patconv * patconv -> patconv - val else_pconv: patconv * patconv -> patconv - val abs_pconv: patconv -> string option * typ -> patconv (*XXX*) - val fun_pconv: patconv -> patconv - val arg_pconv: patconv -> patconv - val imp_pconv: patconv -> patconv - val params_pconv: patconv -> patconv - val forall_pconv: patconv -> string option * typ option -> patconv - val all_pconv: patconv - val for_pconv: patconv -> (string option * typ option) list -> patconv - val concl_pconv: patconv -> patconv - val asm_pconv: patconv -> patconv - val asms_pconv: patconv -> patconv - val judgment_pconv: patconv -> patconv - val in_pconv: patconv -> patconv - val match_pconv: patconv -> term * (string option * typ) list -> patconv - val rewrs_pconv: term option -> thm list -> patconv - - datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list - - val mk_hole: int -> typ -> term - - val rewrite_conv: Proof.context - -> (term * (string * typ) list, string * typ option) pattern list * term option - -> thm list - -> conv -end - -structure Rewrite : REWRITE = -struct - -datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list - -exception NO_TO_MATCH - -val holeN = Name.internal "_hole" - -fun prep_meta_eq ctxt = Simplifier.mksimps ctxt #> map Drule.zero_var_indexes - - -(* holes *) - -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 - | 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 = - (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 - in (Abs (x, T, t'), i') end - | replace_hole Ts (t $ u) i = - let - val (t', i') = replace_hole Ts t i - val (u', i'') = replace_hole Ts u i' - in (t' $ u', i'') end - | replace_hole _ a i = (a, i) - fun prep_holes ts = #1 (fold_map (replace_hole []) ts 1) - in - Context.proof_map (Syntax_Phases.term_check 101 "hole_expansion" (K prep_holes)) - #> Proof_Context.set_mode Proof_Context.mode_pattern - end - - -(* pattern conversions *) - -type patconv = Proof.context -> Type.tyenv * (string * term) list -> cterm -> thm - -fun (cv1 then_pconv cv2) ctxt tytenv ct = (cv1 ctxt tytenv then_conv cv2 ctxt tytenv) ct - -fun (cv1 else_pconv cv2) ctxt tytenv ct = (cv1 ctxt tytenv else_conv cv2 ctxt tytenv) ct - -fun raw_abs_pconv cv ctxt tytenv ct = - case Thm.term_of ct of - Abs _ => CConv.abs_cconv (fn (x, ctxt') => cv x ctxt' tytenv) ctxt ct - | t => raise TERM ("raw_abs_pconv", [t]) - -fun raw_fun_pconv cv ctxt tytenv ct = - case Thm.term_of ct of - _ $ _ => CConv.fun_cconv (cv ctxt tytenv) ct - | t => raise TERM ("raw_fun_pconv", [t]) - -fun raw_arg_pconv cv ctxt tytenv ct = - case Thm.term_of ct of - _ $ _ => CConv.arg_cconv (cv ctxt tytenv) ct - | t => raise TERM ("raw_arg_pconv", [t]) - -fun abs_pconv cv (s,T) ctxt (tyenv, ts) ct = - let val u = Thm.term_of ct - in - case try (fastype_of #> dest_funT) u of - NONE => raise TERM ("abs_pconv: no function type", [u]) - | SOME (U, _) => - let - val tyenv' = - if T = dummyT then tyenv - else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv - val eta_expand_cconv = - case u of - Abs _=> Thm.reflexive - | _ => CConv.rewr_cconv @{thm eta_expand} - fun add_ident NONE _ l = l - | add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l - val abs_cv = CConv.abs_cconv (fn (ct, ctxt) => cv ctxt (tyenv', add_ident s ct ts)) ctxt - in (eta_expand_cconv then_conv abs_cv) ct end - handle Pattern.MATCH => raise TYPE ("abs_pconv: types don't match", [T,U], [u]) - end - -fun fun_pconv cv ctxt tytenv ct = - case Thm.term_of ct of - _ $ _ => CConv.fun_cconv (cv ctxt tytenv) ct - | Abs (_, T, _ $ Bound 0) => abs_pconv (fun_pconv cv) (NONE, T) ctxt tytenv ct - | t => raise TERM ("fun_pconv", [t]) - -local - -fun arg_pconv_gen cv0 cv ctxt tytenv ct = - case Thm.term_of ct of - _ $ _ => cv0 (cv ctxt tytenv) ct - | Abs (_, T, _ $ Bound 0) => abs_pconv (arg_pconv_gen cv0 cv) (NONE, T) ctxt tytenv ct - | t => raise TERM ("arg_pconv_gen", [t]) - -in - -fun arg_pconv ctxt = arg_pconv_gen CConv.arg_cconv ctxt -fun imp_pconv ctxt = arg_pconv_gen (CConv.concl_cconv 1) ctxt - -end - -(* Move to B in !!x_1 ... x_n. B. Do not eta-expand *) -fun params_pconv cv ctxt tytenv ct = - let val pconv = - case Thm.term_of ct of - Const (\<^const_name>\Pure.all\, _) $ Abs _ => (raw_arg_pconv o raw_abs_pconv) (fn _ => params_pconv cv) - | Const (\<^const_name>\Pure.all\, _) => raw_arg_pconv (params_pconv cv) - | _ => cv - in pconv ctxt tytenv ct end - -fun forall_pconv cv ident ctxt tytenv ct = - case Thm.term_of ct of - Const (\<^const_name>\Pure.all\, T) $ _ => - let - val def_U = T |> dest_funT |> fst |> dest_funT |> fst - val ident' = apsnd (the_default (def_U)) ident - in arg_pconv (abs_pconv cv ident') ctxt tytenv ct end - | t => raise TERM ("forall_pconv", [t]) - -fun all_pconv _ _ = Thm.reflexive - -fun for_pconv cv idents ctxt tytenv ct = - let - fun f rev_idents (Const (\<^const_name>\Pure.all\, _) $ t) = - let val (rev_idents', cv') = f rev_idents (case t of Abs (_,_,u) => u | _ => t) - in - case rev_idents' of - [] => ([], forall_pconv cv' (NONE, NONE)) - | (x :: xs) => (xs, forall_pconv cv' x) - end - | f rev_idents _ = (rev_idents, cv) - in - case f (rev idents) (Thm.term_of ct) of - ([], cv') => cv' ctxt tytenv ct - | _ => raise CTERM ("for_pconv", [ct]) - end - -fun concl_pconv cv ctxt tytenv ct = - case Thm.term_of ct of - (Const (\<^const_name>\Pure.imp\, _) $ _) $ _ => imp_pconv (concl_pconv cv) ctxt tytenv ct - | _ => cv ctxt tytenv ct - -fun asm_pconv cv ctxt tytenv ct = - case Thm.term_of ct of - (Const (\<^const_name>\Pure.imp\, _) $ _) $ _ => CConv.with_prems_cconv ~1 (cv ctxt tytenv) ct - | t => raise TERM ("asm_pconv", [t]) - -fun asms_pconv cv ctxt tytenv ct = - case Thm.term_of ct of - (Const (\<^const_name>\Pure.imp\, _) $ _) $ _ => - ((CConv.with_prems_cconv ~1 oo cv) else_pconv imp_pconv (asms_pconv cv)) ctxt tytenv ct - | t => raise TERM ("asms_pconv", [t]) - -fun judgment_pconv cv ctxt tytenv ct = - if Object_Logic.is_judgment ctxt (Thm.term_of ct) - then arg_pconv cv ctxt tytenv ct - else cv ctxt tytenv ct - -fun in_pconv cv ctxt tytenv ct = - (cv else_pconv - raw_fun_pconv (in_pconv cv) else_pconv - raw_arg_pconv (in_pconv cv) else_pconv - raw_abs_pconv (fn _ => in_pconv cv)) - ctxt tytenv ct - -fun replace_idents idents t = - let - fun subst ((n1, s)::ss) (t as Free (n2, _)) = if n1 = n2 then s else subst ss t - | subst _ t = t - in Term.map_aterms (subst idents) t end - -fun match_pconv cv (t,fixes) ctxt (tyenv, env_ts) ct = - let - val t' = replace_idents env_ts t - val thy = Proof_Context.theory_of ctxt - val u = Thm.term_of ct - - fun descend_hole fixes (Abs (_, _, t)) = - (case descend_hole fixes t of - NONE => NONE - | SOME (fix :: fixes', pos) => SOME (fixes', abs_pconv pos fix) - | SOME ([], _) => raise Match (* less fixes than abstractions on path to hole *)) - | descend_hole fixes (t as l $ r) = - let val (f, _) = strip_comb t - in - if is_hole f - then SOME (fixes, cv) - else - (case descend_hole fixes l of - SOME (fixes', pos) => SOME (fixes', fun_pconv pos) - | NONE => - (case descend_hole fixes r of - SOME (fixes', pos) => SOME (fixes', arg_pconv pos) - | NONE => NONE)) - end - | descend_hole fixes t = - if is_hole t then SOME (fixes, cv) else NONE - - val to_hole = descend_hole (rev fixes) #> the_default ([], cv) #> snd - in - case try (Pattern.match thy (apply2 Logic.mk_term (t',u))) (tyenv, Vartab.empty) of - NONE => raise TERM ("match_pconv: Does not match pattern", [t, t',u]) - | SOME (tyenv', _) => to_hole t ctxt (tyenv', env_ts) ct - end - -fun rewrs_pconv to thms ctxt (tyenv, env_ts) = - let - fun instantiate_normalize_env ctxt env thm = - let - val prop = Thm.prop_of thm - val norm_type = Envir.norm_type o Envir.type_env - val insts = Term.add_vars prop [] - |> map (fn x as (s, T) => - ((s, norm_type env T), Thm.cterm_of ctxt (Envir.norm_term env (Var x)))) - val tyinsts = Term.add_tvars prop [] - |> map (fn x => (x, Thm.ctyp_of ctxt (norm_type env (TVar x)))) - in Drule.instantiate_normalize (tyinsts, insts) thm end - - fun unify_with_rhs context to env thm = - let - val (_, rhs) = thm |> Thm.concl_of |> Logic.dest_equals - val env' = Pattern.unify context (Logic.mk_term to, Logic.mk_term rhs) env - handle Pattern.Unif => raise NO_TO_MATCH - in env' end - - fun inst_thm_to _ (NONE, _) thm = thm - | inst_thm_to (ctxt : Proof.context) (SOME to, env) thm = - instantiate_normalize_env ctxt (unify_with_rhs (Context.Proof ctxt) to env thm) thm - - fun inst_thm ctxt idents (to, tyenv) thm = - let - (* Replace any identifiers with their corresponding bound variables. *) - val maxidx = Term.maxidx_typs (map (snd o snd) (Vartab.dest tyenv)) 0 - val env = Envir.Envir {maxidx = maxidx, tenv = Vartab.empty, tyenv = tyenv} - val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (the_list to) - val thm' = Thm.incr_indexes (maxidx + 1) thm - in SOME (inst_thm_to ctxt (Option.map (replace_idents idents) to, env) thm') end - handle NO_TO_MATCH => NONE - - in CConv.rewrs_cconv (map_filter (inst_thm ctxt env_ts (to, tyenv)) thms) end - -fun rewrite_conv ctxt (pattern, to) thms ct = - let - fun apply_pat At = judgment_pconv - | apply_pat In = in_pconv - | apply_pat Asm = params_pconv o asms_pconv - | apply_pat Concl = params_pconv o concl_pconv - | apply_pat (For idents) = (fn cv => for_pconv cv (map (apfst SOME) idents)) - | apply_pat (Term x) = (fn cv => match_pconv cv (apsnd (map (apfst SOME)) x)) - - val cv = fold_rev apply_pat pattern - - fun distinct_prems th = - case Seq.pull (distinct_subgoals_tac th) of - NONE => th - | SOME (th', _) => th' - - val rewrite = rewrs_pconv to (maps (prep_meta_eq ctxt) thms) - in cv rewrite ctxt (Vartab.empty, []) ct |> distinct_prems end - -fun rewrite_export_tac ctxt (pat, pat_ctxt) thms = - let - val export = case pat_ctxt of - NONE => I - | SOME inner => singleton (Proof_Context.export inner ctxt) - in CCONVERSION (export o rewrite_conv ctxt pat thms) end - -val _ = - Theory.setup - let - fun mk_fix s = (Binding.name s, NONE, NoSyn) - - val raw_pattern : (string, binding * string option * mixfix) pattern list parser = - let - val sep = (Args.$$$ "at" >> K At) || (Args.$$$ "in" >> K In) - val atom = (Args.$$$ "asm" >> K Asm) || - (Args.$$$ "concl" >> K Concl) || - (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.vars []) >> For) || - (Parse.term >> Term) - val sep_atom = sep -- atom >> (fn (s,a) => [s,a]) - - fun append_default [] = [Concl, In] - | append_default (ps as Term _ :: _) = Concl :: In :: ps - | append_default [For x, In] = [For x, Concl, In] - | append_default (For x :: (ps as In :: Term _:: _)) = For x :: Concl :: ps - | append_default ps = ps - - in Scan.repeats sep_atom >> (rev #> append_default) end - - fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) => - let - val (r, toks') = scan toks - val (r', context') = Context.map_proof_result (fn ctxt => f ctxt r) context - in (r', (context', toks' : Token.T list)) end - - fun read_fixes fixes ctxt = - let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx) - in Proof_Context.add_fixes (map read_typ fixes) ctxt end - - fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) = - let - fun add_constrs ctxt n (Abs (x, T, t)) = - let - val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt - in - (case add_constrs ctxt' (n+1) t of - NONE => NONE - | SOME ((ctxt'', n', xs), t') => - let - val U = Type_Infer.mk_param n [] - val u = Type.constraint (U --> dummyT) (Abs (x, T, t')) - in SOME ((ctxt'', n', (x', U) :: xs), u) end) - end - | add_constrs ctxt n (l $ r) = - (case add_constrs ctxt n l of - SOME (c, l') => SOME (c, l' $ r) - | NONE => - (case add_constrs ctxt n r of - SOME (c, r') => SOME (c, l $ r') - | NONE => NONE)) - | add_constrs ctxt n t = - if is_hole_const t then SOME ((ctxt, n, []), t) else NONE - - fun prep (Term s) (n, ctxt) = - let - val t = Syntax.parse_term ctxt s - val ((ctxt', n', bs), t') = - the_default ((ctxt, n, []), t) (add_constrs ctxt (n+1) t) - in (Term (t', bs), (n', ctxt')) end - | prep (For ss) (n, ctxt) = - let val (ns, ctxt') = read_fixes ss ctxt - in (For ns, (n, ctxt')) end - | prep At (n,ctxt) = (At, (n, ctxt)) - | prep In (n,ctxt) = (In, (n, ctxt)) - | prep Concl (n,ctxt) = (Concl, (n, ctxt)) - | prep Asm (n,ctxt) = (Asm, (n, ctxt)) - - val (xs, (_, ctxt')) = fold_map prep ps (0, ctxt) - - in (xs, ctxt') end - - fun prep_args ctxt (((raw_pats, raw_to), raw_ths)) = - let - - fun check_terms ctxt ps to = - let - fun safe_chop (0: int) xs = ([], xs) - | safe_chop n (x :: xs) = chop (n - 1) xs |>> cons x - | safe_chop _ _ = raise Match - - fun reinsert_pat _ (Term (_, cs)) (t :: ts) = - let val (cs', ts') = safe_chop (length cs) ts - in (Term (t, map dest_Free cs'), ts') end - | reinsert_pat _ (Term _) [] = raise Match - | reinsert_pat ctxt (For ss) ts = - let val fixes = map (fn s => (s, Variable.default_type ctxt s)) ss - in (For fixes, ts) end - | reinsert_pat _ At ts = (At, ts) - | reinsert_pat _ In ts = (In, ts) - | reinsert_pat _ Concl ts = (Concl, ts) - | reinsert_pat _ Asm ts = (Asm, ts) - - fun free_constr (s,T) = Type.constraint T (Free (s, dummyT)) - fun mk_free_constrs (Term (t, cs)) = t :: map free_constr cs - | mk_free_constrs _ = [] - - val ts = maps mk_free_constrs ps @ the_list to - |> Syntax.check_terms (hole_syntax ctxt) - val ctxt' = fold Variable.declare_term ts ctxt - val (ps', (to', ts')) = fold_map (reinsert_pat ctxt') ps ts - ||> (fn xs => case to of NONE => (NONE, xs) | SOME _ => (SOME (hd xs), tl xs)) - val _ = case ts' of (_ :: _) => raise Match | [] => () - in ((ps', to'), ctxt') end - - val (pats, ctxt') = prep_pats ctxt raw_pats - - val ths = Attrib.eval_thms ctxt' raw_ths - val to = Option.map (Syntax.parse_term ctxt') raw_to - - val ((pats', to'), ctxt'') = check_terms ctxt' pats to - - in ((pats', ths, (to', ctxt)), ctxt'') end - - val to_parser = Scan.option ((Args.$$$ "to") |-- Parse.term) - - val subst_parser = - let val scan = raw_pattern -- to_parser -- Parse.thms1 - in context_lift scan prep_args end - - fun rewrite_export_ctac inputs inthms = - CONTEXT_TACTIC' (fn ctxt => rewrite_export_tac ctxt inputs inthms) - in - Method.setup \<^binding>\rewr\ (subst_parser >> - (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => SIMPLE_METHOD' - (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms))) - "single-step rewriting, allowing subterm selection via patterns" #> - Method.setup \<^binding>\rewrite\ (subst_parser >> - (fn (pattern, inthms, (to, pat_ctxt)) => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS 0 - (rewrite_export_ctac ((pattern, to), SOME pat_ctxt) inthms))))) - "single-step rewriting with auto-typechecking" - end -end diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy index 1501221..4beb9b6 100644 --- a/spartan/lib/List.thy +++ b/spartan/lib/List.thy @@ -114,7 +114,7 @@ Lemma head_type [type]: Lemma head_of_cons [comp]: assumes "A: U i" "x: A" "xs: List A" shows "head (x # xs) \ some x" - unfolding head_def by reduce + unfolding head_def by compute Lemma tail_type [type]: assumes "A: U i" "xs: List A" @@ -124,7 +124,7 @@ Lemma tail_type [type]: Lemma tail_of_cons [comp]: assumes "A: U i" "x: A" "xs: List A" shows "tail (x # xs) \ xs" - unfolding tail_def by reduce + unfolding tail_def by compute subsection \Append\ @@ -185,7 +185,7 @@ Lemma rev_type [type]: Lemma rev_nil [comp]: assumes "A: U i" shows "rev (nil A) \ nil A" - unfolding rev_def by reduce + unfolding rev_def by compute end diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy index e06a07b..452acc2 100644 --- a/spartan/lib/Maybe.thy +++ b/spartan/lib/Maybe.thy @@ -40,7 +40,7 @@ Lemma Maybe_comp_none: shows "MaybeInd A C c\<^sub>0 f (none A) \ c\<^sub>0" using assms unfolding Maybe_def MaybeInd_def none_def some_def - by reduce + by compute Lemma Maybe_comp_some: assumes @@ -52,7 +52,7 @@ Lemma Maybe_comp_some: shows "MaybeInd A C c\<^sub>0 f (some A a) \ f a" using assms unfolding Maybe_def MaybeInd_def none_def some_def - by reduce + by compute lemmas [form] = MaybeF and diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy index 0043c1e..56adbfc 100644 --- a/spartan/lib/Prelude.thy +++ b/spartan/lib/Prelude.thy @@ -116,7 +116,7 @@ Lemma if_true: shows "ifelse C true a b \ a" unfolding ifelse_def true_def using assms unfolding Bool_def true_def false_def - by reduce + by compute Lemma if_false: assumes @@ -126,7 +126,7 @@ Lemma if_false: shows "ifelse C false a b \ b" unfolding ifelse_def false_def using assms unfolding Bool_def true_def false_def - by reduce + by compute lemmas [form] = BoolF and @@ -145,7 +145,7 @@ translations "if x then a else b" \ "CONST ifelse C x a b" subsection \Logical connectives\ -definition not ("!_") where "not x \ ifelse (K Bool) x false true" +definition not ("!_") where "!x \ ifelse (K Bool) x false true" end -- cgit v1.2.3