equal
deleted
inserted
replaced
47 and list_exprel_refl: "(Xs,Xs) \<in> listrel(exprel)" |
47 and list_exprel_refl: "(Xs,Xs) \<in> listrel(exprel)" |
48 by (induct X and Xs rule: compat_freeExp.induct compat_freeExp_list.induct) |
48 by (induct X and Xs rule: compat_freeExp.induct compat_freeExp_list.induct) |
49 (blast intro: exprel.intros listrel.intros)+ |
49 (blast intro: exprel.intros listrel.intros)+ |
50 |
50 |
51 theorem equiv_exprel: "equiv UNIV exprel" |
51 theorem equiv_exprel: "equiv UNIV exprel" |
52 proof - |
52 proof (rule equivI) |
53 have "refl exprel" by (simp add: refl_on_def exprel_refl) |
53 show "refl exprel" by (simp add: refl_on_def exprel_refl) |
54 moreover have "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM) |
54 show "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM) |
55 moreover have "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS) |
55 show "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS) |
56 ultimately show ?thesis by (simp add: equiv_def) |
|
57 qed |
56 qed |
58 |
57 |
59 theorem equiv_list_exprel: "equiv UNIV (listrel exprel)" |
58 theorem equiv_list_exprel: "equiv UNIV (listrel exprel)" |
60 using equiv_listrel [OF equiv_exprel] by simp |
59 using equiv_listrel [OF equiv_exprel] by simp |
61 |
60 |