equal
deleted
inserted
replaced
18 "list_all2 (op =) = (op =)" |
18 "list_all2 (op =) = (op =)" |
19 proof (rule ext)+ |
19 proof (rule ext)+ |
20 fix xs ys |
20 fix xs ys |
21 show "list_all2 (op =) xs ys \<longleftrightarrow> xs = ys" |
21 show "list_all2 (op =) xs ys \<longleftrightarrow> xs = ys" |
22 by (induct xs ys rule: list_induct2') simp_all |
22 by (induct xs ys rule: list_induct2') simp_all |
|
23 qed |
|
24 |
|
25 lemma reflp_list_all2: |
|
26 assumes "reflp R" |
|
27 shows "reflp (list_all2 R)" |
|
28 proof (rule reflpI) |
|
29 from assms have *: "\<And>xs. R xs xs" by (rule reflpE) |
|
30 fix xs |
|
31 show "list_all2 R xs xs" |
|
32 by (induct xs) (simp_all add: *) |
23 qed |
33 qed |
24 |
34 |
25 lemma list_symp: |
35 lemma list_symp: |
26 assumes "symp R" |
36 assumes "symp R" |
27 shows "symp (list_all2 R)" |
37 shows "symp (list_all2 R)" |