42 lemma rlist_Nil_Cons [intro]: |
42 lemma rlist_Nil_Cons [intro]: |
43 "[|a \<in> A; l \<in> list(A)|] ==> <[], Cons(a,l)> \<in> rlist(A, r)" |
43 "[|a \<in> A; l \<in> list(A)|] ==> <[], Cons(a,l)> \<in> rlist(A, r)" |
44 by (simp add: shorterI) |
44 by (simp add: shorterI) |
45 |
45 |
46 lemma linear_rlist: |
46 lemma linear_rlist: |
47 "linear(A,r) ==> linear(list(A),rlist(A,r))" |
47 assumes r: "linear(A,r)" shows "linear(list(A),rlist(A,r))" |
48 apply (simp (no_asm_simp) add: linear_def) |
48 proof - |
49 apply (rule ballI) |
49 { fix xs ys |
50 apply (induct_tac x) |
50 have "xs \<in> list(A) \<Longrightarrow> ys \<in> list(A) \<Longrightarrow> \<langle>xs,ys\<rangle> \<in> rlist(A,r) \<or> xs = ys \<or> \<langle>ys,xs\<rangle> \<in> rlist(A, r) " |
51 apply (rule ballI) |
51 proof (induct xs arbitrary: ys rule: list.induct) |
52 apply (induct_tac y) |
52 case Nil |
53 apply (simp_all add: shorterI) |
53 thus ?case by (induct ys rule: list.induct) (auto simp add: shorterI) |
54 apply (rule ballI) |
54 next |
55 apply (erule_tac a=y in list.cases) |
55 case (Cons x xs) |
56 apply (rename_tac [2] a2 l2) |
56 { fix y ys |
57 apply (rule_tac [2] i = "length(l)" and j = "length(l2)" in Ord_linear_lt) |
57 assume "y \<in> A" and "ys \<in> list(A)" |
58 apply (simp_all add: shorterI) |
58 with Cons |
59 apply (erule_tac x=a and y=a2 in linearE) |
59 have "\<langle>Cons(x,xs),Cons(y,ys)\<rangle> \<in> rlist(A,r) \<or> x=y & xs = ys \<or> \<langle>Cons(y,ys), Cons(x,xs)\<rangle> \<in> rlist(A,r)" |
60 apply (simp_all add: diffI) |
60 apply (rule_tac i = "length(xs)" and j = "length(ys)" in Ord_linear_lt) |
61 apply (blast intro: sameI) |
61 apply (simp_all add: shorterI) |
62 done |
62 apply (rule linearE [OF r, of x y]) |
|
63 apply (auto simp add: diffI intro: sameI) |
|
64 done |
|
65 } |
|
66 note yConsCase = this |
|
67 show ?case using `ys \<in> list(A)` |
|
68 by (cases rule: list.cases) (simp_all add: Cons rlist_Nil_Cons yConsCase) |
|
69 qed |
|
70 } |
|
71 thus ?thesis by (simp add: linear_def) |
|
72 qed |
63 |
73 |
64 |
74 |
65 subsubsection{*Well-foundedness*} |
75 subsubsection{*Well-foundedness*} |
66 |
76 |
67 text{*Nothing preceeds Nil in this ordering.*} |
77 text{*Nothing preceeds Nil in this ordering.*} |
462 by (blast dest: L_implies_AC) |
472 by (blast dest: L_implies_AC) |
463 thus "\<exists>r. wellordered(L,x,r)" |
473 thus "\<exists>r. wellordered(L,x,r)" |
464 by (blast intro: well_ord_imp_relativized) |
474 by (blast intro: well_ord_imp_relativized) |
465 qed |
475 qed |
466 |
476 |
467 text{*In order to prove @{term" \<exists>r[L]. wellordered(L, A, r)"}, it's necessary to know |
477 text{*In order to prove @{term" \<exists>r[L]. wellordered(L,x,r)"}, it's necessary to know |
468 that @{term r} is actually constructible. Of course, it follows from the assumption ``@{term V} equals @{term L''}, |
478 that @{term r} is actually constructible. It follows from the assumption ``@{term V} equals @{term L''}, |
469 but this reasoning doesn't appear to work in Isabelle.*} |
479 but this reasoning doesn't appear to work in Isabelle.*} |
470 |
480 |
471 end |
481 end |