equal
deleted
inserted
replaced
68 by auto |
68 by auto |
69 |
69 |
70 lemma Gr_fst_snd: "(Gr R fst)^-1 O Gr R snd = R" |
70 lemma Gr_fst_snd: "(Gr R fst)^-1 O Gr R snd = R" |
71 unfolding Gr_def by auto |
71 unfolding Gr_def by auto |
72 |
72 |
73 lemma subst_rel_def: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g" |
73 lemma O_Gr_cong: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g" |
74 by simp |
|
75 |
|
76 lemma abs_pred_def: "\<lbrakk>\<And>x y. (x, y) \<in> rel = pred x y\<rbrakk> \<Longrightarrow> rel = Collect (split pred)" |
|
77 by auto |
|
78 |
|
79 lemma Collect_split_cong: "Collect (split pred) = Collect (split pred') \<Longrightarrow> pred = pred'" |
|
80 by blast |
|
81 |
|
82 lemma pred_def_abs: "rel = Collect (split pred) \<Longrightarrow> pred = (\<lambda>x y. (x, y) \<in> rel)" |
|
83 by auto |
|
84 |
|
85 lemma mem_Id_eq_eq: "(\<lambda>x y. (x, y) \<in> Id) = (op =)" |
|
86 by simp |
74 by simp |
87 |
75 |
88 ML_file "Tools/bnf_comp_tactics.ML" |
76 ML_file "Tools/bnf_comp_tactics.ML" |
89 ML_file "Tools/bnf_comp.ML" |
77 ML_file "Tools/bnf_comp.ML" |
90 |
78 |