author  haftmann 
Sat, 05 Jul 2014 11:01:53 +0200  
changeset 57514  bdc2c6b40bf2 
parent 39157  b98909faaea8 
child 58889  5b7a9633cfa8 
permissions  rwrr 
39157
b98909faaea8
more explicit HOLProofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
36862
diff
changeset

1 
(* Title: HOL/Proofs/Lambda/ListBeta.thy 
5261  2 
Author: Tobias Nipkow 
3 
Copyright 1998 TU Muenchen 

4 
*) 

5 

9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

6 
header {* Lifting betareduction to lists *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

7 

16417  8 
theory ListBeta imports ListApplication ListOrder begin 
9762  9 

9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

10 
text {* 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

11 
Lifting betareduction to lists of terms, reducing exactly one element. 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

12 
*} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

13 

19363  14 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20503
diff
changeset

15 
list_beta :: "dB list => dB list => bool" (infixl "=>" 50) where 
22271  16 
"rs => ss == step1 beta rs ss" 
9762  17 

18513  18 
lemma head_Var_reduction: 
22271  19 
"Var n \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss" 
20503  20 
apply (induct u == "Var n \<degree>\<degree> rs" v arbitrary: rs set: beta) 
9762  21 
apply simp 
22 
apply (rule_tac xs = rs in rev_exhaust) 

23 
apply simp 

18513  24 
apply (atomize, force intro: append_step1I) 
9762  25 
apply (rule_tac xs = rs in rev_exhaust) 
26 
apply simp 

9771  27 
apply (auto 0 3 intro: disjI2 [THEN append_step1I]) 
9762  28 
done 
29 

18513  30 
lemma apps_betasE [elim!]: 
22271  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" 

18513  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 

36 
proof  

37 
from major have 

22271  38 
"(\<exists>r'. r \<rightarrow>\<^sub>\<beta> r' \<and> s = r' \<degree>\<degree> rs) \<or> 
18513  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)" 

20503  41 
apply (induct u == "r \<degree>\<degree> rs" s arbitrary: r rs set: beta) 
18513  42 
apply (case_tac r) 
43 
apply simp 

44 
apply (simp add: App_eq_foldl_conv) 

45 
apply (split split_if_asm) 

46 
apply simp 

47 
apply blast 

48 
apply simp 

49 
apply (simp add: App_eq_foldl_conv) 

50 
apply (split split_if_asm) 

51 
apply simp 

9762  52 
apply simp 
18513  53 
apply (drule App_eq_foldl_conv [THEN iffD1]) 
10653  54 
apply (split split_if_asm) 
9762  55 
apply simp 
56 
apply blast 

18513  57 
apply (force intro!: disjI1 [THEN append_step1I]) 
58 
apply (drule App_eq_foldl_conv [THEN iffD1]) 

10653  59 
apply (split split_if_asm) 
9762  60 
apply simp 
18513  61 
apply blast 
62 
apply (clarify, auto 0 3 intro!: exI intro: append_step1I) 

63 
done 

64 
with cases show ?thesis by blast 

65 
qed 

9762  66 

67 
lemma apps_preserves_beta [simp]: 

22271  68 
"r \<rightarrow>\<^sub>\<beta> s ==> r \<degree>\<degree> ss \<rightarrow>\<^sub>\<beta> s \<degree>\<degree> ss" 
18241  69 
by (induct ss rule: rev_induct) auto 
9762  70 

71 
lemma apps_preserves_beta2 [simp]: 

12011  72 
"r >> s ==> r \<degree>\<degree> ss >> s \<degree>\<degree> ss" 
23750  73 
apply (induct set: rtranclp) 
9762  74 
apply blast 
23750  75 
apply (blast intro: apps_preserves_beta rtranclp.rtrancl_into_rtrancl) 
9762  76 
done 
77 

18241  78 
lemma apps_preserves_betas [simp]: 
22271  79 
"rs => ss \<Longrightarrow> r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> r \<degree>\<degree> ss" 
20503  80 
apply (induct rs arbitrary: ss rule: rev_induct) 
9762  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 

5261  89 

11639  90 
end 