src/HOL/Lambda/ListApplication.thy
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 11549 e7265e70fd7c
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
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
wenzelm@9771
     9
theory ListApplication = Lambda:
wenzelm@9771
    10
wenzelm@9771
    11
syntax
wenzelm@9771
    12
  "_list_application" :: "dB => dB list => dB"   (infixl "$$" 150)
wenzelm@9771
    13
translations
wenzelm@9771
    14
  "t $$ ts" == "foldl (op $) t ts"
wenzelm@9771
    15
wenzelm@9771
    16
lemma apps_eq_tail_conv [iff]: "(r $$ ts = s $$ ts) = (r = s)"
wenzelm@9771
    17
  apply (induct_tac ts rule: rev_induct)
wenzelm@9771
    18
   apply auto
wenzelm@9771
    19
  done
wenzelm@9771
    20
wenzelm@9941
    21
lemma Var_eq_apps_conv [rule_format, iff]:
wenzelm@9771
    22
    "\<forall>s. (Var m = s $$ ss) = (Var m = s \<and> ss = [])"
wenzelm@9771
    23
  apply (induct_tac ss)
wenzelm@9771
    24
   apply auto
wenzelm@9771
    25
  done
wenzelm@9771
    26
wenzelm@9941
    27
lemma Var_apps_eq_Var_apps_conv [rule_format, iff]:
wenzelm@9771
    28
    "\<forall>ss. (Var m $$ rs = Var n $$ ss) = (m = n \<and> rs = ss)"
wenzelm@9771
    29
  apply (induct_tac rs rule: rev_induct)
wenzelm@9771
    30
   apply simp
wenzelm@9771
    31
   apply blast
wenzelm@9771
    32
  apply (rule allI)
wenzelm@9771
    33
  apply (induct_tac ss rule: rev_induct)
wenzelm@9771
    34
   apply auto
wenzelm@9771
    35
  done
wenzelm@9771
    36
wenzelm@9771
    37
lemma App_eq_foldl_conv:
wenzelm@9771
    38
  "(r $ s = t $$ ts) =
wenzelm@9771
    39
    (if ts = [] then r $ s = t
wenzelm@9771
    40
    else (\<exists>ss. ts = ss @ [s] \<and> r = t $$ ss))"
wenzelm@9771
    41
  apply (rule_tac xs = ts in rev_exhaust)
wenzelm@9771
    42
   apply auto
wenzelm@9771
    43
  done
wenzelm@9771
    44
wenzelm@9771
    45
lemma Abs_eq_apps_conv [iff]:
wenzelm@9771
    46
    "(Abs r = s $$ ss) = (Abs r = s \<and> ss = [])"
wenzelm@9771
    47
  apply (induct_tac ss rule: rev_induct)
wenzelm@9771
    48
   apply auto
wenzelm@9771
    49
  done
wenzelm@9771
    50
wenzelm@9771
    51
lemma apps_eq_Abs_conv [iff]: "(s $$ ss = Abs r) = (s = Abs r \<and> ss = [])"
wenzelm@9771
    52
  apply (induct_tac ss rule: rev_induct)
wenzelm@9771
    53
   apply auto
wenzelm@9771
    54
  done
wenzelm@9771
    55
wenzelm@9771
    56
lemma Abs_apps_eq_Abs_apps_conv [iff]:
wenzelm@9771
    57
    "\<forall>ss. (Abs r $$ rs = Abs s $$ ss) = (r = s \<and> rs = ss)"
wenzelm@9771
    58
  apply (induct_tac rs rule: rev_induct)
wenzelm@9771
    59
   apply simp
wenzelm@9771
    60
   apply blast
wenzelm@9771
    61
  apply (rule allI)
wenzelm@9771
    62
  apply (induct_tac ss rule: rev_induct)
wenzelm@9771
    63
   apply auto
wenzelm@9771
    64
  done
wenzelm@9771
    65
wenzelm@9771
    66
lemma Abs_App_neq_Var_apps [iff]:
wenzelm@9771
    67
    "\<forall>s t. Abs s $ t ~= Var n $$ ss"
wenzelm@9771
    68
  apply (induct_tac ss rule: rev_induct)
wenzelm@9771
    69
   apply auto
wenzelm@9771
    70
  done
wenzelm@9771
    71
wenzelm@9941
    72
lemma Var_apps_neq_Abs_apps [rule_format, iff]:
wenzelm@9771
    73
    "\<forall>ts. Var n $$ ts ~= Abs r $$ ss"
wenzelm@9771
    74
  apply (induct_tac ss rule: rev_induct)
wenzelm@9771
    75
   apply simp
wenzelm@9771
    76
  apply (rule allI)
