From c2dfffffb7586662c67e44a2d255a1a97ab0398b Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 2 Apr 2020 17:57:48 +0200 Subject: Brand-spanking new version using Spartan infrastructure --- Prod.thy | 169 --------------------------------------------------------------- 1 file changed, 169 deletions(-) delete mode 100644 Prod.thy (limited to 'Prod.thy') diff --git a/Prod.thy b/Prod.thy deleted file mode 100644 index a35138c..0000000 --- a/Prod.thy +++ /dev/null @@ -1,169 +0,0 @@ -(******** -Isabelle/HoTT: Dependent product (dependent function) -Feb 2019 - -********) - -theory Prod -imports HoTT_Base HoTT_Methods - -begin - - -section \Basic type definitions\ - -axiomatization - Prod :: "[t, t \ t] \ t" and - lam :: "[t, t \ t] \ t" and - app :: "[t, t] \ t" ("(2_`/_)" [120, 121] 120) - \ \Application should bind tighter than abstraction.\ - -syntax - "_Prod" :: "[idt, t, t] \ t" ("(2\'(_: _')./ _)" 30) - "_Prod'" :: "[idt, t, t] \ t" ("(2\_: _./ _)" 30) - "_lam" :: "[idt, t, t] \ t" ("(2\'(_: _')./ _)" 30) - "_lam'" :: "[idt, t, t] \ t" ("(2\_: _./ _)" 30) -translations - "\x: A. B" \ "(CONST Prod) A (\x. B)" - "\(x: A). B" \ "(CONST Prod) A (\x. B)" - "\(x: A). b" \ "(CONST lam) A (\x. b)" - "\x: A. b" \ "(CONST lam) A (\x. b)" - -text \ -The syntax translations above bind the variable @{term x} in the expressions @{term B} and @{term b}. -\ - -text \Non-dependent functions are a special case:\ - -abbreviation Fun :: "[t, t] \ t" (infixr "\" 40) -where "A \ B \ \_: A. B" - -axiomatization where -\ \Type rules\ - - Prod_form: "\A: U i; B: A \ U i\ \ \x: A. B x: U i" and - - Prod_intro: "\\x. x: A \ b x: B x; A: U i\ \ \x: A. b x: \x: A. B x" and - - Prod_elim: "\f: \x: A. B x; a: A\ \ f`a: B a" and - - Prod_cmp: "\\x. x: A \ b x: B x; a: A\ \ (\x: A. b x)`a \ b a" and - - Prod_uniq: "f: \x: A. B x \ \x: A. f`x \ f" and - -\ \Congruence rules\ - - Prod_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" and - - Prod_intro_eq: "\\x. x: A \ b x \ c x; A: U i\ \ \x: A. b x \ \x: A. c x" - -text \ -The Pure rules for \\\ only let us judge strict syntactic equality of object lambda expressions. -The actual definitional equality rule in the type theory is @{thm Prod_intro_eq}. -Note that this is a separate rule from function extensionality. -\ - -lemmas Prod_form [form] -lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim -lemmas Prod_comp [comp] = Prod_cmp Prod_uniq -lemmas Prod_cong [cong] = Prod_form_eq Prod_intro_eq - - -section \Function composition\ - -definition compose :: "[t, t, t] \ t" -where "compose A g f \ \x: A. g`(f`x)" - -syntax "_compose" :: "[t, t, t] \ t" ("(2_ o[_]/ _)" [111, 0, 110] 110) -translations "g o[A] f" \ "(CONST compose) A g f" - -text \The composition @{term "g o[A] f"} is annotated with the domain @{term A} of @{term f}.\ - -syntax "_compose'" :: "[t, t] \ t" (infixr "o" 110) - -text \Pretty-printing switch for composition; hides domain type information.\ - -ML \val pretty_compose = Attrib.setup_config_bool @{binding "pretty_compose"} (K true)\ - -print_translation \ -let fun compose_tr' ctxt [A, g, f] = - if Config.get ctxt pretty_compose - then Syntax.const @{syntax_const "_compose'"} $ g $ f - else @{const compose} $ A $ g $ f -in - [(@{const_syntax compose}, compose_tr')] -end -\ - -lemma compose_type: - assumes - "A: U i" and "B: U i" and "C: B \ U i" and - "f: A \ B" and "g: \x: B. C x" - shows "g o[A] f: \x: A. C (f`x)" -unfolding compose_def by (derive lems: assms) - -lemma compose_comp: - assumes "A: U i" and "\x. x: A \ b x: B" and "\x. x: B \ c x: C x" - shows "(\x: B. c x) o[A] (\x: A. b x) \ \x: A. c (b x)" -unfolding compose_def by (derive lems: assms cong) - -declare - compose_type [intro] - compose_comp [comp] - -lemma compose_assoc: - assumes "A: U i" and "f: A \ B" and "g: B \ C" and "h: \x: C. D x" - shows "(h o[B] g) o[A] f \ h o[A] g o[A] f" -unfolding compose_def by (derive lems: assms cong) - -abbreviation id :: "t \ t" ("(id _)" [115] 114) where "id A \ \x: A. x" - -lemma id_type: "\A. A: U i \ id A: A \ A" by derive - -lemma id_compl: - assumes [intro]: "A: U i" "B: U i" "f: A \ B" - shows "id B o[A] f \ f" -unfolding compose_def proof - - { - fix x assume [intro]: "x: A" - have "(id B)`(f`x) \ f`x" by derive - } - hence "\x: A. (id B)`(f`x) \ \x: A. f`x" by (derive lems: cong) derive - also have "\x: A. f`x \ f" by derive - finally show "\(x: A). (id B)`(f`x) \ f" by simp -qed - -lemma id_compr: - assumes [intro]: "A: U i" "B: U i" "f: A \ B" - shows "f o[A] id A \ f" -unfolding compose_def proof - - { - fix x assume [intro]: "x: A" - have "f`((id A)`x) \ f`x" by derive - } - hence "\x: A. f`((id A)`x) \ \x: A. f`x" by (derive lems: cong) derive - also have "\x: A. f`x \ f" by derive - finally show "\x: A. f`((id A)`x) \ f" by simp -qed - -declare id_type [intro] -lemmas id_comp [comp] = id_compl id_compr - -section \Universal quantification\ - -text \ -It will often be useful to convert a proof goal asserting the inhabitation of a dependent product to one that instead uses Pure universal quantification. - -Method @{theory_text quantify_all} converts the goal -@{text "t: \x1: A1. ... \xn: An. B x1 ... xn"}, -where @{term B} is not a product, to -@{text "\x1 ... xn . \x1: A1; ...; xn: An\ \ ?b x1 ... xn: B x1 ... xn"}. - -Method @{theory_text "quantify k"} does the same, but only for the first k unknowns. -\ - -method quantify_all = (rule Prod_intro)+ -method_setup quantify = \repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\ - -end -- cgit v1.2.3