author  haftmann 
Sat, 05 Jul 2014 11:01:53 +0200  
changeset 57514  bdc2c6b40bf2 
parent 45605  a89b4bc311a5 
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:
33704
diff
changeset

1 
(* Title: HOL/Proofs/Lambda/NormalForm.thy 
24537
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

2 
Author: Stefan Berghofer, TU Muenchen, 2003 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

3 
*) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

4 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

5 
header {* Inductive characterization of lambda terms in normal form *} 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

6 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

7 
theory NormalForm 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

8 
imports ListBeta 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

9 
begin 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

10 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

11 
subsection {* Terms in normal form *} 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

12 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

13 
definition 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

14 
listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

15 
"listall P xs \<equiv> (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

16 

33704
6aeb8454efc1
add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature;
wenzelm
parents:
32960
diff
changeset

17 
declare listall_def [extraction_expand_def] 
24537
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

18 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

19 
theorem listall_nil: "listall P []" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

20 
by (simp add: listall_def) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

21 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

22 
theorem listall_nil_eq [simp]: "listall P [] = True" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

23 
by (iprover intro: listall_nil) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

24 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

25 
theorem listall_cons: "P x \<Longrightarrow> listall P xs \<Longrightarrow> listall P (x # xs)" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

26 
apply (simp add: listall_def) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

27 
apply (rule allI impI)+ 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

28 
apply (case_tac i) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

29 
apply simp+ 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

30 
done 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

31 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

32 
theorem listall_cons_eq [simp]: "listall P (x # xs) = (P x \<and> listall P xs)" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

33 
apply (rule iffI) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

34 
prefer 2 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

35 
apply (erule conjE) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

36 
apply (erule listall_cons) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

37 
apply assumption 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

38 
apply (unfold listall_def) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

39 
apply (rule conjI) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

40 
apply (erule_tac x=0 in allE) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

41 
apply simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

42 
apply simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

43 
apply (rule allI) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

44 
apply (erule_tac x="Suc i" in allE) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

45 
apply simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

46 
done 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

47 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

48 
lemma listall_conj1: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall P xs" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

49 
by (induct xs) simp_all 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

50 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

51 
lemma listall_conj2: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall Q xs" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

52 
by (induct xs) simp_all 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

53 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

54 
lemma listall_app: "listall P (xs @ ys) = (listall P xs \<and> listall P ys)" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

55 
apply (induct xs) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

56 
apply (rule iffI, simp, simp) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

57 
apply (rule iffI, simp, simp) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

58 
done 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

59 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

60 
lemma listall_snoc [simp]: "listall P (xs @ [x]) = (listall P xs \<and> P x)" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

61 
apply (rule iffI) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

62 
apply (simp add: listall_app)+ 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

63 
done 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

64 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

65 
lemma listall_cong [cong, extraction_expand]: 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

66 
"xs = ys \<Longrightarrow> listall P xs = listall P ys" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

67 
 {* Currently needed for strange technical reasons *} 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

68 
by (unfold listall_def) simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

69 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

70 
text {* 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

71 
@{term "listsp"} is equivalent to @{term "listall"}, but cannot be 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

72 
used for program extraction. 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

73 
*} 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

74 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

75 
lemma listall_listsp_eq: "listall P xs = listsp P xs" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

76 
by (induct xs) (auto intro: listsp.intros) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

77 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

78 
inductive NF :: "dB \<Rightarrow> bool" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

79 
where 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

80 
App: "listall NF ts \<Longrightarrow> NF (Var x \<degree>\<degree> ts)" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

81 
 Abs: "NF t \<Longrightarrow> NF (Abs t)" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

82 
monos listall_def 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

83 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

84 
lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

85 
apply (induct m) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

86 
apply (case_tac n) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

87 
apply (case_tac [3] n) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

88 
apply (simp only: nat.simps, iprover?)+ 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

89 
done 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

90 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

91 
lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

92 
apply (induct m) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

93 
apply (case_tac n) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

94 
apply (case_tac [3] n) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

95 
apply (simp del: simp_thms, iprover?)+ 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

96 
done 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

97 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

98 
lemma App_NF_D: assumes NF: "NF (Var n \<degree>\<degree> ts)" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

99 
shows "listall NF ts" using NF 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

100 
by cases simp_all 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

101 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

102 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

103 
subsection {* Properties of @{text NF} *} 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

104 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

105 
lemma Var_NF: "NF (Var n)" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

106 
apply (subgoal_tac "NF (Var n \<degree>\<degree> [])") 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

107 
apply simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

108 
apply (rule NF.App) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

109 
apply simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

110 
done 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

111 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

112 
lemma Abs_NF: 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

113 
assumes NF: "NF (Abs t \<degree>\<degree> ts)" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

114 
shows "ts = []" using NF 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

115 
proof cases 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

116 
case (App us i) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

117 
thus ?thesis by (simp add: Var_apps_neq_Abs_apps [THEN not_sym]) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

118 
next 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

119 
case (Abs u) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

120 
thus ?thesis by simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

121 
qed 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

122 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

123 
lemma subst_terms_NF: "listall NF ts \<Longrightarrow> 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

124 
listall (\<lambda>t. \<forall>i j. NF (t[Var i/j])) ts \<Longrightarrow> 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

125 
listall NF (map (\<lambda>t. t[Var i/j]) ts)" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

126 
by (induct ts) simp_all 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

127 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

128 
lemma subst_Var_NF: "NF t \<Longrightarrow> NF (t[Var i/j])" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

