src/HOL/Proofs/Lambda/ListApplication.thy
author haftmann
Sat, 05 Jul 2014 11:01:53 +0200
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 58889 5b7a9633cfa8
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39157
b98909faaea8 more explicit HOL-Proofs 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
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     2
    Author:     Tobias Nipkow
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     3
    Copyright   1998 TU Muenchen
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
     4
*)
5261
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     5
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
     6
header {* Application of a term to a list of terms *}
5261
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14066
diff changeset
     8
theory ListApplication imports Lambda begin
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
     9
19363
667b5ea637dd refined 'abbreviation';
wenzelm
parents: 19086
diff changeset
    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
667b5ea637dd refined 'abbreviation';
wenzelm
parents: 19086
diff changeset
    12
  "t \<degree>\<degree> ts == foldl (op \<degree>) t ts"
11943
a9672446b45f tuned notation;
wenzelm
parents: 11549
diff changeset
    13
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11947
diff changeset
    14
lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    15
  by (induct ts rule: rev_induct) auto
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    16
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    17
lemma Var_eq_apps_conv [iff]: "(Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19363
diff changeset
    18
  by (induct ss arbitrary: s) auto
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    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
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    21
    "(Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19363
diff changeset
    22
  apply (induct rs arbitrary: ss rule: rev_induct)
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    23
   apply simp
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    24
   apply blast
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    25
  apply (induct_tac ss rule: rev_induct)
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    26
   apply auto
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    27
  done
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    28
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    29
lemma App_eq_foldl_conv:
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11947
diff changeset
    30
  "(r \<degree> s = t \<degree>\<degree> ts) =
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11947
diff changeset
    31
    (if ts = [] then r \<degree> s = t
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11947
diff changeset
    32
    else (\<exists>ss. ts = ss @ [s] \<and> r = t \<degree>\<degree> ss))"
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    33
  apply (rule_tac xs = ts in rev_exhaust)
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    34
   apply auto
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    35
  done
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    36
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    37
lemma Abs_eq_apps_conv [iff]:
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11947
diff changeset
    38
    "(Abs r = s \<degree>\<degree> ss) = (Abs r = s \<and> ss = [])"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    39
  by (induct ss rule: rev_induct) auto
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    40
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11947
diff changeset
    41
lemma apps_eq_Abs_conv [iff]: "(s \<degree>\<degree> ss = Abs r) = (s = Abs r \<and> ss = [])"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    42
  by (induct ss rule: rev_induct) auto
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    43
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    44
lemma Abs_apps_eq_Abs_apps_conv [iff]:
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    45
    "(Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19363
diff changeset
    46
  apply (induct rs arbitrary: ss rule: rev_induct)
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    47
   apply simp
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    48
   apply blast
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    49
  apply (induct_tac ss rule: rev_induct)
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    50
   apply auto
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    51
  done
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    52
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    53
lemma Abs_App_neq_Var_apps [iff]:
18257
2124b24454dd tuned induct proofs;
wenzelm
parents: 18241
diff changeset
    54
    "Abs s \<degree> t \<noteq> Var n \<degree>\<degree> ss"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19363
diff changeset
    55
  by (induct ss arbitrary: s t rule: rev_induct) auto
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    56
13915
28ccb51bd2f3 Eliminated most occurrences of rule_format attribute.
berghofe
parents: 12011
diff changeset
    57
lemma Var_apps_neq_Abs_apps [iff]:
18257
2124b24454dd tuned induct proofs;
wenzelm
parents: 18241
diff changeset
    58
    "Var n \<degree>\<degree> ts \<noteq> Abs r \<degree>\<degree> ss"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19363
diff changeset
    59
  apply (induct ss arbitrary: ts rule: rev_induct)
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    60
   apply simp
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    61
  apply (induct_tac ts rule: rev_induct)
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    62
   apply auto
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    63
  done
