diff options
Diffstat (limited to 'Prod.thy')
| -rw-r--r-- | Prod.thy | 18 |
1 files changed, 9 insertions, 9 deletions
@@ -12,14 +12,14 @@ begin section \<open>Constants and syntax\<close> axiomatization - Prod :: "[Term, Typefam] \<Rightarrow> Term" and - lambda :: "(Term \<Rightarrow> Term) \<Rightarrow> Term" (binder "\<^bold>\<lambda>" 30) and - appl :: "[Term, Term] \<Rightarrow> Term" (infixl "`" 60) + Prod :: "[t, tf] \<Rightarrow> t" and + lambda :: "(t \<Rightarrow> t) \<Rightarrow> t" (binder "\<^bold>\<lambda>" 30) and + appl :: "[t, t] \<Rightarrow> t" (infixl "`" 60) \<comment> \<open>Application binds tighter than abstraction.\<close> syntax - "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Prod>_:_./ _)" 30) - "_PROD_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3PROD _:_./ _)" 30) + "_PROD" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Prod>_:_./ _)" 30) + "_PROD_ASCII" :: "[idt, t, t] \<Rightarrow> t" ("(3PROD _:_./ _)" 30) text "The translations below bind the variable \<open>x\<close> in the expressions \<open>B\<close> and \<open>b\<close>." @@ -29,7 +29,7 @@ translations text "Nondependent functions are a special case." -abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 40) +abbreviation Function :: "[t, t] \<Rightarrow> t" (infixr "\<rightarrow>" 40) where "A \<rightarrow> B \<equiv> \<Prod>_: A. B" @@ -75,15 +75,15 @@ lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim section \<open>Function composition\<close> -definition compose :: "[Term, Term] \<Rightarrow> Term" (infixr "o" 110) where "g o f \<equiv> \<^bold>\<lambda>x. g`(f`x)" +definition compose :: "[t, t] \<Rightarrow> t" (infixr "o" 110) where "g o f \<equiv> \<^bold>\<lambda>x. g`(f`x)" -syntax "_COMPOSE" :: "[Term, Term] \<Rightarrow> Term" (infixr "\<circ>" 110) +syntax "_COMPOSE" :: "[t, t] \<Rightarrow> t" (infixr "\<circ>" 110) translations "g \<circ> f" \<rightleftharpoons> "g o f" section \<open>Polymorphic identity function\<close> -abbreviation id :: Term where "id \<equiv> \<^bold>\<lambda>x. x" +abbreviation id :: t where "id \<equiv> \<^bold>\<lambda>x. x" end |