From 76ac8ed82317f3f62f26ecc88f412c61004bcffa Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 17 Sep 2018 13:13:55 +0200 Subject: Reorganizing theories --- Coprod.thy | 64 +++++++++++++++++++++----------------------------------- Empty.thy | 22 ++++++++----------- HoTT.thy | 2 +- HoTT_Base.thy | 25 ++++++++++++---------- HoTT_Methods.thy | 56 +++++++++++++++++++------------------------------ Nat.thy | 60 ++++++++++++++++++++++++---------------------------- Proj.thy | 56 ++++++++++++++++++------------------------------- Sum.thy | 57 ++++++++++++++++++++----------------------------- Unit.thy | 32 +++++++++++++--------------- 9 files changed, 155 insertions(+), 219 deletions(-) diff --git a/Coprod.thy b/Coprod.thy index 97e0566..d97228e 100644 --- a/Coprod.thy +++ b/Coprod.thy @@ -1,65 +1,49 @@ -(* Title: HoTT/Coprod.thy - Author: Josh Chen +(* +Title: Coprod.thy +Author: Joshua Chen +Date: 2018 Coproduct type *) theory Coprod - imports HoTT_Base -begin +imports HoTT_Base +begin -section \Constants and type rules\ axiomatization - Coprod :: "[t, t] \ t" (infixr "+" 50) and - inl :: "t \ t" and - inr :: "t \ t" and + Coprod :: "[t, t] \ t" (infixr "+" 50) and + inl :: "t \ t" and + inr :: "t \ t" and indCoprod :: "[t \ t, t \ t, t] \ t" ("(1ind\<^sub>+)") where - Coprod_form: "\A: U i; B: U i\ \ A + B: U i" -and - Coprod_intro_inl: "\a: A; B: U i\ \ inl a: A + B" -and - Coprod_intro_inr: "\b: B; A: U i\ \ inr b: A + B" -and + Coprod_form: "\A: U i; B: U i\ \ A + B: U i" and + + Coprod_intro_inl: "\a: A; B: U i\ \ inl a: A + B" and + + Coprod_intro_inr: "\b: B; A: U i\ \ inr b: A + B" and + Coprod_elim: "\ + u: A + B; C: A + B \ U i; \x. x: A \ c x: C (inl x); - \y. y: B \ d y: C (inr y); - u: A + B - \ \ ind\<^sub>+ c d u: C u" -and + \y. y: B \ d y: C (inr y) \ \ ind\<^sub>+ (\ x. c x) (\y. d y) u: C u" and + Coprod_comp_inl: "\ + a: A; C: A + B \ U i; \x. x: A \ c x: C (inl x); - \y. y: B \ d y: C (inr y); - a: A - \ \ ind\<^sub>+ c d (inl a) \ c a" -and + \y. y: B \ d y: C (inr y) \ \ ind\<^sub>+ (\x. c x) (\y. d y) (inl a) \ c a" and + Coprod_comp_inr: "\ + b: B; C: A + B \ U i; \x. x: A \ c x: C (inl x); - \y. y: B \ d y: C (inr y); - b: B - \ \ ind\<^sub>+ c d (inr b) \ d b" - - -text "Admissible formation inference rules:" - -axiomatization where - Coprod_wellform1: "A + B: U i \ A: U i" -and - Coprod_wellform2: "A + B: U i \ B: U i" - - -text "Rule attribute declarations:" - -lemmas Coprod_intro = Coprod_intro_inl Coprod_intro_inr + \y. y: B \ d y: C (inr y) \ \ ind\<^sub>+ (\x. c x) (\y. d y) (inr b) \ d b" +lemmas Coprod_routine [intro] = Coprod_form Coprod_intro_inl Coprod_intro_inr Coprod_elim lemmas Coprod_comp [comp] = Coprod_comp_inl Coprod_comp_inr -lemmas Coprod_wellform [wellform] = Coprod_wellform1 Coprod_wellform2 -lemmas Coprod_routine [intro] = Coprod_form Coprod_intro Coprod_elim end diff --git a/Empty.thy b/Empty.thy index 107f2d7..3060867 100644 --- a/Empty.thy +++ b/Empty.thy @@ -1,28 +1,24 @@ -(* Title: HoTT/Empty.thy - Author: Josh Chen +(* +Title: Empty.thy +Author: Joshua Chen +Date: 2018 Empty type *) theory Empty - imports HoTT_Base -begin - +imports HoTT_Base -section \Constants and type rules\ +begin -section \Empty type\ axiomatization - Empty :: t ("\") and + Empty :: t ("\") and indEmpty :: "t \ t" ("(1ind\<^sub>\)") where - Empty_form: "\: U O" -and - Empty_elim: "\C: \ \ U i; z: \\ \ ind\<^sub>\ z: C z" - + Empty_form: "\: U O" and -text "Rule attribute declarations:" + Empty_elim: "\a: \; C: \ \ U i\ \ ind\<^sub>\ a: C a" lemmas Empty_routine [intro] = Empty_form Empty_elim diff --git a/HoTT.thy b/HoTT.thy index abb1085..3f2d475 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -30,7 +30,7 @@ begin lemmas forms = Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form lemmas intros = - Nat_intro Prod_intro Sum_intro Equal_intro Coprod_intro Unit_intro + Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Equal_intro Coprod_intro_inl Coprod_intro_inr Unit_intro lemmas elims = Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim lemmas routines = diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 07fbfc4..efc6182 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,7 +1,9 @@ -(* Title: HoTT/HoTT_Base.thy - Author: Joshua Chen +(* +Title: HoTT_Base.thy +Author: Joshua Chen +Date: 2018 -Basic setup of a homotopy type theory object logic with a Russell-style cumulative universe hierarchy. +Basic setup of a homotopy type theory object logic with a cumulative Russell-style universe hierarchy. *) theory HoTT_Base @@ -49,8 +51,8 @@ Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blind One should instead use @{method elim}, or instantiate @{thm U_cumulative} suitably. \ -method cumulativity = (elim U_cumulative, proveSuc) \ \Proves \A: U i \ A: U (Suc (... (Suc i) ...))\.\ -method hierarchy = (rule U_hierarchy, proveSuc) \ \Proves \U i: U (Suc (... (Suc i) ...)).\\ +method cumulativity = (elim U_cumulative, proveSuc) \ \Proves \A: U i \ A: U (Suc (... (Suc i) ...))\\ +method hierarchy = (rule U_hierarchy, proveSuc) \ \Proves \U i: U (Suc (... (Suc i) ...))\\ section \Type families\ @@ -59,22 +61,23 @@ abbreviation (input) constrained :: "[t \ t, t, t] \ pro where "f: A \ B \ (\x. x : A \ f x: B)" text \ -The abbreviation @{abbrev constrained} is used to define type families, which are constrained expressions @{term "P: A \ B"} where @{term "A::t"} and @{term "B::t"} are small types. +The abbreviation @{abbrev constrained} is used to define type families, which are constrained expressions @{term "P: A \ B"}, where @{term "A::t"} and @{term "B::t"} are small types. \ -type_synonym tf = "t \ t" \ \Type of type families.\ +type_synonym tf = "t \ t" \ \Type of type families\ section \Named theorems\ +named_theorems comp + text \ Declare named theorems to be used by proof methods defined in @{file HoTT_Methods.thy}. -\wellform\ declares necessary well-formedness conditions for type and inhabitation judgments. -\comp\ declares computation rules, which are usually passed to invocations of the method \subst\ to perform equational rewriting. +@{attribute comp} declares computation rules. +These are used by the \compute\ method, and may also be passed to invocations of the method \subst\ to perform equational rewriting. \ -named_theorems wellform -named_theorems comp +(* Todo: Set up the simplifier! *) end diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index abb6dda..9849195 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -1,63 +1,51 @@ -(* Title: HoTT/HoTT_Methods.thy - Author: Josh Chen +(* +Title: HoTT_Methods.thy +Author: Joshua Chen +Date: 2018 -Method setup for the HoTT library. Relies heavily on Eisbach. +Method setup for the HoTT logic. Relies heavily on Eisbach. *) theory HoTT_Methods - imports - "HOL-Eisbach.Eisbach" - "HOL-Eisbach.Eisbach_Tools" - HoTT_Base +imports + "HOL-Eisbach.Eisbach" + "HOL-Eisbach.Eisbach_Tools" + HoTT_Base + begin section \Deriving typing judgments\ -method routine uses lems = (assumption | rule lems | standard)+ - -text " - @{method routine} proves routine type judgments \a : A\ using the rules declared [intro] in the respective theory files, as well as additional provided lemmas. -" - -text " - \wellformed'\ finds a proof of any valid typing judgment derivable from the judgment passed as \jdmt\. - If no judgment is passed, it will try to resolve with the theorems declared \wellform\. - \wellform\ is like \wellformed'\ but takes multiple judgments. - - The named theorem \wellform\ is declared in HoTT_Base.thy. -" +method routine uses add = (assumption | rule add | rule)+ -method wellformed' uses jdmt declares wellform = - match wellform in rl: "PROP ?P" \ \( - catch \rule rl[OF jdmt]\ \fail\ | - catch \wellformed' jdmt: rl[OF jdmt]\ \fail\ - )\ - -method wellformed uses lems = - match lems in lem: "?X : ?Y" \ \wellformed' jdmt: lem\ +text \ +The method @{method routine} proves type judgments @{prop "a : A"} using the rules declared @{attribute intro} in the respective theory files, as well as additional provided lemmas passed using the modifier \add\. +\ section \Substitution and simplification\ -text "Import the \subst\ method, used for substituting definitional equalities." - 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" -text "Perform basic single-step computations:" +\ \Import the @{method subst} method, used for substituting definitional equalities.\ -method compute uses lems = (subst lems comp | rule lems comp) +method compute declares comp = (subst comp) +text \ +Method @{method compute} performs single-step simplifications, using any rules declared @{attribute comp} in the context. +Premises of the rule(s) applied are added as new subgoals. +\ section \Derivation search\ -text " Combine \routine\, \wellformed\, and \compute\ to search for derivations of judgments." +text \Combine @{method routine} and @{method compute} to search for derivations of judgments.\ -method derive uses lems = (routine lems: lems | compute lems: lems | wellformed lems: lems)+ +method derive uses lems = (routine add: lems | compute comp: lems)+ section \Induction\ diff --git a/Nat.thy b/Nat.thy index a82e7cb..46b1af5 100644 --- a/Nat.thy +++ b/Nat.thy @@ -1,54 +1,48 @@ -(* Title: HoTT/Nat.thy - Author: Josh Chen +(* +Title: Nat.thy +Author: Joshua Chen +Date: 2018 Natural numbers *) theory Nat - imports HoTT_Base -begin +imports HoTT_Base +begin -section \Constants and type rules\ axiomatization - Nat :: t ("\") and - zero :: t ("0") and - succ :: "t \ t" and + Nat :: t ("\") and + zero :: t ("0") and + succ :: "t \ t" and indNat :: "[[t, t] \ t, t, t] \ t" ("(1ind\<^sub>\)") where - Nat_form: "\: U O" -and - Nat_intro_0: "0: \" -and - Nat_intro_succ: "n: \ \ succ n: \" -and + Nat_form: "\: U O" and + + Nat_intro_0: "0: \" and + + Nat_intro_succ: "n: \ \ succ n: \" and + Nat_elim: "\ - C: \ \ U i; - \n c. \n: \; c: C n\ \ f n c: C (succ n); a: C 0; - n: \ - \ \ ind\<^sub>\ f a n: C n" -and + n: \; + C: \ \ U i; + \n c. \n: \; c: C n\ \ f n c: C (succ n) \ \ ind\<^sub>\ (\n c. f n c) a n: C n" and + Nat_comp_0: "\ + a: C 0; C: \ \ U i; - \n c. \n: \; c: C(n)\ \ f n c: C (succ n); - a: C 0 - \ \ ind\<^sub>\ f a 0 \ a" -and + \n c. \n: \; c: C(n)\ \ f n c: C (succ n) \ \ ind\<^sub>\ (\n c. f n c) a 0 \ a" and + Nat_comp_succ: "\ - C: \ \ U i; - \n c. \n: \; c: C n\ \ f n c: C (succ n); a: C 0; - n: \ - \ \ ind\<^sub>\ f a (succ n) \ f n (ind\<^sub>\ f a n)" - - -text "Rule attribute declarations:" + n: \; + C: \ \ U i; + \n c. \n: \; c: C n\ \ f n c: C (succ n) \ \ ind\<^sub>\ (\n c. f n c) a (succ n) \ f n (ind\<^sub>\ f a n)" -lemmas Nat_intro = Nat_intro_0 Nat_intro_succ -lemmas Nat_comp [comp] = Nat_comp_0 Nat_comp_succ -lemmas Nat_routine [intro] = Nat_form Nat_intro Nat_elim +lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim +lemmas Nat_comps [comp] = Nat_comp_0 Nat_comp_succ end diff --git a/Proj.thy b/Proj.thy index 74c561c..f272224 100644 --- a/Proj.thy +++ b/Proj.thy @@ -1,62 +1,46 @@ -(* Title: HoTT/Proj.thy - Author: Josh Chen +(* +Title: Proj.thy +Author: Joshua Chen +Date: 2018 Projection functions \fst\ and \snd\ for the dependent sum type. *) theory Proj - imports - HoTT_Methods - Prod - Sum -begin +imports + HoTT_Methods + Prod + Sum +begin -definition fst :: "Term \ Term" where "fst p \ ind\<^sub>\ (\x y. x) p" -definition snd :: "Term \ Term" where "snd p \ ind\<^sub>\ (\x y. y) p" -text "Typing judgments and computation rules for the dependent and non-dependent projection functions." +definition fst :: "t \ t" where "fst p \ ind\<^sub>\ (\x y. x) p" +definition snd :: "t \ t" where "snd p \ ind\<^sub>\ (\x y. y) p" lemma fst_type: - assumes "\x:A. B x: U i" and "p: \x:A. B x" shows "fst p: A" + assumes "A: U i" and "B: A \ U i" and "p: \x:A. B x" shows "fst p: A" unfolding fst_def by (derive lems: assms) lemma fst_comp: assumes "A: U i" and "B: A \ U i" and "a: A" and "b: B a" shows "fst \ a" -unfolding fst_def -proof compute - show "a: A" and "b: B a" by fact+ -qed (routine lems: assms)+ +unfolding fst_def by compute (derive lems: assms) lemma snd_type: - assumes "\x:A. B x: U i" and "p: \x:A. B x" shows "snd p: B (fst p)" -unfolding snd_def -proof + assumes "A: U i" and "B: A \ U i" and "p: \x:A. B x" shows "snd p: B (fst p)" +unfolding snd_def proof show "\p. p: \x:A. B x \ B (fst p): U i" by (derive lems: assms fst_type) - fix x y - assume asm: "x: A" "y: B x" - show "y: B (fst )" - proof (subst fst_comp) - show "A: U i" by (wellformed lems: assms(1)) - show "\x. x: A \ B x: U i" by (wellformed lems: assms(1)) - qed fact+ + fix x y assume asm: "x: A" "y: B x" + show "y: B (fst )" by (derive lems: asm assms fst_comp) qed fact lemma snd_comp: assumes "A: U i" and "B: A \ U i" and "a: A" and "b: B a" shows "snd \ b" -unfolding snd_def -proof compute - show "\x y. y: B x \ y: B x" . - show "a: A" by fact - show "b: B a" by fact -qed (routine lems: assms) - - -text "Rule attribute declarations:" +unfolding snd_def by (derive lems: assms) -lemmas Proj_type [intro] = fst_type snd_type -lemmas Proj_comp [comp] = fst_comp snd_comp +lemmas Proj_types [intro] = fst_type snd_type +lemmas Proj_comps [comp] = fst_comp snd_comp end diff --git a/Sum.thy b/Sum.thy index 92375b9..422e01b 100644 --- a/Sum.thy +++ b/Sum.thy @@ -1,69 +1,58 @@ -(* Title: HoTT/Sum.thy - Author: Josh Chen +(* +Title: Sum.thy +Author: Joshua Chen +Date: 2018 Dependent sum type *) theory Sum - imports HoTT_Base -begin +imports HoTT_Base +begin -section \Constants and syntax\ axiomatization - Sum :: "[t, Typefam] \ t" and - pair :: "[t, t] \ t" ("(1<_,/ _>)") and + Sum :: "[t, tf] \ t" and + pair :: "[t, t] \ t" ("(1<_,/ _>)") and indSum :: "[[t, t] \ t, t] \ t" ("(1ind\<^sub>\)") syntax - "_SUM" :: "[idt, t, t] \ t" ("(3\_:_./ _)" 20) - "_SUM_ASCII" :: "[idt, t, t] \ t" ("(3SUM _:_./ _)" 20) + "_sum" :: "[idt, t, t] \ t" ("(3\_:_./ _)" 20) + "_sum_ascii" :: "[idt, t, t] \ t" ("(3SUM _:_./ _)" 20) translations "\x:A. B" \ "CONST Sum A (\x. B)" "SUM x:A. B" \ "CONST Sum A (\x. B)" -text "Nondependent pair." - abbreviation Pair :: "[t, t] \ t" (infixr "\" 50) where "A \ B \ \_:A. B" +axiomatization where +\ \Type rules\ -section \Type rules\ + Sum_form: "\A: U i; B: A \ U i\ \ \x:A. B x: U i" and + + Sum_intro: "\B: A \ U i; a: A; b: B a\ \ : \x:A. B x" and -axiomatization where - Sum_form: "\A: U i; B: A \ U i\ \ \x:A. B x: U i" -and - Sum_intro: "\B: A \ U i; a: A; b: B a\ \ : \x:A. B x" -and Sum_elim: "\ p: \x:A. B x; - \x y. \x: A; y: B x\ \ f x y: C ; - C: \x:A. B x \ U i - \ \ ind\<^sub>\ f p: C p" (* What does writing \x y. f(x, y) change? *) -and + C: \x:A. B x \ U i; + \x y. \x: A; y: B x\ \ f x y: C \ \ ind\<^sub>\ (\x y. f x y) p: C p" and + Sum_comp: "\ a: A; b: B a; - \x y. \x: A; y: B(x)\ \ f x y: C ; B: A \ U i; - C: \x:A. B x \ U i - \ \ ind\<^sub>\ f \ f a b" - -text "Admissible inference rules for sum formation:" - -axiomatization where - Sum_wellform1: "(\x:A. B x: U i) \ A: U i" -and - Sum_wellform2: "(\x:A. B x: U i) \ B: A \ U i" + C: \x:A. B x \ U i; + \x y. \x: A; y: B(x)\ \ f x y: C \ \ ind\<^sub>\ (\x y. f x y) \ f a b" and +\ \Congruence rules\ -text "Rule attribute declarations:" + Sum_form_eq: "\A: U i; B: A \ U i; C: A \ U i; \x. x: A \ B x \ C x\ \ \x:A. B x \ \x:A. C x" -lemmas Sum_comp [comp] -lemmas Sum_wellform [wellform] = Sum_wellform1 Sum_wellform2 lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim +lemmas Sum_comp [comp] end diff --git a/Unit.thy b/Unit.thy index 6760f27..61c6439 100644 --- a/Unit.thy +++ b/Unit.thy @@ -1,33 +1,31 @@ -(* Title: HoTT/Unit.thy - Author: Josh Chen +(* +Title: Unit.thy +Author: Joshua Chen +Date: 2018 Unit type *) theory Unit - imports HoTT_Base -begin +imports HoTT_Base +begin -section \Constants and type rules\ axiomatization - Unit :: Term ("\") and - pt :: Term ("\") and - indUnit :: "[Term, Term] \ Term" ("(1ind\<^sub>\)") + Unit :: t ("\") and + pt :: t ("\") and + indUnit :: "[t, t] \ t" ("(1ind\<^sub>\)") where - Unit_form: "\: U O" -and - Unit_intro: "\: \" -and - Unit_elim: "\C: \ \ U i; c: C \; a: \\ \ ind\<^sub>\ c a: C a" -and - Unit_comp: "\C: \ \ U i; c: C \\ \ ind\<^sub>\ c \ \ c" + Unit_form: "\: U O" and + Unit_intro: "\: \" and -text "Rule attribute declarations:" + Unit_elim: "\a: \; c: C \; C: \ \ U i\ \ ind\<^sub>\ c a: C a" and + + Unit_comp: "\c: C \; C: \ \ U i\ \ ind\<^sub>\ c \ \ c" -lemmas Unit_comp [comp] lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim +lemmas Unit_comp [comp] end -- cgit v1.2.3