129 
apply (induct arbitrary: i j set: NF) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

130 
apply simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

131 
apply (frule listall_conj1) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

132 
apply (drule listall_conj2) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

133 
apply (drule_tac i=i and j=j in subst_terms_NF) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

134 
apply assumption 
45605  135 
apply (rule_tac m1=x and n1=j in nat_eq_dec [THEN disjE]) 
24537
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

136 
apply simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

137 
apply (erule NF.App) 
45605  138 
apply (rule_tac m1=j and n1=x in nat_le_dec [THEN disjE]) 
24537
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

139 
apply simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

140 
apply (iprover intro: NF.App) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

141 
apply simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

142 
apply (iprover intro: NF.App) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

143 
apply simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

144 
apply (iprover intro: NF.Abs) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

145 
done 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

146 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

147 
lemma app_Var_NF: "NF t \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

148 
apply (induct set: NF) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

149 
apply (simplesubst app_last) {*Using @{text subst} makes extraction fail*} 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

150 
apply (rule exI) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

151 
apply (rule conjI) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

152 
apply (rule rtranclp.rtrancl_refl) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

153 
apply (rule NF.App) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

154 
apply (drule listall_conj1) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

155 
apply (simp add: listall_app) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

156 
apply (rule Var_NF) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

157 
apply (rule exI) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

158 
apply (rule conjI) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

159 
apply (rule rtranclp.rtrancl_into_rtrancl) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

160 
apply (rule rtranclp.rtrancl_refl) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

161 
apply (rule beta) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

162 
apply (erule subst_Var_NF) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

163 
done 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

164 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

165 
lemma lift_terms_NF: "listall NF ts \<Longrightarrow> 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

166 
listall (\<lambda>t. \<forall>i. NF (lift t i)) ts \<Longrightarrow> 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

167 
listall NF (map (\<lambda>t. lift t i) ts)" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

168 
by (induct ts) simp_all 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

169 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

170 
lemma lift_NF: "NF t \<Longrightarrow> NF (lift t i)" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

171 
apply (induct arbitrary: i set: NF) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

172 
apply (frule listall_conj1) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

173 
apply (drule listall_conj2) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

174 
apply (drule_tac i=i in lift_terms_NF) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

175 
apply assumption 
45605  176 
apply (rule_tac m1=x and n1=i in nat_le_dec [THEN disjE]) 
24537
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

177 
apply simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

178 
apply (rule NF.App) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

179 
apply assumption 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

180 
apply simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

181 
apply (rule NF.App) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

182 
apply assumption 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

183 
apply simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

184 
apply (rule NF.Abs) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

185 
apply simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

186 
done 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

187 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

188 
text {* 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

189 
@{term NF} characterizes exactly the terms that are in normal form. 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

190 
*} 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

191 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

192 
lemma NF_eq: "NF t = (\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t')" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

193 
proof 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

194 
assume "NF t" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

195 
then have "\<And>t'. \<not> t \<rightarrow>\<^sub>\<beta> t'" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

196 
proof induct 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

197 
case (App ts t) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

198 
show ?case 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

199 
proof 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

200 
assume "Var t \<degree>\<degree> ts \<rightarrow>\<^sub>\<beta> t'" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

201 
then obtain rs where "ts => rs" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24537
diff
changeset

202 
by (iprover dest: head_Var_reduction) 
24537
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

203 
with App show False 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24537
diff
changeset

204 
by (induct rs arbitrary: ts) auto 
24537
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

205 
qed 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

206 
next 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

207 
case (Abs t) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

208 
show ?case 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

209 
proof 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

210 
assume "Abs t \<rightarrow>\<^sub>\<beta> t'" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

211 
then show False using Abs by cases simp_all 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

212 
qed 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

213 
qed 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

214 
then show "\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t'" .. 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

215 
next 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

216 
assume H: "\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t'" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

217 
then show "NF t" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

218 
proof (induct t rule: Apps_dB_induct) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

219 
case (1 n ts) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

220 
then have "\<forall>ts'. \<not> ts => ts'" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

221 
by (iprover intro: apps_preserves_betas) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

222 
with 1(1) have "listall NF ts" 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

223 
by (induct ts) auto 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

224 
then show ?case by (rule NF.App) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

225 
next 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

226 
case (2 u ts) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

227 
show ?case 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

228 
proof (cases ts) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

229 
case Nil 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

230 
from 2 have "\<forall>u'. \<not> u \<rightarrow>\<^sub>\<beta> u'" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24537
diff
changeset

231 
by (auto intro: apps_preserves_beta) 
24537
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

232 
then have "NF u" by (rule 2) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

233 
then have "NF (Abs u)" by (rule NF.Abs) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

234 
with Nil show ?thesis by simp 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

235 
next 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

236 
case (Cons r rs) 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

237 
have "Abs u \<degree> r \<rightarrow>\<^sub>\<beta> u[r/0]" .. 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

238 
then have "Abs u \<degree> r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> u[r/0] \<degree>\<degree> rs" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24537
diff
changeset

239 
by (rule apps_preserves_beta) 
24537
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

240 
with Cons have "Abs u \<degree>\<degree> ts \<rightarrow>\<^sub>\<beta> u[r/0] \<degree>\<degree> rs" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24537
diff
changeset

241 
by simp 
24537
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

242 
with 2 show ?thesis by iprover 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

243 
qed 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

244 
qed 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

245 
qed 
57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

246 

57c7dfaa0153
Definition of normal forms (taken from theory WeakNorm).
berghofe
parents:
diff
changeset

247 
end 