equal
deleted
inserted
replaced
6 |
6 |
7 theory FinFunPred imports "~~/src/HOL/Library/FinFun" begin |
7 theory FinFunPred imports "~~/src/HOL/Library/FinFun" begin |
8 |
8 |
9 text {* Instantiate FinFun predicates just like predicates *} |
9 text {* Instantiate FinFun predicates just like predicates *} |
10 |
10 |
11 type_synonym 'a pred\<^isub>f = "'a \<Rightarrow>\<^isub>f bool" |
11 type_synonym 'a pred\<^isub>f = "'a \<Rightarrow>f bool" |
12 |
12 |
13 instantiation "finfun" :: (type, ord) ord |
13 instantiation "finfun" :: (type, ord) ord |
14 begin |
14 begin |
15 |
15 |
16 definition le_finfun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f\<^sub>f x \<le> g\<^sub>f x)" |
16 definition le_finfun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f\<^sub>f x \<le> g\<^sub>f x)" |
17 |
17 |
18 definition [code del]: "(f\<Colon>'a \<Rightarrow>\<^isub>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> f \<ge> g" |
18 definition [code del]: "(f\<Colon>'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> f \<ge> g" |
19 |
19 |
20 instance .. |
20 instance .. |
21 |
21 |
22 lemma le_finfun_code [code]: |
22 lemma le_finfun_code [code]: |
23 "f \<le> g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x \<le> y) \<circ>\<^isub>f (f, g)\<^sup>f)" |
23 "f \<le> g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x \<le> y) \<circ>\<^isub>f (f, g)\<^sup>f)" |