aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2019-02-17 23:13:57 +0100
committerJosh Chen2019-02-17 23:13:57 +0100
commitff95b7b5113121d06662ed1508e90fadeb05c161 (patch)
tree69f64da36acfe279f3353bb937eb269575a14f9f
parent68aa069172933b875d70a5ef71e9db0ae685a92d (diff)
finalize quantify methods
-rw-r--r--Prod.thy5
1 files changed, 2 insertions, 3 deletions
diff --git a/Prod.thy b/Prod.thy
index a843c7a..ff62ee6 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -75,7 +75,7 @@ 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
+Method @{theory_text quantify_all} 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"}.
@@ -83,9 +83,8 @@ where @{term B} is not a product, to
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)+
+method_setup quantify = \<open>repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\<close>
section \<open>Function composition\<close>