author  haftmann 
Sat, 05 Jul 2014 11:01:53 +0200  
changeset 57514  bdc2c6b40bf2 
parent 54295  45a5523d4a63 
child 58372  bfd497f2f4c2 
permissions  rwrr 
39157
b98909faaea8
more explicit HOLProofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39126
diff
changeset

1 
(* Title: HOL/Proofs/Lambda/ListOrder.thy 
5261  2 
Author: Tobias Nipkow 
3 
Copyright 1998 TU Muenchen 

4 
*) 

5 

9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

6 
header {* Lifting an order to lists of elements *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

7 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
19086
diff
changeset

8 
theory ListOrder imports Main begin 
5261  9 

46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset

10 
declare [[syntax_ambiguity_warning = false]] 
39126
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
36862
diff
changeset

11 

ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
36862
diff
changeset

12 

9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

13 
text {* 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

14 
Lifting an order to lists of elements, relating exactly one 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

15 
element. 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

16 
*} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

17 

19086  18 
definition 
22270  19 
step1 :: "('a => 'a => bool) => 'a list => 'a list => bool" where 
19086  20 
"step1 r = 
22270  21 
(\<lambda>ys xs. \<exists>us z z' vs. xs = us @ z # vs \<and> r z' z \<and> ys = 
22 
us @ z' # vs)" 

9771  23 

24 

22270  25 
lemma step1_converse [simp]: "step1 (r^1) = (step1 r)^1" 
26 
apply (unfold step1_def) 

27 
apply (blast intro!: order_antisym) 

28 
done 

29 

30 
lemma in_step1_converse [iff]: "(step1 (r^1) x y) = ((step1 r)^1 x y)" 

31 
apply auto 

32 
done 

33 

34 
lemma not_Nil_step1 [iff]: "\<not> step1 r [] xs" 

9771  35 
apply (unfold step1_def) 
36 
apply blast 

37 
done 

38 

22270  39 
lemma not_step1_Nil [iff]: "\<not> step1 r xs []" 
9771  40 
apply (unfold step1_def) 
41 
apply blast 

42 
done 

43 

44 
lemma Cons_step1_Cons [iff]: 

22270  45 
"(step1 r (y # ys) (x # xs)) = 
46 
(r y x \<and> xs = ys \<or> x = y \<and> step1 r ys xs)" 

9771  47 
apply (unfold step1_def) 
48 
apply (rule iffI) 

49 
apply (erule exE) 

50 
apply (rename_tac ts) 

51 
apply (case_tac ts) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
39157
diff
changeset

52 
apply fastforce 
9771  53 
apply force 
54 
apply (erule disjE) 

55 
apply blast 

56 
apply (blast intro: Cons_eq_appendI) 

57 
done 

58 

59 
lemma append_step1I: 

22270  60 
"step1 r ys xs \<and> vs = us \<or> ys = xs \<and> step1 r vs us 
61 
==> step1 r (ys @ vs) (xs @ us)" 

9771  62 
apply (unfold step1_def) 
63 
apply auto 

64 
apply blast 

65 
apply (blast intro: append_eq_appendI) 

66 
done 

67 

18257  68 
lemma Cons_step1E [elim!]: 
22270  69 
assumes "step1 r ys (x # xs)" 
70 
and "!!y. ys = y # xs \<Longrightarrow> r y x \<Longrightarrow> R" 

71 
and "!!zs. ys = x # zs \<Longrightarrow> step1 r zs xs \<Longrightarrow> R" 

18257  72 
shows R 
23464  73 
using assms 
18257  74 
apply (cases ys) 
9771  75 
apply (simp add: step1_def) 
76 
apply blast 

77 
done 

78 

79 
lemma Snoc_step1_SnocD: 

22270  80 
"step1 r (ys @ [y]) (xs @ [x]) 
81 
==> (step1 r ys xs \<and> y = x \<or> ys = xs \<and> r y x)" 

9771  82 
apply (unfold step1_def) 
83 
apply (clarify del: disjCI) 

84 
apply (rename_tac vs) 

85 
apply (rule_tac xs = vs in rev_exhaust) 

86 
apply force 

87 
apply simp 

88 
apply blast 

89 
done 

90 

18241  91 
lemma Cons_acc_step1I [intro!]: 
54295  92 
"Wellfounded.accp r x ==> Wellfounded.accp (step1 r) xs \<Longrightarrow> Wellfounded.accp (step1 r) (x # xs)" 
93 
apply (induct arbitrary: xs set: Wellfounded.accp) 

9771  94 
apply (erule thin_rl) 
23750  95 
apply (erule accp_induct) 
96 
apply (rule accp.accI) 

9771  97 
apply blast 
98 
done 

99 

54295  100 
lemma lists_accD: "listsp (Wellfounded.accp r) xs ==> Wellfounded.accp (step1 r) xs" 
22270  101 
apply (induct set: listsp) 
23750  102 
apply (rule accp.accI) 
9771  103 
apply simp 
23750  104 
apply (rule accp.accI) 
105 
apply (fast dest: accp_downward) 

9771  106 
done 
107 

9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

108 
lemma ex_step1I: 
22270  109 
"[ x \<in> set xs; r y x ] 
110 
==> \<exists>ys. step1 r ys xs \<and> y \<in> set ys" 

9771  111 
apply (unfold step1_def) 
112 
apply (drule in_set_conv_decomp [THEN iffD1]) 

113 
apply force 

114 
done 

115 

54295  116 
lemma lists_accI: "Wellfounded.accp (step1 r) xs ==> listsp (Wellfounded.accp r) xs" 
117 
apply (induct set: Wellfounded.accp) 

9771  118 
apply clarify 
23750  119 
apply (rule accp.accI) 
22270  120 
apply (drule_tac r=r in ex_step1I, assumption) 
9771  121 
apply blast 
122 
done 

5261  123 

11639  124 
end 