equal
deleted
inserted
replaced
42 and list_exprel_refl: "(Xs,Xs) \<in> listrel(exprel)" |
42 and list_exprel_refl: "(Xs,Xs) \<in> listrel(exprel)" |
43 by (induct X and Xs) (blast intro: exprel.intros listrel.intros)+ |
43 by (induct X and Xs) (blast intro: exprel.intros listrel.intros)+ |
44 |
44 |
45 theorem equiv_exprel: "equiv UNIV exprel" |
45 theorem equiv_exprel: "equiv UNIV exprel" |
46 proof - |
46 proof - |
47 have "reflexive exprel" by (simp add: refl_def exprel_refl) |
47 have "refl exprel" by (simp add: refl_on_def exprel_refl) |
48 moreover have "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM) |
48 moreover have "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM) |
49 moreover have "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS) |
49 moreover have "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS) |
50 ultimately show ?thesis by (simp add: equiv_def) |
50 ultimately show ?thesis by (simp add: equiv_def) |
51 qed |
51 qed |
52 |
52 |