From 68aa069172933b875d70a5ef71e9db0ae685a92d Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 17 Feb 2019 18:34:38 +0100
Subject: Method "quantify" converts product inhabitation into Pure universal
 statements. Also misc. cleanups.

---
 Prod.thy | 28 +++++++++++++++++++++++++---
 1 file changed, 25 insertions(+), 3 deletions(-)

(limited to 'Prod.thy')

diff --git a/Prod.thy b/Prod.thy
index 4235793..a843c7a 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -9,6 +9,7 @@ imports HoTT_Base HoTT_Methods
 
 begin
 
+
 section \<open>Basic type definitions\<close>
 
 axiomatization
@@ -35,14 +36,14 @@ The syntax translations above bind the variable @{term x} in the expressions @{t
 text \<open>Non-dependent functions are a special case:\<close>
 
 abbreviation Fun :: "[t, t] \<Rightarrow> t"  (infixr "\<rightarrow>" 40)
-where "A \<rightarrow> B \<equiv> \<Prod>(_: A). B"
+where "A \<rightarrow> B \<equiv> \<Prod>_: A. B"
 
 axiomatization where
 \<comment> \<open>Type rules\<close>
 
   Prod_form: "\<lbrakk>A: U i; B: A \<leadsto> U i\<rbrakk> \<Longrightarrow> \<Prod>x: A. B x: U i" and
 
-  Prod_intro: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> b x: B x\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x: \<Prod>x: A. B x" and
+  Prod_intro: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; A: U i\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x: \<Prod>x: A. B x" and
 
   Prod_elim: "\<lbrakk>f: \<Prod>x: A. B x; a: A\<rbrakk> \<Longrightarrow> f`a: B a" and
 
@@ -68,6 +69,25 @@ 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 \<open>Universal quantification\<close>
+
+text \<open>
+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} converts the goal
+@{text "t: \<Prod>x1: A1. ... \<Prod>xn: An. B x1 ... xn"},
+where @{term B} is not a product, to
+@{text "\<And>x1 ... xn . \<lbrakk>x1: A1; ...; xn: An\<rbrakk> \<Longrightarrow> ?b x1 ... xn: B x1 ... xn"}.
+
+Method @{theory_text "quantify k"} does the same, but only for the first k unknowns.
+\<close>
+
+method_setup quantify = \<open>repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\<close>
+
+method quantify_all = (rule Prod_intro)+
+
+
 section \<open>Function composition\<close>
 
 definition compose :: "[t, t, t] \<Rightarrow> t"
@@ -76,6 +96,7 @@ where "compose A g f \<equiv> \<lambda>x: A. g`(f`x)"
 declare compose_def [comp]
 
 syntax "_compose" :: "[t, t] \<Rightarrow> t"  (infixr "o" 110)
+(*
 parse_translation \<open>
 let fun compose_tr ctxt [g, f] =
   let
@@ -98,6 +119,7 @@ in
   [("_compose", compose_tr)]
 end
 \<close>
+*)
 
 text \<open>Pretty-printing switch for composition; hides domain type information.\<close>
 
@@ -120,7 +142,7 @@ by (derive lems: assms cong)
 
 lemma compose_comp:
   assumes "A: U i" and "\<And>x. x: A \<Longrightarrow> b x: B" and "\<And>x. x: B \<Longrightarrow> c x: C x"
-  shows "(\<lambda>x: B. c x) o (\<lambda>x: A. b x) \<equiv> \<lambda>x: A. c (b x)"
+  shows "compose A (\<lambda>x: B. c x) (\<lambda>x: A. b x) \<equiv> \<lambda>x: A. c (b x)"
 by (derive lems: assms cong)
 
 abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> \<lambda>x: A. x"
-- 
cgit v1.2.3