From 2feb56660700af107abb5a28a7120052ac405518 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sun, 31 Jan 2021 02:54:51 +0000 Subject: rename things + some small changes --- spartan/core/Spartan.thy | 571 ----------------------------------------------- 1 file changed, 571 deletions(-) delete mode 100644 spartan/core/Spartan.thy (limited to 'spartan/core/Spartan.thy') diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy deleted file mode 100644 index 5046b6a..0000000 --- a/spartan/core/Spartan.thy +++ /dev/null @@ -1,571 +0,0 @@ -text \Spartan type theory\ - -theory Spartan -imports - Pure - "HOL-Eisbach.Eisbach" - "HOL-Eisbach.Eisbach_Tools" -keywords - "Theorem" "Lemma" "Corollary" "Proposition" "Definition" :: thy_goal_stmt and - "assuming" :: prf_asm % "proof" and - "focus" "\<^item>" "\<^enum>" "\" "\" "~" :: prf_script_goal % "proof" and - "calc" "print_coercions" :: thy_decl and - "rhs" "def" "vars" :: quasi_command - -begin - -section \Notation\ - -declare [[eta_contract=false]] - -text \ -Rebind notation for meta-lambdas since we want to use \\\ for the object -lambdas. Metafunctions now use the binder \fn\. -\ -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 ("(3%_./ _)", [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 "_app" :: \logic \ logic \ logic\ (infixr "$" 3) -translations "a $ b" \ "a (b)" - -abbreviation (input) K where "K x \ fn _. x" - - -section \Metalogic\ - -text \ -HOAS embedding of dependent type theory: metatype of expressions, and typing -judgment. -\ - -typedecl o - -consts has_type :: \o \ o \ prop\ ("(2_:/ _)" 999) - - -section \Axioms\ - -subsection \Universes\ - -text \\-many cumulative Russell universes.\ - -typedecl lvl - -axiomatization - O :: \lvl\ and - S :: \lvl \ lvl\ and - lt :: \lvl \ lvl \ prop\ (infix "<" 900) - where - O_min: "O < S i" and - lt_S: "i < S i" and - lt_trans: "i < j \ j < k \ i < k" - -axiomatization U :: \lvl \ o\ where - Ui_in_Uj: "i < j \ U i: U j" and - U_cumul: "A: U i \ i < j \ A: U j" - -lemma Ui_in_USi: - "U i: U (S i)" - by (rule Ui_in_Uj, rule lt_S) - -lemma U_lift: - "A: U i \ A: U (S i)" - by (erule U_cumul, rule lt_S) - -subsection \\-type\ - -axiomatization - Pi :: \o \ (o \ o) \ o\ and - lam :: \o \ (o \ o) \ o\ and - app :: \o \ o \ o\ ("(1_ `_)" [120, 121] 120) - -syntax - "_Pi" :: \idts \ o \ o \ o\ ("(2\_: _./ _)" 30) - "_Pi2" :: \idts \ o \ o \ o\ - "_lam" :: \idts \ o \ o \ o\ ("(2\_: _./ _)" 30) - "_lam2" :: \idts \ o \ o \ o\ -translations - "\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 (fn x. b)" - -abbreviation Fn (infixr "\" 40) where "A \ B \ \_: A. B" - -axiomatization where - PiF: "\A: U i; \x. x: A \ B x: U i\ \ \x: A. B x: U i" and - - PiI: "\A: U i; \x. x: A \ b x: B x\ \ \x: A. b x: \x: A. B x" and - - PiE: "\f: \x: A. B x; a: A\ \ f `a: B a" and - - beta: "\a: A; \x. x: A \ b x: B x\ \ (\x: A. b x) `a \ b a" and - - eta: "f: \x: A. B x \ \x: A. f `x \ f" and - - Pi_cong: "\ - \x. x: A \ B x \ B' x; - A: U i; - \x. x: A \ B x: U j; - \x. x: A \ B' x: U j - \ \ \x: A. B x \ \x: A. B' x" and - - lam_cong: "\\x. x: A \ b x \ c x; A: U i\ \ \x: A. b x \ \x: A. c x" - -subsection \\-type\ - -axiomatization - Sig :: \o \ (o \ o) \ o\ and - pair :: \o \ o \ o\ ("(2<_,/ _>)") and - SigInd :: \o \ (o \ o) \ (o \ o) \ (o \ o \ o) \ o \ o\ - -syntax "_Sum" :: \idt \ o \ o \ o\ ("(2\_: _./ _)" 20) - -translations "\x: A. B" \ "CONST Sig A (fn x. B)" - -abbreviation Prod (infixl "\" 60) - where "A \ B \ \_: A. B" - -abbreviation "and" (infixl "\" 60) - where "A \ B \ A \ B" - -axiomatization where - SigF: "\A: U i; \x. x: A \ B x: U i\ \ \x: A. B x: U i" and - - SigI: "\\x. x: A \ B x: U i; a: A; b: B a\ \ : \x: A. B x" and - - SigE: "\ - p: \x: A. B x; - A: U i; - \x. x : A \ B x: U j; - \p. p: \x: A. B x \ C p: U k; - \x y. \x: A; y: B x\ \ f x y: C - \ \ SigInd A (fn x. B x) (fn p. C p) f p: C p" and - - Sig_comp: "\ - a: A; - b: B a; - \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 (fn x. B x) (fn p. C p) f \ f a b" and - - Sig_cong: "\ - \x. x: A \ B x \ B' x; - A: U i; - \x. x : A \ B x: U j; - \x. x : A \ B' x: U j - \ \ \x: A. B x \ \x: A. B' x" - - -section \Type checking & inference\ - -ML_file \lib.ML\ -ML_file \context_facts.ML\ -ML_file \context_tactical.ML\ - -\ \Rule attributes for the typechecker\ -named_theorems form and intr and comp - -\ \Elimination/induction automation and the `elim` attribute\ -ML_file \elimination.ML\ - -lemmas - [form] = PiF SigF and - [intr] = PiI SigI and - [elim ?f] = PiE and - [elim ?p] = SigE and - [comp] = beta Sig_comp and - [cong] = Pi_cong lam_cong Sig_cong - -\ \Subsumption rule\ -lemma sub: - assumes "a: A" "A \ A'" - shows "a: A'" - using assms by simp - -\ \Basic rewriting of computational equality\ -ML_file \~~/src/Tools/misc_legacy.ML\ -ML_file \~~/src/Tools/IsaPlanner/isand.ML\ -ML_file \~~/src/Tools/IsaPlanner/rw_inst.ML\ -ML_file \~~/src/Tools/IsaPlanner/zipper.ML\ -ML_file \~~/src/Tools/eqsubst.ML\ - -\ \Term normalization, type checking & inference\ -ML_file \types.ML\ - -method_setup typechk = - \Scan.succeed (K (CONTEXT_METHOD ( - CHEADGOAL o Types.check_infer)))\ - -method_setup known = - \Scan.succeed (K (CONTEXT_METHOD ( - CHEADGOAL o Types.known_ctac)))\ - -setup \ -let val typechk = fn ctxt => - NO_CONTEXT_TACTIC ctxt o Types.check_infer - (Simplifier.prems_of ctxt @ Context_Facts.known ctxt) -in - map_theory_simpset (fn ctxt => ctxt - addSolver (mk_solver "" typechk)) -end -\ - - -section \Statements and goals\ - -ML_file \focus.ML\ -ML_file \elaboration.ML\ -ML_file \elaborated_statement.ML\ -ML_file \goals.ML\ - - -section \Proof methods\ - -named_theorems intro \ \Logical introduction rules\ - -lemmas [intro] = PiI[rotated] SigI - -\ \Case reasoning rules\ -ML_file \cases.ML\ - -ML_file \tactics.ML\ - -method_setup rule = - \Attrib.thms >> (fn ths => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS 0 (rule_ctac ths))))\ - -method_setup dest = - \Scan.lift (Scan.option (Args.parens Parse.nat)) - -- Attrib.thms >> (fn (n_opt, ths) => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS 0 (dest_ctac n_opt ths))))\ - -method_setup intro = - \Scan.succeed (K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS 0 intro_ctac)))\ - -method_setup intros = - \Scan.lift (Scan.option Parse.nat) >> (fn n_opt => - K (CONTEXT_METHOD (fn facts => - case n_opt of - SOME n => CREPEAT_N n (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts)) - | NONE => CCHANGED (CREPEAT (CCHANGED ( - CHEADGOAL (SIDE_CONDS 0 intro_ctac facts)))))))\ - -method_setup elim = - \Scan.repeat Args.term >> (fn tms => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS 0 (elim_ctac tms))))\ - -method_setup cases = - \Args.term >> (fn tm => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS 0 (cases_ctac tm))))\ - -method elims = elim+ -method facts = fact+ - - -subsection \Reflexivity\ - -named_theorems refl -method refl = (rule refl) - - -subsection \Trivial proofs (modulo automatic discharge of side conditions)\ - -method_setup this = - \Scan.succeed (K (CONTEXT_METHOD (fn facts => - CHEADGOAL (SIDE_CONDS 0 - (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts)) - facts))))\ - - -subsection \Rewriting\ - -consts compute_hole :: "'a::{}" ("\") - -lemma eta_expand: - fixes f :: "'a::{} \ 'b::{}" - shows "f \ fn x. f x" . - -lemma rewr_imp: - assumes "PROP A \ PROP B" - shows "(PROP A \ PROP C) \ (PROP B \ PROP C)" - apply (Pure.rule Pure.equal_intr_rule) - apply (drule equal_elim_rule2[OF assms]; assumption) - apply (drule equal_elim_rule1[OF assms]; assumption) - done - -lemma imp_cong_eq: - "(PROP A \ (PROP B \ PROP C) \ (PROP B' \ PROP C')) \ - ((PROP B \ PROP A \ PROP C) \ (PROP B' \ PROP A \ PROP C'))" - apply (Pure.intro Pure.equal_intr_rule) - apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; - assumption)+ - apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+ - done - -ML_file \~~/src/HOL/Library/cconv.ML\ -ML_file \comp.ML\ - -\ \\compute\ simplifies terms via computational equalities\ -method compute uses add = - changed \repeat_new \(simp add: comp add | subst comp); typechk?\\ - - -subsection \Calculational reasoning\ - -consts "rhs" :: \'a\ ("..") - -ML_file \calc.ML\ - - -section \Implicits\ - -text \ - \{}\ is used to mark implicit arguments in definitions, while \?\ is expanded - immediately for elaboration in statements. -\ - -consts - iarg :: \'a\ ("{}") - hole :: \'b\ ("?") - -ML_file \implicits.ML\ - -attribute_setup implicit = \Scan.succeed Implicits.implicit_defs_attr\ - -ML \val _ = Context.>> (Syntax_Phases.term_check 1 "" Implicits.make_holes)\ - -text \Automatically insert inhabitation judgments where needed:\ - -syntax inhabited :: \o \ prop\ ("(_)") -translations "inhabited A" \ "CONST has_type ? A" - - -subsection \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)" - -translations "\x. b" \ "\x: A. b" - - -section \Lambda coercion\ - -\ \Coerce object lambdas to meta-lambdas\ -abbreviation (input) lambda :: \o \ o \ o\ - where "lambda f \ fn x. f `x" - -ML_file \~~/src/Tools/subtyping.ML\ -declare [[coercion_enabled, coercion lambda]] - -translations "f x" \ "f `x" - - -section \Functions\ - -Lemma eta_exp: - assumes "f: \x: A. B x" - shows "f \ \x: A. f x" - by (rule eta[symmetric]) - -Lemma refine_codomain: - assumes - "A: U i" - "f: \x: A. B x" - "\x. x: A \ f `x: C x" - shows "f: \x: A. C x" - by (comp eta_exp) - -Lemma lift_universe_codomain: - assumes "A: U i" "f: A \ U j" - shows "f: A \ U (S j)" - using U_lift - by (rule refine_codomain) - -subsection \Function composition\ - -definition "funcomp A g f \ \x: A. g `(f `x)" - -syntax - "_funcomp" :: \o \ o \ o \ o\ ("(2_ \\<^bsub>_\<^esub>/ _)" [111, 0, 110] 110) -translations - "g \\<^bsub>A\<^esub> f" \ "CONST funcomp A g f" - -Lemma funcompI [type]: - assumes - "A: U i" - "B: U i" - "\x. x: B \ C x: U i" - "f: A \ B" - "g: \x: B. C x" - shows - "g \\<^bsub>A\<^esub> f: \x: A. C (f x)" - unfolding funcomp_def by typechk - -Lemma funcomp_assoc [comp]: - assumes - "A: U i" - "f: A \ B" - "g: B \ C" - "h: \x: C. D x" - shows - "(h \\<^bsub>B\<^esub> g) \\<^bsub>A\<^esub> f \ h \\<^bsub>A\<^esub> g \\<^bsub>A\<^esub> f" - unfolding funcomp_def by compute - -Lemma funcomp_lambda_comp [comp]: - assumes - "A: U i" - "\x. x: A \ b x: B" - "\x. x: B \ c x: C x" - shows - "(\x: B. c x) \\<^bsub>A\<^esub> (\x: A. b x) \ \x: A. c (b x)" - unfolding funcomp_def by compute - -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" - shows "(g \\<^bsub>A\<^esub> f) x \ g (f x)" - unfolding funcomp_def by compute - -subsection \Notation\ - -definition funcomp_i (infixr "\" 120) - where [implicit]: "funcomp_i g f \ g \\<^bsub>{}\<^esub> f" - -translations "g \ f" \ "g \\<^bsub>A\<^esub> f" - -subsection \Identity function\ - -abbreviation id where "id A \ \x: A. x" - -lemma - id_type [type]: "A: U i \ id A: A \ A" and - id_comp [comp]: "x: A \ (id A) x \ x" \ \for the occasional manual rewrite\ - by compute+ - -Lemma id_left [comp]: - assumes "A: U i" "B: U i" "f: A \ B" - shows "(id B) \\<^bsub>A\<^esub> f \ f" - by (comp eta_exp[of f]) (compute, rule eta) - -Lemma id_right [comp]: - assumes "A: U i" "B: U i" "f: A \ B" - shows "f \\<^bsub>A\<^esub> (id A) \ f" - by (comp eta_exp[of f]) (compute, rule eta) - -lemma id_U [type]: - "id (U i): U i \ U i" - using Ui_in_USi by typechk - - -section \Pairs\ - -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 [type]: - assumes "A: U i" "\x. x: A \ B x: U i" - shows "fst A B: (\x: A. B x) \ A" - unfolding fst_def by typechk - -Lemma fst_comp [comp]: - assumes - "A: U i" "\x. x: A \ B x: U i" "a: A" "b: B a" - shows "fst A B \ a" - unfolding fst_def by compute - -Lemma snd_type [type]: - assumes "A: U i" "\x. x: A \ B x: U i" - shows "snd A B: \p: \x: A. B x. B (fst A B p)" - unfolding snd_def by typechk - -Lemma snd_comp [comp]: - assumes "A: U i" "\x. x: A \ B x: U i" "a: A" "b: B a" - shows "snd A B \ b" - unfolding snd_def by compute - -subsection \Notation\ - -definition fst_i ("fst") - where [implicit]: "fst \ Spartan.fst {} {}" - -definition snd_i ("snd") - where [implicit]: "snd \ Spartan.snd {} {}" - -translations - "fst" \ "CONST Spartan.fst A B" - "snd" \ "CONST Spartan.snd A B" - -subsection \Projections\ - -Lemma fst [type]: - assumes - "A: U i" "\x. x: A \ B x: U i" - "p: \x: A. B x" - shows "fst p: A" - by typechk - -Lemma snd [type]: - assumes - "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[where ?p=p] -method snd for p::o = rule snd[where ?p=p] - -text \Double projections:\ - -definition [implicit]: "p\<^sub>1\<^sub>1 p \ Spartan.fst {} {} (Spartan.fst {} {} p)" -definition [implicit]: "p\<^sub>1\<^sub>2 p \ Spartan.snd {} {} (Spartan.fst {} {} p)" -definition [implicit]: "p\<^sub>2\<^sub>1 p \ Spartan.fst {} {} (Spartan.snd {} {} p)" -definition [implicit]: "p\<^sub>2\<^sub>2 p \ Spartan.snd {} {} (Spartan.snd {} {} p)" - -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 - "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 - - -end -- cgit v1.2.3