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