author  haftmann 
Sat, 05 Jul 2014 11:01:53 +0200  
changeset 57514  bdc2c6b40bf2 
parent 57442  2373b4c61111 
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/ParRed.thy 
1120  2 
Author: Tobias Nipkow 
3 
Copyright 1995 TU Muenchen 

4 

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

5 
Properties of => and "cd", in particular the diamond property of => and 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

6 
confluence of beta. 
1120  7 
*) 
8 

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

9 
header {* Parallel reduction and a complete developments *} 
1120  10 

16417  11 
theory ParRed imports Lambda Commutation begin 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

12 

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

13 

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

14 
subsection {* Parallel reduction *} 
1120  15 

23750  16 
inductive par_beta :: "[dB, dB] => bool" (infixl "=>" 50) 
22271  17 
where 
18 
var [simp, intro!]: "Var n => Var n" 

19 
 abs [simp, intro!]: "s => t ==> Abs s => Abs t" 

20 
 app [simp, intro!]: "[ s => s'; t => t' ] ==> s \<degree> t => s' \<degree> t'" 

21 
 beta [simp, intro!]: "[ s => s'; t => t' ] ==> (Abs s) \<degree> t => s'[t'/0]" 

1120  22 

23750  23 
inductive_cases par_beta_cases [elim!]: 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

24 
"Var n => t" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

25 
"Abs s => Abs t" 
12011  26 
"(Abs s) \<degree> t => u" 
27 
"s \<degree> t => u" 

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

28 
"Abs s => t" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

29 

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

30 

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

31 
subsection {* Inclusions *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

32 

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

33 
text {* @{text "beta \<subseteq> par_beta \<subseteq> beta^*"} \medskip *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

34 

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

35 
lemma par_beta_varL [simp]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

36 
"(Var n => t) = (t = Var n)" 
18241  37 
by blast 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

38 

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

39 
lemma par_beta_refl [simp]: "t => t" (* par_beta_refl [intro!] causes search to blow up *) 
18241  40 
by (induct t) simp_all 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

41 

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

42 
lemma beta_subset_par_beta: "beta <= par_beta" 
22271  43 
apply (rule predicate2I) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

44 
apply (erule beta.induct) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

45 
apply (blast intro!: par_beta_refl)+ 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

46 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

47 

22271  48 
lemma par_beta_subset_beta: "par_beta <= beta^**" 
49 
apply (rule predicate2I) 

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

50 
apply (erule par_beta.induct) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

51 
apply blast 
23750  52 
apply (blast del: rtranclp.rtrancl_refl intro: rtranclp.rtrancl_into_rtrancl)+ 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

53 
 {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

54 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

55 

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

56 

25972  57 
subsection {* Misc properties of @{text "par_beta"} *} 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

58 

18241  59 
lemma par_beta_lift [simp]: 
60 
"t => t' \<Longrightarrow> lift t n => lift t' n" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
39157
diff
changeset

61 
by (induct t arbitrary: t' n) fastforce+ 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

62 

18241  63 
lemma par_beta_subst: 
64 
"s => s' \<Longrightarrow> t => t' \<Longrightarrow> t[s/n] => t'[s'/n]" 

20503  65 
apply (induct t arbitrary: s s' t' n) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

66 
apply (simp add: subst_Var) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

67 
apply (erule par_beta_cases) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

68 
apply simp 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

69 
apply (simp add: subst_subst [symmetric]) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
39157
diff
changeset

70 
apply (fastforce intro!: par_beta_lift) 
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
39157
diff
changeset

71 
apply fastforce 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

72 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

73 

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

74 

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

75 
subsection {* Confluence (directly) *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

76 

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

77 
lemma diamond_par_beta: "diamond par_beta" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

78 
apply (unfold diamond_def commute_def square_def) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

79 
apply (rule impI [THEN allI [THEN allI]]) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

80 
apply (erule par_beta.induct) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

81 
apply (blast intro!: par_beta_subst)+ 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

82 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

83 

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

84 

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

85 
subsection {* Complete developments *} 
1120  86 

35440  87 
fun 
57442
2373b4c61111
removed obsolete Isar system commands  raw ML console is normally used for system tinkering;
wenzelm
parents:
44890
diff
changeset

88 
cd :: "dB => dB" 
35440  89 
where 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

90 
"cd (Var n) = Var n" 
35440  91 
 "cd (Var n \<degree> t) = Var n \<degree> cd t" 
92 
 "cd ((s1 \<degree> s2) \<degree> t) = cd (s1 \<degree> s2) \<degree> cd t" 

93 
 "cd (Abs u \<degree> t) = (cd u)[cd t/0]" 

94 
 "cd (Abs s) = Abs (cd s)" 

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

95 

18241  96 
lemma par_beta_cd: "s => t \<Longrightarrow> t => cd s" 
20503  97 
apply (induct s arbitrary: t rule: cd.induct) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

98 
apply auto 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

99 
apply (fast intro!: par_beta_subst) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

100 
done 
1120  101 

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

102 

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

103 
subsection {* Confluence (via complete developments) *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

104 

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

105 
lemma diamond_par_beta2: "diamond par_beta" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

106 
apply (unfold diamond_def commute_def square_def) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

107 
apply (blast intro: par_beta_cd) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

108 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

109 

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

110 
theorem beta_confluent: "confluent beta" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

111 
apply (rule diamond_par_beta2 diamond_to_confluence 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

112 
par_beta_subset_beta beta_subset_par_beta)+ 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

113 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
8624
diff
changeset

114 

11638  115 
end 