src/HOL/Lambda/ListApplication.thy
author nipkow
Thu Dec 11 08:52:50 2008 +0100 (2008-12-11)
changeset 29106 25e28a4070f3
parent 23464 bc2563c37b1a
child 36862 952b2b102a0a
permissions -rw-r--r--
Testfile for Stefan's code generator
nipkow@5261
     1
(*  Title:      HOL/Lambda/ListApplication.thy
nipkow@5261
     2
    ID:         $Id$
nipkow@5261
     3
    Author:     Tobias Nipkow
nipkow@5261
     4
    Copyright   1998 TU Muenchen
wenzelm@9811
     5
*)
nipkow@5261
     6
wenzelm@9811
     7
header {* Application of a term to a list of terms *}
nipkow@5261
     8
haftmann@16417
     9
theory ListApplication imports Lambda begin
wenzelm@9771
    10
wenzelm@19363
    11
abbreviation
wenzelm@21404
    12
  list_application :: "dB => dB list => dB"  (infixl "\<degree>\<degree>" 150) where
wenzelm@19363
    13
  "t \<degree>\<degree> ts == foldl (op \<degree>) t ts"
wenzelm@11943
    14
wenzelm@12011
    15
lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
wenzelm@18241
    16
  by (induct ts rule: rev_induct) auto
wenzelm@9771
    17
wenzelm@18241
    18
lemma Var_eq_apps_conv [iff]: "(Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
wenzelm@20503
    19
  by (induct ss arbitrary: s) auto
wenzelm@9771
    20
berghofe@13915
    21
lemma Var_apps_eq_Var_apps_conv [iff]:
wenzelm@18241
    22
    "(Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
wenzelm@20503
    23
  apply (induct rs arbitrary: ss rule: rev_induct)
wenzelm@9771
    24
   apply simp
wenzelm@9771
    25
   apply blast
wenzelm@9771
    26
  apply (induct_tac ss rule: rev_induct)
wenzelm@9771
    27
   apply auto
wenzelm@9771
    28
  done
wenzelm@9771
    29
wenzelm@9771
    30
lemma App_eq_foldl_conv:
wenzelm@12011
    31
  "(r \<degree> s = t \<degree>\<degree> ts) =
wenzelm@12011
    32
    (if ts = [] then r \<degree> s = t
wenzelm@12011
    33
    else (\<exists>ss. ts = ss @ [s] \<and> r = t \<degree>\<degree> ss))"
wenzelm@9771
    34
  apply (rule_tac xs = ts in rev_exhaust)
wenzelm@9771
    35
   apply auto
wenzelm@9771
    36
  done
wenzelm@9771
    37
wenzelm@9771
    38
lemma Abs_eq_apps_conv [iff]:
wenzelm@12011
    39
    "(Abs r = s \<degree>\<degree> ss) = (Abs r = s \<and> ss = [])"
wenzelm@18241
    40
  by (induct ss rule: rev_induct) auto
wenzelm@9771
    41
wenzelm@12011
    42
lemma apps_eq_Abs_conv [iff]: "(s \<degree>\<degree> ss = Abs r) = (s = Abs r \<and> ss = [])"
wenzelm@18241
    43
  by (induct ss rule: rev_induct) auto
wenzelm@9771
    44
wenzelm@9771
    45
lemma Abs_apps_eq_Abs_apps_conv [iff]:
wenzelm@18241
    46
    "(Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
wenzelm@20503
    47
  apply (induct rs arbitrary: ss rule: rev_induct)
wenzelm@9771
    48
   apply simp
wenzelm@9771
    49
   apply blast
wenzelm@9771
    50
  apply (induct_tac ss rule: rev_induct)
wenzelm@9771
    51
   apply auto
wenzelm@9771
    52
  done
wenzelm@9771
    53
wenzelm@9771
    54
lemma Abs_App_neq_Var_apps [iff]:
wenzelm@18257
    55
    "Abs s \<degree> t \<noteq> Var n \<degree>\<degree> ss"
wenzelm@20503
    56
  by (induct ss arbitrary: s t rule: rev_induct) auto
wenzelm@9771
    57
berghofe@13915
    58
lemma Var_apps_neq_Abs_apps [iff]:
wenzelm@18257
    59
    "Var n \<degree>\<degree> ts \<noteq> Abs r \<degree>\<degree> ss"
wenzelm@20503
    60
  apply (induct ss arbitrary: ts rule: rev_induct)
wenzelm@9771
    61
   apply simp
wenzelm@9771
    62
  apply (induct_tac ts rule: rev_induct)
wenzelm@9771
    63
   apply auto
wenzelm@9771
    64
  done
