diff options
| author | Josh Chen | 2019-02-17 23:13:57 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-02-17 23:13:57 +0100 |
| commit | ff95b7b5113121d06662ed1508e90fadeb05c161 (patch) | |
| tree | 69f64da36acfe279f3353bb937eb269575a14f9f | |
| parent | 68aa069172933b875d70a5ef71e9db0ae685a92d (diff) | |
finalize quantify methods
| -rw-r--r-- | Prod.thy | 5 |
1 files changed, 2 insertions, 3 deletions
@@ -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> |