--- a/src/HOL/Lambda/Eta.thy Wed Oct 31 22:04:29 2001 +0100
+++ b/src/HOL/Lambda/Eta.thy Wed Oct 31 22:05:37 2001 +0100
@@ -15,7 +15,7 @@
free :: "dB => nat => bool"
primrec
"free (Var j) i = (j = i)"
- "free (s $ t) i = (free s i \<or> free t i)"
+ "free (s \<degree> t) i = (free s i \<or> free t i)"
"free (Abs s) i = free s (i + 1)"
consts
@@ -32,14 +32,14 @@
inductive eta
intros
- eta [simp, intro]: "\<not> free s 0 ==> Abs (s $ Var 0) -e> s[dummy/0]"
- appL [simp, intro]: "s -e> t ==> s $ u -e> t $ u"
- appR [simp, intro]: "s -e> t ==> u $ s -e> u $ t"
+ eta [simp, intro]: "\<not> free s 0 ==> Abs (s \<degree> Var 0) -e> s[dummy/0]"
+ appL [simp, intro]: "s -e> t ==> s \<degree> u -e> t \<degree> u"
+ appR [simp, intro]: "s -e> t ==> u \<degree> s -e> u \<degree> t"
abs [simp, intro]: "s -e> t ==> Abs s -e> Abs t"
inductive_cases eta_cases [elim!]:
"Abs s -e> z"
- "s $ t -e> u"
+ "s \<degree> t -e> u"
"Var i -e> t"
@@ -118,18 +118,18 @@
apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
done
-lemma rtrancl_eta_AppL: "s -e>> s' ==> s $ t -e>> s' $ t"
+lemma rtrancl_eta_AppL: "s -e>> s' ==> s \<degree> t -e>> s' \<degree> t"
apply (erule rtrancl_induct)
apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
done
-lemma rtrancl_eta_AppR: "t -e>> t' ==> s $ t -e>> s $ t'"
+lemma rtrancl_eta_AppR: "t -e>> t' ==> s \<degree> t -e>> s \<degree> t'"
apply (erule rtrancl_induct)
apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
done
lemma rtrancl_eta_App:
- "[| s -e>> s'; t -e>> t' |] ==> s $ t -e>> s' $ t'"
+ "[| s -e>> s'; t -e>> t' |] ==> s \<degree> t -e>> s' \<degree> t'"
apply (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
done
@@ -189,7 +189,7 @@
subsection "Implicit definition of eta"
-text {* @{term "Abs (lift s 0 $ Var 0) -e> s"} *}
+text {* @{term "Abs (lift s 0 \<degree> Var 0) -e> s"} *}
lemma not_free_iff_lifted [rule_format]:
"\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
@@ -218,7 +218,7 @@
apply (rule iffI)
apply (elim conjE exE)
apply (rename_tac u1 u2)
- apply (rule_tac x = "u1 $ u2" in exI)
+ apply (rule_tac x = "u1 \<degree> u2" in exI)
apply simp
apply (erule exE)
apply (erule rev_mp)
@@ -244,8 +244,8 @@
done
theorem explicit_is_implicit:
- "(\<forall>s u. (\<not> free s 0) --> R (Abs (s $ Var 0)) (s[u/0])) =
- (\<forall>s. R (Abs (lift s 0 $ Var 0)) s)"
+ "(\<forall>s u. (\<not> free s 0) --> R (Abs (s \<degree> Var 0)) (s[u/0])) =
+ (\<forall>s. R (Abs (lift s 0 \<degree> Var 0)) s)"
apply (auto simp add: not_free_iff_lifted)
done
--- a/src/HOL/Lambda/InductTermi.thy Wed Oct 31 22:04:29 2001 +0100
+++ b/src/HOL/Lambda/InductTermi.thy Wed Oct 31 22:05:37 2001 +0100
@@ -19,16 +19,16 @@
inductive IT
intros
- Var [intro]: "rs : lists IT ==> Var n $$ rs : IT"
+ Var [intro]: "rs : lists IT ==> Var n \<degree>\<degree> rs : IT"
Lambda [intro]: "r : IT ==> Abs r : IT"
- Beta [intro]: "(r[s/0]) $$ ss : IT ==> s : IT ==> (Abs r $ s) $$ ss : IT"
+ Beta [intro]: "(r[s/0]) \<degree>\<degree> ss : IT ==> s : IT ==> (Abs r \<degree> s) \<degree>\<degree> ss : IT"
subsection {* Every term in IT terminates *}
lemma double_induction_lemma [rule_format]:
"s : termi beta ==> \<forall>t. t : termi beta -->
- (\<forall>r ss. t = r[s/0] $$ ss --> Abs r $ s $$ ss : termi beta)"
+ (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> Abs r \<degree> s \<degree>\<degree> ss : termi beta)"
apply (erule acc_induct)
apply (erule thin_rl)
apply (rule allI)
@@ -65,19 +65,19 @@
declare Var_apps_neq_Abs_apps [THEN not_sym, simp]
-lemma [simp, THEN not_sym, simp]: "Var n $$ ss \<noteq> Abs r $ s $$ ts"
+lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts"
apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
done
lemma [simp]:
- "(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r = r' \<and> s = s' \<and> ss = ss')"
+ "(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')"
apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
done
inductive_cases [elim!]:
- "Var n $$ ss : IT"
+ "Var n \<degree>\<degree> ss : IT"
"Abs t : IT"
- "Abs r $ s $$ ts : IT"
+ "Abs r \<degree> s \<degree>\<degree> ts : IT"
theorem termi_implies_IT: "r : termi beta ==> r : IT"
apply (erule acc_induct)
@@ -96,7 +96,7 @@
apply (drule ex_step1I, assumption)
apply clarify
apply (rename_tac us)
- apply (erule_tac x = "Var n $$ us" in allE)
+ apply (erule_tac x = "Var n \<degree>\<degree> us" in allE)
apply force
apply (rename_tac u ts)
apply (case_tac ts)
@@ -110,7 +110,7 @@
apply (erule mp)
apply clarify
apply (rename_tac t)
- apply (erule_tac x = "Abs u $ t $$ ss" in allE)
+ apply (erule_tac x = "Abs u \<degree> t \<degree>\<degree> ss" in allE)
apply force
done
--- a/src/HOL/Lambda/Lambda.thy Wed Oct 31 22:04:29 2001 +0100
+++ b/src/HOL/Lambda/Lambda.thy Wed Oct 31 22:05:37 2001 +0100
@@ -13,25 +13,22 @@
datatype dB =
Var nat
- | App dB dB (infixl "$" 200)
+ | App dB dB (infixl "\<degree>" 200)
| Abs dB
-syntax (symbols)
- App :: "dB => dB => dB" (infixl "\<^sub>\<degree>" 200)
-
consts
subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300)
lift :: "[dB, nat] => dB"
primrec
"lift (Var i) k = (if i < k then Var i else Var (i + 1))"
- "lift (s $ t) k = lift s k $ lift t k"
+ "lift (s \<degree> t) k = lift s k \<degree> lift t k"
"lift (Abs s) k = Abs (lift s (k + 1))"
primrec (* FIXME base names *)
subst_Var: "(Var i)[s/k] =
(if k < i then Var (i - 1) else if i = k then s else Var i)"
- subst_App: "(t $ u)[s/k] = t[s/k] $ u[s/k]"
+ subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
declare subst_Var [simp del]
@@ -44,13 +41,13 @@
primrec
"liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
- "liftn n (s $ t) k = liftn n s k $ liftn n t k"
+ "liftn n (s \<degree> t) k = liftn n s k \<degree> liftn n t k"
"liftn n (Abs s) k = Abs (liftn n s (k + 1))"
primrec
"substn (Var i) s k =
(if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)"
- "substn (t $ u) s k = substn t s k $ substn u s k"
+ "substn (t \<degree> u) s k = substn t s k \<degree> substn u s k"
"substn (Abs t) s k = Abs (substn t s (k + 1))"
@@ -68,15 +65,15 @@
inductive beta
intros
- beta [simp, intro!]: "Abs s $ t -> s[t/0]"
- appL [simp, intro!]: "s -> t ==> s $ u -> t $ u"
- appR [simp, intro!]: "s -> t ==> u $ s -> u $ t"
+ beta [simp, intro!]: "Abs s \<degree> t -> s[t/0]"
+ appL [simp, intro!]: "s -> t ==> s \<degree> u -> t \<degree> u"
+ appR [simp, intro!]: "s -> t ==> u \<degree> s -> u \<degree> t"
abs [simp, intro!]: "s -> t ==> Abs s -> Abs t"
inductive_cases beta_cases [elim!]:
"Var i -> t"
"Abs r -> s"
- "s $ t -> u"
+ "s \<degree> t -> u"
declare if_not_P [simp] not_less_eq [simp]
-- {* don't add @{text "r_into_rtrancl[intro!]"} *}
@@ -91,19 +88,19 @@
done
lemma rtrancl_beta_AppL:
- "s ->> s' ==> s $ t ->> s' $ t"
+ "s ->> s' ==> s \<degree> t ->> s' \<degree> t"
apply (erule rtrancl_induct)
apply (blast intro: rtrancl_into_rtrancl)+
done
lemma rtrancl_beta_AppR:
- "t ->> t' ==> s $ t ->> s $ t'"
+ "t ->> t' ==> s \<degree> t ->> s \<degree> t'"
apply (erule rtrancl_induct)
apply (blast intro: rtrancl_into_rtrancl)+
done
lemma rtrancl_beta_App [intro]:
- "[| s ->> s'; t ->> t' |] ==> s $ t ->> s' $ t'"
+ "[| s ->> s'; t ->> t' |] ==> s \<degree> t ->> s' \<degree> t'"
apply (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR
intro: rtrancl_trans)
done
--- a/src/HOL/Lambda/ListApplication.thy Wed Oct 31 22:04:29 2001 +0100
+++ b/src/HOL/Lambda/ListApplication.thy Wed Oct 31 22:05:37 2001 +0100
@@ -9,26 +9,23 @@
theory ListApplication = Lambda:
syntax
- "_list_application" :: "dB => dB list => dB" (infixl "$$" 150)
-syntax (symbols)
- "_list_application" :: "dB => dB list => dB" (infixl "\<^sub>\<degree>\<^sub>\<degree>" 150)
+ "_list_application" :: "dB => dB list => dB" (infixl "\<degree>\<degree>" 150)
+translations
+ "t \<degree>\<degree> ts" == "foldl (op \<degree>) t ts"
-translations
- "t $$ ts" == "foldl (op $) t ts"
-
-lemma apps_eq_tail_conv [iff]: "(r $$ ts = s $$ ts) = (r = s)"
+lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
apply (induct_tac ts rule: rev_induct)
apply auto
done
lemma Var_eq_apps_conv [rule_format, iff]:
- "\<forall>s. (Var m = s $$ ss) = (Var m = s \<and> ss = [])"
+ "\<forall>s. (Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
apply (induct_tac ss)
apply auto
done
lemma Var_apps_eq_Var_apps_conv [rule_format, iff]:
- "\<forall>ss. (Var m $$ rs = Var n $$ ss) = (m = n \<and> rs = ss)"
+ "\<forall>ss. (Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
apply (induct_tac rs rule: rev_induct)
apply simp
apply blast
@@ -38,26 +35,26 @@
done
lemma App_eq_foldl_conv:
- "(r $ s = t $$ ts) =
- (if ts = [] then r $ s = t
- else (\<exists>ss. ts = ss @ [s] \<and> r = t $$ ss))"
+ "(r \<degree> s = t \<degree>\<degree> ts) =
+ (if ts = [] then r \<degree> s = t
+ else (\<exists>ss. ts = ss @ [s] \<and> r = t \<degree>\<degree> ss))"
apply (rule_tac xs = ts in rev_exhaust)
apply auto
done
lemma Abs_eq_apps_conv [iff]:
- "(Abs r = s $$ ss) = (Abs r = s \<and> ss = [])"
+ "(Abs r = s \<degree>\<degree> ss) = (Abs r = s \<and> ss = [])"
apply (induct_tac ss rule: rev_induct)
apply auto
done
-lemma apps_eq_Abs_conv [iff]: "(s $$ ss = Abs r) = (s = Abs r \<and> ss = [])"
+lemma apps_eq_Abs_conv [iff]: "(s \<degree>\<degree> ss = Abs r) = (s = Abs r \<and> ss = [])"
apply (induct_tac ss rule: rev_induct)
apply auto
done
lemma Abs_apps_eq_Abs_apps_conv [iff]:
- "\<forall>ss. (Abs r $$ rs = Abs s $$ ss) = (r = s \<and> rs = ss)"
+ "\<forall>ss. (Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
apply (induct_tac rs rule: rev_induct)
apply simp
apply blast
@@ -67,13 +64,13 @@
done
lemma Abs_App_neq_Var_apps [iff]:
- "\<forall>s t. Abs s $ t ~= Var n $$ ss"
+ "\<forall>s t. Abs s \<degree> t ~= Var n \<degree>\<degree> ss"
apply (induct_tac ss rule: rev_induct)
apply auto
done
lemma Var_apps_neq_Abs_apps [rule_format, iff]:
- "\<forall>ts. Var n $$ ts ~= Abs r $$ ss"
+ "\<forall>ts. Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss"
apply (induct_tac ss rule: rev_induct)
apply simp
apply (rule allI)
@@ -82,19 +79,19 @@
done
lemma ex_head_tail:
- "\<exists>ts h. t = h $$ ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
+ "\<exists>ts h. t = h \<degree>\<degree> ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
apply (induct_tac t)
apply (rule_tac x = "[]" in exI)
apply simp
apply clarify
apply (rename_tac ts1 ts2 h1 h2)
- apply (rule_tac x = "ts1 @ [h2 $$ ts2]" in exI)
+ apply (rule_tac x = "ts1 @ [h2 \<degree>\<degree> ts2]" in exI)
apply simp
apply simp
done
lemma size_apps [simp]:
- "size (r $$ rs) = size r + foldl (op +) 0 (map size rs) + length rs"
+ "size (r \<degree>\<degree> rs) = size r + foldl (op +) 0 (map size rs) + length rs"
apply (induct_tac rs rule: rev_induct)
apply auto
done
@@ -104,11 +101,11 @@
done
-text {* \medskip A customized induction schema for @{text "$$"}. *}
+text {* \medskip A customized induction schema for @{text "\<degree>\<degree>"}. *}
lemma lem [rule_format (no_asm)]:
- "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
- !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
+ "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts);
+ !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)
|] ==> \<forall>t. size t = n --> P t"
proof -
case rule_context
@@ -149,8 +146,8 @@
qed
theorem Apps_dB_induct:
- "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
- !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
+ "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts);
+ !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)
|] ==> P t"
proof -
case rule_context
--- a/src/HOL/Lambda/ListBeta.thy Wed Oct 31 22:04:29 2001 +0100
+++ b/src/HOL/Lambda/ListBeta.thy Wed Oct 31 22:05:37 2001 +0100
@@ -18,7 +18,7 @@
"rs => ss" == "(rs, ss) : step1 beta"
lemma head_Var_reduction_aux:
- "v -> v' ==> \<forall>rs. v = Var n $$ rs --> (\<exists>ss. rs => ss \<and> v' = Var n $$ ss)"
+ "v -> v' ==> \<forall>rs. v = Var n \<degree>\<degree> rs --> (\<exists>ss. rs => ss \<and> v' = Var n \<degree>\<degree> ss)"
apply (erule beta.induct)
apply simp
apply (rule allI)
@@ -32,16 +32,16 @@
done
lemma head_Var_reduction:
- "Var n $$ rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n $$ ss)"
+ "Var n \<degree>\<degree> rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss)"
apply (drule head_Var_reduction_aux)
apply blast
done
lemma apps_betasE_aux:
- "u -> u' ==> \<forall>r rs. u = r $$ rs -->
- ((\<exists>r'. r -> r' \<and> u' = r' $$ rs) \<or>
- (\<exists>rs'. rs => rs' \<and> u' = r $$ rs') \<or>
- (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] $$ ts))"
+ "u -> u' ==> \<forall>r rs. u = r \<degree>\<degree> rs -->
+ ((\<exists>r'. r -> r' \<and> u' = r' \<degree>\<degree> rs) \<or>
+ (\<exists>rs'. rs => rs' \<and> u' = r \<degree>\<degree> rs') \<or>
+ (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] \<degree>\<degree> ts))"
apply (erule beta.induct)
apply (clarify del: disjCI)
apply (case_tac r)
@@ -70,12 +70,12 @@
done
lemma apps_betasE [elim!]:
- "[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R;
- !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R;
- !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |]
+ "[| r \<degree>\<degree> rs -> s; !!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R;
+ !!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R;
+ !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R |]
==> R"
proof -
- assume major: "r $$ rs -> s"
+ assume major: "r \<degree>\<degree> rs -> s"
case rule_context
show ?thesis
apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
@@ -84,20 +84,20 @@
qed
lemma apps_preserves_beta [simp]:
- "r -> s ==> r $$ ss -> s $$ ss"
+ "r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss"
apply (induct_tac ss rule: rev_induct)
apply auto
done
lemma apps_preserves_beta2 [simp]:
- "r ->> s ==> r $$ ss ->> s $$ ss"
+ "r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
apply (erule rtrancl_induct)
apply blast
apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
done
lemma apps_preserves_betas [rule_format, simp]:
- "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
+ "\<forall>ss. rs => ss --> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
apply (induct_tac rs rule: rev_induct)
apply simp
apply simp
--- a/src/HOL/Lambda/ParRed.thy Wed Oct 31 22:04:29 2001 +0100
+++ b/src/HOL/Lambda/ParRed.thy Wed Oct 31 22:05:37 2001 +0100
@@ -26,14 +26,14 @@
intros
var [simp, intro!]: "Var n => Var n"
abs [simp, intro!]: "s => t ==> Abs s => Abs t"
- app [simp, intro!]: "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
- beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
+ app [simp, intro!]: "[| s => s'; t => t' |] ==> s \<degree> t => s' \<degree> t'"
+ beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) \<degree> t => s'[t'/0]"
inductive_cases par_beta_cases [elim!]:
"Var n => t"
"Abs s => Abs t"
- "(Abs s) $ t => u"
- "s $ t => u"
+ "(Abs s) \<degree> t => u"
+ "s \<degree> t => u"
"Abs s => t"
@@ -105,9 +105,9 @@
"cd" :: "dB => dB"
recdef "cd" "measure size"
"cd (Var n) = Var n"
- "cd (Var n $ t) = Var n $ cd t"
- "cd ((s1 $ s2) $ t) = cd (s1 $ s2) $ cd t"
- "cd (Abs u $ t) = (cd u)[cd t/0]"
+ "cd (Var n \<degree> t) = Var n \<degree> cd t"
+ "cd ((s1 \<degree> s2) \<degree> t) = cd (s1 \<degree> s2) \<degree> cd t"
+ "cd (Abs u \<degree> t) = (cd u)[cd t/0]"
"cd (Abs s) = Abs (cd s)"
lemma par_beta_cd [rule_format]:
--- a/src/HOL/Lambda/Type.thy Wed Oct 31 22:04:29 2001 +0100
+++ b/src/HOL/Lambda/Type.thy Wed Oct 31 22:05:37 2001 +0100
@@ -18,8 +18,10 @@
subsection {* Environments *}
constdefs
+ shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_<_:_>" [90, 0, 0] 91)
+ "e<i:a> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
+syntax (symbols)
shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
- "e\<langle>i:a\<rangle> \<equiv> \<lambda>j. if j < i then e j else if j = i then a else e (j - 1)"
lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
by (simp add: shift_def)
@@ -69,11 +71,11 @@
intros
Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T"
Abs [intro!]: "env\<langle>0:T\<rangle> \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs t : (T \<Rightarrow> U)"
- App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<^sub>\<degree> t) : U"
+ App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
inductive_cases typing_elims [elim!]:
"e \<turnstile> Var i : T"
- "e \<turnstile> t \<^sub>\<degree> u : T"
+ "e \<turnstile> t \<degree> u : T"
"e \<turnstile> Abs t : T"
primrec
@@ -86,44 +88,44 @@
subsection {* Some examples *}
-lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<^sub>\<degree> (Var 2 \<^sub>\<degree> Var 1 \<^sub>\<degree> Var 0)))) : ?T"
+lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T"
by force
-lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<^sub>\<degree> Var 0 \<^sub>\<degree> (Var 1 \<^sub>\<degree> Var 0)))) : ?T"
+lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T"
by force
subsection {* n-ary function types *}
lemma list_app_typeD:
- "\<And>t T. e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
+ "\<And>t T. e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
apply (induct ts)
apply simp
apply atomize
apply simp
- apply (erule_tac x = "t \<^sub>\<degree> a" in allE)
+ apply (erule_tac x = "t \<degree> a" in allE)
apply (erule_tac x = T in allE)
apply (erule impE)
apply assumption
apply (elim exE conjE)
- apply (ind_cases "e \<turnstile> t \<^sub>\<degree> u : T")
+ apply (ind_cases "e \<turnstile> t \<degree> u : T")
apply (rule_tac x = "Ta # Ts" in exI)
apply simp
done
lemma list_app_typeE:
- "e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<Longrightarrow> (\<And>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> C) \<Longrightarrow> C"
+ "e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> (\<And>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> C) \<Longrightarrow> C"
by (insert list_app_typeD) fast
lemma list_app_typeI:
- "\<And>t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T"
+ "\<And>t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T"
apply (induct ts)
apply simp
apply atomize
apply (case_tac Ts)
apply simp
apply simp
- apply (erule_tac x = "t \<^sub>\<degree> a" in allE)
+ apply (erule_tac x = "t \<degree> a" in allE)
apply (erule_tac x = T in allE)
apply (erule_tac x = lista in allE)
apply (erule impE)
@@ -152,11 +154,11 @@
subsection {* Lifting preserves termination and well-typedness *}
lemma lift_map [simp]:
- "\<And>t. lift (t \<^sub>\<degree>\<^sub>\<degree> ts) i = lift t i \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. lift t i) ts"
+ "\<And>t. lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
by (induct ts) simp_all
lemma subst_map [simp]:
- "\<And>t. subst (t \<^sub>\<degree>\<^sub>\<degree> ts) u i = subst t u i \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. subst t u i) ts"
+ "\<And>t. subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
by (induct ts) simp_all
lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> (\<And>i. lift t i \<in> IT)"
@@ -206,39 +208,19 @@
apply blast
done
-lemma substs_lemma [rule_format]:
- "e \<turnstile> u : T \<Longrightarrow> \<forall>Ts. e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<longrightarrow>
+lemma substs_lemma:
+ "\<And>Ts. e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow>
e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts"
- apply (induct_tac ts)
- apply (intro strip)
+ apply (induct ts)
apply (case_tac Ts)
apply simp
apply simp
- apply (intro strip)
+ apply atomize
apply (case_tac Ts)
apply simp
apply simp
apply (erule conjE)
- apply (erule subst_lemma)
- apply assumption
- apply (rule refl)
- done
-
-lemma substs_lemma [rule_format]:
- "e \<turnstile> u : T \<Longrightarrow> \<forall>Ts. e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<longrightarrow>
- e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts"
- apply (induct_tac ts)
- apply (intro strip)
- apply (case_tac Ts)
- apply simp
- apply simp
- apply (intro strip)
- apply (case_tac Ts)
- apply simp
- apply simp
- apply (erule conjE)
- apply (erule subst_lemma)
- apply assumption
+ apply (erule (1) subst_lemma)
apply (rule refl)
done
@@ -250,7 +232,7 @@
apply blast
apply blast
apply atomize
- apply (ind_cases "s \<^sub>\<degree> t -> t'")
+ apply (ind_cases "s \<degree> t -> t'")
apply hypsubst
apply (ind_cases "env \<turnstile> Abs t : T \<Rightarrow> U")
apply (rule subst_lemma)
@@ -264,13 +246,12 @@
subsection {* Additional lemmas *}
-lemma app_last: "(t \<^sub>\<degree>\<^sub>\<degree> ts) \<^sub>\<degree> u = t \<^sub>\<degree>\<^sub>\<degree> (ts @ [u])"
+lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])"
by simp
lemma subst_Var_IT: "r \<in> IT \<Longrightarrow> (\<And>i j. r[Var i/j] \<in> IT)"
apply (induct set: IT)
txt {* Case @{term Var}: *}
- apply atomize
apply (simp (no_asm) add: subst_Var)
apply
((rule conjI impI)+,
@@ -297,13 +278,13 @@
done
lemma Var_IT: "Var n \<in> IT"
- apply (subgoal_tac "Var n \<^sub>\<degree>\<^sub>\<degree> [] \<in> IT")
+ apply (subgoal_tac "Var n \<degree>\<degree> [] \<in> IT")
apply simp
apply (rule IT.Var)
apply (rule lists.Nil)
done
-lemma app_Var_IT: "t \<in> IT \<Longrightarrow> t \<^sub>\<degree> Var i \<in> IT"
+lemma app_Var_IT: "t \<in> IT \<Longrightarrow> t \<degree> Var i \<in> IT"
apply (induct set: IT)
apply (subst app_last)
apply (rule IT.Var)
@@ -355,11 +336,11 @@
assume uT: "e \<turnstile> u : T"
{
case (Var n rs)
- assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree>\<^sub>\<degree> rs : T'"
+ assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'"
let ?ty = "{t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'}"
let ?R = "\<lambda>t. \<forall>e T' u i.
e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> u \<in> IT \<longrightarrow> e \<turnstile> u : T \<longrightarrow> t[u/i] \<in> IT"
- show "(Var n \<^sub>\<degree>\<^sub>\<degree> rs)[u/i] \<in> IT"
+ show "(Var n \<degree>\<degree> rs)[u/i] \<in> IT"
proof (cases "n = i")
case True
show ?thesis
@@ -368,9 +349,9 @@
with uIT True show ?thesis by simp
next
case (Cons a as)
- with nT have "e\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as : T'" by simp
+ with nT have "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a \<degree>\<degree> as : T'" by simp
then obtain Ts
- where headT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<^sub>\<degree> a : Ts \<Rrightarrow> T'"
+ where headT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a : Ts \<Rrightarrow> T'"
and argsT: "e\<langle>i:T\<rangle> \<tturnstile> as : Ts"
by (rule list_app_typeE)
from headT obtain T''
@@ -380,14 +361,14 @@
from varT True have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'"
by cases auto
with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp
- from T have "(Var 0 \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. lift t 0)
- (map (\<lambda>t. t[u/i]) as))[(u \<^sub>\<degree> a[u/i])/0] \<in> IT"
+ from T have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0)
+ (map (\<lambda>t. t[u/i]) as))[(u \<degree> a[u/i])/0] \<in> IT"
proof (rule MI2)
- from T have "(lift u 0 \<^sub>\<degree> Var 0)[a[u/i]/0] \<in> IT"
+ from T have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<in> IT"
proof (rule MI1)
have "lift u 0 \<in> IT" by (rule lift_IT)
- thus "lift u 0 \<^sub>\<degree> Var 0 \<in> IT" by (rule app_Var_IT)
- show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<^sub>\<degree> Var 0 : Ts \<Rrightarrow> T'"
+ thus "lift u 0 \<degree> Var 0 \<in> IT" by (rule app_Var_IT)
+ show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
proof (rule typing.App)
show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
by (rule lift_type) (rule uT')
@@ -399,7 +380,7 @@
from argT uT show "e \<turnstile> a[u/i] : T''"
by (rule subst_lemma) simp
qed
- thus "u \<^sub>\<degree> a[u/i] \<in> IT" by simp
+ thus "u \<degree> a[u/i] \<in> IT" by simp
from Var have "as \<in> lists {t. ?R t}"
by cases (simp_all add: Cons)
moreover from argsT have "as \<in> lists ?ty"
@@ -421,18 +402,18 @@
by (rule lists.Cons) (rule Cons)
thus ?case by simp
qed
- thus "Var 0 \<^sub>\<degree>\<^sub>\<degree> ?ls as \<in> IT" by (rule IT.Var)
+ thus "Var 0 \<degree>\<degree> ?ls as \<in> IT" by (rule IT.Var)
have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'"
by (rule typing.Var) simp
moreover from uT argsT have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"
by (rule substs_lemma)
hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> ?ls as : Ts"
by (rule lift_typings)
- ultimately show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<^sub>\<degree>\<^sub>\<degree> ?ls as : T'"
+ ultimately show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> ?ls as : T'"
by (rule list_app_typeI)
from argT uT have "e \<turnstile> a[u/i] : T''"
by (rule subst_lemma) (rule refl)
- with uT' show "e \<turnstile> u \<^sub>\<degree> a[u/i] : Ts \<Rrightarrow> T'"
+ with uT' show "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'"
by (rule typing.App)
qed
with Cons True show ?thesis
@@ -469,25 +450,25 @@
by fastsimp
next
case (Beta r a as)
- assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as : T'"
- assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<^sub>\<degree>\<^sub>\<degree> as) e T' u i T"
+ assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a \<degree>\<degree> as : T'"
+ assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<degree>\<degree> as) e T' u i T"
assume SI2: "\<And>e T' u i. PROP ?Q a e T' u i T"
- have "Abs (r[lift u 0/Suc i]) \<^sub>\<degree> a[u/i] \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
+ have "Abs (r[lift u 0/Suc i]) \<degree> a[u/i] \<degree>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
proof (rule IT.Beta)
- have "Abs r \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as -> r[a/0] \<^sub>\<degree>\<^sub>\<degree> as"
+ have "Abs r \<degree> a \<degree>\<degree> as -> r[a/0] \<degree>\<degree> as"
by (rule apps_preserves_beta) (rule beta.beta)
- with T have "e\<langle>i:T\<rangle> \<turnstile> r[a/0] \<^sub>\<degree>\<^sub>\<degree> as : T'"
+ with T have "e\<langle>i:T\<rangle> \<turnstile> r[a/0] \<degree>\<degree> as : T'"
by (rule subject_reduction)
- hence "(r[a/0] \<^sub>\<degree>\<^sub>\<degree> as)[u/i] \<in> IT"
+ hence "(r[a/0] \<degree>\<degree> as)[u/i] \<in> IT"
by (rule SI1)
- thus "r[lift u 0/Suc i][a[u/i]/0] \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
+ thus "r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
by (simp del: subst_map add: subst_subst subst_map [symmetric])
- from T obtain U where "e\<langle>i:T\<rangle> \<turnstile> Abs r \<^sub>\<degree> a : U"
+ from T obtain U where "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a : U"
by (rule list_app_typeE) fast
then obtain T'' where "e\<langle>i:T\<rangle> \<turnstile> a : T''" by cases simp_all
thus "a[u/i] \<in> IT" by (rule SI2)
qed
- thus "(Abs r \<^sub>\<degree> a \<^sub>\<degree>\<^sub>\<degree> as)[u/i] \<in> IT" by simp
+ thus "(Abs r \<degree> a \<degree>\<degree> as)[u/i] \<in> IT" by simp
}
qed
qed
@@ -506,18 +487,18 @@
show ?case by (rule IT.Lambda)
next
case (App T U e s t)
- have "(Var 0 \<^sub>\<degree> lift t 0)[s/0] \<in> IT"
+ have "(Var 0 \<degree> lift t 0)[s/0] \<in> IT"
proof (rule subst_type_IT)
have "lift t 0 \<in> IT" by (rule lift_IT)
hence "[lift t 0] \<in> lists IT" by (rule lists.Cons) (rule lists.Nil)
- hence "Var 0 \<^sub>\<degree>\<^sub>\<degree> [lift t 0] \<in> IT" by (rule IT.Var)
- also have "Var 0 \<^sub>\<degree>\<^sub>\<degree> [lift t 0] = Var 0 \<^sub>\<degree> lift t 0" by simp
+ hence "Var 0 \<degree>\<degree> [lift t 0] \<in> IT" by (rule IT.Var)
+ also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<degree> lift t 0" by simp
finally show "\<dots> \<in> IT" .
have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
by (rule typing.Var) simp
moreover have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t 0 : T"
by (rule lift_type)
- ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<^sub>\<degree> lift t 0 : U"
+ ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t 0 : U"
by (rule typing.App)
qed
thus ?case by simp