# HG changeset patch # User paulson # Date 1332438770 0 # Node ID 4a8a8b9bf41496307a65303742337d3106b9b651 # Parent 2e3dcec916539aa9b4eb3667ee7b008d10eac3c3 more structured proofs diff -r 2e3dcec91653 -r 4a8a8b9bf414 src/ZF/Constructible/AC_in_L.thy --- a/src/ZF/Constructible/AC_in_L.thy Thu Mar 22 16:41:22 2012 +0000 +++ b/src/ZF/Constructible/AC_in_L.thy Thu Mar 22 17:52:50 2012 +0000 @@ -44,22 +44,32 @@ by (simp add: shorterI) lemma linear_rlist: - "linear(A,r) ==> linear(list(A),rlist(A,r))" -apply (simp (no_asm_simp) add: linear_def) -apply (rule ballI) -apply (induct_tac x) - apply (rule ballI) - apply (induct_tac y) - apply (simp_all add: shorterI) -apply (rule ballI) -apply (erule_tac a=y in list.cases) - apply (rename_tac [2] a2 l2) - apply (rule_tac [2] i = "length(l)" and j = "length(l2)" in Ord_linear_lt) - apply (simp_all add: shorterI) -apply (erule_tac x=a and y=a2 in linearE) - apply (simp_all add: diffI) -apply (blast intro: sameI) -done + assumes r: "linear(A,r)" shows "linear(list(A),rlist(A,r))" +proof - + { fix xs ys + have "xs \ list(A) \ ys \ list(A) \ \xs,ys\ \ rlist(A,r) \ xs = ys \ \ys,xs\ \ rlist(A, r) " + proof (induct xs arbitrary: ys rule: list.induct) + case Nil + thus ?case by (induct ys rule: list.induct) (auto simp add: shorterI) + next + case (Cons x xs) + { fix y ys + assume "y \ A" and "ys \ list(A)" + with Cons + have "\Cons(x,xs),Cons(y,ys)\ \ rlist(A,r) \ x=y & xs = ys \ \Cons(y,ys), Cons(x,xs)\ \ rlist(A,r)" + apply (rule_tac i = "length(xs)" and j = "length(ys)" in Ord_linear_lt) + apply (simp_all add: shorterI) + apply (rule linearE [OF r, of x y]) + apply (auto simp add: diffI intro: sameI) + done + } + note yConsCase = this + show ?case using `ys \ list(A)` + by (cases rule: list.cases) (simp_all add: Cons rlist_Nil_Cons yConsCase) + qed + } + thus ?thesis by (simp add: linear_def) +qed subsubsection{*Well-foundedness*} @@ -464,8 +474,8 @@ by (blast intro: well_ord_imp_relativized) qed -text{*In order to prove @{term" \r[L]. wellordered(L, A, r)"}, it's necessary to know -that @{term r} is actually constructible. Of course, it follows from the assumption ``@{term V} equals @{term L''}, +text{*In order to prove @{term" \r[L]. wellordered(L,x,r)"}, it's necessary to know +that @{term r} is actually constructible. It follows from the assumption ``@{term V} equals @{term L''}, but this reasoning doesn't appear to work in Isabelle.*} end