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/InductTermi.thy 
5261  2 
Author: Tobias Nipkow 
3 
Copyright 1998 TU Muenchen 

4 

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

5 
Inductive characterization of terminating lambda terms. Goes back to 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

6 
Raamsdonk & Severi. On normalization. CWI TR CSR9545, 1995. Also 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

7 
rediscovered by Matthes and Joachimski. 
5261  8 
*) 
9 

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

10 
header {* Inductive characterization of terminating lambda terms *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

11 

16417  12 
theory InductTermi imports ListBeta begin 
5261  13 

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

14 
subsection {* Terminating lambda terms *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9771
diff
changeset

15 

23750  16 
inductive IT :: "dB => bool" 
22271  17 
where 
18 
Var [intro]: "listsp IT rs ==> IT (Var n \<degree>\<degree> rs)" 

19 
 Lambda [intro]: "IT r ==> IT (Abs r)" 

20 
 Beta [intro]: "IT ((r[s/0]) \<degree>\<degree> ss) ==> IT s ==> IT ((Abs r \<degree> s) \<degree>\<degree> ss)" 

9716  21 

22 

25972  23 
subsection {* Every term in @{text "IT"} terminates *} 
9716  24 

9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset

25 
lemma double_induction_lemma [rule_format]: 
23750  26 
"termip beta s ==> \<forall>t. termip beta t > 
27 
(\<forall>r ss. t = r[s/0] \<degree>\<degree> ss > termip beta (Abs r \<degree> s \<degree>\<degree> ss))" 

28 
apply (erule accp_induct) 

9716  29 
apply (rule allI) 
30 
apply (rule impI) 

18513  31 
apply (erule thin_rl) 
23750  32 
apply (erule accp_induct) 
9716  33 
apply clarify 
23750  34 
apply (rule accp.accI) 
9771  35 
apply (safe elim!: apps_betasE) 
9716  36 
apply (blast intro: subst_preserves_beta apps_preserves_beta) 
23750  37 
apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtranclp_converseI 
38 
dest: accp_downwards) (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *) 

9716  39 
apply (blast dest: apps_preserves_betas) 
40 
done 

41 

23750  42 
lemma IT_implies_termi: "IT t ==> termip beta t" 
18241  43 
apply (induct set: IT) 
23750  44 
apply (drule rev_predicate1D [OF _ listsp_mono [where B="termip beta"]]) 
26806  45 
apply (fast intro!: predicate1I) 
9716  46 
apply (drule lists_accD) 
23750  47 
apply (erule accp_induct) 
48 
apply (rule accp.accI) 

9716  49 
apply (blast dest: head_Var_reduction) 
23750  50 
apply (erule accp_induct) 
51 
apply (rule accp.accI) 

9716  52 
apply blast 
53 
apply (blast intro: double_induction_lemma) 

54 
done 

55 

56 

25972  57 
subsection {* Every terminating term is in @{text "IT"} *} 
9716  58 

18241  59 
declare Var_apps_neq_Abs_apps [symmetric, simp] 
9716  60 

12011  61 
lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts" 
18241  62 
by (simp add: foldl_Cons [symmetric] del: foldl_Cons) 
9716  63 

64 
lemma [simp]: 

12011  65 
"(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')" 
18241  66 
by (simp add: foldl_Cons [symmetric] del: foldl_Cons) 
9716  67 

23750  68 
inductive_cases [elim!]: 
22271  69 
"IT (Var n \<degree>\<degree> ss)" 
70 
"IT (Abs t)" 

71 
"IT (Abs r \<degree> s \<degree>\<degree> ts)" 

9716  72 

23750  73 
theorem termi_implies_IT: "termip beta r ==> IT r" 
74 
apply (erule accp_induct) 

9716  75 
apply (rename_tac r) 
76 
apply (erule thin_rl) 

77 
apply (erule rev_mp) 

78 
apply simp 

79 
apply (rule_tac t = r in Apps_dB_induct) 

80 
apply clarify 

81 
apply (rule IT.intros) 

82 
apply clarify 

83 
apply (drule bspec, assumption) 

84 
apply (erule mp) 

85 
apply clarify 

22271  86 
apply (drule_tac r=beta in conversepI) 
87 
apply (drule_tac r="beta^1" in ex_step1I, assumption) 

9716  88 
apply clarify 
89 
apply (rename_tac us) 

12011  90 
apply (erule_tac x = "Var n \<degree>\<degree> us" in allE) 
9716  91 
apply force 
92 
apply (rename_tac u ts) 

93 
apply (case_tac ts) 

94 
apply simp 

11946  95 
apply blast 
9716  96 
apply (rename_tac s ss) 
97 
apply simp 

98 
apply clarify 

99 
apply (rule IT.intros) 

100 
apply (blast intro: apps_preserves_beta) 

101 
apply (erule mp) 

102 
apply clarify 

103 
apply (rename_tac t) 

12011  104 
apply (erule_tac x = "Abs u \<degree> t \<degree>\<degree> ss" in allE) 
9716  105 
apply force 
106 
done 

5261  107 

11639  108 
end 