From 831f33468f227c0dc96bd31380236f2c77e70c52 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 9 Jul 2020 13:35:39 +0200 Subject: Non-annotated object lambda --- spartan/core/Spartan.thy | 65 ++++++++++++++++++++++++++++++++-------------- spartan/lib/List.thy | 12 ++++----- spartan/lib/Maybe.thy | 13 ++++------ spartan/lib/More_Types.thy | 12 ++++----- 4 files changed, 62 insertions(+), 40 deletions(-) (limited to 'spartan') diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index ed21934..1ca027f 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -15,24 +15,37 @@ keywords begin -section \Preamble\ +section \Prelude\ declare [[eta_contract=false]] +setup \ +let + val typ = Simple_Syntax.read_typ + fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range) +in + Sign.del_syntax (Print_Mode.ASCII, true) + [("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3fn _./ _)", [0, 3], 3))] + #> Sign.del_syntax Syntax.mode_default + [("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3\_./ _)", [0, 3], 3))] + #> Sign.add_syntax Syntax.mode_default + [("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3fn _./ _)", [0, 3], 3))] +end +\ + syntax "_dollar" :: \logic \ logic \ logic\ (infixr "$" 3) translations "a $ b" \ "a (b)" -abbreviation (input) K where "K x \ \_. x" - - -section \Metatype setup\ +abbreviation (input) K where "K x \ fn _. x" typedecl o +judgment has_type :: \o \ o \ prop\ ("(2_:/ _)" 999) -section \Judgments\ -judgment has_type :: \o \ o \ prop\ ("(2_:/ _)" 999) +section \Type annotations\ + +consts anno :: \o \ o \ o\ ("'(_: _')") section \Universes\ @@ -74,15 +87,15 @@ syntax "_lam" :: \idts \ o \ o \ o\ ("(2\_: _./ _)" 30) "_lam2" :: \idts \ o \ o \ o\ translations - "\x xs: A. B" \ "CONST Pi A (\x. _Pi2 xs A B)" - "_Pi2 x A B" \ "\x: A. B" - "\x: A. B" \ "CONST Pi A (\x. B)" - "\x xs: A. b" \ "CONST lam A (\x. _lam2 xs A b)" + "\x xs: A. B" \ "CONST Pi A (fn x. _Pi2 xs A B)" + "_Pi2 x A B" \ "\x: A. B" + "\x: A. B" \ "CONST Pi A (fn x. B)" + "\x xs: A. b" \ "CONST lam A (fn x. _lam2 xs A b)" "_lam2 x A b" \ "\x: A. b" - "\x: A. b" \ "CONST lam A (\x. b)" + "\x: A. b" \ "CONST lam A (fn x. b)" abbreviation Fn (infixr "\" 40) where "A \ B \ \_: A. B" - +term "\x: A. b x" axiomatization where PiF: "\\x. x: A \ B x: U i; A: U i\ \ \x: A. B x: U i" and @@ -113,7 +126,7 @@ axiomatization syntax "_Sum" :: \idt \ o \ o \ o\ ("(2\_: _./ _)" 20) -translations "\x: A. B" \ "CONST Sig A (\x. B)" +translations "\x: A. B" \ "CONST Sig A (fn x. B)" abbreviation Prod (infixl "\" 60) where "A \ B \ \_: A. B" @@ -132,7 +145,7 @@ axiomatization where \x. x : A \ B x: U i; \x y. \x: A; y: B x\ \ f x y: C ; \p. p: \x: A. B x \ C p: U i - \ \ SigInd A (\x. B x) (\p. C p) f p: C p" and + \ \ SigInd A (fn x. B x) (fn p. C p) f p: C p" and Sig_comp: "\ a: A; @@ -140,7 +153,7 @@ axiomatization where \x. x: A \ B x: U i; \p. p: \x: A. B x \ C p: U i; \x y. \x: A; y: B x\ \ f x y: C - \ \ SigInd A (\x. B x) (\p. C p) f \ f a b" and + \ \ SigInd A (fn x. B x) (fn p. C p) f \ f a b" and Sig_cong: "\ \x. x: A \ B x \ B' x; @@ -249,7 +262,7 @@ consts rewrite_HOLE :: "'a::{}" ("\") lemma eta_expand: fixes f :: "'a::{} \ 'b::{}" - shows "f \ \x. f x" . + shows "f \ fn x. f x" . lemma rewr_imp: assumes "PROP A \ PROP B" @@ -301,11 +314,23 @@ text \Automatically insert inhabitation judgments where needed:\ syntax inhabited :: \o \ prop\ ("(_)") translations "inhabited A" \ "CONST has_type {} A" +text \Implicit lambdas\ + +definition lam_i where [implicit]: "lam_i f \ lam ? f" + +syntax + "_lam_i" :: \idts \ o \ o\ ("(2\_./ _)" 30) + "_lam_i2" :: \idts \ o \ o\ +translations + "\x xs. b" \ "CONST lam_i (fn x. _lam_i2 xs b)" + "_lam_i2 x b" \ "\x. b" + "\x. b" \ "CONST lam_i (fn x. b)" + subsection \Lambda coercion\ \ \Coerce object lambdas to meta-lambdas\ abbreviation (input) lambda :: \o \ o \ o\ - where "lambda f \ \x. f `x" + where "lambda f \ fn x. f `x" ML_file \~~/src/Tools/subtyping.ML\ declare [[coercion_enabled, coercion lambda]] @@ -409,8 +434,8 @@ lemma id_U [typechk]: section \Pairs\ -definition "fst A B \ \p: \x: A. B x. SigInd A B (\_. A) (\x y. x) p" -definition "snd A B \ \p: \x: A. B x. SigInd A B (\p. B (fst A B p)) (\x y. y) p" +definition "fst A B \ \p: \x: A. B x. SigInd A B (fn _. A) (fn x y. x) p" +definition "snd A B \ \p: \x: A. B x. SigInd A B (fn p. B (fst A B p)) (fn x y. y) p" lemma fst_type [typechk]: assumes "A: U i" "\x. x: A \ B x: U i" diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy index 11b8406..a755859 100644 --- a/spartan/lib/List.thy +++ b/spartan/lib/List.thy @@ -26,13 +26,13 @@ where c\<^sub>0: C (nil A); \x xs rec. \x: A; xs: List A; rec: C xs\ \ f x xs rec: C (cons A x xs); \xs. xs: List A \ C xs: U i - \ \ ListInd A (\xs. C xs) c\<^sub>0 (\x xs rec. f x xs rec) xs: C xs" and + \ \ ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) xs: C xs" and List_comp_nil: "\ c\<^sub>0: C (nil A); \x xs rec. \x: A; xs: List A; rec: C xs\ \ f x xs rec: C (cons A x xs); \xs. xs: List A \ C xs: U i - \ \ ListInd A (\xs. C xs) c\<^sub>0 (\x xs rec. f x xs rec) (nil A) \ c\<^sub>0" and + \ \ ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) (nil A) \ c\<^sub>0" and List_comp_cons: "\ xs: List A; @@ -40,15 +40,15 @@ where \x xs rec. \x: A; xs: List A; rec: C xs\ \ f x xs rec: C (cons A x xs); \xs. xs: List A \ C xs: U i \ \ - ListInd A (\xs. C xs) c\<^sub>0 (\x xs rec. f x xs rec) (cons A x xs) \ - f x xs (ListInd A (\xs. C xs) c\<^sub>0 (\x xs rec. f x xs rec) xs)" + ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) (cons A x xs) \ + f x xs (ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) xs)" lemmas [intros] = ListF List_nil List_cons and [elims "?xs"] = ListE and [comps] = List_comp_nil List_comp_cons -abbreviation "ListRec A C \ ListInd A (\_. C)" +abbreviation "ListRec A C \ ListInd A (fn _. C)" Lemma list_cases [cases]: assumes @@ -56,7 +56,7 @@ Lemma list_cases [cases]: nil_case: "c\<^sub>0: C (nil A)" and cons_case: "\x xs. \x: A; xs: List A\ \ f x xs: C (cons A x xs)" and "\xs. xs: List A \ C xs: U i" - shows "?List_cases A (\xs. C xs) c\<^sub>0 (\x xs. f x xs) xs: C xs" + shows "C xs" by (elim xs) (fact nil_case, rule cons_case) diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy index 6729812..d821920 100644 --- a/spartan/lib/Maybe.thy +++ b/spartan/lib/Maybe.thy @@ -24,7 +24,7 @@ Definition MaybeInd: "c\<^sub>0: C (none A)" "\a. a: A \ f a: C (some A a)" "m: Maybe A" - shows "?MaybeInd A (\m. C m) c\<^sub>0 (\a. f a) m: C m" + shows "C m" supply assms[unfolded Maybe_def none_def some_def] apply (elim m) \ unfolding Maybe_def . @@ -38,7 +38,7 @@ Lemma Maybe_comp_none: "c\<^sub>0: C (none A)" "\a. a: A \ f a: C (some A a)" "\m. m: Maybe A \ C m: U i" - shows "MaybeInd A (\m. C m) c\<^sub>0 (\a. f a) (none A) \ c\<^sub>0" + 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 @@ -49,7 +49,7 @@ Lemma Maybe_comp_some: "c\<^sub>0: C (none A)" "\a. a: A \ f a: C (some A a)" "\m. m: Maybe A \ C m: U i" - shows "MaybeInd A (\m. C m) c\<^sub>0 (\a. f a) (some A a) \ f a" + 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) @@ -62,11 +62,8 @@ lemmas abbreviation "MaybeRec A C \ MaybeInd A (K C)" -definition none_i ("none") - where [implicit]: "none \ Maybe.none ?" - -definition some_i ("some") - where [implicit]: "some a \ Maybe.some ? a" +definition none_i ("none") where [implicit]: "none \ Maybe.none ?" +definition some_i ("some") where [implicit]: "some a \ Maybe.some ? a" translations "none" \ "CONST Maybe.none A" diff --git a/spartan/lib/More_Types.thy b/spartan/lib/More_Types.thy index 38ba2aa..0d7096f 100644 --- a/spartan/lib/More_Types.thy +++ b/spartan/lib/More_Types.thy @@ -25,21 +25,21 @@ axiomatization where \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 (\s. C s) (\a. c a) (\b. d b) s: C s" and + \ \ 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 (\s. C s) (\a. c a) (\b. d b) (inl A B a) \ c a" and + \ \ 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 (\s. C s) (\a. c a) (\b. d b) (inr A B b) \ d b" + \ \ SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) (inr A B b) \ d b" lemmas [intros] = SumF Sum_inl Sum_inr and @@ -67,13 +67,13 @@ axiomatization where TopI: "tt: \" and - TopE: "\a: \; \x. x: \ \ C x: U i; c: C tt\ \ TopInd (\x. C x) c a: C a" 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 (\x. C x) c tt \ c" + 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 (\x. C x) x: C x" + BotE: "\x: \; \x. x: \ \ C x: U i\ \ BotInd (fn x. C x) x: C x" lemmas [intros] = TopF TopI BotF and -- cgit v1.2.3