1(* Title: HOL/Proofs/Lambda/ListBeta.thy 2 Author: Tobias Nipkow 3 Copyright 1998 TU Muenchen 4*) 5 6section \<open>Lifting beta-reduction to lists\<close> 7 8theory ListBeta imports ListApplication ListOrder begin 9 10text \<open> 11 Lifting beta-reduction to lists of terms, reducing exactly one element. 12\<close> 13 14abbreviation 15 list_beta :: "dB list => dB list => bool" (infixl "=>" 50) where 16 "rs => ss == step1 beta rs ss" 17 18lemma head_Var_reduction: 19 "Var n \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss" 20 apply (induct u == "Var n \<degree>\<degree> rs" v arbitrary: rs set: beta) 21 apply simp 22 apply (rule_tac xs = rs in rev_exhaust) 23 apply simp 24 apply (atomize, force intro: append_step1I) 25 apply (rule_tac xs = rs in rev_exhaust) 26 apply simp 27 apply (auto 0 3 intro: disjI2 [THEN append_step1I]) 28 done 29 30lemma apps_betasE [elim!]: 31 assumes major: "r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> s" 32 and cases: "!!r'. [| r \<rightarrow>\<^sub>\<beta> r'; s = r' \<degree>\<degree> rs |] ==> R" 33 "!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R" 34 "!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R" 35 shows R 36proof - 37 from major have 38 "(\<exists>r'. r \<rightarrow>\<^sub>\<beta> r' \<and> s = r' \<degree>\<degree> rs) \<or> 39 (\<exists>rs'. rs => rs' \<and> s = r \<degree>\<degree> rs') \<or> 40 (\<exists>t u us. r = Abs t \<and> rs = u # us \<and> s = t[u/0] \<degree>\<degree> us)" 41 apply (induct u == "r \<degree>\<degree> rs" s arbitrary: r rs set: beta) 42 apply (case_tac r) 43 apply simp 44 apply (simp add: App_eq_foldl_conv) 45 apply (split if_split_asm) 46 apply simp 47 apply blast 48 apply simp 49 apply (simp add: App_eq_foldl_conv) 50 apply (split if_split_asm) 51 apply simp 52 apply simp 53 apply (drule App_eq_foldl_conv [THEN iffD1]) 54 apply (split if_split_asm) 55 apply simp 56 apply blast 57 apply (force intro!: disjI1 [THEN append_step1I]) 58 apply (drule App_eq_foldl_conv [THEN iffD1]) 59 apply (split if_split_asm) 60 apply simp 61 apply blast 62 apply (clarify, auto 0 3 intro!: exI intro: append_step1I) 63 done 64 with cases show ?thesis by blast 65qed 66 67lemma apps_preserves_beta [simp]: 68 "r \<rightarrow>\<^sub>\<beta> s ==> r \<degree>\<degree> ss \<rightarrow>\<^sub>\<beta> s \<degree>\<degree> ss" 69 by (induct ss rule: rev_induct) auto 70 71lemma apps_preserves_beta2 [simp]: 72 "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r \<degree>\<degree> ss \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree>\<degree> ss" 73 apply (induct set: rtranclp) 74 apply blast 75 apply (blast intro: apps_preserves_beta rtranclp.rtrancl_into_rtrancl) 76 done 77 78lemma apps_preserves_betas [simp]: 79 "rs => ss \<Longrightarrow> r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> r \<degree>\<degree> ss" 80 apply (induct rs arbitrary: ss rule: rev_induct) 81 apply simp 82 apply simp 83 apply (rule_tac xs = ss in rev_exhaust) 84 apply simp 85 apply simp 86 apply (drule Snoc_step1_SnocD) 87 apply blast 88 done 89 90end 91