author  haftmann 
Sat, 05 Jul 2014 11:01:53 +0200  
changeset 57514  bdc2c6b40bf2 
parent 57512  cc97b347b301 
child 58889  5b7a9633cfa8 
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:
36862
diff
changeset

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

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

4 
*) 
5261  5 

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

6 
header {* Application of a term to a list of terms *} 
5261  7 

16417  8 
theory ListApplication imports Lambda begin 
9771  9 

19363  10 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20503
diff
changeset

11 
list_application :: "dB => dB list => dB" (infixl "\<degree>\<degree>" 150) where 
19363  12 
"t \<degree>\<degree> ts == foldl (op \<degree>) t ts" 
11943  13 

12011  14 
lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)" 
18241  15 
by (induct ts rule: rev_induct) auto 
9771  16 

18241  17 
lemma Var_eq_apps_conv [iff]: "(Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])" 
20503  18 
by (induct ss arbitrary: s) auto 
9771  19 

13915
28ccb51bd2f3
Eliminated most occurrences of rule_format attribute.
berghofe
parents:
12011
diff
changeset

20 
lemma Var_apps_eq_Var_apps_conv [iff]: 
18241  21 
"(Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)" 
20503  22 
apply (induct rs arbitrary: ss rule: rev_induct) 
9771  23 
apply simp 
24 
apply blast 

25 
apply (induct_tac ss rule: rev_induct) 

26 
apply auto 

27 
done 

28 

29 
lemma App_eq_foldl_conv: 

12011  30 
"(r \<degree> s = t \<degree>\<degree> ts) = 
31 
(if ts = [] then r \<degree> s = t 

32 
else (\<exists>ss. ts = ss @ [s] \<and> r = t \<degree>\<degree> ss))" 

9771  33 
apply (rule_tac xs = ts in rev_exhaust) 
34 
apply auto 

35 
done 

36 

37 
lemma Abs_eq_apps_conv [iff]: 

12011  38 
"(Abs r = s \<degree>\<degree> ss) = (Abs r = s \<and> ss = [])" 
18241  39 
by (induct ss rule: rev_induct) auto 
9771  40 

12011  41 
lemma apps_eq_Abs_conv [iff]: "(s \<degree>\<degree> ss = Abs r) = (s = Abs r \<and> ss = [])" 
18241  42 
by (induct ss rule: rev_induct) auto 
9771  43 

44 
lemma Abs_apps_eq_Abs_apps_conv [iff]: 

18241  45 
"(Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)" 
20503  46 
apply (induct rs arbitrary: ss rule: rev_induct) 
9771  47 
apply simp 
48 
apply blast 

49 
apply (induct_tac ss rule: rev_induct) 

50 
apply auto 

51 
done 

52 

53 
lemma Abs_App_neq_Var_apps [iff]: 

18257  54 
"Abs s \<degree> t \<noteq> Var n \<degree>\<degree> ss" 
20503  55 
by (induct ss arbitrary: s t rule: rev_induct) auto 
9771  56 

13915
28ccb51bd2f3
Eliminated most occurrences of rule_format attribute.
berghofe
parents:
12011
diff
changeset

57 
lemma Var_apps_neq_Abs_apps [iff]: 
18257  58 
"Var n \<degree>\<degree> ts \<noteq> Abs r \<degree>\<degree> ss" 
20503  59 
apply (induct ss arbitrary: ts rule: rev_induct) 
9771  60 
apply simp 
61 
apply (induct_tac ts rule: rev_induct) 

62 
apply auto 

63 
done 

5261  64 

9771  65 
lemma ex_head_tail: 
12011  66 
"\<exists>ts h. t = h \<degree>\<degree> ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))" 
18241  67 
apply (induct t) 
9771  68 
apply (rule_tac x = "[]" in exI) 
69 
apply simp 

70 
apply clarify 

71 
apply (rename_tac ts1 ts2 h1 h2) 

12011  72 
apply (rule_tac x = "ts1 @ [h2 \<degree>\<degree> ts2]" in exI) 
9771  73 
apply simp 
74 
apply simp 

75 
done 

76 

77 
lemma size_apps [simp]: 

12011  78 
"size (r \<degree>\<degree> rs) = size r + foldl (op +) 0 (map size rs) + length rs" 
18241  79 
by (induct rs rule: rev_induct) auto 
9771  80 

81 
lemma lem0: "[ (0::nat) < k; m <= n ] ==> m < n + k" 

18241  82 
by simp 
9771  83 

14066  84 
lemma lift_map [simp]: 
18241  85 
"lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts" 
20503  86 
by (induct ts arbitrary: t) simp_all 
14066  87 

88 
lemma subst_map [simp]: 

18241  89 
"subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts" 
20503  90 
by (induct ts arbitrary: t) simp_all 
14066  91 

92 
lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])" 

93 
by simp 

94 

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

95 

12011  96 
text {* \medskip A customized induction schema for @{text "\<degree>\<degree>"}. *} 
9771  97 

18241  98 
lemma lem: 
99 
assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)" 

100 
and "!!u ts. [ P u; \<forall>t \<in> set ts. P t ] ==> P (Abs u \<degree>\<degree> ts)" 

101 
shows "size t = n \<Longrightarrow> P t" 

20503  102 
apply (induct n arbitrary: t rule: nat_less_induct) 
18241  103 
apply (cut_tac t = t in ex_head_tail) 
104 
apply clarify 

105 
apply (erule disjE) 

106 
apply clarify 

23464  107 
apply (rule assms) 
9771  108 
apply clarify 
18241  109 
apply (erule allE, erule impE) 
110 
prefer 2 

111 
apply (erule allE, erule mp, rule refl) 

112 
apply simp 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
47397
diff
changeset

113 
apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev) 
47397
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
39157
diff
changeset

114 
apply (fastforce simp add: listsum_map_remove1) 
18241  115 
apply clarify 
23464  116 
apply (rule assms) 
18241  117 
apply (erule allE, erule impE) 
118 
prefer 2 

119 
apply (erule allE, erule mp, rule refl) 

120 
apply simp 

121 
apply clarify 

122 
apply (erule allE, erule impE) 

123 
prefer 2 

124 
apply (erule allE, erule mp, rule refl) 

125 
apply simp 

126 
apply (rule le_imp_less_Suc) 

127 
apply (rule trans_le_add1) 

128 
apply (rule trans_le_add2) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
47397
diff
changeset

129 
apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev) 
47397
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
39157
diff
changeset

130 
apply (simp add: member_le_listsum_nat) 
18241  131 
done 
9771  132 

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

133 
theorem Apps_dB_induct: 
18241  134 
assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)" 
135 
and "!!u ts. [ P u; \<forall>t \<in> set ts. P t ] ==> P (Abs u \<degree>\<degree> ts)" 

136 
shows "P t" 

137 
apply (rule_tac t = t in lem) 

138 
prefer 3 

139 
apply (rule refl) 

23464  140 
using assms apply iprover+ 
18241  141 
done 
5261  142 

9870  143 
end 
47397
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
39157
diff
changeset

144 