author  wenzelm 
Mon, 04 Sep 2000 11:21:24 +0200  
changeset 9827  ce6e22ff89c3 
parent 9811  39ffdb8cab03 
child 9906  5c027cca6262 
permissions  rwrr 
5261  1 
(* Title: HOL/Lambda/ListBeta.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 1998 TU Muenchen 

5 
*) 

6 

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

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

8 

9762  9 
theory ListBeta = ListApplication + ListOrder: 
10 

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

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

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

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

14 

9762  15 
syntax 
16 
"_list_beta" :: "dB => dB => bool" (infixl "=>" 50) 

17 
translations 

9827  18 
"rs => ss" == "(rs, ss) : step1 beta" 
9762  19 

20 
lemma head_Var_reduction_aux: 

21 
"v > v' ==> \<forall>rs. v = Var n $$ rs > (\<exists>ss. rs => ss \<and> v' = Var n $$ ss)" 

22 
apply (erule beta.induct) 

23 
apply simp 

24 
apply (rule allI) 

25 
apply (rule_tac xs = rs in rev_exhaust) 

26 
apply simp 

27 
apply (force intro: append_step1I) 

28 
apply (rule allI) 

29 
apply (rule_tac xs = rs in rev_exhaust) 

30 
apply simp 

9771  31 
apply (auto 0 3 intro: disjI2 [THEN append_step1I]) 
9762  32 
done 
33 

34 
lemma head_Var_reduction: 

35 
"Var n $$ rs > v ==> (\<exists>ss. rs => ss \<and> v = Var n $$ ss)" 

36 
apply (drule head_Var_reduction_aux) 

37 
apply blast 

38 
done 

5261  39 

9762  40 
lemma apps_betasE_aux: 
41 
"u > u' ==> \<forall>r rs. u = r $$ rs > 

9771  42 
((\<exists>r'. r > r' \<and> u' = r' $$ rs) \<or> 
43 
(\<exists>rs'. rs => rs' \<and> u' = r $$ rs') \<or> 

44 
(\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] $$ ts))" 

9762  45 
apply (erule beta.induct) 
46 
apply (clarify del: disjCI) 

47 
apply (case_tac r) 

48 
apply simp 

49 
apply (simp add: App_eq_foldl_conv) 

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

50 
apply (split (asm) split_if_asm) 
9762  51 
apply simp 
52 
apply blast 

53 
apply simp 

54 
apply (simp add: App_eq_foldl_conv) 

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

55 
apply (split (asm) split_if_asm) 
9762  56 
apply simp 
57 
apply simp 

58 
apply (clarify del: disjCI) 

59 
apply (drule App_eq_foldl_conv [THEN iffD1]) 

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

60 
apply (split (asm) split_if_asm) 
9762  61 
apply simp 
62 
apply blast 

63 
apply (force intro: disjI1 [THEN append_step1I]) 

64 
apply (clarify del: disjCI) 

65 
apply (drule App_eq_foldl_conv [THEN iffD1]) 

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

66 
apply (split (asm) split_if_asm) 
9762  67 
apply simp 
68 
apply blast 

9771  69 
apply (auto 0 3 intro: disjI2 [THEN append_step1I]) 
9762  70 
done 
71 

72 
lemma apps_betasE [elim!]: 

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

73 
"[ r $$ rs > s; !!r'. [ r > r'; s = r' $$ rs ] ==> R; 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

74 
!!rs'. [ rs => rs'; s = r $$ rs' ] ==> R; 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

75 
!!t u us. [ r = Abs t; rs = u # us; s = t[u/0] $$ us ] ==> R ] 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

76 
==> R" 
9762  77 
proof  
78 
assume major: "r $$ rs > s" 

79 
case antecedent 

80 
show ?thesis 

81 
apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec]) 

82 
apply (assumption  rule refl  erule prems exE conjE impE disjE)+ 

83 
done 

84 
qed 

85 

86 
lemma apps_preserves_beta [simp]: 

87 
"r > s ==> r $$ ss > s $$ ss" 

88 
apply (induct_tac ss rule: rev_induct) 

89 
apply auto 

90 
done 

91 

92 
lemma apps_preserves_beta2 [simp]: 

93 
"r >> s ==> r $$ ss >> s $$ ss" 

94 
apply (erule rtrancl_induct) 

95 
apply blast 

96 
apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl) 

97 
done 

98 

99 
lemma apps_preserves_betas [rulify, simp]: 

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

100 
"\<forall>ss. rs => ss > r $$ rs > r $$ ss" 
9762  101 
apply (induct_tac rs rule: rev_induct) 
102 
apply simp 

103 
apply simp 

104 
apply clarify 

105 
apply (rule_tac xs = ss in rev_exhaust) 

106 
apply simp 

107 
apply simp 

108 
apply (drule Snoc_step1_SnocD) 

109 
apply blast 

110 
done 

5261  111 

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

112 
end 