5261
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
    64
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    65
lemma ex_head_tail:
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11947
diff changeset
    66
  "\<exists>ts h. t = h \<degree>\<degree> ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    67
  apply (induct t)
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    68
    apply (rule_tac x = "[]" in exI)
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    69
    apply simp
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    70
   apply clarify
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    71
   apply (rename_tac ts1 ts2 h1 h2)
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11947
diff changeset
    72
   apply (rule_tac x = "ts1 @ [h2 \<degree>\<degree> ts2]" in exI)
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    73
   apply simp
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    74
  apply simp
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    75
  done
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    76
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    77
lemma size_apps [simp]:
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11947
diff changeset
    78
  "size (r \<degree>\<degree> rs) = size r + foldl (op +) 0 (map size rs) + length rs"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    79
  by (induct rs rule: rev_induct) auto
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    80
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    81
lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    82
  by simp
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    83
14066
fe45b97b62ea Added lift_map and subst_map.
berghofe
parents: 13915
diff changeset
    84
lemma lift_map [simp]:
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    85
    "lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19363
diff changeset
    86
  by (induct ts arbitrary: t) simp_all
14066
fe45b97b62ea Added lift_map and subst_map.
berghofe
parents: 13915
diff changeset
    87
fe45b97b62ea Added lift_map and subst_map.
berghofe
parents: 13915
diff changeset
    88
lemma subst_map [simp]:
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    89
    "subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19363
diff changeset
    90
  by (induct ts arbitrary: t) simp_all
14066
fe45b97b62ea Added lift_map and subst_map.
berghofe
parents: 13915
diff changeset
    91
fe45b97b62ea Added lift_map and subst_map.
berghofe
parents: 13915
diff changeset
    92
lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])"
fe45b97b62ea Added lift_map and subst_map.
berghofe
parents: 13915
diff changeset
    93
  by simp
fe45b97b62ea Added lift_map and subst_map.
berghofe
parents: 13915
diff changeset
    94
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
    95
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11947
diff changeset
    96
text {* \medskip A customized induction schema for @{text "\<degree>\<degree>"}. *}
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
    97
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    98
lemma lem:
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
    99
  assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)"
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   100
    and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)"
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   101
  shows "size t = n \<Longrightarrow> P t"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19363
diff changeset
   102
  apply (induct n arbitrary: t rule: nat_less_induct)
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   103
  apply (cut_tac t = t in ex_head_tail)
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   104
  apply clarify
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   105
  apply (erule disjE)
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   106
   apply clarify
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 21404
diff changeset
   107
   apply (rule assms)
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
   108
   apply clarify
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   109
   apply (erule allE, erule impE)
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   110
    prefer 2
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   111
    apply (erule allE, erule mp, rule refl)
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   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
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   115
  apply clarify
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 21404
diff changeset
   116
  apply (rule assms)
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   117
   apply (erule allE, erule impE)
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   118
    prefer 2
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   119
    apply (erule allE, erule mp, rule refl)
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   120
   apply simp
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   121
  apply clarify
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   122
  apply (erule allE, erule impE)
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   123
   prefer 2
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   124
   apply (erule allE, erule mp, rule refl)
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   125
  apply simp
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   126
  apply (rule le_imp_less_Suc)
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   127
  apply (rule trans_le_add1)
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   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
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   131
  done
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9102
diff changeset
   132
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9771
diff changeset
   133
theorem Apps_dB_induct:
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   134
  assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)"
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   135
    and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)"
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   136
  shows "P t"
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   137
  apply (rule_tac t = t in lem)
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   138
    prefer 3
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   139
    apply (rule refl)
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 21404
diff changeset
   140
    using assms apply iprover+
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 16417
diff changeset
   141
  done
5261
ce3c25c8a694 First steps towards termination of simply typed terms.
nipkow
parents:
diff changeset
   142
9870
2374ba026fc6 less_induct -> nat_less_induct
nipkow
parents: 9811
diff changeset
   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