nipkow@5261
    65
wenzelm@9771
    66
lemma ex_head_tail:
wenzelm@12011
    67
  "\<exists>ts h. t = h \<degree>\<degree> ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
wenzelm@18241
    68
  apply (induct t)
wenzelm@9771
    69
    apply (rule_tac x = "[]" in exI)
wenzelm@9771
    70
    apply simp
wenzelm@9771
    71
   apply clarify
wenzelm@9771
    72
   apply (rename_tac ts1 ts2 h1 h2)
wenzelm@12011
    73
   apply (rule_tac x = "ts1 @ [h2 \<degree>\<degree> ts2]" in exI)
wenzelm@9771
    74
   apply simp
wenzelm@9771
    75
  apply simp
wenzelm@9771
    76
  done
wenzelm@9771
    77
wenzelm@9771
    78
lemma size_apps [simp]:
wenzelm@12011
    79
  "size (r \<degree>\<degree> rs) = size r + foldl (op +) 0 (map size rs) + length rs"
wenzelm@18241
    80
  by (induct rs rule: rev_induct) auto
wenzelm@9771
    81
wenzelm@9771
    82
lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k"
wenzelm@18241
    83
  by simp
wenzelm@9771
    84
berghofe@14066
    85
lemma lift_map [simp]:
wenzelm@18241
    86
    "lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
wenzelm@20503
    87
  by (induct ts arbitrary: t) simp_all
berghofe@14066
    88
berghofe@14066
    89
lemma subst_map [simp]:
wenzelm@18241
    90
    "subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
wenzelm@20503
    91
  by (induct ts arbitrary: t) simp_all
berghofe@14066
    92
berghofe@14066
    93
lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])"
berghofe@14066
    94
  by simp
berghofe@14066
    95
wenzelm@9811
    96
wenzelm@12011
    97
text {* \medskip A customized induction schema for @{text "\<degree>\<degree>"}. *}
wenzelm@9771
    98
wenzelm@18241
    99
lemma lem:
wenzelm@18241
   100
  assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)"
wenzelm@18241
   101
    and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)"
wenzelm@18241
   102
  shows "size t = n \<Longrightarrow> P t"
wenzelm@20503
   103
  apply (induct n arbitrary: t rule: nat_less_induct)
wenzelm@18241
   104
  apply (cut_tac t = t in ex_head_tail)
wenzelm@18241
   105
  apply clarify
wenzelm@18241
   106
  apply (erule disjE)
wenzelm@18241
   107
   apply clarify
wenzelm@23464
   108
   apply (rule assms)
wenzelm@9771
   109
   apply clarify
wenzelm@18241
   110
   apply (erule allE, erule impE)
wenzelm@18241
   111
    prefer 2
wenzelm@18241
   112
    apply (erule allE, erule mp, rule refl)
wenzelm@18241
   113
   apply simp
wenzelm@18241
   114
   apply (rule lem0)
wenzelm@9771
   115
    apply force
wenzelm@18241
   116
   apply (rule elem_le_sum)
wenzelm@18241
   117
   apply force
wenzelm@18241
   118
  apply clarify
wenzelm@23464
   119
  apply (rule assms)
wenzelm@18241
   120
   apply (erule allE, erule impE)
wenzelm@18241
   121
    prefer 2
wenzelm@18241
   122
    apply (erule allE, erule mp, rule refl)
wenzelm@18241
   123
   apply simp
wenzelm@18241
   124
  apply clarify
wenzelm@18241
   125
  apply (erule allE, erule impE)
wenzelm@18241
   126
   prefer 2
wenzelm@18241
   127
   apply (erule allE, erule mp, rule refl)
wenzelm@18241
   128
  apply simp
wenzelm@18241
   129
  apply (rule le_imp_less_Suc)
wenzelm@18241
   130
  apply (rule trans_le_add1)
wenzelm@18241
   131
  apply (rule trans_le_add2)
wenzelm@18241
   132
  apply (rule elem_le_sum)
wenzelm@18241
   133
  apply force
wenzelm@18241
   134
  done
wenzelm@9771
   135
wenzelm@9811
   136
theorem Apps_dB_induct:
wenzelm@18241
   137
  assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)"
wenzelm@18241
   138
    and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)"
wenzelm@18241
   139
  shows "P t"
wenzelm@18241
   140
  apply (rule_tac t = t in lem)
wenzelm@18241
   141
    prefer 3
wenzelm@18241
   142
    apply (rule refl)
wenzelm@23464
   143
    using assms apply iprover+
wenzelm@18241
   144
  done
nipkow@5261
   145
nipkow@9870
   146
end