diff options
Diffstat (limited to '')
| -rw-r--r-- | spartan/core/Spartan.thy | 65 | ||||
| -rw-r--r-- | spartan/lib/List.thy | 12 | ||||
| -rw-r--r-- | spartan/lib/Maybe.thy | 13 | ||||
| -rw-r--r-- | spartan/lib/More_Types.thy | 12 |
4 files changed, 62 insertions, 40 deletions
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 \<open>Preamble\<close> +section \<open>Prelude\<close> declare [[eta_contract=false]] +setup \<open> +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 \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3fn _./ _)", [0, 3], 3))] + #> Sign.del_syntax Syntax.mode_default + [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3\<lambda>_./ _)", [0, 3], 3))] + #> Sign.add_syntax Syntax.mode_default + [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3fn _./ _)", [0, 3], 3))] +end +\<close> + syntax "_dollar" :: \<open>logic \<Rightarrow> logic \<Rightarrow> logic\<close> (infixr "$" 3) translations "a $ b" \<rightharpoonup> "a (b)" -abbreviation (input) K where "K x \<equiv> \<lambda>_. x" - - -section \<open>Metatype setup\<close> +abbreviation (input) K where "K x \<equiv> fn _. x" typedecl o +judgment has_type :: \<open>o \<Rightarrow> o \<Rightarrow> prop\<close> ("(2_:/ _)" 999) -section \<open>Judgments\<close> -judgment has_type :: \<open>o \<Rightarrow> o \<Rightarrow> prop\<close> ("(2_:/ _)" 999) +section \<open>Type annotations\<close> + +consts anno :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> ("'(_: _')") section \<open>Universes\<close> @@ -74,15 +87,15 @@ syntax "_lam" :: \<open>idts \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<lambda>_: _./ _)" 30) "_lam2" :: \<open>idts \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> translations - "\<Prod>x xs: A. B" \<rightharpoonup> "CONST Pi A (\<lambda>x. _Pi2 xs A B)" - "_Pi2 x A B" \<rightharpoonup> "\<Prod>x: A. B" - "\<Prod>x: A. B" \<rightleftharpoons> "CONST Pi A (\<lambda>x. B)" - "\<lambda>x xs: A. b" \<rightharpoonup> "CONST lam A (\<lambda>x. _lam2 xs A b)" + "\<Prod>x xs: A. B" \<rightharpoonup> "CONST Pi A (fn x. _Pi2 xs A B)" + "_Pi2 x A B" \<rightharpoonup> "\<Prod>x: A. B" + "\<Prod>x: A. B" \<rightleftharpoons> "CONST Pi A (fn x. B)" + "\<lambda>x xs: A. b" \<rightharpoonup> "CONST lam A (fn x. _lam2 xs A b)" "_lam2 x A b" \<rightharpoonup> "\<lambda>x: A. b" - "\<lambda>x: A. b" \<rightleftharpoons> "CONST lam A (\<lambda>x. b)" + "\<lambda>x: A. b" \<rightleftharpoons> "CONST lam A (fn x. b)" abbreviation Fn (infixr "\<rightarrow>" 40) where "A \<rightarrow> B \<equiv> \<Prod>_: A. B" - +term "\<lambda>x: A. b x" axiomatization where PiF: "\<lbrakk>\<And>x. x: A \<Longrightarrow> B x: U i; A: U i\<rbrakk> \<Longrightarrow> \<Prod>x: A. B x: U i" and @@ -113,7 +126,7 @@ axiomatization syntax "_Sum" :: \<open>idt \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<Sum>_: _./ _)" 20) -translations "\<Sum>x: A. B" \<rightleftharpoons> "CONST Sig A (\<lambda>x. B)" +translations "\<Sum>x: A. B" \<rightleftharpoons> "CONST Sig A (fn x. B)" abbreviation Prod (infixl "\<times>" 60) where "A \<times> B \<equiv> \<Sum>_: A. B" @@ -132,7 +145,7 @@ axiomatization where \<And>x. x : A \<Longrightarrow> B x: U i; \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y>; \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U i - \<rbrakk> \<Longrightarrow> SigInd A (\<lambda>x. B x) (\<lambda>p. C p) f p: C p" and + \<rbrakk> \<Longrightarrow> SigInd A (fn x. B x) (fn p. C p) f p: C p" and Sig_comp: "\<lbrakk> a: A; @@ -140,7 +153,7 @@ axiomatization where \<And>x. x: A \<Longrightarrow> B x: U i; \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U i; \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y> - \<rbrakk> \<Longrightarrow> SigInd A (\<lambda>x. B x) (\<lambda>p. C p) f <a, b> \<equiv> f a b" and + \<rbrakk> \<Longrightarrow> SigInd A (fn x. B x) (fn p. C p) f <a, b> \<equiv> f a b" and Sig_cong: "\<lbrakk> \<And>x. x: A \<Longrightarrow> B x \<equiv> B' x; @@ -249,7 +262,7 @@ consts rewrite_HOLE :: "'a::{}" ("\<hole>") lemma eta_expand: fixes f :: "'a::{} \<Rightarrow> 'b::{}" - shows "f \<equiv> \<lambda>x. f x" . + shows "f \<equiv> fn x. f x" . lemma rewr_imp: assumes "PROP A \<equiv> PROP B" @@ -301,11 +314,23 @@ text \<open>Automatically insert inhabitation judgments where needed:\<close> syntax inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)") translations "inhabited A" \<rightharpoonup> "CONST has_type {} A" +text \<open>Implicit lambdas\<close> + +definition lam_i where [implicit]: "lam_i f \<equiv> lam ? f" + +syntax + "_lam_i" :: \<open>idts \<Rightarrow> o \<Rightarrow> o\<close> ("(2\<lambda>_./ _)" 30) + "_lam_i2" :: \<open>idts \<Rightarrow> o \<Rightarrow> o\<close> +translations + "\<lambda>x xs. b" \<rightharpoonup> "CONST lam_i (fn x. _lam_i2 xs b)" + "_lam_i2 x b" \<rightharpoonup> "\<lambda>x. b" + "\<lambda>x. b" \<rightleftharpoons> "CONST lam_i (fn x. b)" + subsection \<open>Lambda coercion\<close> \<comment> \<open>Coerce object lambdas to meta-lambdas\<close> abbreviation (input) lambda :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> - where "lambda f \<equiv> \<lambda>x. f `x" + where "lambda f \<equiv> fn x. f `x" ML_file \<open>~~/src/Tools/subtyping.ML\<close> declare [[coercion_enabled, coercion lambda]] @@ -409,8 +434,8 @@ lemma id_U [typechk]: section \<open>Pairs\<close> -definition "fst A B \<equiv> \<lambda>p: \<Sum>x: A. B x. SigInd A B (\<lambda>_. A) (\<lambda>x y. x) p" -definition "snd A B \<equiv> \<lambda>p: \<Sum>x: A. B x. SigInd A B (\<lambda>p. B (fst A B p)) (\<lambda>x y. y) p" +definition "fst A B \<equiv> \<lambda>p: \<Sum>x: A. B x. SigInd A B (fn _. A) (fn x y. x) p" +definition "snd A B \<equiv> \<lambda>p: \<Sum>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" "\<And>x. x: A \<Longrightarrow> 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); \<And>x xs rec. \<lbrakk>x: A; xs: List A; rec: C xs\<rbrakk> \<Longrightarrow> f x xs rec: C (cons A x xs); \<And>xs. xs: List A \<Longrightarrow> C xs: U i - \<rbrakk> \<Longrightarrow> ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs rec. f x xs rec) xs: C xs" and + \<rbrakk> \<Longrightarrow> ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) xs: C xs" and List_comp_nil: "\<lbrakk> c\<^sub>0: C (nil A); \<And>x xs rec. \<lbrakk>x: A; xs: List A; rec: C xs\<rbrakk> \<Longrightarrow> f x xs rec: C (cons A x xs); \<And>xs. xs: List A \<Longrightarrow> C xs: U i - \<rbrakk> \<Longrightarrow> ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs rec. f x xs rec) (nil A) \<equiv> c\<^sub>0" and + \<rbrakk> \<Longrightarrow> ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) (nil A) \<equiv> c\<^sub>0" and List_comp_cons: "\<lbrakk> xs: List A; @@ -40,15 +40,15 @@ where \<And>x xs rec. \<lbrakk>x: A; xs: List A; rec: C xs\<rbrakk> \<Longrightarrow> f x xs rec: C (cons A x xs); \<And>xs. xs: List A \<Longrightarrow> C xs: U i \<rbrakk> \<Longrightarrow> - ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs rec. f x xs rec) (cons A x xs) \<equiv> - f x xs (ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>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) \<equiv> + 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 \<equiv> ListInd A (\<lambda>_. C)" +abbreviation "ListRec A C \<equiv> 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: "\<And>x xs. \<lbrakk>x: A; xs: List A\<rbrakk> \<Longrightarrow> f x xs: C (cons A x xs)" and "\<And>xs. xs: List A \<Longrightarrow> C xs: U i" - shows "?List_cases A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>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)" "\<And>a. a: A \<Longrightarrow> f a: C (some A a)" "m: Maybe A" - shows "?MaybeInd A (\<lambda>m. C m) c\<^sub>0 (\<lambda>a. f a) m: C m" + shows "C m" supply assms[unfolded Maybe_def none_def some_def] apply (elim m) \<guillemotright> unfolding Maybe_def . @@ -38,7 +38,7 @@ Lemma Maybe_comp_none: "c\<^sub>0: C (none A)" "\<And>a. a: A \<Longrightarrow> f a: C (some A a)" "\<And>m. m: Maybe A \<Longrightarrow> C m: U i" - shows "MaybeInd A (\<lambda>m. C m) c\<^sub>0 (\<lambda>a. f a) (none A) \<equiv> c\<^sub>0" + shows "MaybeInd A C c\<^sub>0 f (none A) \<equiv> 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)" "\<And>a. a: A \<Longrightarrow> f a: C (some A a)" "\<And>m. m: Maybe A \<Longrightarrow> C m: U i" - shows "MaybeInd A (\<lambda>m. C m) c\<^sub>0 (\<lambda>a. f a) (some A a) \<equiv> f a" + shows "MaybeInd A C c\<^sub>0 f (some A a) \<equiv> 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 \<equiv> MaybeInd A (K C)" -definition none_i ("none") - where [implicit]: "none \<equiv> Maybe.none ?" - -definition some_i ("some") - where [implicit]: "some a \<equiv> Maybe.some ? a" +definition none_i ("none") where [implicit]: "none \<equiv> Maybe.none ?" +definition some_i ("some") where [implicit]: "some a \<equiv> Maybe.some ? a" translations "none" \<leftharpoondown> "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 \<And>s. s: A \<or> B \<Longrightarrow> C s: U i; \<And>a. a: A \<Longrightarrow> c a: C (inl A B a); \<And>b. b: B \<Longrightarrow> d b: C (inr A B b) - \<rbrakk> \<Longrightarrow> SumInd A B (\<lambda>s. C s) (\<lambda>a. c a) (\<lambda>b. d b) s: C s" and + \<rbrakk> \<Longrightarrow> SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) s: C s" and Sum_comp_inl: "\<lbrakk> a: A; \<And>s. s: A \<or> B \<Longrightarrow> C s: U i; \<And>a. a: A \<Longrightarrow> c a: C (inl A B a); \<And>b. b: B \<Longrightarrow> d b: C (inr A B b) - \<rbrakk> \<Longrightarrow> SumInd A B (\<lambda>s. C s) (\<lambda>a. c a) (\<lambda>b. d b) (inl A B a) \<equiv> c a" and + \<rbrakk> \<Longrightarrow> SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) (inl A B a) \<equiv> c a" and Sum_comp_inr: "\<lbrakk> b: B; \<And>s. s: A \<or> B \<Longrightarrow> C s: U i; \<And>a. a: A \<Longrightarrow> c a: C (inl A B a); \<And>b. b: B \<Longrightarrow> d b: C (inr A B b) - \<rbrakk> \<Longrightarrow> SumInd A B (\<lambda>s. C s) (\<lambda>a. c a) (\<lambda>b. d b) (inr A B b) \<equiv> d b" + \<rbrakk> \<Longrightarrow> SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) (inr A B b) \<equiv> d b" lemmas [intros] = SumF Sum_inl Sum_inr and @@ -67,13 +67,13 @@ axiomatization where TopI: "tt: \<top>" and - TopE: "\<lbrakk>a: \<top>; \<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (\<lambda>x. C x) c a: C a" and + TopE: "\<lbrakk>a: \<top>; \<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (fn x. C x) c a: C a" and - Top_comp: "\<lbrakk>\<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (\<lambda>x. C x) c tt \<equiv> c" + Top_comp: "\<lbrakk>\<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (fn x. C x) c tt \<equiv> c" and BotF: "\<bottom>: U i" and - BotE: "\<lbrakk>x: \<bottom>; \<And>x. x: \<bottom> \<Longrightarrow> C x: U i\<rbrakk> \<Longrightarrow> BotInd (\<lambda>x. C x) x: C x" + BotE: "\<lbrakk>x: \<bottom>; \<And>x. x: \<bottom> \<Longrightarrow> C x: U i\<rbrakk> \<Longrightarrow> BotInd (fn x. C x) x: C x" lemmas [intros] = TopF TopI BotF and |