Up to index of Isabelle/HOL/Lambda
theory ListApplication(* Title: HOL/Lambda/ListApplication.thy ID: $Id: ListApplication.thy,v 1.14 2005/06/17 14:13:08 haftmann Exp $ Author: Tobias Nipkow Copyright 1998 TU Muenchen *) header {* Application of a term to a list of terms *} theory ListApplication imports Lambda begin syntax "_list_application" :: "dB => dB list => dB" (infixl "°°" 150) translations "t °° ts" == "foldl (op °) t ts" lemma apps_eq_tail_conv [iff]: "(r °° ts = s °° ts) = (r = s)" apply (induct_tac ts rule: rev_induct) apply auto done lemma Var_eq_apps_conv [iff]: "!!s. (Var m = s °° ss) = (Var m = s ∧ ss = [])" apply (induct ss) apply auto done lemma Var_apps_eq_Var_apps_conv [iff]: "!!ss. (Var m °° rs = Var n °° ss) = (m = n ∧ rs = ss)" apply (induct rs rule: rev_induct) apply simp apply blast apply (induct_tac ss rule: rev_induct) apply auto done lemma App_eq_foldl_conv: "(r ° s = t °° ts) = (if ts = [] then r ° s = t else (∃ss. ts = ss @ [s] ∧ r = t °° ss))" apply (rule_tac xs = ts in rev_exhaust) apply auto done lemma Abs_eq_apps_conv [iff]: "(Abs r = s °° ss) = (Abs r = s ∧ ss = [])" apply (induct_tac ss rule: rev_induct) apply auto done lemma apps_eq_Abs_conv [iff]: "(s °° ss = Abs r) = (s = Abs r ∧ ss = [])" apply (induct_tac ss rule: rev_induct) apply auto done lemma Abs_apps_eq_Abs_apps_conv [iff]: "!!ss. (Abs r °° rs = Abs s °° ss) = (r = s ∧ rs = ss)" apply (induct rs rule: rev_induct) apply simp apply blast apply (induct_tac ss rule: rev_induct) apply auto done lemma Abs_App_neq_Var_apps [iff]: "∀s t. Abs s ° t ~= Var n °° ss" apply (induct_tac ss rule: rev_induct) apply auto done lemma Var_apps_neq_Abs_apps [iff]: "!!ts. Var n °° ts ~= Abs r °° ss" apply (induct ss rule: rev_induct) apply simp apply (induct_tac ts rule: rev_induct) apply auto done lemma ex_head_tail: "∃ts h. t = h °° ts ∧ ((∃n. h = Var n) ∨ (∃u. h = Abs u))" apply (induct_tac t) apply (rule_tac x = "[]" in exI) apply simp apply clarify apply (rename_tac ts1 ts2 h1 h2) apply (rule_tac x = "ts1 @ [h2 °° ts2]" in exI) apply simp apply simp done lemma size_apps [simp]: "size (r °° rs) = size r + foldl (op +) 0 (map size rs) + length rs" apply (induct_tac rs rule: rev_induct) apply auto done lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k" apply simp done lemma lift_map [simp]: "!!t. lift (t °° ts) i = lift t i °° map (λt. lift t i) ts" by (induct ts) simp_all lemma subst_map [simp]: "!!t. subst (t °° ts) u i = subst t u i °° map (λt. subst t u i) ts" by (induct ts) simp_all lemma app_last: "(t °° ts) ° u = t °° (ts @ [u])" by simp text {* \medskip A customized induction schema for @{text "°°"}. *} lemma lem [rule_format (no_asm)]: "[| !!n ts. ∀t ∈ set ts. P t ==> P (Var n °° ts); !!u ts. [| P u; ∀t ∈ set ts. P t |] ==> P (Abs u °° ts) |] ==> ∀t. size t = n --> P t" proof - case rule_context show ?thesis apply (induct_tac n rule: nat_less_induct) apply (rule allI) apply (cut_tac t = t in ex_head_tail) apply clarify apply (erule disjE) apply clarify apply (rule prems) apply clarify apply (erule allE, erule impE) prefer 2 apply (erule allE, erule mp, rule refl) apply simp apply (rule lem0) apply force apply (rule elem_le_sum) apply force apply clarify apply (rule prems) apply (erule allE, erule impE) prefer 2 apply (erule allE, erule mp, rule refl) apply simp apply clarify apply (erule allE, erule impE) prefer 2 apply (erule allE, erule mp, rule refl) apply simp apply (rule le_imp_less_Suc) apply (rule trans_le_add1) apply (rule trans_le_add2) apply (rule elem_le_sum) apply force done qed theorem Apps_dB_induct: "[| !!n ts. ∀t ∈ set ts. P t ==> P (Var n °° ts); !!u ts. [| P u; ∀t ∈ set ts. P t |] ==> P (Abs u °° ts) |] ==> P t" proof - case rule_context show ?thesis apply (rule_tac t = t in lem) prefer 3 apply (rule refl) apply (assumption | rule prems)+ done qed end
lemma apps_eq_tail_conv:
(r °° ts = s °° ts) = (r = s)
lemma Var_eq_apps_conv:
(Var m = s °° ss) = (Var m = s ∧ ss = [])
lemma Var_apps_eq_Var_apps_conv:
(Var m °° rs = Var n °° ss) = (m = n ∧ rs = ss)
lemma App_eq_foldl_conv:
(r ° s = t °° ts) = (if ts = [] then r ° s = t else ∃ss. ts = ss @ [s] ∧ r = t °° ss)
lemma Abs_eq_apps_conv:
(Abs r = s °° ss) = (Abs r = s ∧ ss = [])
lemma apps_eq_Abs_conv:
(s °° ss = Abs r) = (s = Abs r ∧ ss = [])
lemma Abs_apps_eq_Abs_apps_conv:
(Abs r °° rs = Abs s °° ss) = (r = s ∧ rs = ss)
lemma Abs_App_neq_Var_apps:
∀s t. Abs s ° t ≠ Var n °° ss
lemma Var_apps_neq_Abs_apps:
Var n °° ts ≠ Abs r °° ss
lemma ex_head_tail:
∃ts h. t = h °° ts ∧ ((∃n. h = Var n) ∨ (∃u. h = Abs u))
lemma size_apps:
size (r °° rs) = size r + foldl op + 0 (map size rs) + length rs
lemma lem0:
[| 0 < k; m ≤ n |] ==> m < n + k
lemma lift_map:
lift (t °° ts) i = lift t i °° map (%t. lift t i) ts
lemma subst_map:
(t °° ts)[u/i] = t[u/i] °° map (%t. t[u/i]) ts
lemma app_last:
(t °° ts) ° u = t °° (ts @ [u])
lemma lem:
[| !!n ts. Ball (set ts) P ==> P (Var n °° ts); !!u ts. [| P u; Ball (set ts) P |] ==> P (Abs u °° ts); size t = n |] ==> P t
theorem Apps_dB_induct:
[| !!n ts. ∀t∈set ts. P t ==> P (Var n °° ts); !!u ts. [| P u; ∀t∈set ts. P t |] ==> P (Abs u °° ts) |] ==> P t