wenzelm@9771
    77
  apply (induct_tac ts rule: rev_induct)
wenzelm@9771
    78
   apply auto
wenzelm@9771
    79
  done
nipkow@5261
    80
wenzelm@9771
    81
lemma ex_head_tail:
wenzelm@9771
    82
  "\<exists>ts h. t = h $$ ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
wenzelm@9771
    83
  apply (induct_tac t)
wenzelm@9771
    84
    apply (rule_tac x = "[]" in exI)
wenzelm@9771
    85
    apply simp
wenzelm@9771
    86
   apply clarify
wenzelm@9771
    87
   apply (rename_tac ts1 ts2 h1 h2)
wenzelm@9771
    88
   apply (rule_tac x = "ts1 @ [h2 $$ ts2]" in exI)
wenzelm@9771
    89
   apply simp
wenzelm@9771
    90
  apply simp
wenzelm@9771
    91
  done
wenzelm@9771
    92
wenzelm@9771
    93
lemma size_apps [simp]:
wenzelm@9771
    94
  "size (r $$ rs) = size r + foldl (op +) 0 (map size rs) + length rs"
wenzelm@9771
    95
  apply (induct_tac rs rule: rev_induct)
wenzelm@9771
    96
   apply auto
wenzelm@9771
    97
  done
wenzelm@9771
    98
wenzelm@9771
    99
lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k"
wenzelm@9771
   100
  apply simp
wenzelm@9771
   101
  done
wenzelm@9771
   102
wenzelm@9811
   103
wenzelm@9811
   104
text {* \medskip A customized induction schema for @{text "$$"}. *}
wenzelm@9771
   105
wenzelm@9941
   106
lemma lem [rule_format (no_asm)]:
wenzelm@9771
   107
  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
wenzelm@9811
   108
    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
wenzelm@9771
   109
  |] ==> \<forall>t. size t = n --> P t"
wenzelm@9771
   110
proof -
wenzelm@9771
   111
  case antecedent
wenzelm@9771
   112
  show ?thesis
nipkow@9870
   113
   apply (induct_tac n rule: nat_less_induct)
wenzelm@9771
   114
   apply (rule allI)
wenzelm@9771
   115
   apply (cut_tac t = t in ex_head_tail)
wenzelm@9771
   116
   apply clarify
wenzelm@9771
   117
   apply (erule disjE)
wenzelm@9771
   118
    apply clarify
wenzelm@9771
   119
    apply (rule prems)
wenzelm@9771
   120
    apply clarify
wenzelm@9771
   121
    apply (erule allE, erule impE)
wenzelm@9771
   122
      prefer 2
wenzelm@9771
   123
      apply (erule allE, erule mp, rule refl)
wenzelm@9771
   124
     apply simp
wenzelm@9771
   125
     apply (rule lem0)
wenzelm@9771
   126
      apply force
wenzelm@9771
   127
     apply (rule elem_le_sum)
wenzelm@9771
   128
     apply force
wenzelm@9771
   129
    apply clarify
wenzelm@9771
   130
    apply (rule prems)
wenzelm@9771
   131
     apply (erule allE, erule impE)
wenzelm@9771
   132
      prefer 2
wenzelm@9771
   133
      apply (erule allE, erule mp, rule refl)
wenzelm@9771
   134
     apply simp
wenzelm@9771
   135
    apply clarify
wenzelm@9771
   136
    apply (erule allE, erule impE)
wenzelm@9771
   137
     prefer 2
wenzelm@9771
   138
     apply (erule allE, erule mp, rule refl)
wenzelm@9771
   139
    apply simp
wenzelm@9771
   140
    apply (rule le_imp_less_Suc)
wenzelm@9771
   141
    apply (rule trans_le_add1)
wenzelm@9771
   142
    apply (rule trans_le_add2)
wenzelm@9771
   143
    apply (rule elem_le_sum)
wenzelm@9771
   144
    apply force
wenzelm@9771
   145
    done
wenzelm@9771
   146
qed
wenzelm@9771
   147
wenzelm@9811
   148
theorem Apps_dB_induct:
wenzelm@9771
   149
  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
wenzelm@9811
   150
    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
wenzelm@9771
   151
  |] ==> P t"
wenzelm@9771
   152
proof -
wenzelm@9771
   153
  case antecedent
wenzelm@9771
   154
  show ?thesis
wenzelm@9771
   155
    apply (rule_tac t = t in lem)
wenzelm@9771
   156
      prefer 3
wenzelm@9771
   157
      apply (rule refl)
wenzelm@9771
   158
     apply (assumption | rule prems)+
wenzelm@9771
   159
    done
wenzelm@9771
   160
qed
nipkow@5261
   161
nipkow@9870
   162
end