From ff5454812f9e2720bd90c3a5437505644f63b487 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 31 Jul 2020 14:56:24 +0200 Subject: (FEAT) Term elaboration of assumption and goal statements. . spartan/core/goals.ML . spartan/core/elaboration.ML . spartan/core/elaborated_statement.ML (FEAT) More context tacticals and search tacticals. . spartan/core/context_tactical.ML (FEAT) Improved subgoal focus. Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY). . spartan/core/focus.ML (FIX) Normalize facts in order to be able to resolve properly. . spartan/core/typechecking.ML (MAIN) New definitions. (MAIN) Renamed theories and theorems. (MAIN) Refactor theories to fit new features. --- ROOT | 6 +- hott/Equivalence.thy | 456 +++++++++++++++++++--------------- hott/Identity.thy | 239 +++++++++--------- hott/List+.thy | 18 ++ hott/More_List.thy | 18 -- hott/More_Nat.thy | 43 ---- hott/Nat.thy | 58 ++--- spartan/core/Spartan.thy | 70 +++--- spartan/core/context_tactical.ML | 100 ++++++++ spartan/core/elaborated_assumption.ML | 446 --------------------------------- spartan/core/elaborated_statement.ML | 441 ++++++++++++++++++++++++++++++++ spartan/core/elaboration.ML | 17 +- spartan/core/focus.ML | 96 ++++--- spartan/core/goals.ML | 10 +- spartan/core/tactics.ML | 3 +- spartan/core/typechecking.ML | 8 +- spartan/lib/List.thy | 10 +- spartan/lib/Maybe.thy | 19 +- spartan/lib/More_Types.thy | 150 ----------- spartan/lib/Prelude.thy | 150 +++++++++++ 20 files changed, 1250 insertions(+), 1108 deletions(-) create mode 100644 hott/List+.thy delete mode 100644 hott/More_List.thy delete mode 100644 hott/More_Nat.thy delete mode 100644 spartan/core/elaborated_assumption.ML create mode 100644 spartan/core/elaborated_statement.ML delete mode 100644 spartan/lib/More_Types.thy create mode 100644 spartan/lib/Prelude.thy diff --git a/ROOT b/ROOT index 00d020a..b3aa520 100644 --- a/ROOT +++ b/ROOT @@ -14,7 +14,7 @@ session Spartan in spartan = Spartan_Core + directories lib theories - More_Types + Prelude Maybe List @@ -29,6 +29,4 @@ session HoTT in hott = Spartan + Identity Equivalence Nat - More_List - More_Nat - + "List+" diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index d844b59..66c64f6 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -16,53 +16,68 @@ Lemma homotopy_type [typechk]: assumes "A: U i" "\x. x: A \ B x: U i" - "f: \x: A. B x" "g: \x: A. B x" + "f: \x: A. B x" + "g: \x: A. B x" shows "f ~ g: U i" - unfolding homotopy_def by typechk + unfolding homotopy_def + by typechk -Lemma (derive) homotopy_refl [refl]: +Lemma apply_homotopy: + assumes + "A: U i" "\x. x: A \ B x: U i" + "f: \x: A. B x" "g: \x: A. B x" + "H: f ~ g" + "x: A" + shows "H x: f x = g x" + using \H:_\ unfolding homotopy_def + by typechk + +method htpy for H::o = rule apply_homotopy[where ?H=H] + +Lemma (def) homotopy_refl [refl]: assumes "A: U i" "f: \x: A. B x" shows "f ~ f" - unfolding homotopy_def by intros + unfolding homotopy_def + by intros -Lemma (derive) hsym: +Lemma (def) hsym: assumes - "f: \x: A. B x" - "g: \x: A. B x" "A: U i" "\x. x: A \ B x: U i" + "f: \x: A. B x" + "g: \x: A. B x" "H: f ~ g" shows "g ~ f" -unfolding homotopy_def -proof intro - fix x assume "x: A" then have "H x: f x = g x" - using \H:_\[unfolded homotopy_def] - \ \this should become unnecessary when definitional unfolding is implemented\ - by typechk - thus "g x = f x" by (rule pathinv) fact -qed typechk - -Lemma (derive) htrans: + unfolding homotopy_def + proof intro + fix x assume "x: A" then have "f x = g x" + by (htpy H) + thus "g x = f x" + by (rule pathinv) fact + qed + +Lemma (def) htrans: assumes + "A: U i" + "\x. x: A \ B x: U i" "f: \x: A. B x" "g: \x: A. B x" "h: \x: A. B x" - "A: U i" - "\x. x: A \ B x: U i" - shows "\H1: f ~ g; H2: g ~ h\ \ f ~ h" + "H1: f ~ g" + "H2: g ~ h" + shows "f ~ h" unfolding homotopy_def - apply intro - \ vars x - apply (rule pathcomp[where ?y="g x"]) - \<^item> by (elim H1) - \<^item> by (elim H2) - done - \ by typechk - done + proof intro + fix x assume "x: A" + have *: "f x = g x" "g x = h x" + by (htpy H1, htpy H2) + show "f x = h x" + by (rule pathcomp; (rule *)?) typechk + qed -text \For calculations:\ +section \Rewriting homotopies\ congruence "f ~ g" rhs g @@ -70,229 +85,258 @@ lemmas homotopy_sym [sym] = hsym[rotated 4] and homotopy_trans [trans] = htrans[rotated 5] -Lemma (derive) commute_homotopy: - assumes - "A: U i" "B: U i" - "x: A" "y: A" - "p: x = y" - "f: A \ B" "g: A \ B" - "H: f ~ g" - shows "(H x) \ g[p] = f[p] \ (H y)" - \ \Need this assumption unfolded for typechecking\ - supply assms(8)[unfolded homotopy_def] - apply (eq p) - focus vars x - apply reduce - \ \Here it would really be nice to have automation for transport and - propositional equality.\ - apply (rule use_transport[where ?y="H x \ refl (g x)"]) - \ by (rule pathcomp_refl) - \ by (rule pathinv) (rule refl_pathcomp) - \ by typechk - done - done - -Corollary (derive) commute_homotopy': - assumes - "A: U i" - "x: A" - "f: A \ A" - "H: f ~ (id A)" - shows "H (f x) = f [H x]" -oops - -Lemma homotopy_id_left [typechk]: +Lemma id_funcomp_htpy: assumes "A: U i" "B: U i" "f: A \ B" shows "homotopy_refl A f: (id B) \ f ~ f" - unfolding homotopy_refl_def homotopy_def by reduce + by reduce -Lemma homotopy_id_right [typechk]: +Lemma funcomp_id_htpy: assumes "A: U i" "B: U i" "f: A \ B" shows "homotopy_refl A f: f \ (id A) ~ f" - unfolding homotopy_refl_def homotopy_def - by reduce + by reduce -Lemma homotopy_funcomp_left: +Lemma funcomp_left_htpy: assumes - "H: homotopy B C g g'" + "A: U i" "B: U i" + "\x. x: B \ C x: U i" "f: A \ B" "g: \x: B. C x" "g': \x: B. C x" - "A: U i" "B: U i" - "\x. x: B \ C x: U i" - shows "homotopy A {} (g \\<^bsub>A\<^esub> f) (g' \\<^bsub>A\<^esub> f)" + "H: g ~ g'" + shows "(g \ f) ~ (g' \ f)" unfolding homotopy_def - apply (intro; reduce) - apply (insert \H: _\[unfolded homotopy_def]) - apply (elim H) + apply (intro, reduce) + apply (htpy H) done -Lemma homotopy_funcomp_right: +Lemma funcomp_right_htpy: assumes - "H: homotopy A (fn _. B) f f'" + "A: U i" "B: U i" "C: U i" "f: A \ B" "f': A \ B" "g: B \ C" - "A: U i" "B: U i" "C: U i" - shows "homotopy A {} (g \\<^bsub>A\<^esub> f) (g \\<^bsub>A\<^esub> f')" + "H: f ~ f'" + shows "(g \ f) ~ (g \ f')" unfolding homotopy_def - apply (intro; reduce) - apply (insert \H: _\[unfolded homotopy_def]) - apply (dest PiE, assumption) - apply (rule ap, assumption) - done + proof (intro, reduce) + fix x assume "x: A" + have *: "f x = f' x" + by (htpy H) + show "g (f x) = g (f' x)" + by (transport eq: *) refl + qed -method id_htpy = (rule homotopy_id_left) -method htpy_id = (rule homotopy_id_right) -method htpy_o = (rule homotopy_funcomp_left) -method o_htpy = (rule homotopy_funcomp_right) +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" + "x: A" "y: A" + "p: x = y" + "f: A \ B" "g: A \ B" + "H: f ~ g" + 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) + by refl + +Corollary (def) commute_homotopy': + assumes + "A: U i" + "x: A" + "f: A \ A" + "H: f ~ (id A)" + shows "H (f x) = f [H x]" +oops section \Quasi-inverse and bi-invertibility\ subsection \Quasi-inverses\ -definition "qinv A B f \ \g: B \ A. +definition "is_qinv A B f \ \g: B \ A. homotopy A (fn _. A) (g \\<^bsub>A\<^esub> f) (id A) \ homotopy B (fn _. B) (f \\<^bsub>B\<^esub> g) (id B)" -lemma qinv_type [typechk]: +lemma is_qinv_type [typechk]: assumes "A: U i" "B: U i" "f: A \ B" - shows "qinv A B f: U i" - unfolding qinv_def by typechk + shows "is_qinv A B f: U i" + unfolding is_qinv_def + by typechk -definition qinv_i ("qinv") - where [implicit]: "qinv f \ Equivalence.qinv ? ? f" +definition is_qinv_i ("is'_qinv") + where [implicit]: "is_qinv f \ Equivalence.is_qinv ? ? f" -translations "qinv f" \ "CONST Equivalence.qinv A B f" +no_translations "is_qinv f" \ "CONST Equivalence.is_qinv A B f" -Lemma (derive) id_qinv: +Lemma (def) id_is_qinv: assumes "A: U i" - shows "qinv (id A)" - unfolding qinv_def + shows "is_qinv (id A)" + unfolding is_qinv_def proof intro show "id A: A \ A" by typechk qed (reduce, intro; refl) -Lemma (derive) quasiinv_qinv: - assumes "A: U i" "B: U i" "f: A \ B" - shows "prf: qinv f \ qinv (fst prf)" - unfolding qinv_def - apply intro - \ by (rule \f:_\) - \ apply (elim "prf") - focus vars g HH - apply intro - \<^item> by reduce (snd HH) - \<^item> by reduce (fst HH) - done - done +Lemma is_qinvI: + assumes + "A: U i" "B: U i" "f: A \ B" + "g: B \ A" + "H1: g \ f ~ id A" + "H2: f \ g ~ id B" + shows "is_qinv f" + unfolding is_qinv_def + proof intro + show "g: B \ A" by fact + show "g \ f ~ id A \ f \ g ~ id B" by (intro; fact) + qed + +Lemma is_qinv_components [typechk]: + assumes "A: U i" "B: U i" "f: A \ B" "pf: is_qinv f" + shows + fst_of_is_qinv: "fst pf: B \ A" and + p\<^sub>2\<^sub>1_of_is_qinv: "p\<^sub>2\<^sub>1 pf: fst pf \ f ~ id A" and + p\<^sub>2\<^sub>2_of_is_qinv: "p\<^sub>2\<^sub>2 pf: f \ fst pf ~ id B" + using assms unfolding is_qinv_def + by typechk+ + +Lemma (def) qinv_is_qinv: + assumes "A: U i" "B: U i" "f: A \ B" "pf: is_qinv f" + shows "is_qinv (fst pf)" +using [[debug_typechk]] + using [[solve_side_conds=2]] + apply (rule is_qinvI) + back \ \Typechecking/inference goes too far here. Problem would likely be + solved with definitional unfolding\ + \<^item> by (fact \f:_\) + \<^item> by (rule p\<^sub>2\<^sub>2_of_is_qinv) + \<^item> by (rule p\<^sub>2\<^sub>1_of_is_qinv) done -Lemma (derive) funcomp_qinv: +Lemma (def) funcomp_is_qinv: assumes "A: U i" "B: U i" "C: U i" "f: A \ B" "g: B \ C" - shows "qinv f \ qinv g \ qinv (g \ f)" - apply (intros, unfold qinv_def, elims) - focus prems vars _ _ finv _ ginv - apply (intro, rule funcompI[where ?f=ginv and ?g=finv]) - proof (reduce, intro) - have "finv \ ginv \ g \ f ~ finv \ (ginv \ g) \ f" by reduce refl - also have ".. ~ finv \ id B \ f" by (o_htpy, htpy_o) fact - also have ".. ~ id A" by reduce fact - finally show "finv \ ginv \ g \ f ~ id A" by this - - have "g \ f \ finv \ ginv ~ g \ (f \ finv) \ ginv" by reduce refl - also have ".. ~ g \ id B \ ginv" by (o_htpy, htpy_o) fact - also have ".. ~ id C" by reduce fact - finally show "g \ f \ finv \ ginv ~ id C" by this - qed + shows "is_qinv f \ is_qinv g \ is_qinv (g \ f)" + apply intros + unfolding is_qinv_def apply elims + focus vars _ _ finv _ ginv + apply intro + \<^item> by (rule funcompI[where ?f=ginv and ?g=finv]) + \<^item> proof intro + show "(finv \ ginv) \ g \ f ~ id A" + proof - + 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 + qed + + show "(g \ f) \ finv \ ginv ~ id C" + proof - + 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 + qed + qed + done done subsection \Bi-invertible maps\ -definition "biinv A B f \ +definition "is_biinv A B f \ (\g: B \ A. homotopy A (fn _. A) (g \\<^bsub>A\<^esub> f) (id A)) \ (\g: B \ A. homotopy B (fn _. B) (f \\<^bsub>B\<^esub> g) (id B))" -lemma biinv_type [typechk]: +lemma is_biinv_type [typechk]: assumes "A: U i" "B: U i" "f: A \ B" - shows "biinv A B f: U i" - unfolding biinv_def by typechk + shows "is_biinv A B f: U i" + unfolding is_biinv_def by typechk -definition biinv_i ("biinv") - where [implicit]: "biinv f \ Equivalence.biinv ? ? f" +definition is_biinv_i ("is'_biinv") + where [implicit]: "is_biinv f \ Equivalence.is_biinv ? ? f" -translations "biinv f" \ "CONST Equivalence.biinv A B f" +translations "is_biinv f" \ "CONST Equivalence.is_biinv A B f" -Lemma (derive) qinv_imp_biinv: +Lemma is_biinvI: assumes - "A: U i" "B: U i" - "f: A \ B" - shows "?prf: qinv f \ biinv f" - apply intros - unfolding qinv_def biinv_def - by (rule Sig_dist_exp) - -text \ - Show that bi-invertible maps are quasi-inverses, as a demonstration of how to - work in this system. -\ + "A: U i" "B: U i" "f: A \ B" + "g: B \ A" "h: B \ A" + "H1: g \ f ~ id A" "H2: f \ h ~ id B" + shows "is_biinv f" + unfolding is_biinv_def + proof intro + show ": {}" by typechk + show ": {}" by typechk + qed -Lemma (derive) biinv_imp_qinv: +Lemma is_biinv_components [typechk]: + assumes "A: U i" "B: U i" "f: A \ B" "pf: is_biinv f" + shows + p\<^sub>1\<^sub>1_of_is_biinv: "p\<^sub>1\<^sub>1 pf: B \ A" and + p\<^sub>2\<^sub>1_of_is_biinv: "p\<^sub>2\<^sub>1 pf: B \ A" and + p\<^sub>1\<^sub>2_of_is_biinv: "p\<^sub>1\<^sub>2 pf: p\<^sub>1\<^sub>1 pf \ f ~ id A" and + p\<^sub>2\<^sub>2_of_is_biinv: "p\<^sub>2\<^sub>2 pf: f \ p\<^sub>2\<^sub>1 pf ~ id B" + using assms unfolding is_biinv_def + by typechk+ + +Lemma (def) is_qinv_imp_is_biinv: assumes "A: U i" "B: U i" "f: A \ B" - shows "biinv f \ qinv f" + shows "is_qinv f \ is_biinv f" + apply intros + unfolding is_qinv_def is_biinv_def + by (rule distribute_Sig) - text \Split the hypothesis \<^term>\biinv f\ into its components:\ - apply intro - unfolding biinv_def - apply elims - - text \Name the components:\ - focus prems vars _ _ _ g H1 h H2 - thm \g:_\ \h:_\ \H1:_\ \H2:_\ - - text \ - \<^term>\g\ is a quasi-inverse to \<^term>\f\, so the proof will be a triple - \<^term>\>\. - \ - unfolding qinv_def +Lemma (def) is_biinv_imp_is_qinv: + assumes "A: U i" "B: U i" "f: A \ B" + shows "is_biinv f \ is_qinv f" apply intro - \ by (fact \g: _\) - \ apply intro - text \The first part \<^prop>\?H1: g \ f ~ id A\ is given by \<^term>\H1\.\ - apply (fact \H1: _\) + text \Split the hypothesis \<^term>\is_biinv f\ into its components and name them.\ + unfolding is_biinv_def apply elims + focus vars _ _ _ g H1 h H2 + text \Need to give the required function and homotopies.\ + apply (rule is_qinvI) + text \We claim that \<^term>\g\ is a quasi-inverse to \<^term>\f\.\ + \<^item> by (fact \g: _\) + + text \The first part \<^prop>\?H1: g \ f ~ id A\ is given by \<^term>\H1\.\ + \<^item> by (fact \H1: _\) + text \ It remains to prove \<^prop>\?H2: f \ g ~ id B\. First show that \g ~ h\, then the result follows from @{thm \H2: f \ h ~ id B\}. Here a proof - block is used to calculate "forward". + block is used for calculational reasoning. \ - proof - - have "g ~ g \ (id B)" by reduce refl - also have ".. ~ g \ f \ h" by o_htpy (rule \H2:_\[symmetric]) - also have ".. ~ (id A) \ h" by (subst funcomp_assoc[symmetric]) (htpy_o, fact) - also have ".. ~ h" by reduce refl - finally have "g ~ h" by this - then have "f \ g ~ f \ h" by (o_htpy, this) - also note \H2:_\ - finally show "f \ g ~ id B" by this - qed + \<^item> proof - + have "g ~ g \ (id B)" by reduce 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 + finally have "g ~ h" by this + then have "f \ g ~ f \ h" by (rhtpy, this) + also note \H2:_\ + finally show "f \ g ~ id B" by this + qed done done -Lemma (derive) id_biinv: - "A: U i \ biinv (id A)" - by (rule qinv_imp_biinv) (rule id_qinv) +Lemma (def) id_is_biinv: + "A: U i \ is_biinv (id A)" + by (rule is_qinv_imp_is_biinv) (rule id_is_qinv) -Lemma (derive) funcomp_biinv: +Lemma (def) funcomp_is_biinv: assumes "A: U i" "B: U i" "C: U i" "f: A \ B" "g: B \ C" - shows "biinv f \ biinv g \ biinv (g \ f)" + shows "is_biinv f \ is_biinv g \ is_biinv (g \ f)" apply intros - focus vars biinv\<^sub>f biinv\<^sub>g - by (rule qinv_imp_biinv) (rule funcomp_qinv; rule biinv_imp_qinv) + focus vars pf pg + by (rule is_qinv_imp_is_biinv) + (rule funcomp_is_qinv; rule is_biinv_imp_is_qinv, fact) done @@ -304,19 +348,19 @@ text \ \ definition equivalence (infix "\" 110) - where "A \ B \ \f: A \ B. Equivalence.biinv A B f" + where "A \ B \ \f: A \ B. Equivalence.is_biinv A B f" lemma equivalence_type [typechk]: assumes "A: U i" "B: U i" shows "A \ B: U i" unfolding equivalence_def by typechk -Lemma (derive) equivalence_refl: +Lemma (def) equivalence_refl: assumes "A: U i" shows "A \ A" unfolding equivalence_def proof intro - show "biinv (id A)" by (rule qinv_imp_biinv) (rule id_qinv) + show "is_biinv (id A)" by (rule is_qinv_imp_is_biinv) (rule id_is_qinv) qed typechk text \ @@ -324,32 +368,30 @@ text \ univalence?)... \ -Lemma (derive) equivalence_symmetric: +Lemma (def) equivalence_symmetric: assumes "A: U i" "B: U i" shows "A \ B \ B \ A" apply intros unfolding equivalence_def apply elim - \ vars _ f "prf" - apply (dest (4) biinv_imp_qinv) - apply intro - \<^item> unfolding qinv_def by (rule fst[of "(biinv_imp_qinv A B f) prf"]) - \<^item> by (rule qinv_imp_biinv) (rule quasiinv_qinv) - done + apply (dest (4) is_biinv_imp_is_qinv) + apply intro + \<^item> by (rule fst_of_is_qinv) facts + \<^item> by (rule is_qinv_imp_is_biinv) (rule qinv_is_qinv) done -Lemma (derive) equivalence_transitive: +Lemma (def) equivalence_transitive: assumes "A: U i" "B: U i" "C: U i" shows "A \ B \ B \ C \ A \ C" proof intros fix AB BC assume *: "AB: A \ B" "BC: B \ C" then have - "fst AB: A \ B" and 1: "snd AB: biinv (fst AB)" - "fst BC: B \ C" and 2: "snd BC: biinv (fst BC)" + "fst AB: A \ B" and 1: "snd AB: is_biinv (fst AB)" + "fst BC: B \ C" and 2: "snd BC: is_biinv (fst BC)" unfolding equivalence_def by typechk+ then have "fst BC \ fst AB: A \ C" by typechk - moreover have "biinv (fst BC \ fst AB)" - using * unfolding equivalence_def by (rules funcomp_biinv 1 2) + moreover have "is_biinv (fst BC \ fst AB)" + using * unfolding equivalence_def by (rule funcomp_is_biinv 1 2) facts ultimately show "A \ C" unfolding equivalence_def by intro facts qed @@ -370,14 +412,14 @@ text \ (2) we don't yet have universe automation. \ -Lemma (derive) id_imp_equiv: +Lemma (def) id_imp_equiv: assumes "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B" shows ": A \ B" unfolding equivalence_def apply intros defer - \ apply (eq p) - \<^item> prems vars A B + \<^item> apply (eq p) + \<^enum> vars A B apply (rewrite at A in "A \ B" id_comp[symmetric]) using [[solve_side_conds=1]] apply (rewrite at B in "_ \ B" id_comp[symmetric]) @@ -385,16 +427,16 @@ Lemma (derive) id_imp_equiv: apply (rule lift_universe_codomain, rule Ui_in_USi) apply (typechk, rule Ui_in_USi) done - \<^item> prems vars A + \<^enum> vars A using [[solve_side_conds=1]] apply (subst transport_comp) - \<^enum> by (rule Ui_in_USi) - \<^enum> by reduce (rule in_USi_if_in_Ui) - \<^enum> by reduce (rule id_biinv) + \ by (rule Ui_in_USi) + \ by reduce (rule in_USi_if_in_Ui) + \ by reduce (rule id_is_biinv) done done - \ \ \Similar proof as in the first subgoal above\ + \<^item> \ \Similar proof as in the first subgoal above\ apply (rewrite at A in "A \ B" id_comp[symmetric]) using [[solve_side_conds=1]] apply (rewrite at B in "_ \ B" id_comp[symmetric]) @@ -419,8 +461,8 @@ no_translations "lift P p u" \ "CONST pathlift A P x y p u" "apd f p" \ "CONST Identity.apd A P f x y p" "f ~ g" \ "CONST homotopy A B f g" - "qinv f" \ "CONST Equivalence.qinv A B f" - "biinv f" \ "CONST Equivalence.biinv A B f" + "is_qinv f" \ "CONST Equivalence.is_qinv A B f" + "is_biinv f" \ "CONST Equivalence.is_biinv A B f" *) diff --git a/hott/Identity.thy b/hott/Identity.thy index 728537c..d6efbf8 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -42,7 +42,7 @@ axiomatization where lemmas [form] = IdF and [intro, intros] = IdI and - [elim "?p" "?a" "?b"] = IdE and + [elim ?p ?a ?b] = IdE and [comp] = Id_comp and [refl] = IdI @@ -77,34 +77,34 @@ method_setup eq = section \Symmetry and transitivity\ -Lemma (derive) pathinv: +Lemma (def) pathinv: assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" shows "y =\<^bsub>A\<^esub> x" by (eq p) intro lemma pathinv_comp [comp]: - assumes "x: A" "A: U i" + assumes "A: U i" "x: A" shows "pathinv A x x (refl x) \ refl x" unfolding pathinv_def by reduce -Lemma (derive) pathcomp: +Lemma (def) pathcomp: assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z" shows "x =\<^bsub>A\<^esub> z" - apply (eq p) - focus prems vars x p - apply (eq p) - apply intro - done - done + proof (eq p) + fix x q assume "x: A" and "q: x =\<^bsub>A\<^esub> z" + show "x =\<^bsub>A\<^esub> z" by (eq q) refl + qed lemma pathcomp_comp [comp]: - assumes "a: A" "A: U i" + assumes "A: U i" "a: A" shows "pathcomp A a a a (refl a) (refl a) \ refl a" unfolding pathcomp_def by reduce +method pathcomp for p q :: o = rule pathcomp[where ?p=p and ?q=q] + section \Notation\ @@ -134,26 +134,22 @@ lemmas section \Basic propositional equalities\ -Lemma (derive) refl_pathcomp: +Lemma (def) refl_pathcomp: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "(refl x) \ p = p" - apply (eq p) - apply (reduce; intro) - done + by (eq p) (reduce, refl) -Lemma (derive) pathcomp_refl: +Lemma (def) pathcomp_refl: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p \ (refl y) = p" - apply (eq p) - apply (reduce; intro) - done + by (eq p) (reduce, refl) -definition [implicit]: "ru p \ pathcomp_refl ? ? ? p" definition [implicit]: "lu p \ refl_pathcomp ? ? ? p" +definition [implicit]: "ru p \ pathcomp_refl ? ? ? p" translations - "CONST ru p" \ "CONST pathcomp_refl A x y p" "CONST lu p" \ "CONST refl_pathcomp A x y p" + "CONST ru p" \ "CONST pathcomp_refl A x y p" Lemma lu_refl [comp]: assumes "A: U i" "x: A" @@ -165,40 +161,40 @@ Lemma ru_refl [comp]: shows "ru (refl x) \ refl (refl x)" unfolding pathcomp_refl_def by reduce -Lemma (derive) inv_pathcomp: +Lemma (def) inv_pathcomp: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p\ \ p = refl y" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) -Lemma (derive) pathcomp_inv: +Lemma (def) pathcomp_inv: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p \ p\ = refl x" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) -Lemma (derive) pathinv_pathinv: +Lemma (def) pathinv_pathinv: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p\\ = p" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) -Lemma (derive) pathcomp_assoc: +Lemma (def) pathcomp_assoc: assumes "A: U i" "x: A" "y: A" "z: A" "w: A" "p: x = y" "q: y = z" "r: z = w" shows "p \ (q \ r) = p \ q \ r" - apply (eq p) - focus prems vars x p - apply (eq p) - focus prems vars x p - apply (eq p) - apply (reduce; intro) - done - done - done + proof (eq p) + fix x q assuming "x: A" "q: x = z" + show "refl x \ (q \ r) = refl x \ q \ r" + 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) + qed + qed section \Functoriality of functions\ -Lemma (derive) ap: +Lemma (def) ap: assumes "A: U i" "B: U i" "x: A" "y: A" @@ -213,11 +209,11 @@ definition ap_i ("_[_]" [1000, 0]) translations "f[p]" \ "CONST ap A B x y f p" Lemma ap_refl [comp]: - assumes "f: A \ B" "x: A" "A: U i" "B: U i" + assumes "A: U i" "B: U i" "f: A \ B" "x: A" shows "f[refl x] \ refl (f x)" unfolding ap_def by reduce -Lemma (derive) ap_pathcomp: +Lemma (def) ap_pathcomp: assumes "A: U i" "B: U i" "x: A" "y: A" "z: A" @@ -225,48 +221,45 @@ Lemma (derive) ap_pathcomp: "p: x = y" "q: y = z" shows "f[p \ q] = f[p] \ f[q]" - apply (eq p) - focus prems vars x p - apply (eq p) - apply (reduce; intro) - done - done + 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) + qed -Lemma (derive) ap_pathinv: +Lemma (def) ap_pathinv: assumes "A: U i" "B: U i" "x: A" "y: A" "f: A \ B" "p: x = y" shows "f[p\] = f[p]\" - by (eq p) (reduce; intro) - -text \The next two proofs currently use some low-level rewriting.\ + by (eq p) (reduce, refl) -Lemma (derive) ap_funcomp: +Lemma (def) ap_funcomp: assumes "A: U i" "B: U i" "C: U i" "x: A" "y: A" "f: A \ B" "g: B \ C" "p: x = y" - shows "(g \ f)[p] = g[f[p]]" + shows "(g \ f)[p] = g[f[p]]" thm ap apply (eq p) - \ by reduce - \ by reduce intro + \<^item> by reduce + \<^item> by reduce refl done -Lemma (derive) ap_id: +Lemma (def) ap_id: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "(id A)[p] = p" apply (eq p) - \ by reduce - \ by reduce intro + \<^item> by reduce + \<^item> by reduce refl done section \Transport\ -Lemma (derive) transport: +Lemma (def) transport: assumes "A: U i" "\x. x: A \ P x: U i" @@ -288,22 +281,18 @@ Lemma transport_comp [comp]: shows "trans P (refl a) \ id (P a)" unfolding transport_def by reduce -\ \TODO: Build transport automation!\ - -Lemma use_transport: +Lemma apply_transport: assumes + "A: U i" "\x. x: A \ P x: U i" + "x: A" "y: A" "p: y =\<^bsub>A\<^esub> x" "u: P x" - "x: A" "y: A" - "A: U i" - "\x. x: A \ P x: U i" shows "trans P p\ u: P y" - unfolding transport_def pathinv_def by typechk -method transport uses eq = (rule use_transport[OF eq]) +method transport uses eq = (rule apply_transport[OF _ _ _ _ eq]) -Lemma (derive) transport_left_inv: +Lemma (def) transport_left_inv: assumes "A: U i" "\x. x: A \ P x: U i" @@ -312,16 +301,16 @@ Lemma (derive) transport_left_inv: shows "(trans P p\) \ (trans P p) = id (P x)" by (eq p) (reduce; refl) -Lemma (derive) transport_right_inv: +Lemma (def) transport_right_inv: assumes "A: U i" "\x. x: A \ P x: U i" "x: A" "y: A" "p: x = y" shows "(trans P p) \ (trans P p\) = id (P y)" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) -Lemma (derive) transport_pathcomp: +Lemma (def) transport_pathcomp: assumes "A: U i" "\x. x: A \ P x: U i" @@ -329,14 +318,14 @@ Lemma (derive) transport_pathcomp: "u: P x" "p: x = y" "q: y = z" shows "trans P q (trans P p u) = trans P (p \ q) u" - apply (eq p) - focus prems vars x p - apply (eq p) - apply (reduce; intro) - done - done - -Lemma (derive) transport_compose_typefam: +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" + by (eq q) (reduce, refl) +qed + +Lemma (def) transport_compose_typefam: assumes "A: U i" "B: U i" "\x. x: B \ P x: U i" @@ -345,9 +334,9 @@ Lemma (derive) transport_compose_typefam: "p: x = y" "u: P (f x)" shows "trans (fn x. P (f x)) p u = trans P f[p] u" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) -Lemma (derive) transport_function_family: +Lemma (def) transport_function_family: assumes "A: U i" "\x. x: A \ P x: U i" @@ -357,15 +346,15 @@ Lemma (derive) transport_function_family: "u: P x" "p: x = y" shows "trans Q p ((f x) u) = (f y) (trans P p u)" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) -Lemma (derive) transport_const: +Lemma (def) transport_const: assumes "A: U i" "B: U i" "x: A" "y: A" "p: x = y" shows "\b: B. trans (fn _. B) p b = b" - by (intro, eq p) (reduce; intro) + by intro (eq p, reduce, refl) definition transport_const_i ("trans'_const") where [implicit]: "trans_const B p \ transport_const ? B ? ? p" @@ -376,10 +365,10 @@ 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 "trans_const B (refl x) b \ refl b" unfolding transport_const_def by reduce -Lemma (derive) pathlift: +Lemma (def) pathlift: assumes "A: U i" "\x. x: A \ P x: U i" @@ -387,7 +376,7 @@ Lemma (derive) pathlift: "p: x = y" "u: P x" shows " = " - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) definition pathlift_i ("lift") where [implicit]: "lift P p u \ pathlift ? P ? ? p u" @@ -403,7 +392,7 @@ Lemma pathlift_comp [comp]: shows "lift P (refl x) u \ refl " unfolding pathlift_def by reduce -Lemma (derive) pathlift_fst: +Lemma (def) pathlift_fst: assumes "A: U i" "\x. x: A \ P x: U i" @@ -412,14 +401,14 @@ Lemma (derive) pathlift_fst: "p: x = y" shows "fst[lift P p u] = p" apply (eq p) - \ by reduce - \ by reduce intro + \<^item> by reduce + \<^item> by reduce refl done section \Dependent paths\ -Lemma (derive) apd: +Lemma (def) apd: assumes "A: U i" "\x. x: A \ P x: U i" @@ -427,7 +416,7 @@ Lemma (derive) apd: "x: A" "y: A" "p: x = y" shows "trans P p (f x) = f y" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) definition apd_i ("apd") where [implicit]: "apd f p \ Identity.apd ? ? f ? ? p" @@ -443,26 +432,25 @@ Lemma dependent_map_comp [comp]: shows "apd f (refl x) \ refl (f x)" unfolding apd_def by reduce -Lemma (derive) apd_ap: +Lemma (def) apd_ap: assumes "A: U i" "B: U i" "f: A \ B" "x: A" "y: A" "p: x = y" shows "apd f p = trans_const B p (f x) \ f[p]" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) section \Whiskering\ -Lemma (derive) right_whisker: +Lemma (def) right_whisker: assumes "A: U i" "a: A" "b: A" "c: A" and "p: a = b" "q: a = b" "r: b = c" and "\: p = q" shows "p \ r = q \ r" apply (eq r) - focus prems vars x s t - proof - + focus vars x s t proof - have "t \ refl x = t" by (rule pathcomp_refl) also have ".. = s" by fact also have ".. = s \ refl x" by (rule pathcomp_refl[symmetric]) @@ -470,14 +458,13 @@ Lemma (derive) right_whisker: qed done -Lemma (derive) left_whisker: +Lemma (def) left_whisker: assumes "A: U i" "a: A" "b: A" "c: A" and "p: b = c" "q: b = c" "r: a = b" and "\: p = q" shows "r \ p = r \ q" apply (eq r) - focus prems prms vars x s t - proof - + focus vars x s t proof - have "refl x \ t = t" by (rule refl_pathcomp) also have ".. = s" by fact also have ".. = refl x \ s" by (rule refl_pathcomp[symmetric]) @@ -485,24 +472,24 @@ Lemma (derive) left_whisker: qed done -definition right_whisker_i (infix "\\<^sub>r\<^bsub>_\<^esub>" 121) - where [implicit]: "\ \\<^sub>r\<^bsub>a\<^esub> r \ right_whisker ? a ? ? ? ? r \" +definition right_whisker_i (infix "\\<^sub>r" 121) + where [implicit]: "\ \\<^sub>r r \ right_whisker ? ? ? ? ? ? r \" -definition left_whisker_i (infix "\\<^sub>l\<^bsub>_\<^esub>" 121) - where [implicit]: "r \\<^sub>l\<^bsub>c\<^esub> \ \ left_whisker ? ? ? c ? ? r \" +definition left_whisker_i (infix "\\<^sub>l" 121) + where [implicit]: "r \\<^sub>l \ \ left_whisker ? ? ? ? ? ? r \" translations - "\ \\<^sub>r\<^bsub>a\<^esub> r" \ "CONST right_whisker A a b c p q r \" - "r \\<^sub>l\<^bsub>c\<^esub> \" \ "CONST left_whisker A a b c p q r \" + "\ \\<^sub>r r" \ "CONST right_whisker A a b c p q r \" + "r \\<^sub>l \" \ "CONST left_whisker A a b c p q r \" Lemma whisker_refl [comp]: assumes "A: U i" "a: A" "b: A" "p: a = b" "q: a = b" "\: p = q" - shows "\ \\<^sub>r\<^bsub>a\<^esub> (refl b) \ ru p \ \ \ (ru q)\" + shows "\ \\<^sub>r (refl b) \ ru p \ \ \ (ru q)\" unfolding right_whisker_def by reduce 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\<^bsub>b\<^esub> \ \ (lu p) \ \ \ (lu q)\" + shows "(refl a) \\<^sub>l \ \ (lu p) \ \ \ (lu q)\" unfolding left_whisker_def by reduce method left_whisker = (rule left_whisker) @@ -521,7 +508,7 @@ assumes assums: "r: b =\<^bsub>A\<^esub> c" "s: b =\<^bsub>A\<^esub> c" begin -Lemma (derive) horiz_pathcomp: +Lemma (def) horiz_pathcomp: notes assums assumes "\: p = q" "\: r = s" shows "p \ r = q \ s" @@ -532,7 +519,7 @@ qed typechk text \A second horizontal composition:\ -Lemma (derive) horiz_pathcomp': +Lemma (def) horiz_pathcomp': notes assums assumes "\: p = q" "\: r = s" shows "p \ r = q \ s" @@ -544,14 +531,14 @@ qed typechk notation horiz_pathcomp (infix "\" 121) notation horiz_pathcomp' (infix "\''" 121) -Lemma (derive) horiz_pathcomp_eq_horiz_pathcomp': +Lemma (def) horiz_pathcomp_eq_horiz_pathcomp': notes assums assumes "\: p = q" "\: r = s" shows "\ \ \ = \ \' \" unfolding horiz_pathcomp_def horiz_pathcomp'_def apply (eq \, eq \) focus vars p apply (eq p) - focus vars _ q by (eq q) (reduce; refl) + focus vars a q by (eq q) (reduce, refl) done done @@ -580,12 +567,20 @@ interpretation \2: notation \2.horiz_pathcomp (infix "\" 121) notation \2.horiz_pathcomp' (infix "\''" 121) -Lemma (derive) pathcomp_eq_horiz_pathcomp: +Lemma [typechk]: + assumes "\: \2 A a" and "\: \2 A a" + shows horiz_pathcomp_type: "\ \ \: \2 A a" + and horiz_pathcomp'_type: "\ \' \: \2 A a" + using assms + unfolding \2.horiz_pathcomp_def \2.horiz_pathcomp'_def \2_alt_def + by reduce+ + +Lemma (def) pathcomp_eq_horiz_pathcomp: assumes "\: \2 A a" "\: \2 A a" shows "\ \ \ = \ \ \" unfolding \2.horiz_pathcomp_def using assms[unfolded \2_alt_def] - proof (reduce, rule pathinv) + proof (reduce, rule pathinv) \ \Propositional equality rewriting needs to be improved\ have "{} = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) @@ -596,12 +591,12 @@ Lemma (derive) pathcomp_eq_horiz_pathcomp: finally have eq\: "{} = \" by this have "refl (refl a) \ \ \ refl (refl a) \ (refl (refl a) \ \ \ refl (refl a)) - = \ \ {}" by right_whisker (rule eq\) - also have ".. = \ \ \" by left_whisker (rule eq\) + = \ \ {}" by right_whisker (fact eq\) + also have ".. = \ \ \" by left_whisker (fact eq\) finally show "{} = \ \ \" by this qed -Lemma (derive) pathcomp_eq_horiz_pathcomp': +Lemma (def) pathcomp_eq_horiz_pathcomp': assumes "\: \2 A a" "\: \2 A a" shows "\ \' \ = \ \ \" unfolding \2.horiz_pathcomp'_def @@ -616,12 +611,12 @@ Lemma (derive) pathcomp_eq_horiz_pathcomp': finally have eq\: "{} = \" by this have "refl (refl a) \ \ \ refl (refl a) \ (refl (refl a) \ \ \ refl (refl a)) - = \ \ {}" by right_whisker (rule eq\) - also have ".. = \ \ \" by left_whisker (rule eq\) + = \ \ {}" by right_whisker (fact eq\) + also have ".. = \ \ \" by left_whisker (fact eq\) finally show "{} = \ \ \" by this qed -Lemma (derive) eckmann_hilton: +Lemma (def) eckmann_hilton: assumes "\: \2 A a" "\: \2 A a" shows "\ \ \ = \ \ \" using assms[unfolded \2_alt_def] @@ -629,11 +624,15 @@ Lemma (derive) eckmann_hilton: have "\ \ \ = \ \ \" by (rule pathcomp_eq_horiz_pathcomp) also have [simplified comp]: ".. = \ \' \" + \ \Danger, Will Robinson! (Inferred implicit has an equivalent form but + needs to be manually simplified.)\ by (transport eq: \2.horiz_pathcomp_eq_horiz_pathcomp') refl also have ".. = \ \ \" by (rule pathcomp_eq_horiz_pathcomp') finally show "\ \ \ = \ \ \" - by this (reduce add: \2.horiz_pathcomp_def \2.horiz_pathcomp'_def)+ + by (this; reduce add: \2_alt_def[symmetric]) + \ \TODO: The finishing call to `reduce` should be unnecessary with some + kind of definitional unfolding.\ qed end diff --git a/hott/List+.thy b/hott/List+.thy new file mode 100644 index 0000000..b73cc24 --- /dev/null +++ b/hott/List+.thy @@ -0,0 +1,18 @@ +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) + Lemma "len [0, suc 0, suc (suc 0)] \ ?n" by (subst comp) +end + + +end diff --git a/hott/More_List.thy b/hott/More_List.thy deleted file mode 100644 index 1b8034f..0000000 --- a/hott/More_List.thy +++ /dev/null @@ -1,18 +0,0 @@ -theory More_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)+ - Lemma "len [0, suc 0, suc (suc 0)] \ ?n" by (subst comp)+ -end - - -end diff --git a/hott/More_Nat.thy b/hott/More_Nat.thy deleted file mode 100644 index 59c8d54..0000000 --- a/hott/More_Nat.thy +++ /dev/null @@ -1,43 +0,0 @@ -theory More_Nat -imports Nat Spartan.More_Types - -begin - -section \Equality on Nat\ - -text \Via the encode-decode method.\ - -context begin - -Lemma (derive) eq: shows "Nat \ Nat \ U O" - apply intro focus vars m apply elim - \ \m \ 0\ - apply intro focus vars n apply elim - \ by (rule TopF) \ \n \ 0\ - \ by (rule BotF) \ \n \ suc _\ - \ by (rule Ui_in_USi) - done - \ \m \ suc k\ - apply intro focus vars k k_eq n apply (elim n) - \ by (rule BotF) \ \n \ 0\ - \ prems vars l proof - show "k_eq l: U O" by typechk qed - \ by (rule Ui_in_USi) - done - by (rule Ui_in_USi) - done - -text \ -\<^term>\eq\ is defined by - eq 0 0 \ \ - eq 0 (suc k) \ \ - eq (suc k) 0 \ \ - eq (suc k) (suc l) \ eq k l -\ - - - - -end - - -end diff --git a/hott/Nat.thy b/hott/Nat.thy index 177ec47..fd567f3 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -77,43 +77,43 @@ lemma add_suc [comp]: shows "m + suc n \ suc (m + n)" unfolding add_def by reduce -Lemma (derive) zero_add: +Lemma (def) zero_add: assumes "n: Nat" shows "0 + n = n" apply (elim n) - \ by (reduce; intro) - \ vars _ ih by reduce (eq ih; intro) + \<^item> by (reduce; intro) + \<^item> vars _ ih by reduce (eq ih; refl) done -Lemma (derive) suc_add: +Lemma (def) suc_add: assumes "m: Nat" "n: Nat" shows "suc m + n = suc (m + n)" apply (elim n) - \ by reduce refl - \ vars _ ih by reduce (eq ih; intro) + \<^item> by reduce refl + \<^item> vars _ ih by reduce (eq ih; refl) done -Lemma (derive) suc_eq: +Lemma (def) suc_eq: assumes "m: Nat" "n: Nat" shows "p: m = n \ suc m = suc n" by (eq p) intro -Lemma (derive) add_assoc: +Lemma (def) add_assoc: assumes "l: Nat" "m: Nat" "n: Nat" shows "l + (m + n) = l + m+ n" apply (elim n) - \ by reduce intro - \ vars _ ih by reduce (eq ih; intro) + \<^item> by reduce intro + \<^item> vars _ ih by reduce (eq ih; refl) done -Lemma (derive) add_comm: +Lemma (def) add_comm: assumes "m: Nat" "n: Nat" shows "m + n = n + m" apply (elim n) - \ by (reduce; rule zero_add[symmetric]) - \ prems vars n ih + \<^item> by (reduce; rule zero_add[symmetric]) + \<^item> vars n ih proof reduce - have "suc (m + n) = suc (n + m)" by (eq ih) intro + 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 qed @@ -143,12 +143,12 @@ lemma mul_suc [comp]: shows "m * suc n \ m + m * n" unfolding mul_def by reduce -Lemma (derive) zero_mul: +Lemma (def) zero_mul: assumes "n: Nat" shows "0 * n = 0" apply (elim n) - \ by reduce refl - \ prems vars n ih + \<^item> by reduce refl + \<^item> vars n ih proof reduce have "0 + 0 * n = 0 + 0 " by (eq ih) refl also have ".. = 0" by reduce refl @@ -156,12 +156,12 @@ Lemma (derive) zero_mul: qed done -Lemma (derive) suc_mul: +Lemma (def) suc_mul: assumes "m: Nat" "n: Nat" shows "suc m * n = m * n + n" apply (elim n) - \ by reduce refl - \ prems vars n ih + \<^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) also have ".. = suc (m + m * n + n)" by (transport eq: add_assoc) refl @@ -169,12 +169,12 @@ Lemma (derive) suc_mul: qed done -Lemma (derive) mul_dist_add: +Lemma (def) mul_dist_add: assumes "l: Nat" "m: Nat" "n: Nat" shows "l * (m + n) = l * m + l * n" apply (elim n) - \ by reduce refl - \ prems prms vars n ih + \<^item> by reduce refl + \<^item> vars n ih proof reduce 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) @@ -184,12 +184,12 @@ Lemma (derive) mul_dist_add: qed done -Lemma (derive) mul_assoc: +Lemma (def) mul_assoc: assumes "l: Nat" "m: Nat" "n: Nat" shows "l * (m * n) = l * m * n" apply (elim n) - \ by reduce refl - \ prems vars n ih + \<^item> by reduce refl + \<^item> vars n ih 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 @@ -197,12 +197,12 @@ Lemma (derive) mul_assoc: qed done -Lemma (derive) mul_comm: +Lemma (def) mul_comm: assumes "m: Nat" "n: Nat" shows "m * n = n * m" apply (elim n) - \ by reduce (transport eq: zero_mul, refl) - \ prems vars n ih + \<^item> by reduce (transport eq: zero_mul, refl) + \<^item> vars n ih proof (reduce, rule pathinv) have "suc n * m = n * m + m" by (rule suc_mul) also have ".. = m + m * n" diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index faa692d..27edd51 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -8,9 +8,9 @@ imports keywords "Theorem" "Lemma" "Corollary" "Proposition" "Definition" :: thy_goal_stmt and "assuming" :: prf_asm % "proof" and - "focus" "\" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and + "focus" "\<^item>" "\<^enum>" "\" "\" "~" :: prf_script_goal % "proof" and "congruence" "print_coercions" :: thy_decl and - "rhs" "derive" "prems" "vars" :: quasi_command + "rhs" "def" "vars" :: quasi_command begin @@ -198,8 +198,8 @@ lemmas [form] = PiF SigF and [intro] = PiI SigI and [intros] = PiI[rotated] SigI and - [elim "?f"] = PiE and - [elim "?p"] = SigE and + [elim ?f] = PiE and + [elim ?p] = SigE and [comp] = beta Sig_comp and [cong] = Pi_cong lam_cong Sig_cong @@ -217,7 +217,7 @@ subsection \Statement commands\ ML_file \focus.ML\ ML_file \elaboration.ML\ -ML_file \elaborated_assumption.ML\ +ML_file \elaborated_statement.ML\ ML_file \goals.ML\ subsection \Proof methods\ @@ -229,10 +229,6 @@ method_setup rule = \Attrib.thms >> (fn ths => K (CONTEXT_METHOD ( CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\ -method_setup rules = - \Attrib.thms >> (fn ths => K (CONTEXT_METHOD ( - CREPEAT o CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\ - method_setup dest = \Scan.lift (Scan.option (Args.parens Parse.int)) -- Attrib.thms >> (fn (n_opt, ths) => K (CONTEXT_METHOD ( @@ -411,10 +407,10 @@ lemma funcompI [typechk]: lemma funcomp_assoc [comp]: assumes + "A: U i" "f: A \ B" "g: B \ C" "h: \x: C. D x" - "A: U i" shows "(h \\<^bsub>B\<^esub> g) \\<^bsub>A\<^esub> f \ h \\<^bsub>A\<^esub> g \\<^bsub>A\<^esub> f" unfolding funcomp_def by reduce @@ -430,10 +426,9 @@ lemma funcomp_lambda_comp [comp]: lemma funcomp_apply_comp [comp]: assumes + "A: U i" "B: U i" "\x y. x: B \ C x: U i" "f: A \ B" "g: \x: B. C x" "x: A" - "A: U i" "B: U i" - "\x y. x: B \ C x: U i" shows "(g \\<^bsub>A\<^esub> f) x \ g (f x)" unfolding funcomp_def by reduce @@ -449,17 +444,17 @@ subsection \Identity function\ abbreviation id where "id A \ \x: A. x" lemma - id_type[typechk]: "A: U i \ id A: A \ A" and + id_type [typechk]: "A: U i \ id A: A \ A" and id_comp [comp]: "x: A \ (id A) x \ x" \ \for the occasional manual rewrite\ by reduce+ lemma id_left [comp]: - assumes "f: A \ B" "A: U i" "B: U i" + assumes "A: U i" "B: U i" "f: A \ B" shows "(id B) \\<^bsub>A\<^esub> f \ f" by (subst eta_exp[of f]) (reduce, rule eta) lemma id_right [comp]: - assumes "f: A \ B" "A: U i" "B: U i" + assumes "A: U i" "B: U i" "f: A \ B" shows "f \\<^bsub>A\<^esub> (id A) \ f" by (subst eta_exp[of f]) (reduce, rule eta) @@ -480,10 +475,7 @@ lemma fst_type [typechk]: lemma fst_comp [comp]: assumes - "a: A" - "b: B a" - "A: U i" - "\x. x: A \ B x: U i" + "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 @@ -493,7 +485,7 @@ lemma snd_type [typechk]: unfolding snd_def by typechk reduce lemma snd_comp [comp]: - assumes "a: A" "b: B a" "A: U i" "\x. x: A \ B x: U i" + 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 @@ -513,36 +505,48 @@ subsection \Projections\ Lemma fst [typechk]: assumes - "p: \x: A. B x" "A: U i" "\x. x: A \ B x: U i" + "p: \x: A. B x" shows "fst p: A" by typechk Lemma snd [typechk]: assumes - "p: \x: A. B x" "A: U i" "\x. x: A \ B x: U i" + "p: \x: A. B x" shows "snd p: B (fst p)" by typechk -method fst for p::o = rule fst[of p] -method snd for p::o = rule snd[of p] +method fst for p::o = rule fst[where ?p=p] +method snd for p::o = rule snd[where ?p=p] -subsection \Properties of \\ +text \Double projections:\ -Lemma (derive) Sig_dist_exp: +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)" + "CONST p\<^sub>1\<^sub>2 p" \ "snd (fst p)" + "CONST p\<^sub>2\<^sub>1 p" \ "fst (snd p)" + "CONST p\<^sub>2\<^sub>2 p" \ "snd (snd p)" + +Lemma (def) distribute_Sig: assumes - "p: \x: A. B x \ C x" "A: U i" "\x. x: A \ B x: U i" "\x. x: A \ C x: U i" + "p: \x: A. B x \ C x" shows "(\x: A. B x) \ (\x: A. C x)" -proof intro - have "fst p: A" and "snd p: B (fst p) \ C (fst p)" by typechk+ - thus ": \x: A. B x" - and ": \x: A. C x" - by typechk+ -qed + proof intro + have "fst p: A" and "snd p: B (fst p) \ C (fst p)" + by typechk+ + thus ": \x: A. B x" + and ": \x: A. C x" + by typechk+ + qed end diff --git a/spartan/core/context_tactical.ML b/spartan/core/context_tactical.ML index a5159f6..b5a6c00 100644 --- a/spartan/core/context_tactical.ML +++ b/spartan/core/context_tactical.ML @@ -2,6 +2,10 @@ Author: Joshua Chen More context tactics, and context tactic combinators. + +Contains code modified from + ~~/Pure/search.ML + ~~/Pure/tactical.ML *) infix 1 CTHEN CTHEN' CTHEN_ALL_NEW CTHEN_ALL_NEW_FWD @@ -23,6 +27,7 @@ val CORELSE': context_tactic' * context_tactic' -> context_tactic' val CAPPEND': context_tactic' * context_tactic' -> context_tactic' val CTRY: context_tactic -> context_tactic val CREPEAT: context_tactic -> context_tactic +val CREPEAT1: context_tactic -> context_tactic val CFILTER: (context_state -> bool) -> context_tactic -> context_tactic val CCHANGED: context_tactic -> context_tactic val CTHEN_ALL_NEW: context_tactic' * context_tactic' -> context_tactic' @@ -34,6 +39,16 @@ val CHEADGOAL: context_tactic' -> context_tactic val CALLGOALS: context_tactic' -> context_tactic val CSOMEGOAL: context_tactic' -> context_tactic val CRANGE: context_tactic' list -> context_tactic' +val CFIRST: context_tactic list -> context_tactic +val CFIRST': context_tactic' list -> context_tactic' +val CTHEN_BEST_FIRST: context_tactic -> (context_state -> bool) -> + (context_state -> int) -> context_tactic -> context_tactic +val CBEST_FIRST: (context_state -> bool) -> (context_state -> int) -> + context_tactic -> context_tactic +val CTHEN_ASTAR: context_tactic -> (context_state -> bool) -> + (int -> context_state -> int) -> context_tactic -> context_tactic +val CASTAR: (context_state -> bool) -> (int -> context_state -> int) -> + context_tactic -> context_tactic end = struct @@ -74,6 +89,8 @@ fun CREPEAT ctac = | SOME (cst, q) => rep (q :: qs) cst); in fn cst => Seq.make_results (Seq.make (fn () => rep [] cst)) end +fun CREPEAT1 ctac = ctac CTHEN CREPEAT ctac + fun CFILTER pred ctac cst = ctac cst |> Seq.filter_results @@ -147,6 +164,89 @@ fun CSOMEGOAL ctac (cst as (_, st)) = fun CRANGE [] _ = all_ctac | CRANGE (ctac :: ctacs) i = CRANGE ctacs (i + 1) CTHEN ctac i +fun CFIRST ctacs = fold_rev (curry op CORELSE) ctacs no_ctac + +(*FIRST' [tac1,...,tacn] i equals tac1 i ORELSE ... ORELSE tacn i*) +fun CFIRST' ctacs = fold_rev (curry op CORELSE') ctacs (K no_ctac) + + +(** Search tacticals **) + +(* Best-first search *) + +structure Thm_Heap = Heap ( + type elem = int * thm; + val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 Thm.prop_of) +) + +structure Context_State_Heap = Heap ( + type elem = int * context_state; + val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 (Thm.prop_of o #2)) +) + +fun some_of_list [] = NONE + | some_of_list (x :: l) = SOME (x, Seq.make (fn () => some_of_list l)) + +(*Check for and delete duplicate proof states*) +fun delete_all_min (cst as (_, st)) heap = + if Context_State_Heap.is_empty heap then heap + else if Thm.eq_thm (st, #2 (#2 (Context_State_Heap.min heap))) + then delete_all_min cst (Context_State_Heap.delete_min heap) + else heap + +(*Best-first search for a state that satisfies satp (incl initial state) + Function sizef estimates size of problem remaining (smaller means better). + tactic tac0 sets up the initial priority queue, while tac1 searches it. *) +fun CTHEN_BEST_FIRST ctac0 satp sizef ctac = + let + fun pairsize cst = (sizef cst, cst); + fun bfs (news, nst_heap) = + (case List.partition satp news of + ([], nonsats) => next (fold_rev Context_State_Heap.insert (map pairsize nonsats) nst_heap) + | (sats, _) => some_of_list sats) + and next nst_heap = + if Context_State_Heap.is_empty nst_heap then NONE + else + let + val (n, cst) = Context_State_Heap.min nst_heap; + in + bfs (Seq.list_of (Seq.filter_results (ctac cst)), delete_all_min cst (Context_State_Heap.delete_min nst_heap)) + end; + fun btac cst = bfs (Seq.list_of (Seq.filter_results (ctac0 cst)), Context_State_Heap.empty) + in fn cst => Seq.make_results (Seq.make (fn () => btac cst)) end + +(*Ordinary best-first search, with no initial tactic*) +val CBEST_FIRST = CTHEN_BEST_FIRST all_ctac + + +(* A*-like search *) + +(*Insertion into priority queue of states, marked with level*) +fun insert_with_level (lnth: int * int * context_state) [] = [lnth] + | insert_with_level (l, m, cst) ((l', n, cst') :: csts) = + if n < m then (l', n, cst') :: insert_with_level (l, m, cst) csts + else if n = m andalso Thm.eq_thm (#2 cst, #2 cst') then (l', n, cst') :: csts + else (l, m, cst) :: (l', n, cst') :: csts; + +fun CTHEN_ASTAR ctac0 satp costf ctac = + let + fun bfs (news, nst, level) = + let fun cost cst = (level, costf level cst, cst) in + (case List.partition satp news of + ([], nonsats) => next (fold_rev (insert_with_level o cost) nonsats nst) + | (sats, _) => some_of_list sats) + end + and next [] = NONE + | next ((level, n, cst) :: nst) = + bfs (Seq.list_of (Seq.filter_results (ctac cst)), nst, level + 1) + in fn cst => Seq.make_results + (Seq.make (fn () => bfs (Seq.list_of (Seq.filter_results (ctac0 cst)), [], 0))) + end + +(*Ordinary ASTAR, with no initial tactic*) +val CASTAR = CTHEN_ASTAR all_ctac; + + end open Context_Tactical diff --git a/spartan/core/elaborated_assumption.ML b/spartan/core/elaborated_assumption.ML deleted file mode 100644 index af3a384..0000000 --- a/spartan/core/elaborated_assumption.ML +++ /dev/null @@ -1,446 +0,0 @@ -(* Title: elaborated_assumption.ML - Author: Joshua Chen - -Term elaboration for goal and proof assumptions. - -Contains code from parts of - ~~/Pure/Isar/element.ML and - ~~/Pure/Isar/expression.ML -in both verbatim and modified forms. -*) - -structure Elaborated_Assumption: sig - -val read_goal_statement: - (string, string, Facts.ref) Element.ctxt list -> - (string, string) Element.stmt -> - Proof.context -> - (Attrib.binding * (term * term list) list) list * Proof.context - -end = struct - - -(*Apply elaboration to the list format assumptions are given in*) -fun elaborate ctxt assms = - let - fun subst_term env = Envir.subst_term (Envir.type_env env, Envir.term_env env) - fun elab_fact (fact, xs) assums = - let val (subst, fact') = Elab.elab_stmt ctxt assums fact in - ((fact', map (subst_term subst) xs), Thm.cterm_of ctxt fact' :: assums) - end - fun elab (b, facts) assums = - let val (facts', assums') = fold_map elab_fact facts assums - in ((b, facts'), assums') end - in #1 (fold_map elab assms []) end - - -(* Goal assumptions *) - -(*Most of the code in this section is copied verbatim from the originals; the - only change is a modification to`activate_i` incorporating elaboration.*) - -local - -fun mk_type T = (Logic.mk_type T, []) -fun mk_term t = (t, []) -fun mk_propp (p, pats) = (Type.constraint propT p, pats) - -fun dest_type (T, []) = Logic.dest_type T -fun dest_term (t, []) = t -fun dest_propp (p, pats) = (p, pats) - -fun extract_inst (_, (_, ts)) = map mk_term ts -fun restore_inst ((l, (p, _)), cs) = (l, (p, map dest_term cs)) - -fun extract_eqns es = map (mk_term o snd) es -fun restore_eqns (es, cs) = map2 (fn (b, _) => fn c => (b, dest_term c)) es cs - -fun extract_elem (Element.Fixes fixes) = map (#2 #> the_list #> map mk_type) fixes - | extract_elem (Element.Constrains csts) = map (#2 #> single #> map mk_type) csts - | extract_elem (Element.Assumes asms) = map (#2 #> map mk_propp) asms - | extract_elem (Element.Defines defs) = map (fn (_, (t, ps)) => [mk_propp (t, ps)]) defs - | extract_elem (Element.Notes _) = [] - | extract_elem (Element.Lazy_Notes _) = [] - -fun restore_elem (Element.Fixes fixes, css) = - (fixes ~~ css) |> map (fn ((x, _, mx), cs) => - (x, cs |> map dest_type |> try hd, mx)) |> Element.Fixes - | restore_elem (Element.Constrains csts, css) = - (csts ~~ css) |> map (fn ((x, _), cs) => - (x, cs |> map dest_type |> hd)) |> Element.Constrains - | restore_elem (Element.Assumes asms, css) = - (asms ~~ css) |> map (fn ((b, _), cs) => (b, map dest_propp cs)) |> Element.Assumes - | restore_elem (Element.Defines defs, css) = - (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Element.Defines - | restore_elem (elem as Element.Notes _, _) = elem - | restore_elem (elem as Element.Lazy_Notes _, _) = elem - -fun prep (_, pats) (ctxt, t :: ts) = - let val ctxt' = Proof_Context.augment t ctxt - in - ((t, Syntax.check_props - (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats), - (ctxt', ts)) - end - -fun check cs ctxt = - let - val (cs', (ctxt', _)) = fold_map prep cs - (ctxt, Syntax.check_terms - (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) (map fst cs)) - in (cs', ctxt') end - -fun inst_morphism params ((prfx, mandatory), insts') ctxt = - let - (*parameters*) - val parm_types = map #2 params; - val type_parms = fold Term.add_tfreesT parm_types []; - - (*type inference*) - val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types; - val type_parms' = fold Term.add_tvarsT parm_types' []; - val checked = - (map (Logic.mk_type o TVar) type_parms' @ map2 Type.constraint parm_types' insts') - |> Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt) - val (type_parms'', insts'') = chop (length type_parms') checked; - - (*context*) - val ctxt' = fold Proof_Context.augment checked ctxt; - val certT = Thm.trim_context_ctyp o Thm.ctyp_of ctxt'; - val cert = Thm.trim_context_cterm o Thm.cterm_of ctxt'; - - (*instantiation*) - val instT = - (type_parms ~~ map Logic.dest_type type_parms'') - |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T)); - val cert_inst = - ((map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'') - |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t)); - in - (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $> - Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt') - end; - -fun abs_def ctxt = - Thm.cterm_of ctxt #> Assumption.assume ctxt #> Local_Defs.abs_def_rule ctxt #> Thm.prop_of; - -fun declare_elem prep_var (Element.Fixes fixes) ctxt = - let val (vars, _) = fold_map prep_var fixes ctxt - in ctxt |> Proof_Context.add_fixes vars |> snd end - | declare_elem prep_var (Element.Constrains csts) ctxt = - ctxt |> fold_map (fn (x, T) => prep_var (Binding.name x, SOME T, NoSyn)) csts |> snd - | declare_elem _ (Element.Assumes _) ctxt = ctxt - | declare_elem _ (Element.Defines _) ctxt = ctxt - | declare_elem _ (Element.Notes _) ctxt = ctxt - | declare_elem _ (Element.Lazy_Notes _) ctxt = ctxt; - -fun parameters_of thy strict (expr, fixed) = - let - val ctxt = Proof_Context.init_global thy; - - fun reject_dups message xs = - (case duplicates (op =) xs of - [] => () - | dups => error (message ^ commas dups)); - - fun parm_eq ((p1, mx1), (p2, mx2)) = - p1 = p2 andalso - (Mixfix.equal (mx1, mx2) orelse - error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression" ^ - Position.here_list [Mixfix.pos_of mx1, Mixfix.pos_of mx2])); - - fun params_loc loc = Locale.params_of thy loc |> map (apfst #1); - fun params_inst (loc, (prfx, (Expression.Positional insts, eqns))) = - let - val ps = params_loc loc; - val d = length ps - length insts; - val insts' = - if d < 0 then - error ("More arguments than parameters in instantiation of locale " ^ - quote (Locale.markup_name ctxt loc)) - else insts @ replicate d NONE; - val ps' = (ps ~~ insts') |> - map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE); - in (ps', (loc, (prfx, (Expression.Positional insts', eqns)))) end - | params_inst (loc, (prfx, (Expression.Named insts, eqns))) = - let - val _ = - reject_dups "Duplicate instantiation of the following parameter(s): " - (map fst insts); - val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps => - if AList.defined (op =) ps p then AList.delete (op =) p ps - else error (quote p ^ " not a parameter of instantiated expression")); - in (ps', (loc, (prfx, (Expression.Named insts, eqns)))) end; - fun params_expr is = - let - val (is', ps') = fold_map (fn i => fn ps => - let - val (ps', i') = params_inst i; - val ps'' = distinct parm_eq (ps @ ps'); - in (i', ps'') end) is [] - in (ps', is') end; - - val (implicit, expr') = params_expr expr; - - val implicit' = map #1 implicit; - val fixed' = map (Variable.check_name o #1) fixed; - val _ = reject_dups "Duplicate fixed parameter(s): " fixed'; - val implicit'' = - if strict then [] - else - let - val _ = - reject_dups - "Parameter(s) declared simultaneously in expression and for clause: " - (implicit' @ fixed'); - in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end; - in (expr', implicit'' @ fixed) end; - -fun parse_elem prep_typ prep_term ctxt = - Element.map_ctxt - {binding = I, - typ = prep_typ ctxt, - term = prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt), - pattern = prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt), - fact = I, - attrib = I}; - -fun prepare_stmt prep_prop prep_obtains ctxt stmt = - (case stmt of - Element.Shows raw_shows => - raw_shows |> (map o apsnd o map) (fn (t, ps) => - (prep_prop (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t, - map (prep_prop (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps)) - | Element.Obtains raw_obtains => - let - val ((_, thesis), thesis_ctxt) = Obtain.obtain_thesis ctxt; - val obtains = prep_obtains thesis_ctxt thesis raw_obtains; - in map (fn (b, t) => ((b, []), [(t, [])])) obtains end); - -fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) => - let val x = Binding.name_of binding - in (binding, AList.lookup (op =) parms x, mx) end) - -fun finish_inst ctxt (loc, (prfx, inst)) = - let - val thy = Proof_Context.theory_of ctxt; - val (morph, _) = inst_morphism (map #1 (Locale.params_of thy loc)) (prfx, inst) ctxt; - in (loc, morph) end - -fun closeup _ _ false elem = elem - | closeup (outer_ctxt, ctxt) parms true elem = - let - (*FIXME consider closing in syntactic phase -- before type checking*) - fun close_frees t = - let - val rev_frees = - Term.fold_aterms (fn Free (x, T) => - if Variable.is_fixed outer_ctxt x orelse AList.defined (op =) parms x then I - else insert (op =) (x, T) | _ => I) t []; - in fold (Logic.all o Free) rev_frees t end; - - fun no_binds [] = [] - | no_binds _ = error "Illegal term bindings in context element"; - in - (case elem of - Element.Assumes asms => Element.Assumes (asms |> map (fn (a, propps) => - (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) - | Element.Defines defs => Element.Defines (defs |> map (fn ((name, atts), (t, ps)) => - let val ((c, _), t') = Local_Defs.cert_def ctxt (K []) (close_frees t) - in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end)) - | e => e) - end - -fun finish_elem _ parms _ (Element.Fixes fixes) = Element.Fixes (finish_fixes parms fixes) - | finish_elem _ _ _ (Element.Constrains _) = Element.Constrains [] - | finish_elem ctxts parms do_close (Element.Assumes asms) = closeup ctxts parms do_close (Element.Assumes asms) - | finish_elem ctxts parms do_close (Element.Defines defs) = closeup ctxts parms do_close (Element.Defines defs) - | finish_elem _ _ _ (elem as Element.Notes _) = elem - | finish_elem _ _ _ (elem as Element.Lazy_Notes _) = elem - -fun check_autofix insts eqnss elems concl ctxt = - let - val inst_cs = map extract_inst insts; - val eqns_cs = map extract_eqns eqnss; - val elem_css = map extract_elem elems; - val concl_cs = (map o map) mk_propp (map snd concl); - (*Type inference*) - val (inst_cs' :: eqns_cs' :: css', ctxt') = - (fold_burrow o fold_burrow) check (inst_cs :: eqns_cs :: elem_css @ [concl_cs]) ctxt; - val (elem_css', [concl_cs']) = chop (length elem_css) css'; - in - ((map restore_inst (insts ~~ inst_cs'), - map restore_eqns (eqnss ~~ eqns_cs'), - map restore_elem (elems ~~ elem_css'), - map fst concl ~~ concl_cs'), ctxt') - end - -fun prep_full_context_statement - parse_typ parse_prop - prep_obtains prep_var_elem prep_inst prep_eqns prep_attr prep_var_inst prep_expr - {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt - ctxt1 - = - let - val thy = Proof_Context.theory_of ctxt1 - val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import) - fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) = - let - val params = map #1 (Locale.params_of thy loc) - val inst' = prep_inst ctxt (map #1 params) inst - val parm_types' = - params |> map (#2 #> Logic.varifyT_global #> - Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #> - Type_Infer.paramify_vars) - val inst'' = map2 Type.constraint parm_types' inst' - val insts' = insts @ [(loc, (prfx, inst''))] - val ((insts'', _, _, _), ctxt2) = check_autofix insts' [] [] [] ctxt - val inst''' = insts'' |> List.last |> snd |> snd - val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt - val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2 - handle ERROR msg => if null eqns then error msg else - (Locale.tracing ctxt1 - (msg ^ "\nFalling back to reading rewrites clause before activation."); - ctxt2) - val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns - val eqns' = (prep_eqns ctxt' o map snd) eqns - val eqnss' = [attrss ~~ eqns'] - val ((_, [eqns''], _, _), _) = check_autofix insts'' eqnss' [] [] ctxt' - val rewrite_morph = eqns' - |> map (abs_def ctxt') - |> Variable.export_terms ctxt' ctxt - |> Element.eq_term_morphism (Proof_Context.theory_of ctxt) - |> the_default Morphism.identity - val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt - val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns'] - in (i + 1, insts', eqnss', ctxt'') end - - fun prep_elem raw_elem ctxt = - let - val ctxt' = ctxt - |> Context_Position.set_visible false - |> declare_elem prep_var_elem raw_elem - |> Context_Position.restore_visible ctxt - val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem - in (elems', ctxt') end - - val fors = fold_map prep_var_inst fixed ctxt1 |> fst - val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd - val (_, insts', eqnss', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], [], ctxt2) - - fun prep_stmt elems ctxt = - check_autofix insts' [] elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt - - val _ = - if fixed_frees then () - else - (case fold (fold (Variable.add_frees ctxt3) o snd o snd) insts' [] of - [] => () - | frees => error ("Illegal free variables in expression: " ^ - commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees)))) - - val ((insts, _, elems', concl), ctxt4) = ctxt3 - |> init_body - |> fold_map prep_elem raw_elems - |-> prep_stmt - - (*parameters from expression and elements*) - val xs = maps (fn Element.Fixes fixes => map (Variable.check_name o #1) fixes | _ => []) - (Element.Fixes fors :: elems') - val (parms, ctxt5) = fold_map Proof_Context.inferred_param xs ctxt4 - val fors' = finish_fixes parms fors - val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors' - val deps = map (finish_inst ctxt5) insts - val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems' - in ((fixed, deps, eqnss', elems'', concl), (parms, ctxt5)) end - -fun prep_inst prep_term ctxt parms (Expression.Positional insts) = - (insts ~~ parms) |> map - (fn (NONE, p) => Free (p, dummyT) - | (SOME t, _) => prep_term ctxt t) - | prep_inst prep_term ctxt parms (Expression.Named insts) = - parms |> map (fn p => - (case AList.lookup (op =) insts p of - SOME t => prep_term ctxt t | - NONE => Free (p, dummyT))) -fun parse_inst x = prep_inst Syntax.parse_term x -fun check_expr thy instances = map (apfst (Locale.check thy)) instances - -val read_full_context_statement = prep_full_context_statement - Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains - Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src - Proof_Context.read_var check_expr - -fun prep_statement prep activate raw_elems raw_stmt ctxt = - let - val ((_, _, _, elems, concl), _) = - prep {strict = true, do_close = false, fixed_frees = true} - ([], []) I raw_elems raw_stmt ctxt; - val ctxt' = ctxt - |> Proof_Context.set_stmt true - |> fold_map activate elems |> #2 - |> Proof_Context.restore_stmt ctxt; - in (concl, ctxt') end - -fun activate_i elem ctxt = - let - val elem' = - (case (Element.map_ctxt_attrib o map) Token.init_assignable elem of - Element.Defines defs => - Element.Defines (defs |> map (fn ((a, atts), (t, ps)) => - ((Thm.def_binding_optional - (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt (K []) t)))) a, atts), - (t, ps)))) - | Element.Assumes assms => Element.Assumes (elaborate ctxt assms) - | e => e); - val ctxt' = Context.proof_map (Element.init elem') ctxt; - in ((Element.map_ctxt_attrib o map) Token.closure elem', ctxt') end - -fun activate raw_elem ctxt = - let val elem = raw_elem |> Element.map_ctxt - {binding = I, - typ = I, - term = I, - pattern = I, - fact = Proof_Context.get_fact ctxt, - attrib = Attrib.check_src ctxt} - in activate_i elem ctxt end - -in - -val read_goal_statement = prep_statement read_full_context_statement activate - -end - - -(* Proof assumption command *) - -local - -val structured_statement = - Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes - >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows)) - -in - -val _ = Outer_Syntax.command \<^command_keyword>\assuming\ "elaborated assumption" - (structured_statement >> (fn (a, b, c) => Toplevel.proof (fn state => - let - val ctxt = Proof.context_of state - - fun read_option_typ NONE = NONE - | read_option_typ (SOME s) = SOME (Syntax.read_typ ctxt s) - fun read_terms (s, ss) = - let val f = Syntax.read_term ctxt in (f s, map f ss) end - - val a' = map (fn (b, s, m) => (b, read_option_typ s, m)) a - val b' = map (map read_terms) b - val c' = c |> map (fn ((b, atts), ss) => - ((b, map (Attrib.attribute_cmd ctxt) atts), map read_terms ss)) - val c'' = elaborate ctxt c' - in Proof.assume a' b' c'' state end))) - -end - - -end \ No newline at end of file diff --git a/spartan/core/elaborated_statement.ML b/spartan/core/elaborated_statement.ML new file mode 100644 index 0000000..81f4a7d --- /dev/null +++ b/spartan/core/elaborated_statement.ML @@ -0,0 +1,441 @@ +(* Title: elaborated_statement.ML + Author: Joshua Chen + +Term elaboration for goal statements and proof commands. + +Contains code from parts of + ~~/Pure/Isar/element.ML and + ~~/Pure/Isar/expression.ML +in both verbatim and modified forms. +*) + +structure Elaborated_Statement: sig + +val read_goal_statement: + (string, string, Facts.ref) Element.ctxt list -> + (string, string) Element.stmt -> + Proof.context -> + (Attrib.binding * (term * term list) list) list * Proof.context + +end = struct + + +(* Elaborated goal statements *) + +local + +fun mk_type T = (Logic.mk_type T, []) +fun mk_term t = (t, []) +fun mk_propp (p, pats) = (Type.constraint propT p, pats) + +fun dest_type (T, []) = Logic.dest_type T +fun dest_term (t, []) = t +fun dest_propp (p, pats) = (p, pats) + +fun extract_inst (_, (_, ts)) = map mk_term ts +fun restore_inst ((l, (p, _)), cs) = (l, (p, map dest_term cs)) + +fun extract_eqns es = map (mk_term o snd) es +fun restore_eqns (es, cs) = map2 (fn (b, _) => fn c => (b, dest_term c)) es cs + +fun extract_elem (Element.Fixes fixes) = map (#2 #> the_list #> map mk_type) fixes + | extract_elem (Element.Constrains csts) = map (#2 #> single #> map mk_type) csts + | extract_elem (Element.Assumes asms) = map (#2 #> map mk_propp) asms + | extract_elem (Element.Defines defs) = map (fn (_, (t, ps)) => [mk_propp (t, ps)]) defs + | extract_elem (Element.Notes _) = [] + | extract_elem (Element.Lazy_Notes _) = [] + +fun restore_elem (Element.Fixes fixes, css) = + (fixes ~~ css) |> map (fn ((x, _, mx), cs) => + (x, cs |> map dest_type |> try hd, mx)) |> Element.Fixes + | restore_elem (Element.Constrains csts, css) = + (csts ~~ css) |> map (fn ((x, _), cs) => + (x, cs |> map dest_type |> hd)) |> Element.Constrains + | restore_elem (Element.Assumes asms, css) = + (asms ~~ css) |> map (fn ((b, _), cs) => (b, map dest_propp cs)) |> Element.Assumes + | restore_elem (Element.Defines defs, css) = + (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Element.Defines + | restore_elem (elem as Element.Notes _, _) = elem + | restore_elem (elem as Element.Lazy_Notes _, _) = elem + +fun prep (_, pats) (ctxt, t :: ts) = + let val ctxt' = Proof_Context.augment t ctxt + in + ((t, Syntax.check_props + (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats), + (ctxt', ts)) + end + +fun check cs ctxt = + let + val (cs', (ctxt', _)) = fold_map prep cs + (ctxt, Syntax.check_terms + (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) (map fst cs)) + in (cs', ctxt') end + +fun inst_morphism params ((prfx, mandatory), insts') ctxt = + let + (*parameters*) + val parm_types = map #2 params; + val type_parms = fold Term.add_tfreesT parm_types []; + + (*type inference*) + val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types; + val type_parms' = fold Term.add_tvarsT parm_types' []; + val checked = + (map (Logic.mk_type o TVar) type_parms' @ map2 Type.constraint parm_types' insts') + |> Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt) + val (type_parms'', insts'') = chop (length type_parms') checked; + + (*context*) + val ctxt' = fold Proof_Context.augment checked ctxt; + val certT = Thm.trim_context_ctyp o Thm.ctyp_of ctxt'; + val cert = Thm.trim_context_cterm o Thm.cterm_of ctxt'; + + (*instantiation*) + val instT = + (type_parms ~~ map Logic.dest_type type_parms'') + |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T)); + val cert_inst = + ((map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'') + |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t)); + in + (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $> + Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt') + end; + +fun abs_def ctxt = + Thm.cterm_of ctxt #> Assumption.assume ctxt #> Local_Defs.abs_def_rule ctxt #> Thm.prop_of; + +fun declare_elem prep_var (Element.Fixes fixes) ctxt = + let val (vars, _) = fold_map prep_var fixes ctxt + in ctxt |> Proof_Context.add_fixes vars |> snd end + | declare_elem prep_var (Element.Constrains csts) ctxt = + ctxt |> fold_map (fn (x, T) => prep_var (Binding.name x, SOME T, NoSyn)) csts |> snd + | declare_elem _ (Element.Assumes _) ctxt = ctxt + | declare_elem _ (Element.Defines _) ctxt = ctxt + | declare_elem _ (Element.Notes _) ctxt = ctxt + | declare_elem _ (Element.Lazy_Notes _) ctxt = ctxt; + +fun parameters_of thy strict (expr, fixed) = + let + val ctxt = Proof_Context.init_global thy; + + fun reject_dups message xs = + (case duplicates (op =) xs of + [] => () + | dups => error (message ^ commas dups)); + + fun parm_eq ((p1, mx1), (p2, mx2)) = + p1 = p2 andalso + (Mixfix.equal (mx1, mx2) orelse + error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression" ^ + Position.here_list [Mixfix.pos_of mx1, Mixfix.pos_of mx2])); + + fun params_loc loc = Locale.params_of thy loc |> map (apfst #1); + fun params_inst (loc, (prfx, (Expression.Positional insts, eqns))) = + let + val ps = params_loc loc; + val d = length ps - length insts; + val insts' = + if d < 0 then + error ("More arguments than parameters in instantiation of locale " ^ + quote (Locale.markup_name ctxt loc)) + else insts @ replicate d NONE; + val ps' = (ps ~~ insts') |> + map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE); + in (ps', (loc, (prfx, (Expression.Positional insts', eqns)))) end + | params_inst (loc, (prfx, (Expression.Named insts, eqns))) = + let + val _ = + reject_dups "Duplicate instantiation of the following parameter(s): " + (map fst insts); + val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps => + if AList.defined (op =) ps p then AList.delete (op =) p ps + else error (quote p ^ " not a parameter of instantiated expression")); + in (ps', (loc, (prfx, (Expression.Named insts, eqns)))) end; + fun params_expr is = + let + val (is', ps') = fold_map (fn i => fn ps => + let + val (ps', i') = params_inst i; + val ps'' = distinct parm_eq (ps @ ps'); + in (i', ps'') end) is [] + in (ps', is') end; + + val (implicit, expr') = params_expr expr; + + val implicit' = map #1 implicit; + val fixed' = map (Variable.check_name o #1) fixed; + val _ = reject_dups "Duplicate fixed parameter(s): " fixed'; + val implicit'' = + if strict then [] + else + let + val _ = + reject_dups + "Parameter(s) declared simultaneously in expression and for clause: " + (implicit' @ fixed'); + in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end; + in (expr', implicit'' @ fixed) end; + +fun parse_elem prep_typ prep_term ctxt = + Element.map_ctxt + {binding = I, + typ = prep_typ ctxt, + term = prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt), + pattern = prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt), + fact = I, + attrib = I}; + +fun prepare_stmt prep_prop prep_obtains ctxt stmt = + (case stmt of + Element.Shows raw_shows => + raw_shows |> (map o apsnd o map) (fn (t, ps) => + (prep_prop (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t, + map (prep_prop (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps)) + | Element.Obtains raw_obtains => + let + val ((_, thesis), thesis_ctxt) = Obtain.obtain_thesis ctxt; + val obtains = prep_obtains thesis_ctxt thesis raw_obtains; + in map (fn (b, t) => ((b, []), [(t, [])])) obtains end); + +fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) => + let val x = Binding.name_of binding + in (binding, AList.lookup (op =) parms x, mx) end) + +fun finish_inst ctxt (loc, (prfx, inst)) = + let + val thy = Proof_Context.theory_of ctxt; + val (morph, _) = inst_morphism (map #1 (Locale.params_of thy loc)) (prfx, inst) ctxt; + in (loc, morph) end + +fun closeup _ _ false elem = elem + | closeup (outer_ctxt, ctxt) parms true elem = + let + (*FIXME consider closing in syntactic phase -- before type checking*) + fun close_frees t = + let + val rev_frees = + Term.fold_aterms (fn Free (x, T) => + if Variable.is_fixed outer_ctxt x orelse AList.defined (op =) parms x then I + else insert (op =) (x, T) | _ => I) t []; + in fold (Logic.all o Free) rev_frees t end; + + fun no_binds [] = [] + | no_binds _ = error "Illegal term bindings in context element"; + in + (case elem of + Element.Assumes asms => Element.Assumes (asms |> map (fn (a, propps) => + (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) + | Element.Defines defs => Element.Defines (defs |> map (fn ((name, atts), (t, ps)) => + let val ((c, _), t') = Local_Defs.cert_def ctxt (K []) (close_frees t) + in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end)) + | e => e) + end + +fun finish_elem _ parms _ (Element.Fixes fixes) = Element.Fixes (finish_fixes parms fixes) + | finish_elem _ _ _ (Element.Constrains _) = Element.Constrains [] + | finish_elem ctxts parms do_close (Element.Assumes asms) = closeup ctxts parms do_close (Element.Assumes asms) + | finish_elem ctxts parms do_close (Element.Defines defs) = closeup ctxts parms do_close (Element.Defines defs) + | finish_elem _ _ _ (elem as Element.Notes _) = elem + | finish_elem _ _ _ (elem as Element.Lazy_Notes _) = elem + +fun check_autofix insts eqnss elems concl ctxt = + let + val inst_cs = map extract_inst insts; + val eqns_cs = map extract_eqns eqnss; + val elem_css = map extract_elem elems; + val concl_cs = (map o map) mk_propp (map snd concl); + (*Type inference*) + val (inst_cs' :: eqns_cs' :: css', ctxt') = + (fold_burrow o fold_burrow) check (inst_cs :: eqns_cs :: elem_css @ [concl_cs]) ctxt; + val (elem_css', [concl_cs']) = chop (length elem_css) css'; + in + ((map restore_inst (insts ~~ inst_cs'), + map restore_eqns (eqnss ~~ eqns_cs'), + map restore_elem (elems ~~ elem_css'), + map fst concl ~~ concl_cs'), ctxt') + end + +fun prep_full_context_statement + parse_typ parse_prop + prep_obtains prep_var_elem prep_inst prep_eqns prep_attr prep_var_inst prep_expr + {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt + ctxt1 + = + let + val thy = Proof_Context.theory_of ctxt1 + val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import) + fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) = + let + val params = map #1 (Locale.params_of thy loc) + val inst' = prep_inst ctxt (map #1 params) inst + val parm_types' = + params |> map (#2 #> Logic.varifyT_global #> + Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #> + Type_Infer.paramify_vars) + val inst'' = map2 Type.constraint parm_types' inst' + val insts' = insts @ [(loc, (prfx, inst''))] + val ((insts'', _, _, _), ctxt2) = check_autofix insts' [] [] [] ctxt + val inst''' = insts'' |> List.last |> snd |> snd + val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt + val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2 + handle ERROR msg => if null eqns then error msg else + (Locale.tracing ctxt1 + (msg ^ "\nFalling back to reading rewrites clause before activation."); + ctxt2) + val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns + val eqns' = (prep_eqns ctxt' o map snd) eqns + val eqnss' = [attrss ~~ eqns'] + val ((_, [eqns''], _, _), _) = check_autofix insts'' eqnss' [] [] ctxt' + val rewrite_morph = eqns' + |> map (abs_def ctxt') + |> Variable.export_terms ctxt' ctxt + |> Element.eq_term_morphism (Proof_Context.theory_of ctxt) + |> the_default Morphism.identity + val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt + val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns'] + in (i + 1, insts', eqnss', ctxt'') end + + fun prep_elem raw_elem ctxt = + let + val ctxt' = ctxt + |> Context_Position.set_visible false + |> declare_elem prep_var_elem raw_elem + |> Context_Position.restore_visible ctxt + val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem + in (elems', ctxt') end + + val fors = fold_map prep_var_inst fixed ctxt1 |> fst + val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd + val (_, insts', eqnss', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], [], ctxt2) + + fun prep_stmt elems ctxt = + check_autofix insts' [] elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt + + val _ = + if fixed_frees then () + else + (case fold (fold (Variable.add_frees ctxt3) o snd o snd) insts' [] of + [] => () + | frees => error ("Illegal free variables in expression: " ^ + commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees)))) + + val ((insts, _, elems', concl), ctxt4) = ctxt3 + |> init_body + |> fold_map prep_elem raw_elems + |-> prep_stmt + + (*parameters from expression and elements*) + val xs = maps (fn Element.Fixes fixes => map (Variable.check_name o #1) fixes | _ => []) + (Element.Fixes fors :: elems') + val (parms, ctxt5) = fold_map Proof_Context.inferred_param xs ctxt4 + val fors' = finish_fixes parms fors + val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors' + val deps = map (finish_inst ctxt5) insts + val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems' + in ((fixed, deps, eqnss', elems'', concl), (parms, ctxt5)) end + +fun prep_inst prep_term ctxt parms (Expression.Positional insts) = + (insts ~~ parms) |> map + (fn (NONE, p) => Free (p, dummyT) + | (SOME t, _) => prep_term ctxt t) + | prep_inst prep_term ctxt parms (Expression.Named insts) = + parms |> map (fn p => + (case AList.lookup (op =) insts p of + SOME t => prep_term ctxt t | + NONE => Free (p, dummyT))) +fun parse_inst x = prep_inst Syntax.parse_term x +fun check_expr thy instances = map (apfst (Locale.check thy)) instances + +val read_full_context_statement = prep_full_context_statement + Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains + Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src + Proof_Context.read_var check_expr + +fun filter_assumes ((x as Element.Assumes _) :: xs) = x :: filter_assumes xs + | filter_assumes (_ :: xs) = filter_assumes xs + | filter_assumes [] = [] + +fun prep_statement prep activate raw_elems raw_stmt ctxt = + let + val ((_, _, _, elems, concl), _) = + prep {strict = true, do_close = false, fixed_frees = true} + ([], []) I raw_elems raw_stmt ctxt + + val (elems', ctxt') = ctxt + |> Proof_Context.set_stmt true + |> fold_map activate elems + |> apsnd (Proof_Context.restore_stmt ctxt) + + val assumes = filter_assumes elems' + val assms = flat (flat (map + (fn (Element.Assumes asms) => + map (fn (_, facts) => map (Thm.cterm_of ctxt' o #1) facts) asms) + assumes)) + val concl' = Elab.elaborate ctxt' assms concl handle error => concl + in (concl', ctxt') end + +fun activate_i elem ctxt = + let + val elem' = + (case (Element.map_ctxt_attrib o map) Token.init_assignable elem of + Element.Defines defs => + Element.Defines (defs |> map (fn ((a, atts), (t, ps)) => + ((Thm.def_binding_optional + (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt (K []) t)))) a, atts), + (t, ps)))) + | Element.Assumes assms => Element.Assumes (Elab.elaborate ctxt [] assms) + | e => e); + val ctxt' = Context.proof_map (Element.init elem') ctxt; + in ((Element.map_ctxt_attrib o map) Token.closure elem', ctxt') end + +fun activate raw_elem ctxt = + let val elem = raw_elem |> Element.map_ctxt + {binding = I, + typ = I, + term = I, + pattern = I, + fact = Proof_Context.get_fact ctxt, + attrib = Attrib.check_src ctxt} + in activate_i elem ctxt end + +in + +val read_goal_statement = prep_statement read_full_context_statement activate + +end + + +(* Proof assumption command *) + +local + +val structured_statement = + Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes + >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows)) + +in + +val _ = Outer_Syntax.command \<^command_keyword>\assuming\ "elaborated assumption" + (structured_statement >> (fn (a, b, c) => Toplevel.proof (fn state => + let + val ctxt = Proof.context_of state + + fun read_option_typ NONE = NONE + | read_option_typ (SOME s) = SOME (Syntax.read_typ ctxt s) + fun read_terms (s, ss) = + let val f = Syntax.read_term ctxt in (f s, map f ss) end + + val a' = map (fn (b, s, m) => (b, read_option_typ s, m)) a + val b' = map (map read_terms) b + val c' = c |> map (fn ((b, atts), ss) => + ((b, map (Attrib.attribute_cmd ctxt) atts), map read_terms ss)) + val c'' = Elab.elaborate ctxt [] c' + in Proof.assume a' b' c'' state end))) + +end + + +end \ No newline at end of file diff --git a/spartan/core/elaboration.ML b/spartan/core/elaboration.ML index 27b6bb0..9e5e0bd 100644 --- a/spartan/core/elaboration.ML +++ b/spartan/core/elaboration.ML @@ -1,13 +1,14 @@ (* Title: elaboration.ML Author: Joshua Chen -Basic elaboration. +Basic term elaboration. *) structure Elab: sig val elab: Proof.context -> cterm list -> term -> Envir.env val elab_stmt: Proof.context -> cterm list -> term -> Envir.env * term +val elaborate: Proof.context -> cterm list -> ('a * (term * term list) list) list -> ('a * (term * term list) list) list end = struct @@ -72,5 +73,19 @@ fun elab_stmt ctxt assums stmt = in (subst', subst_term subst' stmt) end end +(*Apply elaboration to the list format that assumptions and goal statements are + given in*) +fun elaborate ctxt known assms = + let + fun subst_term env = Envir.subst_term (Envir.type_env env, Envir.term_env env) + fun elab_fact (fact, xs) assums = + let val (subst, fact') = elab_stmt ctxt assums fact in + ((fact', map (subst_term subst) xs), Thm.cterm_of ctxt fact' :: assums) + end + fun elab (b, facts) assums = + let val (facts', assums') = fold_map elab_fact facts assums + in ((b, facts'), assums') end + in #1 (fold_map elab assms known) end + end diff --git a/spartan/core/focus.ML b/spartan/core/focus.ML index 1d8de78..2ad4c8a 100644 --- a/spartan/core/focus.ML +++ b/spartan/core/focus.ML @@ -1,14 +1,51 @@ (* Title: focus.ML - Author: Makarius Wenzel, Joshua Chen + Author: Joshua Chen -A modified version of the Isar `subgoal` command -that keeps schematic variables in the goal state. +Focus on head subgoal, with optional variable renaming. -Modified from code originally written by Makarius Wenzel. +Modified from code contained in ~~/Pure/Isar/subgoal.ML. *) local +fun reverse_prems imp = + let val (prems, concl) = (Drule.strip_imp_prems imp, Drule.strip_imp_concl imp) + in fold (curry mk_implies) prems concl end + +fun gen_focus ctxt i bindings raw_st = + let + val st = raw_st + |> Thm.solve_constraints + |> Thm.transfer' ctxt + |> Raw_Simplifier.norm_hhf_protect ctxt + + val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt + + val ((params, goal), ctxt2) = + Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1 + + val (asms, concl) = + (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal) + + fun intern_var_assms asm (asms, concl) = + if Lib.no_vars (Thm.term_of asm) + then (asm :: asms, concl) + else (asms, Drule.mk_implies (asm, concl)) + + val (asms', concl') = fold intern_var_assms asms ([], concl) + |> apfst rev |> apsnd reverse_prems + + val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of (asms')) ctxt2 + val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst) + val schematics = (schematic_types, schematic_terms) + val asms' = map (Thm.instantiate_cterm schematics) asms' + val concl' = Thm.instantiate_cterm schematics concl' + val (prems, context) = Assumption.add_assumes asms' ctxt3 + in + ({context = context, params = params, prems = prems, + asms = asms', concl = concl', schematics = schematics}, Goal.init concl') + end + fun param_bindings ctxt (param_suffix, raw_param_specs) st = let val _ = if Thm.no_prems st then error "No subgoals!" else () @@ -24,8 +61,8 @@ fun param_bindings ctxt (param_suffix, raw_param_specs) st = error ("Excessive subgoal parameter specification" ^ Position.here_list (map snd (drop n raw_param_specs))) - val param_specs = - raw_param_specs |> map + val param_specs = raw_param_specs + |> map (fn (NONE, _) => NONE | (SOME x, pos) => let @@ -39,7 +76,7 @@ fun param_bindings ctxt (param_suffix, raw_param_specs) st = | bindings _ ys = map Binding.name ys in bindings param_specs subgoal_params end -fun gen_schematic_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state = +fun gen_schematic_subgoal prep_atts raw_result_binding param_specs state = let val _ = Proof.assert_backward state @@ -47,17 +84,13 @@ fun gen_schematic_subgoal prep_atts raw_result_binding raw_prems_binding param_s |> Proof.map_context (Proof_Context.set_mode Proof_Context.mode_schematic) |> Proof.refine_insert [] - val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state1 - + val {context = ctxt, facts, goal = st} = Proof.raw_goal state1 val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding - val (prems_binding, do_prems) = - (case raw_prems_binding of - SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true) - | NONE => (Binding.empty_atts, false)) - val (subgoal_focus, _) = - (if do_prems then Subgoal.focus_prems else Subgoal.focus_params) ctxt - 1 (SOME (param_bindings ctxt param_specs st)) st + val subgoal_focus = #1 + (gen_focus ctxt 1 (SOME (param_bindings ctxt param_specs st)) st) + + val prems = #prems subgoal_focus fun after_qed (ctxt'', [[result]]) = Proof.end_block #> (fn state' => @@ -83,31 +116,29 @@ fun gen_schematic_subgoal prep_atts raw_result_binding raw_prems_binding param_s |> Proof.begin_block |> Proof.map_context (fn _ => #context subgoal_focus - |> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2) + |> Proof_Context.note_thmss "" [((Binding.name "prems", []), [(prems, [])])] + |> #2) |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal" - NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2 - |> Proof.using_facts facts + NONE after_qed [] [] [(Binding.empty_atts, [(Thm.term_of (#concl subgoal_focus), [])])] + |> #2 + |> Proof.using_facts (facts @ prems) |> pair subgoal_focus end val opt_fact_binding = - Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) + Scan.optional ((Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) --| Args.colon) Binding.empty_atts -val for_params = - Scan.optional - (\<^keyword>\vars\ |-- - Parse.!!! ((Scan.option Parse.dots >> is_some) -- - (Scan.repeat1 (Parse.maybe_position Parse.name_position)))) - (false, []) +val for_params = Scan.optional + (\<^keyword>\vars\ |-- + Parse.!!! ((Scan.option Parse.dots >> is_some) -- + (Scan.repeat1 (Parse.maybe_position Parse.name_position)))) + (false, []) val schematic_subgoal_cmd = gen_schematic_subgoal Attrib.attribute_cmd -val parser = - opt_fact_binding - -- (Scan.option (\<^keyword>\prems\ |-- Parse.!!! opt_fact_binding)) - -- for_params >> (fn ((a, b), c) => - Toplevel.proofs (Seq.make_results o Seq.single o #2 o schematic_subgoal_cmd a b c)) +val parser = opt_fact_binding -- for_params >> (fn (fact, params) => + Toplevel.proofs (Seq.make_results o Seq.single o #2 o schematic_subgoal_cmd fact params)) in @@ -117,9 +148,10 @@ val _ = Outer_Syntax.command \<^command_keyword>\focus\ "focus on first subgoal within backward refinement, without instantiating schematic vars" parser -val _ = Outer_Syntax.command \<^command_keyword>\\\ "focus bullet" parser val _ = Outer_Syntax.command \<^command_keyword>\\<^item>\ "focus bullet" parser val _ = Outer_Syntax.command \<^command_keyword>\\<^enum>\ "focus bullet" parser +val _ = Outer_Syntax.command \<^command_keyword>\\\ "focus bullet" parser +val _ = Outer_Syntax.command \<^command_keyword>\\\ "focus bullet" parser val _ = Outer_Syntax.command \<^command_keyword>\~\ "focus bullet" parser end diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML index 87ec2b8..540f5c7 100644 --- a/spartan/core/goals.ML +++ b/spartan/core/goals.ML @@ -1,9 +1,9 @@ (* Title: goals.ML - Author: Makarius Wenzel, Joshua Chen + Author: Joshua Chen Goal statements and proof term export. -Modified from code originally written by Makarius Wenzel. +Modified from code contained in ~~/Pure/Isar/specification.ML. *) local @@ -184,15 +184,15 @@ val schematic_theorem_cmd = gen_schematic_theorem Bundle.includes_cmd Attrib.check_src - Elaborated_Assumption.read_goal_statement + Elaborated_Statement.read_goal_statement fun theorem spec descr = Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) - ( Scan.option (Args.parens (Args.$$$ "derive")) + ( Scan.option (Args.parens (Args.$$$ "def")) -- (long_statement || short_statement) >> (fn (opt_derive, (long, binding, includes, elems, concl)) => schematic_theorem_cmd - (case opt_derive of SOME "derive" => true | _ => false) + (case opt_derive of SOME "def" => true | _ => false) long descr NONE (K I) binding includes elems concl) ) fun definition spec descr = diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML index 3922ae0..19d3d71 100644 --- a/spartan/core/tactics.ML +++ b/spartan/core/tactics.ML @@ -19,8 +19,7 @@ end = struct (* Side conditions *) -val solve_side_conds = - Attrib.setup_config_int \<^binding>\solve_side_conds\ (K 2) +val solve_side_conds = Attrib.setup_config_int \<^binding>\solve_side_conds\ (K 2) fun SIDE_CONDS ctac facts i (cst as (ctxt, st)) = cst |> (ctac i CTHEN (case Config.get ctxt solve_side_conds of diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML index 57164a1..a6e1726 100644 --- a/spartan/core/typechecking.ML +++ b/spartan/core/typechecking.ML @@ -51,10 +51,9 @@ fun known_ctac facts = CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) => if Lib.no_vars concl orelse (Lib.is_typing concl andalso Lib.no_vars (Lib.term_of_typing concl)) then - let val ths = facts + let val ths = map (Simplifier.norm_hhf ctxt) + (facts @ map fst (Facts.props (Proof_Context.facts_of ctxt))) (*FIXME: Shouldn't pull nameless facts directly from context*) - @ map fst (Facts.props (Proof_Context.facts_of ctxt)) - |> map (Simplifier.norm_hhf ctxt) in (debug_tac ctxt "resolve" THEN resolve_tac ctxt ths i ORELSE debug_tac ctxt "assume" THEN assume_tac ctxt i) st @@ -70,7 +69,8 @@ fun check_infer_step facts i (ctxt, st) = val tac = SUBGOAL (fn (goal, i) => if Lib.rigid_typing_concl goal then - let val net = Tactic.build_net (facts + let val net = Tactic.build_net ( + map (Simplifier.norm_hhf ctxt) facts (*MAYBE FIXME: Remove `typechk` from this list, and instead perform definitional unfolding to (w?)hnf.*) @(Named_Theorems.get ctxt \<^named_theorems>\typechk\) diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy index be86b63..34873e4 100644 --- a/spartan/lib/List.thy +++ b/spartan/lib/List.thy @@ -132,9 +132,9 @@ Definition app: assumes "A: U i" "xs: List A" "ys: List A" shows "List A" apply (elim xs) - \ by (fact \ys:_\) - \ prems vars x _ rec - proof - show "x # rec: List A" by typechk qed + \<^item> by (fact \ys:_\) + \<^item> vars x _ rec + proof - show "x # rec: List A" by typechk qed done definition app_i ("app") where [implicit]: "app xs ys \ List.app ? xs ys" @@ -169,8 +169,8 @@ Definition rev: assumes "A: U i" "xs: List A" shows "List A" apply (elim xs) - \ by (rule List_nil) - \ prems vars x _ rec proof - show "app rec [x]: List A" by typechk qed + \<^item> by (rule List_nil) + \<^item> vars x _ rec proof - show "app rec [x]: List A" by typechk qed done definition rev_i ("rev") where [implicit]: "rev \ List.rev ?" diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy index 0ce534c..a2e1638 100644 --- a/spartan/lib/Maybe.thy +++ b/spartan/lib/Maybe.thy @@ -1,7 +1,7 @@ chapter \Maybe type\ theory Maybe -imports More_Types +imports Prelude begin @@ -25,11 +25,10 @@ Definition MaybeInd: "\a. a: A \ f a: C (some A a)" "m: Maybe A" shows "C m" - supply assms[unfolded Maybe_def none_def some_def] + using assms[unfolded Maybe_def none_def some_def] apply (elim m) - \ unfolding Maybe_def . - \ by (rule \_ \ _: C (inl _ _ _)\) - \ by elim (rule \_: C (inr _ _ _)\) + apply (rule \_ \ _: C (inl _ _ _)\) + apply (elim, rule \_: C (inr _ _ _)\) done Lemma Maybe_comp_none: @@ -39,8 +38,9 @@ Lemma Maybe_comp_none: "\a. a: A \ f a: C (some A a)" "\m. m: Maybe A \ C m: U i" shows "MaybeInd A C c\<^sub>0 f (none A) \ c\<^sub>0" - supply assms[unfolded Maybe_def some_def none_def] - unfolding MaybeInd_def none_def by reduce + using assms + unfolding Maybe_def MaybeInd_def none_def some_def + by reduce Lemma Maybe_comp_some: assumes @@ -50,8 +50,9 @@ Lemma Maybe_comp_some: "\a. a: A \ f a: C (some A a)" "\m. m: Maybe A \ C m: U i" shows "MaybeInd A C c\<^sub>0 f (some A a) \ f a" - supply assms[unfolded Maybe_def some_def none_def] - unfolding MaybeInd_def some_def by (reduce add: Maybe_def) + using assms + unfolding Maybe_def MaybeInd_def none_def some_def + by reduce lemmas [form] = MaybeF and diff --git a/spartan/lib/More_Types.thy b/spartan/lib/More_Types.thy deleted file mode 100644 index 55e6554..0000000 --- a/spartan/lib/More_Types.thy +++ /dev/null @@ -1,150 +0,0 @@ -theory More_Types -imports Spartan - -begin - -section \Sum type\ - -axiomatization - Sum :: \o \ o \ o\ and - inl :: \o \ o \ o \ o\ and - inr :: \o \ o \ o \ o\ and - SumInd :: \o \ o \ (o \ o) \ (o \ o) \ (o \ o) \ o \ o\ - -notation Sum (infixl "\" 50) - -axiomatization where - SumF: "\A: U i; B: U i\ \ A \ B: U i" and - - Sum_inl: "\B: U i; a: A\ \ inl A B a: A \ B" and - - Sum_inr: "\A: U i; b: B\ \ inr A B b: A \ B" and - - SumE: "\ - s: A \ B; - \s. s: A \ B \ C s: U i; - \a. a: A \ c a: C (inl A B a); - \b. b: B \ d b: C (inr A B b) - \ \ SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) s: C s" and - - Sum_comp_inl: "\ - a: A; - \s. s: A \ B \ C s: U i; - \a. a: A \ c a: C (inl A B a); - \b. b: B \ d b: C (inr A B b) - \ \ SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) (inl A B a) \ c a" and - - Sum_comp_inr: "\ - b: B; - \s. s: A \ B \ C s: U i; - \a. a: A \ c a: C (inl A B a); - \b. b: B \ d b: C (inr A B b) - \ \ SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) (inr A B b) \ d b" - -lemmas - [form] = SumF and - [intro] = Sum_inl Sum_inr and - [intros] = Sum_inl[rotated] Sum_inr[rotated] and - [elim ?s] = SumE and - [comp] = Sum_comp_inl Sum_comp_inr - -method left = rule Sum_inl -method right = rule Sum_inr - - -section \Empty and unit types\ - -axiomatization - Top :: \o\ and - tt :: \o\ and - TopInd :: \(o \ o) \ o \ o \ o\ -and - Bot :: \o\ and - BotInd :: \(o \ o) \ o \ o\ - -notation Top ("\") and Bot ("\") - -axiomatization where - TopF: "\: U i" and - - TopI: "tt: \" and - - TopE: "\a: \; \x. x: \ \ C x: U i; c: C tt\ \ TopInd (fn x. C x) c a: C a" and - - Top_comp: "\\x. x: \ \ C x: U i; c: C tt\ \ TopInd (fn x. C x) c tt \ c" -and - BotF: "\: U i" and - - BotE: "\x: \; \x. x: \ \ C x: U i\ \ BotInd (fn x. C x) x: C x" - -lemmas - [form] = TopF BotF and - [intro, intros] = TopI and - [elim ?a] = TopE and - [elim ?x] = BotE and - [comp] = Top_comp - - -section \Booleans\ - -definition "Bool \ \ \ \" -definition "true \ inl \ \ tt" -definition "false \ inr \ \ tt" - -Lemma - BoolF: "Bool: U i" and - Bool_true: "true: Bool" and - Bool_false: "false: Bool" - unfolding Bool_def true_def false_def by typechk+ - -\ \Definitions like these should be handled by a future function package\ -Definition ifelse [rotated 1]: - assumes *[unfolded Bool_def true_def false_def]: - "\x. x: Bool \ C x: U i" - "x: Bool" - "a: C true" - "b: C false" - shows "C x" - by (elim x) (elim, rule *)+ - -Lemma if_true: - assumes - "\x. x: Bool \ C x: U i" - "a: C true" - "b: C false" - shows "ifelse C true a b \ a" - unfolding ifelse_def true_def - supply assms[unfolded Bool_def true_def false_def] - by reduce - -Lemma if_false: - assumes - "\x. x: Bool \ C x: U i" - "a: C true" - "b: C false" - shows "ifelse C false a b \ b" - unfolding ifelse_def false_def - supply assms[unfolded Bool_def true_def false_def] - by reduce - -lemmas - [form] = BoolF and - [intro, intros] = Bool_true Bool_false and - [comp] = if_true if_false and - [elim ?x] = ifelse -lemmas - BoolE = ifelse - -subsection \Notation\ - -definition ifelse_i ("if _ then _ else _") - 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" - -subsection \Logical connectives\ - -definition not ("!_") where "not x \ ifelse (K Bool) x false true" - - -end diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy new file mode 100644 index 0000000..36f12d2 --- /dev/null +++ b/spartan/lib/Prelude.thy @@ -0,0 +1,150 @@ +theory Prelude +imports Spartan + +begin + +section \Sum type\ + +axiomatization + Sum :: \o \ o \ o\ and + inl :: \o \ o \ o \ o\ and + inr :: \o \ o \ o \ o\ and + SumInd :: \o \ o \ (o \ o) \ (o \ o) \ (o \ o) \ o \ o\ + +notation Sum (infixl "\" 50) + +axiomatization where + SumF: "\A: U i; B: U i\ \ A \ B: U i" and + + Sum_inl: "\B: U i; a: A\ \ inl A B a: A \ B" and + + Sum_inr: "\A: U i; b: B\ \ inr A B b: A \ B" and + + SumE: "\ + s: A \ B; + \s. s: A \ B \ C s: U i; + \a. a: A \ c a: C (inl A B a); + \b. b: B \ d b: C (inr A B b) + \ \ SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) s: C s" and + + Sum_comp_inl: "\ + a: A; + \s. s: A \ B \ C s: U i; + \a. a: A \ c a: C (inl A B a); + \b. b: B \ d b: C (inr A B b) + \ \ SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) (inl A B a) \ c a" and + + Sum_comp_inr: "\ + b: B; + \s. s: A \ B \ C s: U i; + \a. a: A \ c a: C (inl A B a); + \b. b: B \ d b: C (inr A B b) + \ \ SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) (inr A B b) \ d b" + +lemmas + [form] = SumF and + [intro] = Sum_inl Sum_inr and + [intros] = Sum_inl[rotated] Sum_inr[rotated] and + [elim ?s] = SumE and + [comp] = Sum_comp_inl Sum_comp_inr + +method left = rule Sum_inl +method right = rule Sum_inr + + +section \Empty and unit types\ + +axiomatization + Top :: \o\ and + tt :: \o\ and + TopInd :: \(o \ o) \ o \ o \ o\ +and + Bot :: \o\ and + BotInd :: \(o \ o) \ o \ o\ + +notation Top ("\") and Bot ("\") + +axiomatization where + TopF: "\: U i" and + + TopI: "tt: \" and + + TopE: "\a: \; \x. x: \ \ C x: U i; c: C tt\ \ TopInd (fn x. C x) c a: C a" and + + Top_comp: "\\x. x: \ \ C x: U i; c: C tt\ \ TopInd (fn x. C x) c tt \ c" +and + BotF: "\: U i" and + + BotE: "\x: \; \x. x: \ \ C x: U i\ \ BotInd (fn x. C x) x: C x" + +lemmas + [form] = TopF BotF and + [intro, intros] = TopI and + [elim ?a] = TopE and + [elim ?x] = BotE and + [comp] = Top_comp + + +section \Booleans\ + +definition "Bool \ \ \ \" +definition "true \ inl \ \ tt" +definition "false \ inr \ \ tt" + +Lemma + BoolF: "Bool: U i" and + Bool_true: "true: Bool" and + Bool_false: "false: Bool" + unfolding Bool_def true_def false_def by typechk+ + +\ \Definitions like these should be handled by a future function package\ +Definition ifelse [rotated 1]: + assumes *[unfolded Bool_def true_def false_def]: + "\x. x: Bool \ C x: U i" + "x: Bool" + "a: C true" + "b: C false" + shows "C x" + by (elim x) (elim, rule *)+ + +Lemma if_true: + assumes + "\x. x: Bool \ C x: U i" + "a: C true" + "b: C false" + shows "ifelse C true a b \ a" + unfolding ifelse_def true_def + using assms unfolding Bool_def true_def false_def + by reduce + +Lemma if_false: + assumes + "\x. x: Bool \ C x: U i" + "a: C true" + "b: C false" + shows "ifelse C false a b \ b" + unfolding ifelse_def false_def + using assms unfolding Bool_def true_def false_def + by reduce + +lemmas + [form] = BoolF and + [intro, intros] = Bool_true Bool_false and + [comp] = if_true if_false and + [elim ?x] = ifelse +lemmas + BoolE = ifelse + +subsection \Notation\ + +definition ifelse_i ("if _ then _ else _") + 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" + +subsection \Logical connectives\ + +definition not ("!_") where "not x \ ifelse (K Bool) x false true" + + +end -- cgit v1.2.3