--- a/src/HOL/BNF_Def.thy Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/BNF_Def.thy Fri Jun 27 10:11:44 2014 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/BNF_Def.thy
Author: Dmitriy Traytel, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
Copyright 2012
Definition of bounded natural functors.
@@ -8,12 +9,47 @@
header {* Definition of Bounded Natural Functors *}
theory BNF_Def
-imports BNF_Util Fun_Def_Base
+imports BNF_Cardinal_Arithmetic Fun_Def_Base
keywords
"print_bnfs" :: diag and
"bnf" :: thy_goal
begin
+definition
+ rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
+where
+ "rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
+
+lemma rel_funI [intro]:
+ assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
+ shows "rel_fun A B f g"
+ using assms by (simp add: rel_fun_def)
+
+lemma rel_funD:
+ assumes "rel_fun A B f g" and "A x y"
+ shows "B (f x) (g y)"
+ using assms by (simp add: rel_fun_def)
+
+definition collect where
+"collect F x = (\<Union>f \<in> F. f x)"
+
+lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
+by simp
+
+lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
+by simp
+
+lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
+unfolding bij_def inj_on_def by auto blast
+
+(* Operator: *)
+definition "Gr A f = {(a, f a) | a. a \<in> A}"
+
+definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
+
+definition vimage2p where
+ "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
+
lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)"
by (rule ext) (auto simp only: comp_apply collect_def)
@@ -152,6 +188,8 @@
lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"
unfolding vimage2p_def Grp_def by auto
+ML_file "Tools/BNF/bnf_util.ML"
+ML_file "Tools/BNF/bnf_tactics.ML"
ML_file "Tools/BNF/bnf_def_tactics.ML"
ML_file "Tools/BNF/bnf_def.ML"