diff options
author | Josh Chen | 2019-02-22 23:45:50 +0100 |
---|---|---|
committer | Josh Chen | 2019-02-22 23:45:50 +0100 |
commit | 57d183c7955fb54b3eb6dd431f5aec338131266b (patch) | |
tree | ae6bfabbd8fcd63ee7d5140ca842599efbd58c16 /Prod.thy | |
parent | 0036345412d5c145b63693ed672b175018fa3791 (diff) |
Cleanups and reorganization
Diffstat (limited to '')
-rw-r--r-- | Prod.thy | 34 |
1 files changed, 17 insertions, 17 deletions
@@ -70,23 +70,6 @@ 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_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"}. - -Method @{theory_text "quantify k"} does the same, but only for the first k unknowns. -\<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> definition compose :: "[t, t, t] \<Rightarrow> t" @@ -146,4 +129,21 @@ by (derive lems: assms cong) abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> \<lambda>x: A. x" + +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_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"}. + +Method @{theory_text "quantify k"} does the same, but only for the first k unknowns. +\<close> + +method quantify_all = (rule Prod_intro)+ +method_setup quantify = \<open>repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\<close> + end |