Adapted to new inductive definition package.
--- a/src/HOL/Lambda/InductTermi.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/InductTermi.thy Wed Feb 07 17:44:07 2007 +0100
@@ -14,21 +14,18 @@
subsection {* Terminating lambda terms *}
-consts
- IT :: "dB set"
-
-inductive IT
- intros
- Var [intro]: "rs : lists IT ==> Var n \<degree>\<degree> rs : IT"
- Lambda [intro]: "r : IT ==> Abs r : IT"
- Beta [intro]: "(r[s/0]) \<degree>\<degree> ss : IT ==> s : IT ==> (Abs r \<degree> s) \<degree>\<degree> ss : IT"
+inductive2 IT :: "dB => bool"
+ where
+ Var [intro]: "listsp IT rs ==> IT (Var n \<degree>\<degree> rs)"
+ | Lambda [intro]: "IT r ==> IT (Abs r)"
+ | Beta [intro]: "IT ((r[s/0]) \<degree>\<degree> ss) ==> IT s ==> IT ((Abs r \<degree> s) \<degree>\<degree> ss)"
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] \<degree>\<degree> ss --> Abs r \<degree> s \<degree>\<degree> ss : termi beta)"
+ "termi beta s ==> \<forall>t. termi beta t -->
+ (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> termi beta (Abs r \<degree> s \<degree>\<degree> ss))"
apply (erule acc_induct)
apply (rule allI)
apply (rule impI)
@@ -39,17 +36,15 @@
apply (safe elim!: apps_betasE)
apply assumption
apply (blast intro: subst_preserves_beta apps_preserves_beta)
- apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI
+ apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI'
dest: acc_downwards) (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
apply (blast dest: apps_preserves_betas)
done
-lemma IT_implies_termi: "t : IT ==> t : termi beta"
+lemma IT_implies_termi: "IT t ==> termi beta t"
apply (induct set: IT)
- apply (drule rev_subsetD)
- apply (rule lists_mono)
- apply (rule Int_lower2)
- apply simp
+ apply (drule rev_predicate1D [OF _ listsp_mono [where B="termi beta"]])
+ apply fast
apply (drule lists_accD)
apply (erule acc_induct)
apply (rule accI)
@@ -72,12 +67,12 @@
"(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')"
by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
-inductive_cases [elim!]:
- "Var n \<degree>\<degree> ss : IT"
- "Abs t : IT"
- "Abs r \<degree> s \<degree>\<degree> ts : IT"
+inductive_cases2 [elim!]:
+ "IT (Var n \<degree>\<degree> ss)"
+ "IT (Abs t)"
+ "IT (Abs r \<degree> s \<degree>\<degree> ts)"
-theorem termi_implies_IT: "r : termi beta ==> r : IT"
+theorem termi_implies_IT: "termi beta r ==> IT r"
apply (erule acc_induct)
apply (rename_tac r)
apply (erule thin_rl)
@@ -90,8 +85,8 @@
apply (drule bspec, assumption)
apply (erule mp)
apply clarify
- apply (drule converseI)
- apply (drule ex_step1I, assumption)
+ apply (drule_tac r=beta in conversepI)
+ apply (drule_tac r="beta^--1" in ex_step1I, assumption)
apply clarify
apply (rename_tac us)
apply (erule_tac x = "Var n \<degree>\<degree> us" in allE)
--- a/src/HOL/Lambda/Lambda.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/Lambda.thy Wed Feb 07 17:44:07 2007 +0100
@@ -53,29 +53,21 @@
subsection {* Beta-reduction *}
-consts
- beta :: "(dB \<times> dB) set"
-
-abbreviation
- beta_red :: "[dB, dB] => bool" (infixl "->" 50) where
- "s -> t == (s, t) \<in> beta"
+inductive2 beta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+ where
+ beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
+ | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
+ | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
+ | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
abbreviation
beta_reds :: "[dB, dB] => bool" (infixl "->>" 50) where
- "s ->> t == (s, t) \<in> beta^*"
+ "s ->> t == beta^** s t"
notation (latex)
- beta_red (infixl "\<rightarrow>\<^sub>\<beta>" 50) and
beta_reds (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
-inductive beta
- intros
- beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
- appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
- appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
- abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
-
-inductive_cases beta_cases [elim!]:
+inductive_cases2 beta_cases [elim!]:
"Var i \<rightarrow>\<^sub>\<beta> t"
"Abs r \<rightarrow>\<^sub>\<beta> s"
"s \<degree> t \<rightarrow>\<^sub>\<beta> u"
@@ -88,19 +80,19 @@
lemma rtrancl_beta_Abs [intro!]:
"s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
- by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
+ by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
lemma rtrancl_beta_AppL:
"s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
- by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
+ by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
lemma rtrancl_beta_AppR:
"t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
- by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
+ by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
lemma rtrancl_beta_App [intro]:
"[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
- by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtrancl_trans)
+ by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtrancl_trans')
subsection {* Substitution-lemmas *}
@@ -164,8 +156,8 @@
theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
apply (induct set: rtrancl)
- apply (rule rtrancl_refl)
- apply (erule rtrancl_into_rtrancl)
+ apply (rule rtrancl.rtrancl_refl)
+ apply (erule rtrancl.rtrancl_into_rtrancl)
apply (erule subst_preserves_beta)
done
@@ -175,22 +167,22 @@
theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
apply (induct set: rtrancl)
- apply (rule rtrancl_refl)
- apply (erule rtrancl_into_rtrancl)
+ apply (rule rtrancl.rtrancl_refl)
+ apply (erule rtrancl.rtrancl_into_rtrancl)
apply (erule lift_preserves_beta)
done
theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
apply (induct t arbitrary: r s i)
- apply (simp add: subst_Var r_into_rtrancl)
+ apply (simp add: subst_Var r_into_rtrancl')
apply (simp add: rtrancl_beta_App)
apply (simp add: rtrancl_beta_Abs)
done
theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
apply (induct set: rtrancl)
- apply (rule rtrancl_refl)
- apply (erule rtrancl_trans)
+ apply (rule rtrancl.rtrancl_refl)
+ apply (erule rtrancl_trans')
apply (erule subst_preserves_beta2)
done
--- a/src/HOL/Lambda/ListBeta.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/ListBeta.thy Wed Feb 07 17:44:07 2007 +0100
@@ -14,10 +14,10 @@
abbreviation
list_beta :: "dB list => dB list => bool" (infixl "=>" 50) where
- "rs => ss == (rs, ss) : step1 beta"
+ "rs => ss == step1 beta rs ss"
lemma head_Var_reduction:
- "Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
+ "Var n \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
apply (induct u == "Var n \<degree>\<degree> rs" v arbitrary: rs set: beta)
apply simp
apply (rule_tac xs = rs in rev_exhaust)
@@ -29,14 +29,14 @@
done
lemma apps_betasE [elim!]:
- assumes major: "r \<degree>\<degree> rs -> s"
- and cases: "!!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R"
+ assumes major: "r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> s"
+ and cases: "!!r'. [| r \<rightarrow>\<^sub>\<beta> 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"
shows R
proof -
from major have
- "(\<exists>r'. r -> r' \<and> s = r' \<degree>\<degree> rs) \<or>
+ "(\<exists>r'. r \<rightarrow>\<^sub>\<beta> r' \<and> s = r' \<degree>\<degree> rs) \<or>
(\<exists>rs'. rs => rs' \<and> s = r \<degree>\<degree> rs') \<or>
(\<exists>t u us. r = Abs t \<and> rs = u # us \<and> s = t[u/0] \<degree>\<degree> us)"
apply (induct u == "r \<degree>\<degree> rs" s arbitrary: r rs set: beta)
@@ -66,18 +66,18 @@
qed
lemma apps_preserves_beta [simp]:
- "r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss"
+ "r \<rightarrow>\<^sub>\<beta> s ==> r \<degree>\<degree> ss \<rightarrow>\<^sub>\<beta> s \<degree>\<degree> ss"
by (induct ss rule: rev_induct) auto
lemma apps_preserves_beta2 [simp]:
"r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
apply (induct set: rtrancl)
apply blast
- apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
+ apply (blast intro: apps_preserves_beta rtrancl.rtrancl_into_rtrancl)
done
lemma apps_preserves_betas [simp]:
- "rs => ss \<Longrightarrow> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
+ "rs => ss \<Longrightarrow> r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> r \<degree>\<degree> ss"
apply (induct rs arbitrary: ss rule: rev_induct)
apply simp
apply simp
--- a/src/HOL/Lambda/ParRed.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/ParRed.thy Wed Feb 07 17:44:07 2007 +0100
@@ -14,21 +14,14 @@
subsection {* Parallel reduction *}
-consts
- par_beta :: "(dB \<times> dB) set"
-
-abbreviation
- par_beta_red :: "[dB, dB] => bool" (infixl "=>" 50) where
- "s => t == (s, t) \<in> par_beta"
+inductive2 par_beta :: "[dB, dB] => bool" (infixl "=>" 50)
+ where
+ var [simp, intro!]: "Var n => Var n"
+ | abs [simp, intro!]: "s => t ==> Abs s => Abs t"
+ | 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 par_beta
- 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 \<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!]:
+inductive_cases2 par_beta_cases [elim!]:
"Var n => t"
"Abs s => Abs t"
"(Abs s) \<degree> t => u"
@@ -48,18 +41,16 @@
by (induct t) simp_all
lemma beta_subset_par_beta: "beta <= par_beta"
- apply (rule subsetI)
- apply clarify
+ apply (rule predicate2I)
apply (erule beta.induct)
apply (blast intro!: par_beta_refl)+
done
-lemma par_beta_subset_beta: "par_beta <= beta^*"
- apply (rule subsetI)
- apply clarify
+lemma par_beta_subset_beta: "par_beta <= beta^**"
+ apply (rule predicate2I)
apply (erule par_beta.induct)
apply blast
- apply (blast del: rtrancl_refl intro: rtrancl_into_rtrancl)+
+ apply (blast del: rtrancl.rtrancl_refl intro: rtrancl.rtrancl_into_rtrancl)+
-- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *}
done
--- a/src/HOL/Lambda/StrongNorm.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/StrongNorm.thy Wed Feb 07 17:44:07 2007 +0100
@@ -16,41 +16,38 @@
subsection {* Properties of @{text IT} *}
-lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> lift t i \<in> IT"
+lemma lift_IT [intro!]: "IT t \<Longrightarrow> IT (lift t i)"
apply (induct arbitrary: i set: IT)
apply (simp (no_asm))
apply (rule conjI)
apply
(rule impI,
rule IT.Var,
- erule lists.induct,
+ erule listsp.induct,
simp (no_asm),
- rule lists.Nil,
+ rule listsp.Nil,
simp (no_asm),
- erule IntE,
- rule lists.Cons,
+ rule listsp.Cons,
blast,
assumption)+
apply auto
done
-lemma lifts_IT: "ts \<in> lists IT \<Longrightarrow> map (\<lambda>t. lift t 0) ts \<in> lists IT"
+lemma lifts_IT: "listsp IT ts \<Longrightarrow> listsp IT (map (\<lambda>t. lift t 0) ts)"
by (induct ts) auto
-lemma subst_Var_IT: "r \<in> IT \<Longrightarrow> r[Var i/j] \<in> IT"
+lemma subst_Var_IT: "IT r \<Longrightarrow> IT (r[Var i/j])"
apply (induct arbitrary: i j set: IT)
txt {* Case @{term Var}: *}
apply (simp (no_asm) add: subst_Var)
apply
((rule conjI impI)+,
rule IT.Var,
- erule lists.induct,
- simp (no_asm),
- rule lists.Nil,
+ erule listsp.induct,
simp (no_asm),
- erule IntE,
- erule CollectE,
- rule lists.Cons,
+ rule listsp.Nil,
+ simp (no_asm),
+ rule listsp.Cons,
fast,
assumption)+
txt {* Case @{term Lambda}: *}
@@ -65,21 +62,21 @@
apply auto
done
-lemma Var_IT: "Var n \<in> IT"
- apply (subgoal_tac "Var n \<degree>\<degree> [] \<in> IT")
+lemma Var_IT: "IT (Var n)"
+ apply (subgoal_tac "IT (Var n \<degree>\<degree> [])")
apply simp
apply (rule IT.Var)
- apply (rule lists.Nil)
+ apply (rule listsp.Nil)
done
-lemma app_Var_IT: "t \<in> IT \<Longrightarrow> t \<degree> Var i \<in> IT"
+lemma app_Var_IT: "IT t \<Longrightarrow> IT (t \<degree> Var i)"
apply (induct set: IT)
apply (subst app_last)
apply (rule IT.Var)
apply simp
- apply (rule lists.Cons)
+ apply (rule listsp.Cons)
apply (rule Var_IT)
- apply (rule lists.Nil)
+ apply (rule listsp.Nil)
apply (rule IT.Beta [where ?ss = "[]", unfolded foldl_Nil [THEN eq_reflection]])
apply (erule subst_Var_IT)
apply (rule Var_IT)
@@ -94,26 +91,26 @@
subsection {* Well-typed substitution preserves termination *}
lemma subst_type_IT:
- "\<And>t e T u i. t \<in> IT \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow>
- u \<in> IT \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> t[u/i] \<in> IT"
+ "\<And>t e T u i. IT t \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow>
+ IT u \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> IT (t[u/i])"
(is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U")
proof (induct U)
fix T t
assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1"
assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2"
- assume "t \<in> IT"
+ assume "IT t"
thus "\<And>e T' u i. PROP ?Q t e T' u i T"
proof induct
fix e T' u i
- assume uIT: "u \<in> IT"
+ assume uIT: "IT u"
assume uT: "e \<turnstile> u : T"
{
- case (Var n rs e_ T'_ u_ i_)
+ case (Var rs n e_ T'_ u_ i_)
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 ?ty = "\<lambda>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 \<degree>\<degree> rs)[u/i] \<in> IT"
+ e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> IT u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> IT (t[u/i])"
+ show "IT ((Var n \<degree>\<degree> rs)[u/i])"
proof (cases "n = i")
case True
show ?thesis
@@ -134,13 +131,13 @@
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 \<degree>\<degree> map (\<lambda>t. lift t 0)
- (map (\<lambda>t. t[u/i]) as))[(u \<degree> a[u/i])/0] \<in> IT"
+ from T have "IT ((Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0)
+ (map (\<lambda>t. t[u/i]) as))[(u \<degree> a[u/i])/0])"
proof (rule MI2)
- from T have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<in> IT"
+ from T have "IT ((lift u 0 \<degree> Var 0)[a[u/i]/0])"
proof (rule MI1)
- have "lift u 0 \<in> IT" by (rule lift_IT)
- thus "lift u 0 \<degree> Var 0 \<in> IT" by (rule app_Var_IT)
+ have "IT (lift u 0)" by (rule lift_IT)
+ thus "IT (lift u 0 \<degree> Var 0)" 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'"
@@ -149,19 +146,19 @@
by (rule typing.Var) simp
qed
from Var have "?R a" by cases (simp_all add: Cons)
- with argT uIT uT show "a[u/i] \<in> IT" by simp
+ with argT uIT uT show "IT (a[u/i])" by simp
from argT uT show "e \<turnstile> a[u/i] : T''"
by (rule subst_lemma) simp
qed
- thus "u \<degree> a[u/i] \<in> IT" by simp
- from Var have "as \<in> lists {t. ?R t}"
+ thus "IT (u \<degree> a[u/i])" by simp
+ from Var have "listsp ?R as"
by cases (simp_all add: Cons)
- moreover from argsT have "as \<in> lists ?ty"
+ moreover from argsT have "listsp ?ty as"
by (rule lists_typings)
- ultimately have "as \<in> lists ({t. ?R t} \<inter> ?ty)"
- by (rule lists_IntI)
- hence "map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) \<in> lists IT"
- (is "(?ls as) \<in> _")
+ ultimately have "listsp (\<lambda>t. ?R t \<and> ?ty t) as"
+ by simp
+ hence "listsp IT (map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as))"
+ (is "listsp IT (?ls as)")
proof induct
case Nil
show ?case by fastsimp
@@ -169,13 +166,13 @@
case (Cons b bs)
hence I: "?R b" by simp
from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> b : U" by fast
- with uT uIT I have "b[u/i] \<in> IT" by simp
- hence "lift (b[u/i]) 0 \<in> IT" by (rule lift_IT)
- hence "lift (b[u/i]) 0 # ?ls bs \<in> lists IT"
- by (rule lists.Cons) (rule Cons)
+ with uT uIT I have "IT (b[u/i])" by simp
+ hence "IT (lift (b[u/i]) 0)" by (rule lift_IT)
+ hence "listsp IT (lift (b[u/i]) 0 # ?ls bs)"
+ by (rule listsp.Cons) (rule Cons)
thus ?case by simp
qed
- thus "Var 0 \<degree>\<degree> ?ls as \<in> IT" by (rule IT.Var)
+ thus "IT (Var 0 \<degree>\<degree> ?ls as)" 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"
@@ -194,13 +191,13 @@
qed
next
case False
- from Var have "rs \<in> lists {t. ?R t}" by simp
+ from Var have "listsp ?R rs" by simp
moreover from nT obtain Ts where "e\<langle>i:T\<rangle> \<tturnstile> rs : Ts"
by (rule list_app_typeE)
- hence "rs \<in> lists ?ty" by (rule lists_typings)
- ultimately have "rs \<in> lists ({t. ?R t} \<inter> ?ty)"
- by (rule lists_IntI)
- hence "map (\<lambda>x. x[u/i]) rs \<in> lists IT"
+ hence "listsp ?ty rs" by (rule lists_typings)
+ ultimately have "listsp (\<lambda>t. ?R t \<and> ?ty t) rs"
+ by simp
+ hence "listsp IT (map (\<lambda>x. x[u/i]) rs)"
proof induct
case Nil
show ?case by fastsimp
@@ -208,9 +205,9 @@
case (Cons a as)
hence I: "?R a" by simp
from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> a : U" by fast
- with uT uIT I have "a[u/i] \<in> IT" by simp
- hence "(a[u/i] # map (\<lambda>t. t[u/i]) as) \<in> lists IT"
- by (rule lists.Cons) (rule Cons)
+ with uT uIT I have "IT (a[u/i])" by simp
+ hence "listsp IT (a[u/i] # map (\<lambda>t. t[u/i]) as)"
+ by (rule listsp.Cons) (rule Cons)
thus ?case by simp
qed
with False show ?thesis by (auto simp add: subst_Var)
@@ -219,29 +216,29 @@
case (Lambda r e_ T'_ u_ i_)
assume "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
and "\<And>e T' u i. PROP ?Q r e T' u i T"
- with uIT uT show "Abs r[u/i] \<in> IT"
+ with uIT uT show "IT (Abs r[u/i])"
by fastsimp
next
case (Beta r a as e_ T'_ u_ i_)
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]) \<degree> a[u/i] \<degree>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
+ have "IT (Abs (r[lift u 0/Suc i]) \<degree> a[u/i] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)"
proof (rule IT.Beta)
have "Abs r \<degree> a \<degree>\<degree> as \<rightarrow>\<^sub>\<beta> 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] \<degree>\<degree> as : T'"
by (rule subject_reduction)
- hence "(r[a/0] \<degree>\<degree> as)[u/i] \<in> IT"
+ hence "IT ((r[a/0] \<degree>\<degree> as)[u/i])"
by (rule SI1)
- thus "r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
+ thus "IT (r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)"
by (simp del: subst_map add: subst_subst subst_map [symmetric])
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)
+ thus "IT (a[u/i])" by (rule SI2)
qed
- thus "(Abs r \<degree> a \<degree>\<degree> as)[u/i] \<in> IT" by simp
+ thus "IT ((Abs r \<degree> a \<degree>\<degree> as)[u/i])" by simp
}
qed
qed
@@ -251,7 +248,7 @@
lemma type_implies_IT:
assumes "e \<turnstile> t : T"
- shows "t \<in> IT"
+ shows "IT t"
using prems
proof induct
case Var
@@ -260,14 +257,14 @@
case Abs
show ?case by (rule IT.Lambda)
next
- case (App T U e s t)
- have "(Var 0 \<degree> lift t 0)[s/0] \<in> IT"
+ case (App e s T U t)
+ have "IT ((Var 0 \<degree> lift t 0)[s/0])"
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 \<degree>\<degree> [lift t 0] \<in> IT" by (rule IT.Var)
+ have "IT (lift t 0)" by (rule lift_IT)
+ hence "listsp IT [lift t 0]" by (rule listsp.Cons) (rule listsp.Nil)
+ hence "IT (Var 0 \<degree>\<degree> [lift t 0])" 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" .
+ finally show "IT \<dots>" .
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"
@@ -278,10 +275,10 @@
thus ?case by simp
qed
-theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> t \<in> termi beta"
+theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> termi beta t"
proof -
assume "e \<turnstile> t : T"
- hence "t \<in> IT" by (rule type_implies_IT)
+ hence "IT t" by (rule type_implies_IT)
thus ?thesis by (rule IT_implies_termi)
qed
--- a/src/HOL/Lambda/Type.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/Type.thy Wed Feb 07 17:44:07 2007 +0100
@@ -45,8 +45,18 @@
Atom nat
| Fun type type (infixr "\<Rightarrow>" 200)
+inductive2 typing :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50)
+ where
+ 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 \<degree> t) : U"
+
+inductive_cases2 typing_elims [elim!]:
+ "e \<turnstile> Var i : T"
+ "e \<turnstile> t \<degree> u : T"
+ "e \<turnstile> Abs t : T"
+
consts
- typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
abbreviation
@@ -54,32 +64,14 @@
"Ts =>> T == foldr Fun Ts T"
abbreviation
- typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |- _ : _" [50, 50, 50] 50) where
- "env |- t : T == (env, t, T) \<in> typing"
-
-abbreviation
typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
("_ ||- _ : _" [50, 50, 50] 50) where
"env ||- ts : Ts == typings env ts Ts"
-notation (xsymbols)
- typing_rel ("_ \<turnstile> _ : _" [50, 50, 50] 50)
-
notation (latex)
funs (infixr "\<Rrightarrow>" 200) and
typings_rel ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
-inductive typing
- 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 \<degree> t) : U"
-
-inductive_cases typing_elims [elim!]:
- "e \<turnstile> Var i : T"
- "e \<turnstile> t \<degree> u : T"
- "e \<turnstile> Abs t : T"
-
primrec
"(e \<tturnstile> [] : Ts) = (Ts = [])"
"(e \<tturnstile> (t # ts) : Ts) =
@@ -100,16 +92,16 @@
subsection {* Lists of types *}
lemma lists_typings:
- "e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
+ "e \<tturnstile> ts : Ts \<Longrightarrow> listsp (\<lambda>t. \<exists>T. e \<turnstile> t : T) ts"
apply (induct ts arbitrary: Ts)
apply (case_tac Ts)
apply simp
- apply (rule lists.Nil)
+ apply (rule listsp.Nil)
apply simp
apply (case_tac Ts)
apply simp
apply simp
- apply (rule lists.Cons)
+ apply (rule listsp.Cons)
apply blast
apply blast
done
@@ -172,7 +164,7 @@
apply (erule impE)
apply assumption
apply (elim exE conjE)
- apply (ind_cases "e \<turnstile> t \<degree> u : T")
+ apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
apply (rule_tac x = "Ta # Ts" in exI)
apply simp
done
@@ -210,12 +202,12 @@
"e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
apply (induct ts arbitrary: T U rule: rev_induct)
apply simp
- apply (ind_cases "e \<turnstile> Var i : T")
- apply (ind_cases "e \<turnstile> Var i : T")
+ apply (ind_cases2 "e \<turnstile> Var i : T" for T)
+ apply (ind_cases2 "e \<turnstile> Var i : T" for T)
apply simp
apply simp
- apply (ind_cases "e \<turnstile> t \<degree> u : T")
- apply (ind_cases "e \<turnstile> t \<degree> u : T")
+ apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
+ apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
apply atomize
apply (erule_tac x="Ta \<Rightarrow> T" in allE)
apply (erule_tac x="Tb \<Rightarrow> U" in allE)
@@ -238,7 +230,7 @@
apply (rule FalseE)
apply simp
apply (erule list_app_typeE)
- apply (ind_cases "e \<turnstile> t \<degree> u : T")
+ apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
apply (drule_tac T="Atom nat" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
apply assumption
apply simp
@@ -250,7 +242,7 @@
apply (rule types_snoc)
apply assumption
apply (erule list_app_typeE)
- apply (ind_cases "e \<turnstile> t \<degree> u : T")
+ apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
apply (drule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
apply assumption
apply simp
@@ -258,7 +250,7 @@
apply (rule typing.App)
apply assumption
apply (erule list_app_typeE)
- apply (ind_cases "e \<turnstile> t \<degree> u : T")
+ apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
apply (frule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
apply assumption
apply simp
@@ -266,7 +258,7 @@
apply (rule_tac x="type1 # Us" in exI)
apply simp
apply (erule list_app_typeE)
- apply (ind_cases "e \<turnstile> t \<degree> u : T")
+ apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
apply (frule_tac T="type1 \<Rightarrow> Us \<Rrightarrow> T" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
apply assumption
apply simp
@@ -281,13 +273,13 @@
lemma abs_typeE: "e \<turnstile> Abs t : T \<Longrightarrow> (\<And>U V. e\<langle>0:U\<rangle> \<turnstile> t : V \<Longrightarrow> P) \<Longrightarrow> P"
apply (cases T)
apply (rule FalseE)
- apply (erule typing.elims)
+ apply (erule typing.cases)
apply simp_all
apply atomize
apply (erule_tac x="type1" in allE)
apply (erule_tac x="type2" in allE)
apply (erule mp)
- apply (erule typing.elims)
+ apply (erule typing.cases)
apply simp_all
done
@@ -335,14 +327,14 @@
subsection {* Subject reduction *}
-lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t -> t' \<Longrightarrow> e \<turnstile> t' : T"
+lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> e \<turnstile> t' : T"
apply (induct arbitrary: t' set: typing)
apply blast
apply blast
apply atomize
- apply (ind_cases "s \<degree> t -> t'")
+ apply (ind_cases2 "s \<degree> t \<rightarrow>\<^sub>\<beta> t'" for s t t')
apply hypsubst
- apply (ind_cases "env \<turnstile> Abs t : T \<Rightarrow> U")
+ apply (ind_cases2 "env \<turnstile> Abs t : T \<Rightarrow> U" for env t T U)
apply (rule subst_lemma)
apply assumption
apply assumption
--- a/src/HOL/Lambda/WeakNorm.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy Wed Feb 07 17:44:07 2007 +0100
@@ -73,11 +73,10 @@
-- {* Currently needed for strange technical reasons *}
by (unfold listall_def) simp
-consts NF :: "dB set"
-inductive NF
-intros
- App: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow> Var x \<degree>\<degree> ts \<in> NF"
- Abs: "t \<in> NF \<Longrightarrow> Abs t \<in> NF"
+inductive2 NF :: "dB \<Rightarrow> bool"
+where
+ App: "listall NF ts \<Longrightarrow> NF (Var x \<degree>\<degree> ts)"
+| Abs: "NF t \<Longrightarrow> NF (Abs t)"
monos listall_def
lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
@@ -94,26 +93,26 @@
apply (simp del: simp_thms, iprover?)+
done
-lemma App_NF_D: assumes NF: "Var n \<degree>\<degree> ts \<in> NF"
- shows "listall (\<lambda>t. t \<in> NF) ts" using NF
+lemma App_NF_D: assumes NF: "NF (Var n \<degree>\<degree> ts)"
+ shows "listall NF ts" using NF
by cases simp_all
subsection {* Properties of @{text NF} *}
-lemma Var_NF: "Var n \<in> NF"
- apply (subgoal_tac "Var n \<degree>\<degree> [] \<in> NF")
+lemma Var_NF: "NF (Var n)"
+ apply (subgoal_tac "NF (Var n \<degree>\<degree> [])")
apply simp
apply (rule NF.App)
apply simp
done
-lemma subst_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow>
- listall (\<lambda>t. \<forall>i j. t[Var i/j] \<in> NF) ts \<Longrightarrow>
- listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)"
+lemma subst_terms_NF: "listall NF ts \<Longrightarrow>
+ listall (\<lambda>t. \<forall>i j. NF (t[Var i/j])) ts \<Longrightarrow>
+ listall NF (map (\<lambda>t. t[Var i/j]) ts)"
by (induct ts) simp_all
-lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> t[Var i/j] \<in> NF"
+lemma subst_Var_NF: "NF t \<Longrightarrow> NF (t[Var i/j])"
apply (induct arbitrary: i j set: NF)
apply simp
apply (frule listall_conj1)
@@ -132,30 +131,30 @@
apply (iprover intro: NF.Abs)
done
-lemma app_Var_NF: "t \<in> NF \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
+lemma app_Var_NF: "NF t \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
apply (induct set: NF)
apply (simplesubst app_last) --{*Using @{text subst} makes extraction fail*}
apply (rule exI)
apply (rule conjI)
- apply (rule rtrancl_refl)
+ apply (rule rtrancl.rtrancl_refl)
apply (rule NF.App)
apply (drule listall_conj1)
apply (simp add: listall_app)
apply (rule Var_NF)
apply (rule exI)
apply (rule conjI)
- apply (rule rtrancl_into_rtrancl)
- apply (rule rtrancl_refl)
+ apply (rule rtrancl.rtrancl_into_rtrancl)
+ apply (rule rtrancl.rtrancl_refl)
apply (rule beta)
apply (erule subst_Var_NF)
done
-lemma lift_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow>
- listall (\<lambda>t. \<forall>i. lift t i \<in> NF) ts \<Longrightarrow>
- listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t i) ts)"
+lemma lift_terms_NF: "listall NF ts \<Longrightarrow>
+ listall (\<lambda>t. \<forall>i. NF (lift t i)) ts \<Longrightarrow>
+ listall NF (map (\<lambda>t. lift t i) ts)"
by (induct ts) simp_all
-lemma lift_NF: "t \<in> NF \<Longrightarrow> lift t i \<in> NF"
+lemma lift_NF: "NF t \<Longrightarrow> NF (lift t i)"
apply (induct arbitrary: i set: NF)
apply (frule listall_conj1)
apply (drule listall_conj2)
@@ -178,13 +177,13 @@
lemma norm_list:
assumes f_compat: "\<And>t t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> f t \<rightarrow>\<^sub>\<beta>\<^sup>* f t'"
- and f_NF: "\<And>t. t \<in> NF \<Longrightarrow> f t \<in> NF"
- and uNF: "u \<in> NF" and uT: "e \<turnstile> u : T"
+ and f_NF: "\<And>t. NF t \<Longrightarrow> NF (f t)"
+ and uNF: "NF u" and uT: "e \<turnstile> u : T"
shows "\<And>Us. e\<langle>i:T\<rangle> \<tturnstile> as : Us \<Longrightarrow>
listall (\<lambda>t. \<forall>e T' u i. e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow>
- u \<in> NF \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF)) as \<Longrightarrow>
+ NF u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')) as \<Longrightarrow>
\<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) as \<rightarrow>\<^sub>\<beta>\<^sup>*
- Var j \<degree>\<degree> map f as' \<and> Var j \<degree>\<degree> map f as' \<in> NF"
+ Var j \<degree>\<degree> map f as' \<and> NF (Var j \<degree>\<degree> map f as')"
(is "\<And>Us. _ \<Longrightarrow> listall ?R as \<Longrightarrow> \<exists>as'. ?ex Us as as'")
proof (induct as rule: rev_induct)
case (Nil Us)
@@ -200,18 +199,18 @@
with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc)
then obtain bs' where
bsred: "\<And>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> map f bs'"
- and bsNF: "\<And>j. Var j \<degree>\<degree> map f bs' \<in> NF" by iprover
+ and bsNF: "\<And>j. NF (Var j \<degree>\<degree> map f bs')" by iprover
from snoc have "?R b" by simp
- with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF"
+ with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> NF b'"
by iprover
- then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF"
+ then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "NF b'"
by iprover
- from bsNF [of 0] have "listall (\<lambda>t. t \<in> NF) (map f bs')"
+ from bsNF [of 0] have "listall NF (map f bs')"
by (rule App_NF_D)
- moreover have "f b' \<in> NF" by (rule f_NF)
- ultimately have "listall (\<lambda>t. t \<in> NF) (map f (bs' @ [b']))"
+ moreover have "NF (f b')" by (rule f_NF)
+ ultimately have "listall NF (map f (bs' @ [b']))"
by simp
- hence "\<And>j. Var j \<degree>\<degree> map f (bs' @ [b']) \<in> NF" by (rule NF.App)
+ hence "\<And>j. NF (Var j \<degree>\<degree> map f (bs' @ [b']))" by (rule NF.App)
moreover from bred have "f (b[u/i]) \<rightarrow>\<^sub>\<beta>\<^sup>* f b'"
by (rule f_compat)
with bsred have
@@ -222,18 +221,18 @@
qed
lemma subst_type_NF:
- "\<And>t e T u i. t \<in> NF \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow> u \<in> NF \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> \<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
+ "\<And>t e T u i. NF t \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow> NF u \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> \<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
(is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U")
proof (induct U)
fix T t
let ?R = "\<lambda>t. \<forall>e T' u i.
- e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> u \<in> NF \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF)"
+ e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> NF u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')"
assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1"
assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2"
- assume "t \<in> NF"
+ assume "NF t"
thus "\<And>e T' u i. PROP ?Q t e T' u i T"
proof induct
- fix e T' u i assume uNF: "u \<in> NF" and uT: "e \<turnstile> u : T"
+ fix e T' u i assume uNF: "NF u" and uT: "e \<turnstile> u : T"
{
case (App ts x e_ T'_ u_ i_)
assume "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> ts : T'"
@@ -241,7 +240,7 @@
where varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : Us \<Rrightarrow> T'"
and argsT: "e\<langle>i:T\<rangle> \<tturnstile> ts : Us"
by (rule var_app_typesE)
- from nat_eq_dec show "\<exists>t'. (Var x \<degree>\<degree> ts)[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
+ from nat_eq_dec show "\<exists>t'. (Var x \<degree>\<degree> ts)[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
proof
assume eq: "x = i"
show ?thesis
@@ -264,20 +263,20 @@
with lift_preserves_beta' lift_NF uNF uT argsT'
have "\<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*
Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<and>
- Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<in> NF" by (rule norm_list)
+ NF (Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by (rule norm_list)
then obtain as' where
asred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*
Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as'"
- and asNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<in> NF" by iprover
+ and asNF: "NF (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by iprover
from App and Cons have "?R a" by simp
- with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> a' \<in> NF"
+ with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> NF a'"
by iprover
- then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "a' \<in> NF" by iprover
- from uNF have "lift u 0 \<in> NF" by (rule lift_NF)
- hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> u' \<in> NF" by (rule app_Var_NF)
- then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "u' \<in> NF"
+ then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "NF a'" by iprover
+ from uNF have "NF (lift u 0)" by (rule lift_NF)
+ hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> NF u'" by (rule app_Var_NF)
+ then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "NF u'"
by iprover
- from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> ua \<in> NF"
+ from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> NF ua"
proof (rule MI1)
have "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
proof (rule typing.App)
@@ -287,7 +286,7 @@
with ured show "e\<langle>0:T''\<rangle> \<turnstile> u' : Ts \<Rrightarrow> T'" by (rule subject_reduction')
from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction')
qed
- then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "ua \<in> NF"
+ then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "NF ua"
by iprover
from ared have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* (lift u 0 \<degree> Var 0)[a'/0]"
by (rule subst_preserves_beta2')
@@ -296,7 +295,7 @@
also note uared
finally have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" .
hence uared': "u \<degree> a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" by simp
- from T have "\<exists>r. (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r \<and> r \<in> NF"
+ from T have "\<exists>r. (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r \<and> NF r"
proof (rule MI2)
have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as : T'"
proof (rule list_app_typeI)
@@ -315,7 +314,7 @@
with uared' show "e \<turnstile> ua : Ts \<Rrightarrow> T'" by (rule subject_reduction')
qed
then obtain r where rred: "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r"
- and rnf: "r \<in> NF" by iprover
+ and rnf: "NF r" by iprover
from asred have
"(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>*
(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0]"
@@ -332,7 +331,7 @@
from App have "listall ?R ts" by (iprover dest: listall_conj2)
with TrueI TrueI uNF uT argsT
have "\<exists>ts'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. t[u/i]) ts \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> ts' \<and>
- Var j \<degree>\<degree> ts' \<in> NF" (is "\<exists>ts'. ?ex ts'")
+ NF (Var j \<degree>\<degree> ts')" (is "\<exists>ts'. ?ex ts'")
by (rule norm_list [of "\<lambda>t. t", simplified])
then obtain ts' where NF: "?ex ts'" ..
from nat_le_dec show ?thesis
@@ -348,31 +347,22 @@
case (Abs r e_ T'_ u_ i_)
assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle> \<turnstile> r : S" by (rule abs_typeE) simp
- moreover have "lift u 0 \<in> NF" by (rule lift_NF)
+ moreover have "NF (lift u 0)" by (rule lift_NF)
moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" by (rule lift_type)
- ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" by (rule Abs)
- thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
+ ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by (rule Abs)
+ thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
by simp (iprover intro: rtrancl_beta_Abs NF.Abs)
}
qed
qed
-consts -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
- rtyping :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
-
-abbreviation
- rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |-\<^sub>R _ : _" [50, 50, 50] 50) where
- "e |-\<^sub>R t : T == (e, t, T) \<in> rtyping"
-
-notation (xsymbols)
- rtyping_rel ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
-
-inductive rtyping
- intros
+-- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
+inductive2 rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
+ where
Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T"
- Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)"
- App: "e \<turnstile>\<^sub>R s : T \<Rightarrow> U \<Longrightarrow> e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile>\<^sub>R (s \<degree> t) : U"
+ | Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)"
+ | App: "e \<turnstile>\<^sub>R s : T \<Rightarrow> U \<Longrightarrow> e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile>\<^sub>R (s \<degree> t) : U"
lemma rtyping_imp_typing: "e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile> t : T"
apply (induct set: rtyping)
@@ -385,7 +375,7 @@
theorem type_NF:
assumes "e \<turnstile>\<^sub>R t : T"
- shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using prems
+ shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" using prems
proof induct
case Var
show ?case by (iprover intro: Var_NF)
@@ -393,16 +383,16 @@
case Abs
thus ?case by (iprover intro: rtrancl_beta_Abs NF.Abs)
next
- case (App T U e s t)
+ case (App e s T U t)
from App obtain s' t' where
- sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and sNF: "s' \<in> NF"
- and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "t' \<in> NF" by iprover
- have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> u \<in> NF"
+ sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and sNF: "NF s'"
+ and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "NF t'" by iprover
+ have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> NF u"
proof (rule subst_type_NF)
- have "lift t' 0 \<in> NF" by (rule lift_NF)
- hence "listall (\<lambda>t. t \<in> NF) [lift t' 0]" by (rule listall_cons) (rule listall_nil)
- hence "Var 0 \<degree>\<degree> [lift t' 0] \<in> NF" by (rule NF.App)
- thus "Var 0 \<degree> lift t' 0 \<in> NF" by simp
+ have "NF (lift t' 0)" by (rule lift_NF)
+ hence "listall NF [lift t' 0]" by (rule listall_cons) (rule listall_nil)
+ hence "NF (Var 0 \<degree>\<degree> [lift t' 0])" by (rule NF.App)
+ thus "NF (Var 0 \<degree> lift t' 0)" by simp
show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t' 0 : U"
proof (rule typing.App)
show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
@@ -415,9 +405,9 @@
from sred show "e \<turnstile> s' : T \<Rightarrow> U"
by (rule subject_reduction') (rule rtyping_imp_typing)
qed
- then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "u \<in> NF" by simp iprover
+ then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "NF u" by simp iprover
from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App)
- hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtrancl_trans)
+ hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtrancl_trans')
with unf show ?case by iprover
qed
@@ -427,23 +417,23 @@
declare NF.induct [ind_realizer]
declare rtrancl.induct [ind_realizer irrelevant]
declare rtyping.induct [ind_realizer]
-lemmas [extraction_expand] = trans_def conj_assoc listall_cons_eq
+lemmas [extraction_expand] = conj_assoc listall_cons_eq
extract type_NF
-lemma rtranclR_rtrancl_eq: "((a, b) \<in> rtranclR r) = ((a, b) \<in> rtrancl (Collect r))"
+lemma rtranclR_rtrancl_eq: "rtranclR r a b = rtrancl r a b"
apply (rule iffI)
apply (erule rtranclR.induct)
- apply (rule rtrancl_refl)
- apply (erule rtrancl_into_rtrancl)
- apply (erule CollectI)
+ apply (rule rtrancl.rtrancl_refl)
+ apply (erule rtrancl.rtrancl_into_rtrancl)
+ apply assumption
apply (erule rtrancl.induct)
apply (rule rtranclR.rtrancl_refl)
apply (erule rtranclR.rtrancl_into_rtrancl)
- apply (erule CollectD)
+ apply assumption
done
-lemma NFR_imp_NF: "(nf, t) \<in> NFR \<Longrightarrow> t \<in> NF"
+lemma NFR_imp_NF: "NFR nf t \<Longrightarrow> NF t"
apply (erule NFR.induct)
apply (rule NF.intros)
apply (simp add: listall_def)
--- a/src/HOL/MicroJava/BV/BVExample.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy Wed Feb 07 17:44:07 2007 +0100
@@ -65,27 +65,27 @@
text {* The subclass releation spelled out: *}
lemma subcls1:
- "subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
+ "subcls1 E = member2 {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
(Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
apply (simp add: subcls1_def2)
apply (simp add: name_defs class_defs system_defs E_def class_def)
- apply (auto split: split_if_asm)
+ apply (auto simp: member2_inject split: split_if_asm)
done
text {* The subclass relation is acyclic; hence its converse is well founded: *}
lemma notin_rtrancl:
- "(a,b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a,y) \<notin> r) \<Longrightarrow> False"
- by (auto elim: converse_rtranclE)
+ "r\<^sup>*\<^sup>* a b \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. \<not> r a y) \<Longrightarrow> False"
+ by (auto elim: converse_rtranclE')
-lemma acyclic_subcls1_E: "acyclic (subcls1 E)"
- apply (rule acyclicI)
+lemma acyclic_subcls1_E: "acyclicP (subcls1 E)"
+ apply (rule acyclicI [to_pred])
apply (simp add: subcls1)
- apply (auto dest!: tranclD)
+ apply (auto dest!: tranclD')
apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes)
done
-lemma wf_subcls1_E: "wf ((subcls1 E)\<inverse>)"
- apply (rule finite_acyclic_wf_converse)
+lemma wf_subcls1_E: "wfP ((subcls1 E)\<inverse>\<inverse>)"
+ apply (rule finite_acyclic_wf_converse [to_pred])
apply (simp add: subcls1)
apply (rule acyclic_subcls1_E)
done
@@ -431,8 +431,6 @@
apply simp+
done
-lemmas [code] = lessThan_0 lessThan_Suc
-
constdefs
some_elem :: "'a set \<Rightarrow> 'a"
"some_elem == (%S. SOME x. x : S)"
@@ -464,7 +462,7 @@
meta_eq_to_obj_eq [OF JType.sup_def [unfolded exec_lub_def]]
meta_eq_to_obj_eq [OF JVM_le_unfold]
-lemmas [code ind] = rtrancl_refl converse_rtrancl_into_rtrancl
+lemmas [code ind] = rtrancl.rtrancl_refl converse_rtrancl_into_rtrancl'
code_module BV
contains
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Wed Feb 07 17:44:07 2007 +0100
@@ -190,7 +190,7 @@
lemma isIntgI [intro, simp]: "G,hp \<turnstile> v ::\<preceq> PrimT Integer \<Longrightarrow> isIntg v"
apply (unfold conf_def)
apply auto
- apply (erule widen.elims)
+ apply (erule widen.cases)
apply auto
apply (cases v)
apply auto
@@ -322,7 +322,7 @@
obtain apTs X ST' where
ST: "ST = rev apTs @ X # ST'" and
ps: "length apTs = length ps" and
- w: "\<forall>x\<in>set (zip apTs ps). x \<in> widen G" and
+ w: "\<forall>(x, y)\<in>set (zip apTs ps). G \<turnstile> x \<preceq> y" and
C: "G \<turnstile> X \<preceq> Class C" and
mth: "method (G, C) (mn, ps) \<noteq> None"
by (simp del: app'.simps) blast
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Feb 07 17:44:07 2007 +0100
@@ -91,7 +91,7 @@
from False C
have "\<not> match_exception_entry G C pc e"
by - (erule contrapos_nn,
- auto simp add: match_exception_entry_def elim: rtrancl_trans)
+ auto simp add: match_exception_entry_def)
with m
have "match_exception_table G C pc (e#es) = Some pc'" by simp
moreover note C
@@ -640,7 +640,7 @@
apply (simp add: null)
apply (clarsimp simp add: conf_def obj_ty_def)
apply (cases v)
-apply (auto intro: rtrancl_trans)
+apply auto
done
lemmas defs2 = defs1 raise_system_xcpt_def
@@ -838,7 +838,7 @@
s: "s = (rev apTs @ X # ST, LT)" and
l: "length apTs = length pTs" and
X: "G\<turnstile> X \<preceq> Class C'" and
- w: "\<forall>x\<in>set (zip apTs pTs). x \<in> widen G" and
+ w: "\<forall>(x, y)\<in>set (zip apTs pTs). G \<turnstile> x \<preceq> y" and
mC':"method (G, C') (mn, pTs) = Some (D', rT, body)" and
pc: "Suc pc < length ins" and
eff: "G \<turnstile> norm_eff (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc"
--- a/src/HOL/MicroJava/BV/Correct.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Wed Feb 07 17:44:07 2007 +0100
@@ -224,7 +224,7 @@
by (simp add: list_all2_append2 approx_stk_def approx_loc_def)
lemma approx_stk_all_widen:
- "\<lbrakk> approx_stk G hp stk ST; \<forall>x \<in> set (zip ST ST'). x \<in> widen G; length ST = length ST'; wf_prog wt G \<rbrakk>
+ "\<lbrakk> approx_stk G hp stk ST; \<forall>(x, y) \<in> set (zip ST ST'). G \<turnstile> x \<preceq> y; length ST = length ST'; wf_prog wt G \<rbrakk>
\<Longrightarrow> approx_stk G hp stk ST'"
apply (unfold approx_stk_def)
apply (clarsimp simp add: approx_loc_conv_all_nth all_set_conv_all_nth)
--- a/src/HOL/MicroJava/BV/EffectMono.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy Wed Feb 07 17:44:07 2007 +0100
@@ -10,7 +10,7 @@
lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
- by (auto elim: widen.elims)
+ by (auto elim: widen.cases)
lemma sup_loc_some [rule_format]:
@@ -42,7 +42,7 @@
lemma all_widen_is_sup_loc:
"\<forall>b. length a = length b \<longrightarrow>
- (\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map OK a) <=l (map OK b))"
+ (\<forall>(x, y)\<in>set (zip a b). G \<turnstile> x \<preceq> y) = (G \<turnstile> (map OK a) <=l (map OK b))"
(is "\<forall>b. length a = length b \<longrightarrow> ?Q a b" is "?P a")
proof (induct "a")
show "?P []" by simp
@@ -219,7 +219,7 @@
l: "length apTs = length list" and
c: "is_class G cname" and
C: "G \<turnstile> X \<preceq> Class cname" and
- w: "\<forall>x \<in> set (zip apTs list). x \<in> widen G" and
+ w: "\<forall>(x, y) \<in> set (zip apTs list). G \<turnstile> x \<preceq> y" and
m: "method (G, cname) (mname, list) = Some (mD', rT', b')" and
x: "\<forall>C \<in> set (match_any G pc et). is_class G C"
by (simp del: not_None_eq, elim exE conjE) (rule that)
@@ -261,7 +261,7 @@
have "G \<turnstile> map OK apTs' <=l map OK list" .
with l'
- have w': "\<forall>x \<in> set (zip apTs' list). x \<in> widen G"
+ have w': "\<forall>(x, y) \<in> set (zip apTs' list). G \<turnstile> x \<preceq> y"
by (simp add: all_widen_is_sup_loc)
from Invoke s2 l' w' C' m c x
--- a/src/HOL/MicroJava/BV/Err.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy Wed Feb 07 17:44:07 2007 +0100
@@ -155,7 +155,7 @@
lemma acc_err [simp, intro!]: "acc r \<Longrightarrow> acc(le r)"
apply (unfold acc_def lesub_def le_def lesssub_def)
-apply (simp add: wf_eq_minimal split: err.split)
+apply (simp add: wfP_eq_minimal split: err.split)
apply clarify
apply (case_tac "Err : Q")
apply blast
--- a/src/HOL/MicroJava/BV/JType.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy Wed Feb 07 17:44:07 2007 +0100
@@ -13,7 +13,7 @@
"super G C == fst (the (class G C))"
lemma superI:
- "(C,D) \<in> subcls1 G \<Longrightarrow> super G C = D"
+ "G \<turnstile> C \<prec>C1 D \<Longrightarrow> super G C = D"
by (unfold super_def) (auto dest: subcls1D)
constdefs
@@ -34,7 +34,7 @@
is_ty :: "'c prog \<Rightarrow> ty \<Rightarrow> bool"
"is_ty G T == case T of PrimT P \<Rightarrow> True | RefT R \<Rightarrow>
- (case R of NullT \<Rightarrow> True | ClassT C \<Rightarrow> (C,Object):(subcls1 G)^*)"
+ (case R of NullT \<Rightarrow> True | ClassT C \<Rightarrow> (subcls1 G)^** C Object)"
translations
@@ -45,10 +45,10 @@
"esl G == (types G, subtype G, sup G)"
lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
- by (auto elim: widen.elims)
+ by (auto elim: widen.cases)
lemma PrimT_PrimT2: "(G \<turnstile> PrimT p \<preceq> xb) = (xb = PrimT p)"
- by (auto elim: widen.elims)
+ by (auto elim: widen.cases)
lemma is_tyI:
"\<lbrakk> is_type G T; ws_prog G \<rbrakk> \<Longrightarrow> is_ty G T"
@@ -77,8 +77,8 @@
from R wf ty
have "R \<noteq> ClassT Object \<Longrightarrow> ?thesis"
by (auto simp add: is_ty_def is_class_def split_tupled_all
- elim!: subcls1.elims
- elim: converse_rtranclE
+ elim!: subcls1.cases
+ elim: converse_rtranclE'
split: ref_ty.splits)
ultimately
show ?thesis by blast
@@ -86,7 +86,7 @@
qed
lemma order_widen:
- "acyclic (subcls1 G) \<Longrightarrow> order (subtype G)"
+ "acyclicP (subcls1 G) \<Longrightarrow> order (subtype G)"
apply (unfold Semilat.order_def lesub_def subtype_def)
apply (auto intro: widen_trans)
apply (case_tac x)
@@ -102,16 +102,16 @@
apply (case_tac ref_tya)
apply simp
apply simp
- apply (auto dest: acyclic_impl_antisym_rtrancl antisymD)
+ apply (auto dest: acyclic_impl_antisym_rtrancl [to_pred] antisymD)
done
lemma wf_converse_subcls1_impl_acc_subtype:
- "wf ((subcls1 G)^-1) \<Longrightarrow> acc (subtype G)"
-apply (unfold acc_def lesssub_def)
-apply (drule_tac p = "(subcls1 G)^-1 - Id" in wf_subset)
- apply blast
-apply (drule wf_trancl)
-apply (simp add: wf_eq_minimal)
+ "wfP ((subcls1 G)^--1) \<Longrightarrow> acc (subtype G)"
+apply (unfold Semilat.acc_def lesssub_def)
+apply (drule_tac p = "meet ((subcls1 G)^--1) op \<noteq>" in wfP_subset)
+ apply auto
+apply (drule wfP_trancl)
+apply (simp add: wfP_eq_minimal)
apply clarify
apply (unfold lesub_def subtype_def)
apply (rename_tac M T)
@@ -146,20 +146,20 @@
apply (case_tac t)
apply simp
apply simp
-apply (insert rtrancl_r_diff_Id [symmetric, standard, of "(subcls1 G)"])
+apply (insert rtrancl_r_diff_Id' [symmetric, standard, of "subcls1 G"])
apply simp
-apply (erule rtranclE)
+apply (erule rtrancl.cases)
apply blast
-apply (drule rtrancl_converseI)
-apply (subgoal_tac "((subcls1 G)-Id)^-1 = ((subcls1 G)^-1 - Id)")
+apply (drule rtrancl_converseI')
+apply (subgoal_tac "(meet (subcls1 G) op \<noteq>)^--1 = (meet ((subcls1 G)^--1) op \<noteq>)")
prefer 2
- apply blast
-apply simp
-apply (blast intro: rtrancl_into_trancl2)
+ apply (simp add: converse_meet)
+apply simp
+apply (blast intro: rtrancl_into_trancl2')
done
lemma closed_err_types:
- "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk>
+ "\<lbrakk> ws_prog G; single_valuedP (subcls1 G); acyclicP (subcls1 G) \<rbrakk>
\<Longrightarrow> closed (err (types G)) (lift2 (sup G))"
apply (unfold closed_def plussub_def lift2_def sup_def)
apply (auto split: err.split)
@@ -171,13 +171,13 @@
lemma sup_subtype_greater:
- "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G);
+ "\<lbrakk> ws_prog G; single_valuedP (subcls1 G); acyclicP (subcls1 G);
is_type G t1; is_type G t2; sup G t1 t2 = OK s \<rbrakk>
\<Longrightarrow> subtype G t1 s \<and> subtype G t2 s"
proof -
assume ws_prog: "ws_prog G"
- assume single_valued: "single_valued (subcls1 G)"
- assume acyclic: "acyclic (subcls1 G)"
+ assume single_valued: "single_valuedP (subcls1 G)"
+ assume acyclic: "acyclicP (subcls1 G)"
{ fix c1 c2
assume is_class: "is_class G c1" "is_class G c2"
@@ -188,12 +188,12 @@
by (blast intro: subcls_C_Object)
with ws_prog single_valued
obtain u where
- "is_lub ((subcls1 G)^* ) c1 c2 u"
+ "is_lub ((subcls1 G)^** ) c1 c2 u"
by (blast dest: single_valued_has_lubs)
moreover
note acyclic
moreover
- have "\<forall>x y. (x, y) \<in> subcls1 G \<longrightarrow> super G x = y"
+ have "\<forall>x y. G \<turnstile> x \<prec>C1 y \<longrightarrow> super G x = y"
by (blast intro: superI)
ultimately
have "G \<turnstile> c1 \<preceq>C exec_lub (subcls1 G) (super G) c1 c2 \<and>
@@ -210,14 +210,14 @@
qed
lemma sup_subtype_smallest:
- "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G);
+ "\<lbrakk> ws_prog G; single_valuedP (subcls1 G); acyclicP (subcls1 G);
is_type G a; is_type G b; is_type G c;
subtype G a c; subtype G b c; sup G a b = OK d \<rbrakk>
\<Longrightarrow> subtype G d c"
proof -
assume ws_prog: "ws_prog G"
- assume single_valued: "single_valued (subcls1 G)"
- assume acyclic: "acyclic (subcls1 G)"
+ assume single_valued: "single_valuedP (subcls1 G)"
+ assume acyclic: "acyclicP (subcls1 G)"
{ fix c1 c2 D
assume is_class: "is_class G c1" "is_class G c2"
@@ -229,7 +229,7 @@
by (blast intro: subcls_C_Object)
with ws_prog single_valued
obtain u where
- lub: "is_lub ((subcls1 G)^* ) c1 c2 u"
+ lub: "is_lub ((subcls1 G)^** ) c1 c2 u"
by (blast dest: single_valued_has_lubs)
with acyclic
have "exec_lub (subcls1 G) (super G) c1 c2 = u"
@@ -260,12 +260,12 @@
split: ty.splits ref_ty.splits)
lemma err_semilat_JType_esl_lemma:
- "\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk>
+ "\<lbrakk> ws_prog G; single_valuedP (subcls1 G); acyclicP (subcls1 G) \<rbrakk>
\<Longrightarrow> err_semilat (esl G)"
proof -
assume ws_prog: "ws_prog G"
- assume single_valued: "single_valued (subcls1 G)"
- assume acyclic: "acyclic (subcls1 G)"
+ assume single_valued: "single_valuedP (subcls1 G)"
+ assume acyclic: "acyclicP (subcls1 G)"
hence "order (subtype G)"
by (rule order_widen)
@@ -297,9 +297,9 @@
qed
lemma single_valued_subcls1:
- "ws_prog G \<Longrightarrow> single_valued (subcls1 G)"
+ "ws_prog G \<Longrightarrow> single_valuedP (subcls1 G)"
by (auto simp add: ws_prog_def unique_def single_valued_def
- intro: subcls1I elim!: subcls1.elims)
+ intro: subcls1I elim!: subcls1.cases)
theorem err_semilat_JType_esl:
"ws_prog G \<Longrightarrow> err_semilat (esl G)"
--- a/src/HOL/MicroJava/BV/JVM.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy Wed Feb 07 17:44:07 2007 +0100
@@ -40,7 +40,7 @@
simp add: symmetric sl_triple_conv)
apply (simp (no_asm) add: JVM_le_unfold)
apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype
- dest: wf_subcls1 wf_acyclic wf_prog_ws_prog)
+ dest: wf_subcls1 wfP_acyclicP wf_prog_ws_prog)
apply (simp add: JVM_le_unfold)
apply (erule exec_pres_type)
apply assumption
--- a/src/HOL/MicroJava/BV/JVMType.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Wed Feb 07 17:44:07 2007 +0100
@@ -193,7 +193,7 @@
lemma widen_PrimT_conv1 [simp]:
"\<lbrakk> G \<turnstile> S \<preceq> T; S = PrimT x\<rbrakk> \<Longrightarrow> T = PrimT x"
- by (auto elim: widen.elims)
+ by (auto elim: widen.cases)
theorem sup_PTS_eq:
"(G \<turnstile> OK (PrimT p) <=o X) = (X=Err \<or> X = OK (PrimT p))"
--- a/src/HOL/MicroJava/BV/Kildall.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy Wed Feb 07 17:44:07 2007 +0100
@@ -402,7 +402,7 @@
-- "Well-foundedness of the termination relation:"
apply (rule wf_lex_prod)
apply (insert orderI [THEN acc_le_listI])
- apply (simp only: acc_def lesssub_def)
+ apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric])
apply (rule wf_finite_psubset)
-- "Loop decreases along termination relation:"
--- a/src/HOL/MicroJava/BV/Listn.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy Wed Feb 07 17:44:07 2007 +0100
@@ -321,22 +321,22 @@
"\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
apply (unfold acc_def)
apply (subgoal_tac
- "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})")
- apply (erule wf_subset)
+ "wfP (SUP n. (\<lambda>ys xs. size xs = n & size ys = n & xs <_(Listn.le r) ys))")
+ apply (erule wfP_subset)
apply (blast intro: lesssub_list_impl_same_size)
-apply (rule wf_UN)
+apply (rule wfP_SUP)
prefer 2
apply clarify
apply (rename_tac m n)
apply (case_tac "m=n")
apply simp
- apply (fast intro!: equals0I dest: not_sym)
+ apply (fast intro!: equals0I [to_pred] dest: not_sym)
apply clarify
apply (rename_tac n)
apply (induct_tac n)
apply (simp add: lesssub_def cong: conj_cong)
apply (rename_tac k)
-apply (simp add: wf_eq_minimal)
+apply (simp add: wfP_eq_minimal)
apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
apply clarify
apply (rename_tac M m)
--- a/src/HOL/MicroJava/BV/Opt.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy Wed Feb 07 17:44:07 2007 +0100
@@ -272,7 +272,7 @@
lemma acc_le_optI [intro!]:
"acc r \<Longrightarrow> acc(le r)"
apply (unfold acc_def lesub_def le_def lesssub_def)
-apply (simp add: wf_eq_minimal split: option.split)
+apply (simp add: wfP_eq_minimal split: option.split)
apply clarify
apply (case_tac "? a. Some a : Q")
apply (erule_tac x = "{a . Some a : Q}" in allE)
--- a/src/HOL/MicroJava/BV/Product.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Product.thy Wed Feb 07 17:44:07 2007 +0100
@@ -51,8 +51,8 @@
lemma acc_le_prodI [intro!]:
"\<lbrakk> acc rA; acc rB \<rbrakk> \<Longrightarrow> acc(Product.le rA rB)"
apply (unfold acc_def)
-apply (rule wf_subset)
- apply (erule wf_lex_prod)
+apply (rule wfP_subset)
+ apply (erule wf_lex_prod [to_pred, THEN wfP_wf_eq [THEN iffD2]])
apply assumption
apply (auto simp add: lesssub_def less_prod_Pair_conv lex_prod_def)
done
--- a/src/HOL/MicroJava/BV/Semilat.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy Wed Feb 07 17:44:07 2007 +0100
@@ -40,16 +40,13 @@
constdefs
- ord :: "('a*'a)set \<Rightarrow> 'a ord"
-"ord r == %x y. (x,y):r"
-
order :: "'a ord \<Rightarrow> bool"
"order r == (!x. x <=_r x) &
(!x y. x <=_r y & y <=_r x \<longrightarrow> x=y) &
(!x y z. x <=_r y & y <=_r z \<longrightarrow> x <=_r z)"
acc :: "'a ord \<Rightarrow> bool"
-"acc r == wf{(y,x) . x <_r y}"
+"acc r == wfP (\<lambda>y x. x <_r y)"
top :: "'a ord \<Rightarrow> 'a \<Rightarrow> bool"
"top r T == !x. x <=_r T"
@@ -63,13 +60,13 @@
(!x:A. !y:A. y <=_r x +_f y) &
(!x:A. !y:A. !z:A. x <=_r z & y <=_r z \<longrightarrow> x +_f y <=_r z)"
- is_ub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-"is_ub r x y u == (x,u):r & (y,u):r"
+ is_ub :: "'a ord \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+"is_ub r x y u == r x u & r y u"
- is_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
+ is_lub :: "'a ord \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> r u z)"
- some_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ some_lub :: "'a ord \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
"some_lub r x y == SOME z. is_lub r x y z";
locale (open) semilat =
@@ -244,113 +241,113 @@
by(blast intro: order_antisym plus_com_lemma)
lemma is_lubD:
- "is_lub r x y u \<Longrightarrow> is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
+ "is_lub r x y u \<Longrightarrow> is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> r u z)"
by (simp add: is_lub_def)
lemma is_ubI:
- "\<lbrakk> (x,u) : r; (y,u) : r \<rbrakk> \<Longrightarrow> is_ub r x y u"
+ "\<lbrakk> r x u; r y u \<rbrakk> \<Longrightarrow> is_ub r x y u"
by (simp add: is_ub_def)
lemma is_ubD:
- "is_ub r x y u \<Longrightarrow> (x,u) : r & (y,u) : r"
+ "is_ub r x y u \<Longrightarrow> r x u & r y u"
by (simp add: is_ub_def)
lemma is_lub_bigger1 [iff]:
- "is_lub (r^* ) x y y = ((x,y):r^* )"
+ "is_lub (r^** ) x y y = r^** x y"
apply (unfold is_lub_def is_ub_def)
apply blast
done
lemma is_lub_bigger2 [iff]:
- "is_lub (r^* ) x y x = ((y,x):r^* )"
+ "is_lub (r^** ) x y x = r^** y x"
apply (unfold is_lub_def is_ub_def)
apply blast
done
lemma extend_lub:
- "\<lbrakk> single_valued r; is_lub (r^* ) x y u; (x',x) : r \<rbrakk>
- \<Longrightarrow> EX v. is_lub (r^* ) x' y v"
+ "\<lbrakk> single_valuedP r; is_lub (r^** ) x y u; r x' x \<rbrakk>
+ \<Longrightarrow> EX v. is_lub (r^** ) x' y v"
apply (unfold is_lub_def is_ub_def)
-apply (case_tac "(y,x) : r^*")
- apply (case_tac "(y,x') : r^*")
+apply (case_tac "r^** y x")
+ apply (case_tac "r^** y x'")
apply blast
- apply (blast elim: converse_rtranclE dest: single_valuedD)
+ apply (blast elim: converse_rtranclE' dest: single_valuedD)
apply (rule exI)
apply (rule conjI)
- apply (blast intro: converse_rtrancl_into_rtrancl dest: single_valuedD)
-apply (blast intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl
- elim: converse_rtranclE dest: single_valuedD)
+ apply (blast intro: converse_rtrancl_into_rtrancl' dest: single_valuedD)
+apply (blast intro: rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl'
+ elim: converse_rtranclE' dest: single_valuedD)
done
lemma single_valued_has_lubs [rule_format]:
- "\<lbrakk> single_valued r; (x,u) : r^* \<rbrakk> \<Longrightarrow> (!y. (y,u) : r^* \<longrightarrow>
- (EX z. is_lub (r^* ) x y z))"
-apply (erule converse_rtrancl_induct)
+ "\<lbrakk> single_valuedP r; r^** x u \<rbrakk> \<Longrightarrow> (!y. r^** y u \<longrightarrow>
+ (EX z. is_lub (r^** ) x y z))"
+apply (erule converse_rtrancl_induct')
apply clarify
- apply (erule converse_rtrancl_induct)
+ apply (erule converse_rtrancl_induct')
apply blast
- apply (blast intro: converse_rtrancl_into_rtrancl)
+ apply (blast intro: converse_rtrancl_into_rtrancl')
apply (blast intro: extend_lub)
done
lemma some_lub_conv:
- "\<lbrakk> acyclic r; is_lub (r^* ) x y u \<rbrakk> \<Longrightarrow> some_lub (r^* ) x y = u"
+ "\<lbrakk> acyclicP r; is_lub (r^** ) x y u \<rbrakk> \<Longrightarrow> some_lub (r^** ) x y = u"
apply (unfold some_lub_def is_lub_def)
apply (rule someI2)
apply assumption
-apply (blast intro: antisymD dest!: acyclic_impl_antisym_rtrancl)
+apply (blast intro: antisymD dest!: acyclic_impl_antisym_rtrancl [to_pred])
done
lemma is_lub_some_lub:
- "\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^* \<rbrakk>
- \<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)";
+ "\<lbrakk> single_valuedP r; acyclicP r; r^** x u; r^** y u \<rbrakk>
+ \<Longrightarrow> is_lub (r^** ) x y (some_lub (r^** ) x y)";
by (fastsimp dest: single_valued_has_lubs simp add: some_lub_conv)
subsection{*An executable lub-finder*}
constdefs
- exec_lub :: "('a * 'a) set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a binop"
-"exec_lub r f x y == while (\<lambda>z. (x,z) \<notin> r\<^sup>*) f y"
+ exec_lub :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a binop"
+"exec_lub r f x y == while (\<lambda>z. \<not> r\<^sup>*\<^sup>* x z) f y"
lemma acyclic_single_valued_finite:
- "\<lbrakk>acyclic r; single_valued r; (x,y) \<in> r\<^sup>*\<rbrakk>
- \<Longrightarrow> finite (r \<inter> {a. (x, a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})"
-apply(erule converse_rtrancl_induct)
+ "\<lbrakk>acyclicP r; single_valuedP r; r\<^sup>*\<^sup>* x y \<rbrakk>
+ \<Longrightarrow> finite (Collect2 r \<inter> {a. r\<^sup>*\<^sup>* x a} \<times> {b. r\<^sup>*\<^sup>* b y})"
+apply(erule converse_rtrancl_induct')
apply(rule_tac B = "{}" in finite_subset)
- apply(simp only:acyclic_def)
- apply(blast intro:rtrancl_into_trancl2 rtrancl_trancl_trancl)
+ apply(simp only:acyclic_def [to_pred])
+ apply(blast intro:rtrancl_into_trancl2' rtrancl_trancl_trancl')
apply simp
apply(rename_tac x x')
-apply(subgoal_tac "r \<inter> {a. (x,a) \<in> r\<^sup>*} \<times> {b. (b,y) \<in> r\<^sup>*} =
- insert (x,x') (r \<inter> {a. (x', a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})")
+apply(subgoal_tac "Collect2 r \<inter> {a. r\<^sup>*\<^sup>* x a} \<times> {b. r\<^sup>*\<^sup>* b y} =
+ insert (x,x') (Collect2 r \<inter> {a. r\<^sup>*\<^sup>* x' a} \<times> {b. r\<^sup>*\<^sup>* b y})")
apply simp
-apply(blast intro:converse_rtrancl_into_rtrancl
- elim:converse_rtranclE dest:single_valuedD)
+apply(blast intro:converse_rtrancl_into_rtrancl'
+ elim:converse_rtranclE' dest:single_valuedD)
done
lemma exec_lub_conv:
- "\<lbrakk> acyclic r; !x y. (x,y) \<in> r \<longrightarrow> f x = y; is_lub (r\<^sup>*) x y u \<rbrakk> \<Longrightarrow>
+ "\<lbrakk> acyclicP r; !x y. r x y \<longrightarrow> f x = y; is_lub (r\<^sup>*\<^sup>*) x y u \<rbrakk> \<Longrightarrow>
exec_lub r f x y = u";
apply(unfold exec_lub_def)
-apply(rule_tac P = "\<lambda>z. (y,z) \<in> r\<^sup>* \<and> (z,u) \<in> r\<^sup>*" and
- r = "(r \<inter> {(a,b). (y,a) \<in> r\<^sup>* \<and> (b,u) \<in> r\<^sup>*})^-1" in while_rule)
+apply(rule_tac P = "\<lambda>z. r\<^sup>*\<^sup>* y z \<and> r\<^sup>*\<^sup>* z u" and
+ r = "(Collect2 r \<inter> {(a,b). r\<^sup>*\<^sup>* y a \<and> r\<^sup>*\<^sup>* b u})^-1" in while_rule)
apply(blast dest: is_lubD is_ubD)
apply(erule conjE)
- apply(erule_tac z = u in converse_rtranclE)
+ apply(erule_tac z = u in converse_rtranclE')
apply(blast dest: is_lubD is_ubD)
- apply(blast dest:rtrancl_into_rtrancl)
+ apply(blast dest: rtrancl.rtrancl_into_rtrancl)
apply(rename_tac s)
- apply(subgoal_tac "is_ub (r\<^sup>*) x y s")
+ apply(subgoal_tac "is_ub (r\<^sup>*\<^sup>*) x y s")
prefer 2; apply(simp add:is_ub_def)
- apply(subgoal_tac "(u, s) \<in> r\<^sup>*")
+ apply(subgoal_tac "r\<^sup>*\<^sup>* u s")
prefer 2; apply(blast dest:is_lubD)
- apply(erule converse_rtranclE)
+ apply(erule converse_rtranclE')
apply blast
- apply(simp only:acyclic_def)
- apply(blast intro:rtrancl_into_trancl2 rtrancl_trancl_trancl)
+ apply(simp only:acyclic_def [to_pred])
+ apply(blast intro:rtrancl_into_trancl2' rtrancl_trancl_trancl')
apply(rule finite_acyclic_wf)
apply simp
apply(erule acyclic_single_valued_finite)
@@ -361,14 +358,14 @@
apply blast
apply simp
apply(erule conjE)
-apply(erule_tac z = u in converse_rtranclE)
+apply(erule_tac z = u in converse_rtranclE')
apply(blast dest: is_lubD is_ubD)
-apply(blast dest:rtrancl_into_rtrancl)
+apply blast
done
lemma is_lub_exec_lub:
- "\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^*; !x y. (x,y) \<in> r \<longrightarrow> f x = y \<rbrakk>
- \<Longrightarrow> is_lub (r^* ) x y (exec_lub r f x y)"
+ "\<lbrakk> single_valuedP r; acyclicP r; r^** x u; r^** y u; !x y. r x y \<longrightarrow> f x = y \<rbrakk>
+ \<Longrightarrow> is_lub (r^** ) x y (exec_lub r f x y)"
by (fastsimp dest: single_valued_has_lubs simp add: exec_lub_conv)
end
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy Wed Feb 07 17:44:07 2007 +0100
@@ -14,14 +14,14 @@
(* If no exception is present after evaluation/execution,
none can have been present before *)
lemma eval_evals_exec_xcpt:
- "((xs,ex,val,xs') \<in> Eval.eval G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
- ((xs,exs,vals,xs') \<in> Eval.evals G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
- ((xs,st,xs') \<in> Eval.exec G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None)"
+ "(G \<turnstile> xs -ex\<succ>val-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
+ (G \<turnstile> xs -exs[\<succ>]vals-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
+ (G \<turnstile> xs -st-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None)"
by (induct rule: eval_evals_exec.induct, auto)
(* instance of eval_evals_exec_xcpt for eval *)
-lemma eval_xcpt: "(xs,ex,val,xs') \<in> Eval.eval G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
+lemma eval_xcpt: "G \<turnstile> xs -ex\<succ>val-> xs' \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
(is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T")
proof-
assume h1: ?H1
@@ -30,7 +30,7 @@
qed
(* instance of eval_evals_exec_xcpt for evals *)
-lemma evals_xcpt: "(xs,exs,vals,xs') \<in> Eval.evals G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
+lemma evals_xcpt: "G \<turnstile> xs -exs[\<succ>]vals-> xs' \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
(is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T")
proof-
assume h1: ?H1
@@ -39,7 +39,7 @@
qed
(* instance of eval_evals_exec_xcpt for exec *)
-lemma exec_xcpt: "(xs,st,xs') \<in> Eval.exec G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
+lemma exec_xcpt: "G \<turnstile> xs -st-> xs' \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
(is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T")
proof-
assume h1: ?H1
@@ -404,7 +404,7 @@
E\<turnstile>ps[::]pTs & max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')})"
apply (simp only: wtpd_expr_def wtpd_exprs_def)
apply (erule exE)
-apply (ind_cases "E \<turnstile> {C}a..mn( {pTs'}ps) :: T")
+apply (ind_cases2 "E \<turnstile> {C}a..mn( {pTs'}ps) :: T" for T)
apply (auto simp: max_spec_preserves_length)
done
@@ -437,7 +437,7 @@
"\<forall> xs'. (G \<turnstile> xk -xj\<succ>xi-> xh \<longrightarrow> True) &
(G\<turnstile> xs -es[\<succ>]vs-> xs' \<longrightarrow> (\<exists> s. (xs' = (None, s))) \<longrightarrow>
length es = length vs) &
- ((xc, xb, xa) \<in> Eval.exec G \<longrightarrow> True)")
+ (G \<turnstile> xc -xb-> xa \<longrightarrow> True)")
apply blast
apply (rule allI)
apply (rule Eval.eval_evals_exec.induct)
@@ -576,7 +576,7 @@
done
lemma state_ok_evals: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_exprs E es;
- (xs,es,vs,xs') \<in> Eval.evals (prg E)\<rbrakk> \<Longrightarrow> xs'::\<preceq>E"
+ prg E \<turnstile> xs -es[\<succ>]vs-> xs'\<rbrakk> \<Longrightarrow> xs'::\<preceq>E"
apply (simp only: wtpd_exprs_def)
apply (erule exE)
apply (case_tac xs) apply (case_tac xs')
@@ -584,7 +584,7 @@
done
lemma state_ok_exec: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_stmt E st;
- (xs,st,xs') \<in> Eval.exec (prg E)\<rbrakk> \<Longrightarrow> xs'::\<preceq>E"
+ prg E \<turnstile> xs -st-> xs'\<rbrakk> \<Longrightarrow> xs'::\<preceq>E"
apply (simp only: wtpd_stmt_def)
apply (case_tac xs', case_tac xs)
apply (auto dest: exec_type_sound)
@@ -618,13 +618,13 @@
apply simp
apply (rule allI)
apply (rule iffI)
- apply (ind_cases "E \<turnstile> [] [::] Ts", assumption)
+ apply (ind_cases2 "E \<turnstile> [] [::] Ts" for Ts, assumption)
apply simp apply (rule WellType.Nil)
apply (simp add: list_all2_Cons1)
apply (rule allI)
apply (rule iffI)
apply (rename_tac a exs Ts)
- apply (ind_cases "E \<turnstile> a # exs [::] Ts") apply blast
+ apply (ind_cases2 "E \<turnstile> a # exs [::] Ts" for a exs Ts) apply blast
apply (auto intro: WellType.Cons)
done
@@ -718,7 +718,7 @@
(* 2. possibly skip env_of_jmb ??? *)
theorem compiler_correctness:
"wf_java_prog G \<Longrightarrow>
- ((xs,ex,val,xs') \<in> Eval.eval G \<longrightarrow>
+ (G \<turnstile> xs -ex\<succ>val-> xs' \<longrightarrow>
gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
(\<forall> os CL S.
(class_sig_defined G CL S) \<longrightarrow>
@@ -729,7 +729,7 @@
>- (compExpr (gmb G CL S) ex) \<rightarrow>
{gh xs', val#os, locvars_xstate G CL S xs'}))) \<and>
- ((xs,exs,vals,xs') \<in> Eval.evals G \<longrightarrow>
+ (G \<turnstile> xs -exs[\<succ>]vals-> xs' \<longrightarrow>
gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
(\<forall> os CL S.
(class_sig_defined G CL S) \<longrightarrow>
@@ -740,7 +740,7 @@
>- (compExprs (gmb G CL S) exs) \<rightarrow>
{gh xs', (rev vals)@os, (locvars_xstate G CL S xs')}))) \<and>
- ((xs,st,xs') \<in> Eval.exec G \<longrightarrow>
+ (G \<turnstile> xs -st-> xs' \<longrightarrow>
gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
(\<forall> os CL S.
(class_sig_defined G CL S) \<longrightarrow>
@@ -1189,7 +1189,7 @@
(* show list_all2 (conf G h) pvs pTs *)
apply (erule exE)+ apply (erule conjE)+
apply (rule_tac Ts="pTsa" in conf_list_gext_widen) apply assumption
-apply (subgoal_tac "((gx s1, gs s1), ps, pvs, x, h, l) \<in> evals G")
+apply (subgoal_tac "G \<turnstile> (gx s1, gs s1) -ps[\<succ>]pvs-> (x, h, l)")
apply (frule_tac E="env_of_jmb G CL S" in evals_type_sound)
apply assumption+
apply (simp only: env_of_jmb_fst)
@@ -1247,7 +1247,7 @@
done
theorem compiler_correctness_exec: "
- \<lbrakk> ((None,hp,loc), st, (None,hp',loc')) \<in> Eval.exec G;
+ \<lbrakk> G \<turnstile> Norm (hp, loc) -st-> Norm (hp', loc');
wf_java_prog G;
class_sig_defined G C S;
wtpd_stmt (env_of_jmb G C S) st;
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Wed Feb 07 17:44:07 2007 +0100
@@ -109,22 +109,24 @@
by (case_tac "class G C", auto simp: is_class_def dest: comp_class_imp)
lemma comp_subcls1: "subcls1 (comp G) = subcls1 G"
-by (auto simp add: subcls1_def2 comp_classname comp_is_class)
+by (auto simp add: subcls1_def2 comp_classname comp_is_class member2_inject)
-lemma comp_widen: "((ty1,ty2) \<in> widen (comp G)) = ((ty1,ty2) \<in> widen G)"
- apply rule
- apply (cases "(ty1,ty2)" "comp G" rule: widen.cases)
+lemma comp_widen: "widen (comp G) = widen G"
+ apply (simp add: expand_fun_eq)
+ apply (intro allI iffI)
+ apply (erule widen.cases)
apply (simp_all add: comp_subcls1 widen.null)
- apply (cases "(ty1,ty2)" G rule: widen.cases)
+ apply (erule widen.cases)
apply (simp_all add: comp_subcls1 widen.null)
done
-lemma comp_cast: "((ty1,ty2) \<in> cast (comp G)) = ((ty1,ty2) \<in> cast G)"
- apply rule
- apply (cases "(ty1,ty2)" "comp G" rule: cast.cases)
+lemma comp_cast: "cast (comp G) = cast G"
+ apply (simp add: expand_fun_eq)
+ apply (intro allI iffI)
+ apply (erule cast.cases)
apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
apply (rule cast.widen) apply (simp add: comp_widen)
- apply (cases "(ty1,ty2)" G rule: cast.cases)
+ apply (erule cast.cases)
apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
apply (rule cast.widen) apply (simp add: comp_widen)
done
@@ -180,16 +182,16 @@
done
-lemma comp_class_rec: " wf ((subcls1 G)^-1) \<Longrightarrow>
+lemma comp_class_rec: " wfP ((subcls1 G)^--1) \<Longrightarrow>
class_rec (comp G) C t f =
class_rec G C t (\<lambda> C' fs' ms' r'. f C' fs' (map (compMethod G C') ms') r')"
-apply (rule_tac a = C in wf_induct) apply assumption
-apply (subgoal_tac "wf ((subcls1 (comp G))\<inverse>)")
+apply (rule_tac a = C in wfP_induct) apply assumption
+apply (subgoal_tac "wfP ((subcls1 (comp G))\<inverse>\<inverse>)")
apply (subgoal_tac "(class G x = None) \<or> (\<exists> D fs ms. (class G x = Some (D, fs, ms)))")
apply (erule disjE)
(* case class G x = None *)
-apply (simp (no_asm_simp) add: class_rec_def comp_subcls1 wfrec cut_apply)
+apply (simp (no_asm_simp) add: class_rec_def comp_subcls1 wfrec [to_pred] cut_apply)
apply (simp add: comp_class_None)
(* case \<exists> D fs ms. (class G x = Some (D, fs, ms)) *)
@@ -214,11 +216,11 @@
apply (simp add: comp_subcls1)
done
-lemma comp_fields: "wf ((subcls1 G)^-1) \<Longrightarrow>
+lemma comp_fields: "wfP ((subcls1 G)^--1) \<Longrightarrow>
fields (comp G,C) = fields (G,C)"
by (simp add: fields_def comp_class_rec)
-lemma comp_field: "wf ((subcls1 G)^-1) \<Longrightarrow>
+lemma comp_field: "wfP ((subcls1 G)^--1) \<Longrightarrow>
field (comp G,C) = field (G,C)"
by (simp add: field_def comp_fields)
@@ -230,7 +232,7 @@
\<Longrightarrow> ((class G C) \<noteq> None) \<longrightarrow>
R (class_rec G C t1 f1) (class_rec G C t2 f2)"
apply (frule wf_subcls1) (* establish wf ((subcls1 G)^-1) *)
-apply (rule_tac a = C in wf_induct) apply assumption
+apply (rule_tac a = C in wfP_induct) apply assumption
apply (intro strip)
apply (subgoal_tac "(\<exists>D rT mb. class G x = Some (D, rT, mb))")
apply (erule exE)+
--- a/src/HOL/MicroJava/J/Eval.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy Wed Feb 07 17:44:07 2007 +0100
@@ -32,86 +32,62 @@
-- "Evaluation relations"
-consts
- eval :: "java_mb prog => (xstate \<times> expr \<times> val \<times> xstate) set"
- evals :: "java_mb prog => (xstate \<times> expr list \<times> val list \<times> xstate) set"
- exec :: "java_mb prog => (xstate \<times> stmt \<times> xstate) set"
-
-syntax (xsymbols)
+inductive2
eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
("_ \<turnstile> _ -_\<succ>_-> _" [51,82,60,82,82] 81)
- evals:: "[java_mb prog,xstate,expr list,
+ and evals :: "[java_mb prog,xstate,expr list,
val list,xstate] => bool "
("_ \<turnstile> _ -_[\<succ>]_-> _" [51,82,60,51,82] 81)
- exec :: "[java_mb prog,xstate,stmt, xstate] => bool "
+ and exec :: "[java_mb prog,xstate,stmt, xstate] => bool "
("_ \<turnstile> _ -_-> _" [51,82,60,82] 81)
-
-syntax
- eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
- ("_ |- _ -_>_-> _" [51,82,60,82,82] 81)
- evals:: "[java_mb prog,xstate,expr list,
- val list,xstate] => bool "
- ("_ |- _ -_[>]_-> _" [51,82,60,51,82] 81)
- exec :: "[java_mb prog,xstate,stmt, xstate] => bool "
- ("_ |- _ -_-> _" [51,82,60,82] 81)
-
+ for G :: "java_mb prog"
+where
-translations
- "G\<turnstile>s -e \<succ> v-> (x,s')" <= "(s, e, v, x, s') \<in> eval G"
- "G\<turnstile>s -e \<succ> v-> s' " == "(s, e, v, s') \<in> eval G"
- "G\<turnstile>s -e[\<succ>]v-> (x,s')" <= "(s, e, v, x, s') \<in> evals G"
- "G\<turnstile>s -e[\<succ>]v-> s' " == "(s, e, v, s') \<in> evals G"
- "G\<turnstile>s -c -> (x,s')" <= "(s, c, x, s') \<in> exec G"
- "G\<turnstile>s -c -> s' " == "(s, c, s') \<in> exec G"
-
-
-inductive "eval G" "evals G" "exec G" intros
-
- (* evaluation of expressions *)
+ -- "evaluation of expressions"
XcptE:"G\<turnstile>(Some xc,s) -e\<succ>arbitrary-> (Some xc,s)" -- "cf. 15.5"
-- "cf. 15.8.1"
- NewC: "[| h = heap s; (a,x) = new_Addr h;
+| NewC: "[| h = heap s; (a,x) = new_Addr h;
h'= h(a\<mapsto>(C,init_vars (fields (G,C)))) |] ==>
G\<turnstile>Norm s -NewC C\<succ>Addr a-> c_hupd h' (x,s)"
-- "cf. 15.15"
- Cast: "[| G\<turnstile>Norm s0 -e\<succ>v-> (x1,s1);
+| Cast: "[| G\<turnstile>Norm s0 -e\<succ>v-> (x1,s1);
x2 = raise_if (\<not> cast_ok G C (heap s1) v) ClassCast x1 |] ==>
G\<turnstile>Norm s0 -Cast C e\<succ>v-> (x2,s1)"
-- "cf. 15.7.1"
- Lit: "G\<turnstile>Norm s -Lit v\<succ>v-> Norm s"
+| Lit: "G\<turnstile>Norm s -Lit v\<succ>v-> Norm s"
- BinOp:"[| G\<turnstile>Norm s -e1\<succ>v1-> s1;
+| BinOp:"[| G\<turnstile>Norm s -e1\<succ>v1-> s1;
G\<turnstile>s1 -e2\<succ>v2-> s2;
v = (case bop of Eq => Bool (v1 = v2)
| Add => Intg (the_Intg v1 + the_Intg v2)) |] ==>
G\<turnstile>Norm s -BinOp bop e1 e2\<succ>v-> s2"
-- "cf. 15.13.1, 15.2"
- LAcc: "G\<turnstile>Norm s -LAcc v\<succ>the (locals s v)-> Norm s"
+| LAcc: "G\<turnstile>Norm s -LAcc v\<succ>the (locals s v)-> Norm s"
-- "cf. 15.25.1"
- LAss: "[| G\<turnstile>Norm s -e\<succ>v-> (x,(h,l));
+| LAss: "[| G\<turnstile>Norm s -e\<succ>v-> (x,(h,l));
l' = (if x = None then l(va\<mapsto>v) else l) |] ==>
G\<turnstile>Norm s -va::=e\<succ>v-> (x,(h,l'))"
-- "cf. 15.10.1, 15.2"
- FAcc: "[| G\<turnstile>Norm s0 -e\<succ>a'-> (x1,s1);
+| FAcc: "[| G\<turnstile>Norm s0 -e\<succ>a'-> (x1,s1);
v = the (snd (the (heap s1 (the_Addr a'))) (fn,T)) |] ==>
G\<turnstile>Norm s0 -{T}e..fn\<succ>v-> (np a' x1,s1)"
-- "cf. 15.25.1"
- FAss: "[| G\<turnstile> Norm s0 -e1\<succ>a'-> (x1,s1); a = the_Addr a';
+| FAss: "[| G\<turnstile> Norm s0 -e1\<succ>a'-> (x1,s1); a = the_Addr a';
G\<turnstile>(np a' x1,s1) -e2\<succ>v -> (x2,s2);
h = heap s2; (c,fs) = the (h a);
h' = h(a\<mapsto>(c,(fs((fn,T)\<mapsto>v)))) |] ==>
G\<turnstile>Norm s0 -{T}e1..fn:=e2\<succ>v-> c_hupd h' (x2,s2)"
-- "cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15"
- Call: "[| G\<turnstile>Norm s0 -e\<succ>a'-> s1; a = the_Addr a';
+| Call: "[| G\<turnstile>Norm s0 -e\<succ>a'-> s1; a = the_Addr a';
G\<turnstile>s1 -ps[\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
(md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs)(This\<mapsto>a'))) -blk-> s3;
@@ -122,13 +98,13 @@
-- "evaluation of expression lists"
-- "cf. 15.5"
- XcptEs:"G\<turnstile>(Some xc,s) -e[\<succ>]arbitrary-> (Some xc,s)"
+| XcptEs:"G\<turnstile>(Some xc,s) -e[\<succ>]arbitrary-> (Some xc,s)"
-- "cf. 15.11.???"
- Nil: "G\<turnstile>Norm s0 -[][\<succ>][]-> Norm s0"
+| Nil: "G\<turnstile>Norm s0 -[][\<succ>][]-> Norm s0"
-- "cf. 15.6.4"
- Cons: "[| G\<turnstile>Norm s0 -e \<succ> v -> s1;
+| Cons: "[| G\<turnstile>Norm s0 -e \<succ> v -> s1;
G\<turnstile> s1 -es[\<succ>]vs-> s2 |] ==>
G\<turnstile>Norm s0 -e#es[\<succ>]v#vs-> s2"
@@ -136,29 +112,29 @@
-- "execution of statements"
-- "cf. 14.1"
- XcptS:"G\<turnstile>(Some xc,s) -c-> (Some xc,s)"
+| XcptS:"G\<turnstile>(Some xc,s) -c-> (Some xc,s)"
-- "cf. 14.5"
- Skip: "G\<turnstile>Norm s -Skip-> Norm s"
+| Skip: "G\<turnstile>Norm s -Skip-> Norm s"
-- "cf. 14.7"
- Expr: "[| G\<turnstile>Norm s0 -e\<succ>v-> s1 |] ==>
+| Expr: "[| G\<turnstile>Norm s0 -e\<succ>v-> s1 |] ==>
G\<turnstile>Norm s0 -Expr e-> s1"
-- "cf. 14.2"
- Comp: "[| G\<turnstile>Norm s0 -c1-> s1;
+| Comp: "[| G\<turnstile>Norm s0 -c1-> s1;
G\<turnstile> s1 -c2-> s2|] ==>
G\<turnstile>Norm s0 -c1;; c2-> s2"
-- "cf. 14.8.2"
- Cond: "[| G\<turnstile>Norm s0 -e\<succ>v-> s1;
+| Cond: "[| G\<turnstile>Norm s0 -e\<succ>v-> s1;
G\<turnstile> s1 -(if the_Bool v then c1 else c2)-> s2|] ==>
G\<turnstile>Norm s0 -If(e) c1 Else c2-> s2"
-- "cf. 14.10, 14.10.1"
- LoopF:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1; \<not>the_Bool v |] ==>
+| LoopF:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1; \<not>the_Bool v |] ==>
G\<turnstile>Norm s0 -While(e) c-> s1"
- LoopT:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1; the_Bool v;
+| LoopT:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1; the_Bool v;
G\<turnstile>s1 -c-> s2; G\<turnstile>s2 -While(e) c-> s3 |] ==>
G\<turnstile>Norm s0 -While(e) c-> s3"
--- a/src/HOL/MicroJava/J/Example.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Wed Feb 07 17:44:07 2007 +0100
@@ -172,19 +172,19 @@
apply (simp (no_asm))
done
-lemma not_Object_subcls [elim!]: "(Object,C) \<in> (subcls1 tprg)^+ ==> R"
-apply (auto dest!: tranclD subcls1D)
+lemma not_Object_subcls [elim!]: "(subcls1 tprg)^++ Object C ==> R"
+apply (auto dest!: tranclD' subcls1D)
done
lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object"
-apply (erule rtrancl_induct)
+apply (erule rtrancl_induct')
apply auto
apply (drule subcls1D)
apply auto
done
-lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+ ==> R"
-apply (auto dest!: tranclD subcls1D)
+lemma not_Base_subcls_Ext [elim!]: "(subcls1 tprg)^++ Base Ext ==> R"
+apply (auto dest!: tranclD' subcls1D)
done
lemma class_tprgD:
@@ -193,11 +193,11 @@
apply (auto split add: split_if_asm simp add: map_of_Cons)
done
-lemma not_class_subcls_class [elim!]: "(C,C) \<in> (subcls1 tprg)^+ ==> R"
-apply (auto dest!: tranclD subcls1D)
+lemma not_class_subcls_class [elim!]: "(subcls1 tprg)^++ C C ==> R"
+apply (auto dest!: tranclD' subcls1D)
apply (frule class_tprgD)
apply (auto dest!:)
-apply (drule rtranclD)
+apply (drule rtranclD')
apply auto
done
@@ -205,7 +205,7 @@
apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
done
-lemmas subcls_direct = subcls1I [THEN r_into_rtrancl]
+lemmas subcls_direct = subcls1I [THEN r_into_rtrancl' [where r="subcls1 G"], standard]
lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base"
apply (rule subcls_direct)
@@ -219,12 +219,12 @@
declare ty_expr_ty_exprs_wt_stmt.intros [intro!]
-lemma acyclic_subcls1_: "acyclic (subcls1 tprg)"
-apply (rule acyclicI)
+lemma acyclic_subcls1_: "acyclicP (subcls1 tprg)"
+apply (rule acyclicI [to_pred])
apply safe
done
-lemmas wf_subcls1_ = acyclic_subcls1_ [THEN finite_subcls1 [THEN finite_acyclic_wf_converse]]
+lemmas wf_subcls1_ = acyclic_subcls1_ [THEN finite_subcls1 [THEN finite_acyclic_wf_converse [to_pred]]]
lemmas fields_rec_ = wf_subcls1_ [THEN [2] fields_rec_lemma]
@@ -345,7 +345,7 @@
apply (fold ExtC_def)
apply (rule mp) defer apply (rule wf_foo_Ext)
apply (auto simp add: wf_mdecl_def)
-apply (drule rtranclD)
+apply (drule rtranclD')
apply auto
done
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Wed Feb 07 17:44:07 2007 +0100
@@ -27,7 +27,7 @@
apply (case_tac "ref_ty")
apply (clarsimp simp add: conf_def)
apply simp
-apply (ind_cases "G \<turnstile> Class cname \<preceq>? Class D", simp)
+apply (ind_cases2 "G \<turnstile> Class cname \<preceq>? Class D" for cname, simp)
apply (rule conf_widen, assumption+) apply (erule widen.subcls)
apply (unfold cast_ok_def)
@@ -205,7 +205,7 @@
-- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
apply( simp_all)
apply( tactic "ALLGOALS strip_tac")
-apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims")
+apply( tactic {* ALLGOALS (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"]
THEN_ALL_NEW Full_simp_tac) *})
apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
@@ -222,7 +222,7 @@
apply( rule conjI)
apply( force elim!: NewC_conforms)
apply( rule conf_obj_AddrI)
-apply( rule_tac [2] rtrancl_refl)
+apply( rule_tac [2] rtrancl.rtrancl_refl)
apply( simp (no_asm))
-- "for Cast"
@@ -245,22 +245,22 @@
apply( fast elim: conforms_localD [THEN lconfD])
-- "for FAss"
-apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims")
+apply( tactic {* EVERY'[eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"]
THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*})
-- "for if"
-apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8*})
+apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 7*})
apply (tactic "forward_hyp_tac")
-- "11+1 if"
-prefer 8
+prefer 7
apply( fast intro: hext_trans)
-prefer 8
+prefer 7
apply( fast intro: hext_trans)
-- "10 Expr"
-prefer 7
+prefer 6
apply( fast)
-- "9 ???"
@@ -280,7 +280,7 @@
-- "7 LAss"
apply (fold fun_upd_def)
-apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims")
+apply( tactic {* (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"]
THEN_ALL_NEW Full_simp_tac) 1 *})
apply (intro strip)
apply (case_tac E)
@@ -315,7 +315,7 @@
-- "2 FAss"
-apply (subgoal_tac "(np a' x1, ab, ba) ::\<preceq> (G, lT)")
+apply (subgoal_tac "(np a' x1, aa, ba) ::\<preceq> (G, lT)")
prefer 2
apply (simp add: np_def)
apply (fast intro: conforms_xcpt_change xconf_raise_if)
--- a/src/HOL/MicroJava/J/TypeRel.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Wed Feb 07 17:44:07 2007 +0100
@@ -8,61 +8,45 @@
theory TypeRel imports Decl begin
-consts
- subcls1 :: "'c prog => (cname \<times> cname) set" -- "subclass"
- widen :: "'c prog => (ty \<times> ty ) set" -- "widening"
- cast :: "'c prog => (ty \<times> ty ) set" -- "casting"
-
-syntax (xsymbols)
+-- "direct subclass, cf. 8.1.3"
+inductive2
subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
- subcls :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70)
- widen :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70)
- cast :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70)
+ for G :: "'c prog"
+where
+ subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
-syntax
- subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
- subcls :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70)
- widen :: "'c prog => [ty , ty ] => bool" ("_ |- _ <= _" [71,71,71] 70)
- cast :: "'c prog => [ty , ty ] => bool" ("_ |- _ <=? _" [71,71,71] 70)
-
-translations
- "G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"
- "G\<turnstile>C \<preceq>C D" == "(C,D) \<in> (subcls1 G)^*"
- "G\<turnstile>S \<preceq> T" == "(S,T) \<in> widen G"
- "G\<turnstile>C \<preceq>? D" == "(C,D) \<in> cast G"
-
--- "direct subclass, cf. 8.1.3"
-inductive "subcls1 G" intros
- subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
+abbreviation
+ subcls :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70)
+ where "G\<turnstile>C \<preceq>C D \<equiv> (subcls1 G)^** C D"
lemma subcls1D:
"G\<turnstile>C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>fs ms. class G C = Some (D,fs,ms))"
-apply (erule subcls1.elims)
+apply (erule subcls1.cases)
apply auto
done
lemma subcls1_def2:
- "subcls1 G =
+ "subcls1 G = member2
(SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
- by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
+ by (auto simp add: is_class_def expand_fun_eq dest: subcls1D intro: subcls1I)
-lemma finite_subcls1: "finite (subcls1 G)"
-apply(subst subcls1_def2)
+lemma finite_subcls1: "finite (Collect2 (subcls1 G))"
+apply(simp add: subcls1_def2)
apply(rule finite_SigmaI [OF finite_is_class])
apply(rule_tac B = "{fst (the (class G C))}" in finite_subset)
apply auto
done
-lemma subcls_is_class: "(C,D) \<in> (subcls1 G)^+ ==> is_class G C"
+lemma subcls_is_class: "(subcls1 G)^++ C D ==> is_class G C"
apply (unfold is_class_def)
-apply(erule trancl_trans_induct)
+apply(erule trancl_trans_induct')
apply (auto dest!: subcls1D)
done
lemma subcls_is_class2 [rule_format (no_asm)]:
"G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
apply (unfold is_class_def)
-apply (erule rtrancl_induct)
+apply (erule rtrancl_induct')
apply (drule_tac [2] subcls1D)
apply auto
done
@@ -70,18 +54,19 @@
constdefs
class_rec :: "'c prog \<Rightarrow> cname \<Rightarrow> 'a \<Rightarrow>
(cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
- "class_rec G == wfrec ((subcls1 G)^-1)
+ "class_rec G == wfrec (Collect2 ((subcls1 G)^--1))
(\<lambda>r C t f. case class G C of
None \<Rightarrow> arbitrary
| Some (D,fs,ms) \<Rightarrow>
f C fs ms (if C = Object then t else r D t f))"
-lemma class_rec_lemma: "wf ((subcls1 G)^-1) \<Longrightarrow> class G C = Some (D,fs,ms) \<Longrightarrow>
+lemma class_rec_lemma: "wfP ((subcls1 G)^--1) \<Longrightarrow> class G C = Some (D,fs,ms) \<Longrightarrow>
class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)"
- by (simp add: class_rec_def wfrec cut_apply [OF converseI [OF subcls1I]])
+ by (simp add: class_rec_def wfrec [to_pred]
+ cut_apply [OF Collect2I [where P="(subcls1 G)^--1"], OF conversepI, OF subcls1I])
definition
- "wf_class G = wf ((subcls1 G)^-1)"
+ "wf_class G = wfP ((subcls1 G)^--1)"
lemma class_rec_func [code func]:
"class_rec G C t f = (if wf_class G then
@@ -93,13 +78,14 @@
case False then show ?thesis by auto
next
case True
- from `wf_class G` have wf: "wf ((subcls1 G)^-1)"
+ from `wf_class G` have wf: "wfP ((subcls1 G)^--1)"
unfolding wf_class_def .
show ?thesis
proof (cases "class G C")
case None
with wf show ?thesis
- by (simp add: class_rec_def wfrec cut_apply [OF converseI [OF subcls1I]])
+ by (simp add: class_rec_def wfrec [to_pred]
+ cut_apply [OF Collect2I [where P="(subcls1 G)^--1"], OF conversepI, OF subcls1I])
next
case (Some x) show ?thesis
proof (cases x)
@@ -121,7 +107,7 @@
defs method_def: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
-lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
+lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wfP ((subcls1 G)^--1)|] ==>
method (G,C) = (if C = Object then empty else method (G,D)) ++
map_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
apply (unfold method_def)
@@ -135,7 +121,7 @@
defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec G C [] (\<lambda>C fs ms ts.
map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
-lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
+lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wfP ((subcls1 G)^--1)|] ==>
fields (G,C) =
map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
apply (unfold fields_def)
@@ -156,56 +142,62 @@
-- "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping"
-inductive "widen G" intros
+inductive2
+ widen :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70)
+ for G :: "'c prog"
+where
refl [intro!, simp]: "G\<turnstile> T \<preceq> T" -- "identity conv., cf. 5.1.1"
- subcls : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
- null [intro!]: "G\<turnstile> NT \<preceq> RefT R"
+| subcls : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
+| null [intro!]: "G\<turnstile> NT \<preceq> RefT R"
-- "casting conversion, cf. 5.5 / 5.1.5"
-- "left out casts on primitve types"
-inductive "cast G" intros
+inductive2
+ cast :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70)
+ for G :: "'c prog"
+where
widen: "G\<turnstile> C\<preceq> D ==> G\<turnstile>C \<preceq>? D"
- subcls: "G\<turnstile> D\<preceq>C C ==> G\<turnstile>Class C \<preceq>? Class D"
+| subcls: "G\<turnstile> D\<preceq>C C ==> G\<turnstile>Class C \<preceq>? Class D"
lemma widen_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>RefT rT) = False"
apply (rule iffI)
-apply (erule widen.elims)
+apply (erule widen.cases)
apply auto
done
lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> \<exists>t. T=RefT t"
-apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply (ind_cases2 "G\<turnstile>RefT R\<preceq>T")
apply auto
done
lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> \<exists>t. S=RefT t"
-apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply (ind_cases2 "G\<turnstile>S\<preceq>RefT R")
apply auto
done
lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> \<exists>D. T=Class D"
-apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply (ind_cases2 "G\<turnstile>Class C\<preceq>T")
apply auto
done
lemma widen_Class_NullT [iff]: "(G\<turnstile>Class C\<preceq>NT) = False"
apply (rule iffI)
-apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply (ind_cases2 "G\<turnstile>Class C\<preceq>NT")
apply auto
done
lemma widen_Class_Class [iff]: "(G\<turnstile>Class C\<preceq> Class D) = (G\<turnstile>C\<preceq>C D)"
apply (rule iffI)
-apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply (ind_cases2 "G\<turnstile>Class C \<preceq> Class D")
apply (auto elim: widen.subcls)
done
lemma widen_NT_Class [simp]: "G \<turnstile> T \<preceq> NT \<Longrightarrow> G \<turnstile> T \<preceq> Class D"
-by (ind_cases "G \<turnstile> T \<preceq> NT", auto)
+by (ind_cases2 "G \<turnstile> T \<preceq> NT", auto)
lemma cast_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>? RefT rT) = False"
apply (rule iffI)
-apply (erule cast.elims)
+apply (erule cast.cases)
apply auto
done
@@ -223,7 +215,7 @@
next
case (subcls C D T)
then obtain E where "T = Class E" by (blast dest: widen_Class)
- with subcls show "G\<turnstile>Class C\<preceq>T" by (auto elim: rtrancl_trans)
+ with subcls show "G\<turnstile>Class C\<preceq>T" by auto
next
case (null R RT)
then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
--- a/src/HOL/MicroJava/J/WellForm.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Wed Feb 07 17:44:07 2007 +0100
@@ -134,13 +134,13 @@
apply (auto intro!: map_of_SomeI)
done
-lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; ws_prog G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+"
-apply( frule r_into_trancl)
+lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; ws_prog G|] ==> D \<noteq> C \<and> \<not> (subcls1 G)^++ D C"
+apply( frule trancl.r_into_trancl [where r="subcls1 G"])
apply( drule subcls1D)
apply(clarify)
apply( drule (1) class_wf_struct)
apply( unfold ws_cdecl_def)
-apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
+apply(force simp add: reflcl_trancl' [THEN sym] simp del: reflcl_trancl')
done
lemma wf_cdecl_supD:
@@ -149,42 +149,42 @@
apply (auto split add: option.split_asm)
done
-lemma subcls_asym: "[|ws_prog G; (C,D)\<in>(subcls1 G)^+|] ==> \<not>(D,C)\<in>(subcls1 G)^+"
-apply(erule tranclE)
+lemma subcls_asym: "[|ws_prog G; (subcls1 G)^++ C D|] ==> \<not> (subcls1 G)^++ D C"
+apply(erule trancl.cases)
apply(fast dest!: subcls1_wfD )
-apply(fast dest!: subcls1_wfD intro: trancl_trans)
+apply(fast dest!: subcls1_wfD intro: trancl_trans')
done
-lemma subcls_irrefl: "[|ws_prog G; (C,D)\<in>(subcls1 G)^+|] ==> C \<noteq> D"
-apply (erule trancl_trans_induct)
+lemma subcls_irrefl: "[|ws_prog G; (subcls1 G)^++ C D|] ==> C \<noteq> D"
+apply (erule trancl_trans_induct')
apply (auto dest: subcls1_wfD subcls_asym)
done
-lemma acyclic_subcls1: "ws_prog G ==> acyclic (subcls1 G)"
-apply (unfold acyclic_def)
+lemma acyclic_subcls1: "ws_prog G ==> acyclicP (subcls1 G)"
+apply (simp add: acyclic_def [to_pred])
apply (fast dest: subcls_irrefl)
done
-lemma wf_subcls1: "ws_prog G ==> wf ((subcls1 G)^-1)"
-apply (rule finite_acyclic_wf)
-apply ( subst finite_converse)
+lemma wf_subcls1: "ws_prog G ==> wfP ((subcls1 G)^--1)"
+apply (rule finite_acyclic_wf [to_pred])
+apply ( subst finite_converse [to_pred])
apply ( rule finite_subcls1)
-apply (subst acyclic_converse)
+apply (subst acyclic_converse [to_pred])
apply (erule acyclic_subcls1)
done
lemma subcls_induct:
-"[|wf_prog wf_mb G; !!C. \<forall>D. (C,D)\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C"
+"[|wf_prog wf_mb G; !!C. \<forall>D. (subcls1 G)^++ C D --> P D ==> P C|] ==> P C"
(is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
proof -
assume p: "PROP ?P"
assume ?A thus ?thesis apply -
apply (drule wf_prog_ws_prog)
apply(drule wf_subcls1)
-apply(drule wf_trancl)
-apply(simp only: trancl_converse)
-apply(erule_tac a = C in wf_induct)
+apply(drule wfP_trancl)
+apply(simp only: trancl_converse')
+apply(erule_tac a = C in wfP_induct)
apply(rule p)
apply(auto)
done
@@ -225,15 +225,15 @@
qed
lemma subcls_induct_struct:
-"[|ws_prog G; !!C. \<forall>D. (C,D)\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C"
+"[|ws_prog G; !!C. \<forall>D. (subcls1 G)^++ C D --> P D ==> P C|] ==> P C"
(is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
proof -
assume p: "PROP ?P"
assume ?A thus ?thesis apply -
apply(drule wf_subcls1)
-apply(drule wf_trancl)
-apply(simp only: trancl_converse)
-apply(erule_tac a = C in wf_induct)
+apply(drule wfP_trancl)
+apply(simp only: trancl_converse')
+apply(erule_tac a = C in wfP_induct)
apply(rule p)
apply(auto)
done
@@ -339,7 +339,7 @@
apply( simp (no_asm))
apply( erule UnE)
apply( force)
-apply( erule r_into_rtrancl [THEN rtrancl_trans])
+apply( erule r_into_rtrancl' [THEN rtrancl_trans'])
apply auto
done
@@ -381,9 +381,9 @@
done
lemma fields_mono_lemma [rule_format (no_asm)]:
- "[|ws_prog G; (C',C)\<in>(subcls1 G)^*|] ==>
+ "[|ws_prog G; (subcls1 G)^** C' C|] ==>
x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))"
-apply(erule converse_rtrancl_induct)
+apply(erule converse_rtrancl_induct')
apply( safe dest!: subcls1D)
apply(subst fields_rec)
apply( auto)
@@ -402,10 +402,10 @@
"[|field (G,C) fn = Some (fd, fT); G\<turnstile>D\<preceq>C C; ws_prog G|]==>
map_of (fields (G,D)) (fn, fd) = Some fT"
apply (drule field_fields)
-apply (drule rtranclD)
+apply (drule rtranclD')
apply safe
apply (frule subcls_is_class)
-apply (drule trancl_into_rtrancl)
+apply (drule trancl_into_rtrancl')
apply (fast dest: fields_mono)
done
@@ -437,10 +437,10 @@
apply (frule map_of_SomeD)
apply (clarsimp simp add: wf_cdecl_def)
apply( clarify)
-apply( rule rtrancl_trans)
+apply( rule rtrancl_trans')
prefer 2
apply( assumption)
-apply( rule r_into_rtrancl)
+apply( rule r_into_rtrancl')
apply( fast intro: subcls1I)
done
@@ -473,10 +473,10 @@
apply (clarsimp simp add: ws_cdecl_def)
apply blast
apply clarify
-apply( rule rtrancl_trans)
+apply( rule rtrancl_trans')
prefer 2
apply( assumption)
-apply( rule r_into_rtrancl)
+apply( rule r_into_rtrancl')
apply( fast intro: subcls1I)
done
@@ -484,15 +484,15 @@
"[|G\<turnstile>T'\<preceq>C T; wf_prog wf_mb G|] ==>
\<forall>D rT b. method (G,T) sig = Some (D,rT ,b) -->
(\<exists>D' rT' b'. method (G,T') sig = Some (D',rT',b') \<and> G\<turnstile>D'\<preceq>C D \<and> G\<turnstile>rT'\<preceq>rT)"
-apply( drule rtranclD)
+apply( drule rtranclD')
apply( erule disjE)
apply( fast)
apply( erule conjE)
-apply( erule trancl_trans_induct)
+apply( erule trancl_trans_induct')
prefer 2
apply( clarify)
apply( drule spec, drule spec, drule spec, erule (1) impE)
-apply( fast elim: widen_trans rtrancl_trans)
+apply( fast elim: widen_trans rtrancl_trans')
apply( clarify)
apply( drule subcls1D)
apply( clarify)
@@ -512,7 +512,7 @@
apply( unfold wf_cdecl_def)
apply( drule map_of_SomeD)
apply (auto simp add: wf_mrT_def)
-apply (rule rtrancl_trans)
+apply (rule rtrancl_trans')
defer
apply (rule method_wf_mhead [THEN conjunct1])
apply (simp only: wf_prog_def)
--- a/src/HOL/MicroJava/J/WellType.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Wed Feb 07 17:44:07 2007 +0100
@@ -106,74 +106,57 @@
java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr"
-- "method body with parameter names, local variables, block, result expression."
-- "local variables might include This, which is hidden anyway"
-
-consts
- ty_expr :: "('c env \<times> expr \<times> ty ) set"
- ty_exprs:: "('c env \<times> expr list \<times> ty list) set"
- wt_stmt :: "('c env \<times> stmt ) set"
-
-syntax (xsymbols)
- ty_expr :: "'c env => [expr , ty ] => bool" ("_ \<turnstile> _ :: _" [51,51,51]50)
- ty_exprs:: "'c env => [expr list, ty list] => bool" ("_ \<turnstile> _ [::] _" [51,51,51]50)
- wt_stmt :: "'c env => stmt => bool" ("_ \<turnstile> _ \<surd>" [51,51 ]50)
-
-syntax
- ty_expr :: "'c env => [expr , ty ] => bool" ("_ |- _ :: _" [51,51,51]50)
- ty_exprs:: "'c env => [expr list, ty list] => bool" ("_ |- _ [::] _" [51,51,51]50)
- wt_stmt :: "'c env => stmt => bool" ("_ |- _ [ok]" [51,51 ]50)
-
-
-translations
- "E\<turnstile>e :: T" == "(E,e,T) \<in> ty_expr"
- "E\<turnstile>e[::]T" == "(E,e,T) \<in> ty_exprs"
- "E\<turnstile>c \<surd>" == "(E,c) \<in> wt_stmt"
-inductive "ty_expr" "ty_exprs" "wt_stmt" intros
+inductive2
+ ty_expr :: "'c env => expr => ty => bool" ("_ \<turnstile> _ :: _" [51, 51, 51] 50)
+ and ty_exprs :: "'c env => expr list => ty list => bool" ("_ \<turnstile> _ [::] _" [51, 51, 51] 50)
+ and wt_stmt :: "'c env => stmt => bool" ("_ \<turnstile> _ \<surd>" [51, 51] 50)
+where
NewC: "[| is_class (prg E) C |] ==>
E\<turnstile>NewC C::Class C" -- "cf. 15.8"
-- "cf. 15.15"
- Cast: "[| E\<turnstile>e::C; is_class (prg E) D;
+| Cast: "[| E\<turnstile>e::C; is_class (prg E) D;
prg E\<turnstile>C\<preceq>? Class D |] ==>
E\<turnstile>Cast D e:: Class D"
-- "cf. 15.7.1"
- Lit: "[| typeof (\<lambda>v. None) x = Some T |] ==>
+| Lit: "[| typeof (\<lambda>v. None) x = Some T |] ==>
E\<turnstile>Lit x::T"
-- "cf. 15.13.1"
- LAcc: "[| localT E v = Some T; is_type (prg E) T |] ==>
+| LAcc: "[| localT E v = Some T; is_type (prg E) T |] ==>
E\<turnstile>LAcc v::T"
- BinOp:"[| E\<turnstile>e1::T;
+| BinOp:"[| E\<turnstile>e1::T;
E\<turnstile>e2::T;
if bop = Eq then T' = PrimT Boolean
else T' = T \<and> T = PrimT Integer|] ==>
E\<turnstile>BinOp bop e1 e2::T'"
-- "cf. 15.25, 15.25.1"
- LAss: "[| v ~= This;
+| LAss: "[| v ~= This;
E\<turnstile>LAcc v::T;
E\<turnstile>e::T';
prg E\<turnstile>T'\<preceq>T |] ==>
E\<turnstile>v::=e::T'"
-- "cf. 15.10.1"
- FAcc: "[| E\<turnstile>a::Class C;
+| FAcc: "[| E\<turnstile>a::Class C;
field (prg E,C) fn = Some (fd,fT) |] ==>
E\<turnstile>{fd}a..fn::fT"
-- "cf. 15.25, 15.25.1"
- FAss: "[| E\<turnstile>{fd}a..fn::T;
+| FAss: "[| E\<turnstile>{fd}a..fn::T;
E\<turnstile>v ::T';
prg E\<turnstile>T'\<preceq>T |] ==>
E\<turnstile>{fd}a..fn:=v::T'"
-- "cf. 15.11.1, 15.11.2, 15.11.3"
- Call: "[| E\<turnstile>a::Class C;
+| Call: "[| E\<turnstile>a::Class C;
E\<turnstile>ps[::]pTs;
max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')} |] ==>
E\<turnstile>{C}a..mn({pTs'}ps)::rT"
@@ -181,32 +164,32 @@
-- "well-typed expression lists"
-- "cf. 15.11.???"
- Nil: "E\<turnstile>[][::][]"
+| Nil: "E\<turnstile>[][::][]"
-- "cf. 15.11.???"
- Cons:"[| E\<turnstile>e::T;
+| Cons:"[| E\<turnstile>e::T;
E\<turnstile>es[::]Ts |] ==>
E\<turnstile>e#es[::]T#Ts"
-- "well-typed statements"
- Skip:"E\<turnstile>Skip\<surd>"
+| Skip:"E\<turnstile>Skip\<surd>"
- Expr:"[| E\<turnstile>e::T |] ==>
+| Expr:"[| E\<turnstile>e::T |] ==>
E\<turnstile>Expr e\<surd>"
- Comp:"[| E\<turnstile>s1\<surd>;
+| Comp:"[| E\<turnstile>s1\<surd>;
E\<turnstile>s2\<surd> |] ==>
E\<turnstile>s1;; s2\<surd>"
-- "cf. 14.8"
- Cond:"[| E\<turnstile>e::PrimT Boolean;
+| Cond:"[| E\<turnstile>e::PrimT Boolean;
E\<turnstile>s1\<surd>;
E\<turnstile>s2\<surd> |] ==>
E\<turnstile>If(e) s1 Else s2\<surd>"
-- "cf. 14.10"
- Loop:"[| E\<turnstile>e::PrimT Boolean;
+| Loop:"[| E\<turnstile>e::PrimT Boolean;
E\<turnstile>s\<surd> |] ==>
E\<turnstile>While(e) s\<surd>"
--- a/src/HOL/Nominal/Examples/Compile.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Nominal/Examples/Compile.thy Wed Feb 07 17:44:07 2007 +0100
@@ -45,62 +45,42 @@
text {* valid contexts *}
-consts
- ctxts :: "((name\<times>'a::pt_name) list) set"
- valid :: "(name\<times>'a::pt_name) list \<Rightarrow> bool"
-translations
- "valid \<Gamma>" \<rightleftharpoons> "\<Gamma> \<in> ctxts"
-
-inductive ctxts
-intros
-v1[intro]: "valid []"
-v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" (* maybe dom of \<Gamma> *)
+inductive2 valid :: "(name\<times>'a::pt_name) list \<Rightarrow> bool"
+where
+ v1[intro]: "valid []"
+| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" (* maybe dom of \<Gamma> *)
text {* typing judgements for trms *}
-consts
- typing :: "(((name\<times>ty) list)\<times>trm\<times>ty) set"
-syntax
- "_typing_judge" :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
-translations
- "\<Gamma> \<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> typing"
-
-inductive typing
-intros
-t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : \<tau>"
-t1[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> \<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App e1 e2 : \<tau>2"
-t2[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,\<tau>1)#\<Gamma>) \<turnstile> t : \<tau>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : \<tau>1\<rightarrow>\<tau>2"
-t3[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : Data(DNat)"
-t4[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : Data(\<sigma>1); \<Gamma> \<turnstile> e2 : Data(\<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Pr e1 e2 : Data (DProd \<sigma>1 \<sigma>2)"
-t5[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd \<sigma>1 \<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Fst e : Data(\<sigma>1)"
-t6[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd \<sigma>1 \<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Snd e : Data(\<sigma>2)"
-t7[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(\<sigma>1)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InL e : Data(DSum \<sigma>1 \<sigma>2)"
-t8[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(\<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InR e : Data(DSum \<sigma>1 \<sigma>2)"
-t9[intro]: "\<lbrakk>x1\<sharp>\<Gamma>; x2\<sharp>\<Gamma>; \<Gamma> \<turnstile> e: Data(DSum \<sigma>1 \<sigma>2);
+inductive2 typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
+where
+ t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : \<tau>"
+| t1[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> \<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App e1 e2 : \<tau>2"
+| t2[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,\<tau>1)#\<Gamma>) \<turnstile> t : \<tau>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : \<tau>1\<rightarrow>\<tau>2"
+| t3[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : Data(DNat)"
+| t4[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : Data(\<sigma>1); \<Gamma> \<turnstile> e2 : Data(\<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Pr e1 e2 : Data (DProd \<sigma>1 \<sigma>2)"
+| t5[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd \<sigma>1 \<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Fst e : Data(\<sigma>1)"
+| t6[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(DProd \<sigma>1 \<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Snd e : Data(\<sigma>2)"
+| t7[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(\<sigma>1)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InL e : Data(DSum \<sigma>1 \<sigma>2)"
+| t8[intro]: "\<lbrakk>\<Gamma> \<turnstile> e : Data(\<sigma>2)\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> InR e : Data(DSum \<sigma>1 \<sigma>2)"
+| t9[intro]: "\<lbrakk>x1\<sharp>\<Gamma>; x2\<sharp>\<Gamma>; \<Gamma> \<turnstile> e: Data(DSum \<sigma>1 \<sigma>2);
((x1,Data(\<sigma>1))#\<Gamma>) \<turnstile> e1 : \<tau>; ((x2,Data(\<sigma>2))#\<Gamma>) \<turnstile> e2 : \<tau>\<rbrakk>
\<Longrightarrow> \<Gamma> \<turnstile> (Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2) : \<tau>"
text {* typing judgements for Itrms *}
-consts
- Ityping :: "(((name\<times>tyI) list)\<times>trmI\<times>tyI) set"
-syntax
- "_typing_judge" :: "(name\<times>tyI) list\<Rightarrow>trmI\<Rightarrow>tyI\<Rightarrow>bool" (" _ I\<turnstile> _ : _ " [80,80,80] 80)
-translations
- "\<Gamma> I\<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> Ityping"
-
-inductive Ityping
-intros
-t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IVar x : \<tau>"
-t1[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> I\<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IApp e1 e2 : \<tau>2"
-t2[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,\<tau>1)#\<Gamma>) I\<turnstile> t : \<tau>2\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> ILam [x].t : \<tau>1\<rightarrow>\<tau>2"
-t3[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> I\<turnstile> IUnit : DataI(OneI)"
-t4[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> I\<turnstile> INat(n) : DataI(NatI)"
-t5[intro]: "\<Gamma> I\<turnstile> e : DataI(NatI) \<Longrightarrow> \<Gamma> I\<turnstile> ISucc(e) : DataI(NatI)"
-t6[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> IRef e : DataI (NatI)"
-t7[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1\<mapsto>e2 : DataI(OneI)"
-t8[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1;;e2 : \<tau>"
-t9[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e: DataI(NatI); \<Gamma> I\<turnstile> e1 : \<tau>; \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> Iif e e1 e2 : \<tau>"
+inductive2 Ityping :: "(name\<times>tyI) list\<Rightarrow>trmI\<Rightarrow>tyI\<Rightarrow>bool" (" _ I\<turnstile> _ : _ " [80,80,80] 80)
+where
+ t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IVar x : \<tau>"
+| t1[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> I\<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IApp e1 e2 : \<tau>2"
+| t2[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,\<tau>1)#\<Gamma>) I\<turnstile> t : \<tau>2\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> ILam [x].t : \<tau>1\<rightarrow>\<tau>2"
+| t3[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> I\<turnstile> IUnit : DataI(OneI)"
+| t4[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> I\<turnstile> INat(n) : DataI(NatI)"
+| t5[intro]: "\<Gamma> I\<turnstile> e : DataI(NatI) \<Longrightarrow> \<Gamma> I\<turnstile> ISucc(e) : DataI(NatI)"
+| t6[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> IRef e : DataI (NatI)"
+| t7[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1\<mapsto>e2 : DataI(OneI)"
+| t8[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1;;e2 : \<tau>"
+| t9[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e: DataI(NatI); \<Gamma> I\<turnstile> e1 : \<tau>; \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> Iif e e1 e2 : \<tau>"
text {* capture-avoiding substitution *}
@@ -257,46 +237,32 @@
text {* big-step evaluation for trms *}
-consts
- big :: "(trm\<times>trm) set"
-syntax
- "_big_judge" :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80)
-translations
- "e1 \<Down> e2" \<rightleftharpoons> "(e1,e2) \<in> big"
-
-inductive big
-intros
-b0[intro]: "Lam [x].e \<Down> Lam [x].e"
-b1[intro]: "\<lbrakk>e1\<Down>Lam [x].e; e2\<Down>e2'; e[x::=e2']\<Down>e'\<rbrakk> \<Longrightarrow> App e1 e2 \<Down> e'"
-b2[intro]: "Const n \<Down> Const n"
-b3[intro]: "\<lbrakk>e1\<Down>e1'; e2\<Down>e2'\<rbrakk> \<Longrightarrow> Pr e1 e2 \<Down> Pr e1' e2'"
-b4[intro]: "e\<Down>Pr e1 e2 \<Longrightarrow> Fst e\<Down>e1"
-b5[intro]: "e\<Down>Pr e1 e2 \<Longrightarrow> Snd e\<Down>e2"
-b6[intro]: "e\<Down>e' \<Longrightarrow> InL e \<Down> InL e'"
-b7[intro]: "e\<Down>e' \<Longrightarrow> InR e \<Down> InR e'"
-b8[intro]: "\<lbrakk>e\<Down>InL e'; e1[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
-b9[intro]: "\<lbrakk>e\<Down>InR e'; e2[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
+inductive2 big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80)
+where
+ b0[intro]: "Lam [x].e \<Down> Lam [x].e"
+| b1[intro]: "\<lbrakk>e1\<Down>Lam [x].e; e2\<Down>e2'; e[x::=e2']\<Down>e'\<rbrakk> \<Longrightarrow> App e1 e2 \<Down> e'"
+| b2[intro]: "Const n \<Down> Const n"
+| b3[intro]: "\<lbrakk>e1\<Down>e1'; e2\<Down>e2'\<rbrakk> \<Longrightarrow> Pr e1 e2 \<Down> Pr e1' e2'"
+| b4[intro]: "e\<Down>Pr e1 e2 \<Longrightarrow> Fst e\<Down>e1"
+| b5[intro]: "e\<Down>Pr e1 e2 \<Longrightarrow> Snd e\<Down>e2"
+| b6[intro]: "e\<Down>e' \<Longrightarrow> InL e \<Down> InL e'"
+| b7[intro]: "e\<Down>e' \<Longrightarrow> InR e \<Down> InR e'"
+| b8[intro]: "\<lbrakk>e\<Down>InL e'; e1[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
+| b9[intro]: "\<lbrakk>e\<Down>InR e'; e2[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
-consts
- Ibig :: "(((nat\<Rightarrow>nat)\<times>trmI)\<times>((nat\<Rightarrow>nat)\<times>trmI)) set"
-syntax
- "_Ibig_judge" :: "((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>bool" ("_ I\<Down> _" [80,80] 80)
-translations
- "(m,e1) I\<Down> (m',e2)" \<rightleftharpoons> "((m,e1),(m',e2)) \<in> Ibig"
-
-inductive Ibig
-intros
-m0[intro]: "(m,ILam [x].e) I\<Down> (m,ILam [x].e)"
-m1[intro]: "\<lbrakk>(m,e1)I\<Down>(m',ILam [x].e); (m',e2)I\<Down>(m'',e3); (m'',e[x::=e3])I\<Down>(m''',e4)\<rbrakk>
+inductive2 Ibig :: "((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>bool" ("_ I\<Down> _" [80,80] 80)
+where
+ m0[intro]: "(m,ILam [x].e) I\<Down> (m,ILam [x].e)"
+| m1[intro]: "\<lbrakk>(m,e1)I\<Down>(m',ILam [x].e); (m',e2)I\<Down>(m'',e3); (m'',e[x::=e3])I\<Down>(m''',e4)\<rbrakk>
\<Longrightarrow> (m,IApp e1 e2) I\<Down> (m''',e4)"
-m2[intro]: "(m,IUnit) I\<Down> (m,IUnit)"
-m3[intro]: "(m,INat(n))I\<Down>(m,INat(n))"
-m4[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,ISucc(e))I\<Down>(m',INat(n+1))"
-m5[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,IRef(e))I\<Down>(m',INat(m' n))"
-m6[intro]: "\<lbrakk>(m,e1)I\<Down>(m',INat(n1)); (m',e2)I\<Down>(m'',INat(n2))\<rbrakk> \<Longrightarrow> (m,e1\<mapsto>e2)I\<Down>(m''(n1:=n2),IUnit)"
-m7[intro]: "\<lbrakk>(m,e1)I\<Down>(m',IUnit); (m',e2)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,e1;;e2)I\<Down>(m'',e)"
-m8[intro]: "\<lbrakk>(m,e)I\<Down>(m',INat(n)); n\<noteq>0; (m',e1)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,Iif e e1 e2)I\<Down>(m'',e)"
-m9[intro]: "\<lbrakk>(m,e)I\<Down>(m',INat(0)); (m',e2)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,Iif e e1 e2)I\<Down>(m'',e)"
+| m2[intro]: "(m,IUnit) I\<Down> (m,IUnit)"
+| m3[intro]: "(m,INat(n))I\<Down>(m,INat(n))"
+| m4[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,ISucc(e))I\<Down>(m',INat(n+1))"
+| m5[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,IRef(e))I\<Down>(m',INat(m' n))"
+| m6[intro]: "\<lbrakk>(m,e1)I\<Down>(m',INat(n1)); (m',e2)I\<Down>(m'',INat(n2))\<rbrakk> \<Longrightarrow> (m,e1\<mapsto>e2)I\<Down>(m''(n1:=n2),IUnit)"
+| m7[intro]: "\<lbrakk>(m,e1)I\<Down>(m',IUnit); (m',e2)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,e1;;e2)I\<Down>(m'',e)"
+| m8[intro]: "\<lbrakk>(m,e)I\<Down>(m',INat(n)); n\<noteq>0; (m',e1)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,Iif e e1 e2)I\<Down>(m'',e)"
+| m9[intro]: "\<lbrakk>(m,e)I\<Down>(m',INat(0)); (m',e2)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,Iif e e1 e2)I\<Down>(m'',e)"
text {* Translation functions *}
--- a/src/HOL/Nominal/Examples/SN.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy Wed Feb 07 17:44:07 2007 +0100
@@ -45,21 +45,16 @@
apply(simp_all add: fresh_atm)
done
-consts
- Beta :: "(lam\<times>lam) set"
-syntax
- "_Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
- "_Beta_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
-translations
- "t1 \<longrightarrow>\<^isub>\<beta> t2" \<rightleftharpoons> "(t1,t2) \<in> Beta"
- "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" \<rightleftharpoons> "(t1,t2) \<in> Beta\<^sup>*"
-inductive Beta
- intros
+inductive2 Beta :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
+where
b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
- b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
- b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)"
- b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
+| b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
+| b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)"
+| b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
+abbreviation "Beta_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80) where
+ "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2 \<equiv> Beta\<^sup>*\<^sup>* t1 t2"
+
lemma eqvt_beta:
fixes pi :: "name prm"
and t :: "lam"
@@ -86,7 +81,7 @@
next
case b2 thus ?case using a2 by (simp, blast intro: eqvt_beta)
next
- case (b3 a s1 s2)
+ case (b3 s1 s2 a)
have j1: "s1 \<longrightarrow>\<^isub>\<beta> s2" by fact
have j2: "\<And>x (pi::name prm). P x (pi\<bullet>s1) (pi\<bullet>s2)" by fact
show ?case
@@ -137,7 +132,7 @@
lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
-apply(ind_cases "Lam [a].t \<longrightarrow>\<^isub>\<beta> t'")
+apply(ind_cases2 "Lam [a].t \<longrightarrow>\<^isub>\<beta> t'")
apply(auto simp add: lam.distinct lam.inject)
apply(auto simp add: alpha)
apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
@@ -201,15 +196,10 @@
"dom_ty [] = []"
"dom_ty (x#\<Gamma>) = (fst x)#(dom_ty \<Gamma>)"
-consts
- ctxts :: "((name\<times>ty) list) set"
- valid :: "(name\<times>ty) list \<Rightarrow> bool"
-translations
- "valid \<Gamma>" \<rightleftharpoons> "\<Gamma> \<in> ctxts"
-inductive ctxts
-intros
-v1[intro]: "valid []"
-v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
+inductive2 valid :: "(name\<times>ty) list \<Rightarrow> bool"
+where
+ v1[intro]: "valid []"
+| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
lemma valid_eqvt:
fixes pi:: "name prm"
@@ -238,7 +228,7 @@
and a :: "name"
and \<tau> :: "ty"
shows "valid ((a,\<tau>)#\<Gamma>) \<Longrightarrow> valid \<Gamma> \<and> a\<sharp>\<Gamma>"
-apply(ind_cases "valid ((a,\<tau>)#\<Gamma>)", simp)
+apply(ind_cases2 "valid ((a,\<tau>)#\<Gamma>)", simp)
done
lemma valid_unicity[rule_format]:
@@ -251,18 +241,11 @@
apply(auto dest!: valid_elim fresh_context)
done
-consts
- typing :: "(((name\<times>ty) list)\<times>lam\<times>ty) set"
-syntax
- "_typing_judge" :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
-translations
- "\<Gamma> \<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> typing"
-
-inductive typing
-intros
-t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
-t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
-t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
+inductive2 typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
+where
+ t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
+| t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
+| t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
lemma eqvt_typing:
fixes \<Gamma> :: "(name\<times>ty) list"
@@ -273,14 +256,14 @@
shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>"
using a
proof (induct)
- case (t1 \<Gamma> \<tau> a)
+ case (t1 \<Gamma> a \<tau>)
have "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
moreover
have "(pi\<bullet>(a,\<tau>))\<in>((pi::name prm)\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst])
ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> ((pi::name prm)\<bullet>Var a) : \<tau>"
using typing.t1 by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
next
- case (t3 \<Gamma> \<sigma> \<tau> a t)
+ case (t3 a \<Gamma> \<tau> t \<sigma>)
moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij)
ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force
qed (auto)
@@ -302,7 +285,7 @@
proof -
from a have "\<And>(pi::name prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau>"
proof (induct)
- case (t1 \<Gamma> \<tau> a)
+ case (t1 \<Gamma> a \<tau>)
have j1: "valid \<Gamma>" by fact
have j2: "(a,\<tau>)\<in>set \<Gamma>" by fact
from j1 have j3: "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
@@ -310,10 +293,10 @@
hence j4: "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_name_inst])
show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Var a)) \<tau>" using a1 j3 j4 by simp
next
- case (t2 \<Gamma> \<sigma> \<tau> t1 t2)
+ case (t2 \<Gamma> t1 \<tau> \<sigma> t2)
thus ?case using a2 by (simp, blast intro: eqvt_typing)
next
- case (t3 \<Gamma> \<sigma> \<tau> a t)
+ case (t3 a \<Gamma> \<tau> t \<sigma>)
have k1: "a\<sharp>\<Gamma>" by fact
have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
have k3: "\<And>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact
@@ -375,17 +358,17 @@
done
lemma t1_elim: "\<Gamma> \<turnstile> Var a : \<tau> \<Longrightarrow> valid \<Gamma> \<and> (a,\<tau>) \<in> set \<Gamma>"
-apply(ind_cases "\<Gamma> \<turnstile> Var a : \<tau>")
+apply(ind_cases2 "\<Gamma> \<turnstile> Var a : \<tau>")
apply(auto simp add: lam.inject lam.distinct)
done
lemma t2_elim: "\<Gamma> \<turnstile> App t1 t2 : \<sigma> \<Longrightarrow> \<exists>\<tau>. (\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<and> \<Gamma> \<turnstile> t2 : \<tau>)"
-apply(ind_cases "\<Gamma> \<turnstile> App t1 t2 : \<sigma>")
+apply(ind_cases2 "\<Gamma> \<turnstile> App t1 t2 : \<sigma>")
apply(auto simp add: lam.inject lam.distinct)
done
lemma t3_elim: "\<lbrakk>\<Gamma> \<turnstile> Lam [a].t : \<sigma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> \<exists>\<tau> \<tau>'. \<sigma>=\<tau>\<rightarrow>\<tau>' \<and> ((a,\<tau>)#\<Gamma>) \<turnstile> t : \<tau>'"
-apply(ind_cases "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")
+apply(ind_cases2 "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")
apply(auto simp add: lam.distinct lam.inject alpha)
apply(drule_tac pi="[(a,aa)]::name prm" in eqvt_typing)
apply(simp)
@@ -534,7 +517,7 @@
constdefs
"SN" :: "lam \<Rightarrow> bool"
- "SN t \<equiv> t\<in>termi Beta"
+ "SN t \<equiv> termi Beta t"
lemma SN_preserved: "\<lbrakk>SN(t1);t1\<longrightarrow>\<^isub>\<beta> t2\<rbrakk>\<Longrightarrow>SN(t2)"
apply(simp add: SN_def)
@@ -561,30 +544,24 @@
"NEUT t \<equiv> (\<exists>a. t=Var a)\<or>(\<exists>t1 t2. t=App t1 t2)"
(* a slight hack to get the first element of applications *)
-consts
- FST :: "(lam\<times>lam) set"
-syntax
- "FST_judge" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
-translations
- "t1 \<guillemotright> t2" \<rightleftharpoons> "(t1,t2) \<in> FST"
-inductive FST
- intros
+inductive2 FST :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
+where
fst[intro!]: "(App t s) \<guillemotright> t"
lemma fst_elim[elim!]:
shows "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
-apply(ind_cases "App t s \<guillemotright> t'")
+apply(ind_cases2 "App t s \<guillemotright> t'")
apply(simp add: lam.inject)
done
lemma qq3: "SN(App t s)\<Longrightarrow>SN(t)"
apply(simp add: SN_def)
-apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> z\<in>termi Beta")(*A*)
+apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> termi Beta z")(*A*)
apply(force)
(*A*)
apply(erule acc_induct)
apply(clarify)
-apply(ind_cases "x \<guillemotright> z")
+apply(ind_cases2 "x \<guillemotright> z" for x z)
apply(clarify)
apply(rule accI)
apply(auto intro: b1)
@@ -626,7 +603,7 @@
apply(force simp only: NEUT_def)
apply(simp (no_asm) add: CR3_RED_def)
apply(clarify)
-apply(ind_cases "App t x \<longrightarrow>\<^isub>\<beta> t'")
+apply(ind_cases2 "App t x \<longrightarrow>\<^isub>\<beta> t'" for x t t')
apply(simp_all add: lam.inject)
apply(simp only: CR3_RED_def)
apply(drule_tac x="s2" in spec)
@@ -701,21 +678,21 @@
qed
lemma double_acc_aux:
- assumes a_acc: "a \<in> acc r"
- and b_acc: "b \<in> acc r"
+ assumes a_acc: "acc r a"
+ and b_acc: "acc r b"
and hyp: "\<And>x z.
- (\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow>
- (\<And>y. (y, x) \<in> r \<Longrightarrow> P y z) \<Longrightarrow>
- (\<And>u. (u, z) \<in> r \<Longrightarrow> u \<in> acc r) \<Longrightarrow>
- (\<And>u. (u, z) \<in> r \<Longrightarrow> P x u) \<Longrightarrow> P x z"
+ (\<And>y. r y x \<Longrightarrow> acc r y) \<Longrightarrow>
+ (\<And>y. r y x \<Longrightarrow> P y z) \<Longrightarrow>
+ (\<And>u. r u z \<Longrightarrow> acc r u) \<Longrightarrow>
+ (\<And>u. r u z \<Longrightarrow> P x u) \<Longrightarrow> P x z"
shows "P a b"
proof -
from a_acc
- have r: "\<And>b. b \<in> acc r \<Longrightarrow> P a b"
+ have r: "\<And>b. acc r b \<Longrightarrow> P a b"
proof (induct a rule: acc.induct)
case (accI x)
note accI' = accI
- have "b \<in> acc r" .
+ have "acc r b" .
thus ?case
proof (induct b rule: acc.induct)
case (accI y)
@@ -734,7 +711,7 @@
qed
lemma double_acc:
- "\<lbrakk>a \<in> acc r; b \<in> acc r; \<forall>x z. ((\<forall>y. (y, x)\<in>r\<longrightarrow>P y z)\<and>(\<forall>u. (u, z)\<in>r\<longrightarrow>P x u))\<longrightarrow>P x z\<rbrakk>\<Longrightarrow>P a b"
+ "\<lbrakk>acc r a; acc r b; \<forall>x z. ((\<forall>y. r y x \<longrightarrow> P y z) \<and> (\<forall>u. r u z \<longrightarrow> P x u)) \<longrightarrow> P x z\<rbrakk> \<Longrightarrow> P a b"
apply(rule_tac r="r" in double_acc_aux)
apply(assumption)+
apply(blast)
@@ -743,7 +720,7 @@
lemma abs_RED: "(\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>)\<longrightarrow>Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
apply(simp)
apply(clarify)
-apply(subgoal_tac "t\<in>termi Beta")(*1*)
+apply(subgoal_tac "termi Beta t")(*1*)
apply(erule rev_mp)
apply(subgoal_tac "u \<in> RED \<tau>")(*A*)
apply(erule rev_mp)
@@ -764,7 +741,7 @@
apply(force simp add: NEUT_def)
apply(simp add: CR3_RED_def)
apply(clarify)
-apply(ind_cases "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'")
+apply(ind_cases2 "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'" for xa z t')
apply(auto simp add: lam.inject lam.distinct)
apply(drule beta_abs)
apply(auto)
@@ -813,7 +790,7 @@
apply(force simp add: NEUT_def)
apply(simp add: NORMAL_def)
apply(clarify)
-apply(ind_cases "Var x \<longrightarrow>\<^isub>\<beta> t'")
+apply(ind_cases2 "Var x \<longrightarrow>\<^isub>\<beta> t'" for t')
apply(auto simp add: lam.inject lam.distinct)
apply(force simp add: RED_props)
apply(simp add: id_subs)
--- a/src/HOL/Tools/inductive_codegen.ML Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Wed Feb 07 17:44:07 2007 +0100
@@ -7,7 +7,7 @@
signature INDUCTIVE_CODEGEN =
sig
- val add : string option -> attribute
+ val add : string option -> int option -> attribute
val setup : theory -> theory
end;
@@ -16,6 +16,17 @@
open Codegen;
+(* read off parameters of inductive predicate from raw induction rule *)
+fun params_of induct =
+ let
+ val (_ $ t $ u :: _) =
+ HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
+ val (_, ts) = strip_comb t;
+ val (_, us) = strip_comb u
+ in
+ List.take (ts, length ts - length us)
+ end;
+
(**** theory data ****)
fun merge_rules tabs =
@@ -26,7 +37,7 @@
(struct
val name = "HOL/inductive_codegen";
type T =
- {intros : (thm * string) list Symtab.table,
+ {intros : (thm * (string * int)) list Symtab.table,
graph : unit Graph.T,
eqns : (thm * string) list Symtab.table};
val empty =
@@ -47,39 +58,46 @@
fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
-fun add optmod = Thm.declaration_attribute (fn thm => Context.mapping (fn thy =>
+fun add optmod optnparms = Thm.declaration_attribute (fn thm => Context.mapping (fn thy =>
let
val {intros, graph, eqns} = CodegenData.get thy;
fun thyname_of s = (case optmod of
NONE => thyname_of_const s thy | SOME s => s);
- in (case concl_of thm of
- _ $ (Const ("op :", _) $ _ $ t) => (case head_of t of
- Const (s, _) =>
- let val cs = foldr add_term_consts [] (prems_of thm)
- in CodegenData.put
- {intros = intros |>
- Symtab.update (s, Symtab.lookup_list intros s @ [(thm, thyname_of s)]),
- graph = foldr (uncurry (Graph.add_edge o pair s))
- (Library.foldl add_node (graph, s :: cs)) cs,
- eqns = eqns} thy
- end
- | _ => (warn thm; thy))
- | _ $ (Const ("op =", _) $ t $ _) => (case head_of t of
+ in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of
+ SOME (Const ("op =", _), [t, _]) => (case head_of t of
Const (s, _) =>
CodegenData.put {intros = intros, graph = graph,
eqns = eqns |> Symtab.update
(s, Symtab.lookup_list eqns s @ [(thm, thyname_of s)])} thy
| _ => (warn thm; thy))
+ | SOME (Const (s, _), _) =>
+ let
+ val cs = foldr add_term_consts [] (prems_of thm);
+ val rules = Symtab.lookup_list intros s;
+ val nparms = (case optnparms of
+ SOME k => k
+ | NONE => (case rules of
+ [] => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of
+ SOME (_, {raw_induct, ...}) => length (params_of raw_induct)
+ | NONE => 0)
+ | xs => snd (snd (snd (split_last xs)))))
+ in CodegenData.put
+ {intros = intros |>
+ Symtab.update (s, rules @ [(thm, (thyname_of s, nparms))]),
+ graph = foldr (uncurry (Graph.add_edge o pair s))
+ (Library.foldl add_node (graph, s :: cs)) cs,
+ eqns = eqns} thy
+ end
| _ => (warn thm; thy))
end) I);
fun get_clauses thy s =
let val {intros, graph, ...} = CodegenData.get thy
in case Symtab.lookup intros s of
- NONE => (case OldInductivePackage.get_inductive thy s of
+ NONE => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of
NONE => NONE
- | SOME ({names, ...}, {intrs, ...}) =>
- SOME (names, thyname_of_const s thy,
+ | SOME ({names, ...}, {intrs, raw_induct, ...}) =>
+ SOME (names, thyname_of_const s thy, length (params_of raw_induct),
preprocess thy intrs))
| SOME _ =>
let
@@ -87,64 +105,11 @@
(fn xs => s mem xs) (Graph.strong_conn graph);
val intrs = List.concat (map
(fn s => the (Symtab.lookup intros s)) names);
- val (_, (_, thyname)) = split_last intrs
- in SOME (names, thyname, preprocess thy (map fst intrs)) end
+ val (_, (_, (thyname, nparms))) = split_last intrs
+ in SOME (names, thyname, nparms, preprocess thy (map fst intrs)) end
end;
-(**** improper tuples ****)
-
-fun prod_factors p (Const ("Pair", _) $ t $ u) =
- p :: prod_factors (1::p) t @ prod_factors (2::p) u
- | prod_factors p _ = [];
-
-fun split_prod p ps t = if p mem ps then (case t of
- Const ("Pair", _) $ t $ u =>
- split_prod (1::p) ps t @ split_prod (2::p) ps u
- | _ => error "Inconsistent use of products") else [t];
-
-fun full_split_prod (Const ("Pair", _) $ t $ u) =
- full_split_prod t @ full_split_prod u
- | full_split_prod t = [t];
-
-datatype factors = FVar of int list list | FFix of int list list;
-
-exception Factors;
-
-fun mg_factor (FVar f) (FVar f') = FVar (f inter f')
- | mg_factor (FVar f) (FFix f') =
- if f' subset f then FFix f' else raise Factors
- | mg_factor (FFix f) (FVar f') =
- if f subset f' then FFix f else raise Factors
- | mg_factor (FFix f) (FFix f') =
- if f subset f' andalso f' subset f then FFix f else raise Factors;
-
-fun dest_factors (FVar f) = f
- | dest_factors (FFix f) = f;
-
-fun infer_factors sg extra_fs (fs, (optf, t)) =
- let fun err s = error (s ^ "\n" ^ Sign.string_of_term sg t)
- in (case (optf, strip_comb t) of
- (SOME f, (Const (name, _), args)) =>
- (case AList.lookup (op =) extra_fs name of
- NONE => AList.update (op =) (name, getOpt
- (Option.map (mg_factor f) (AList.lookup (op =) fs name), f)) fs
- | SOME (fs', f') => (mg_factor f (FFix f');
- Library.foldl (infer_factors sg extra_fs)
- (fs, map (Option.map FFix) fs' ~~ args)))
- | (SOME f, (Var ((name, _), _), [])) =>
- AList.update (op =) (name, getOpt
- (Option.map (mg_factor f) (AList.lookup (op =) fs name), f)) fs
- | (NONE, _) => fs
- | _ => err "Illegal term")
- handle Factors => err "Product factor mismatch in"
- end;
-
-fun string_of_factors p ps = if p mem ps then
- "(" ^ string_of_factors (1::p) ps ^ ", " ^ string_of_factors (2::p) ps ^ ")"
- else "_";
-
-
(**** check if a term contains only constructor functions ****)
fun is_constrt thy =
@@ -202,31 +167,47 @@
fun cprods xss = foldr (map op :: o cprod) [[]] xss;
-datatype mode = Mode of (int list option list * int list) * mode option list;
+datatype mode = Mode of (int list option list * int list) * int list * mode option list;
fun modes_of modes t =
let
- fun mk_modes name args = List.concat
- (map (fn (m as (iss, is)) => map (Mode o pair m) (cprods (map
- (fn (NONE, _) => [NONE]
- | (SOME js, arg) => map SOME
- (List.filter (fn Mode ((_, js'), _) => js=js') (modes_of modes arg)))
- (iss ~~ args)))) ((the o AList.lookup (op =) modes) name))
+ val ks = 1 upto length (binder_types (fastype_of t));
+ val default = [Mode (([], ks), ks, [])];
+ fun mk_modes name args = Option.map (List.concat o
+ map (fn (m as (iss, is)) =>
+ let
+ val (args1, args2) =
+ if length args < length iss then
+ error ("Too few arguments for inductive predicate " ^ name)
+ else chop (length iss) args;
+ val k = length args2;
+ val prfx = 1 upto k
+ in
+ if not (is_prefix op = prfx is) then [] else
+ let val is' = map (fn i => i - k) (List.drop (is, k))
+ in map (fn x => Mode (m, is', x)) (cprods (map
+ (fn (NONE, _) => [NONE]
+ | (SOME js, arg) => map SOME (List.filter
+ (fn Mode (_, js', _) => js=js') (modes_of modes arg)))
+ (iss ~~ args1)))
+ end
+ end)) (AList.lookup op = modes name)
in (case strip_comb t of
(Const ("op =", Type (_, [T, _])), _) =>
- [Mode (([], [1]), []), Mode (([], [2]), [])] @
- (if is_eqT T then [Mode (([], [1, 2]), [])] else [])
- | (Const (name, _), args) => mk_modes name args
- | (Var ((name, _), _), args) => mk_modes name args
- | (Free (name, _), args) => mk_modes name args)
+ [Mode (([], [1]), [1], []), Mode (([], [2]), [2], [])] @
+ (if is_eqT T then [Mode (([], [1, 2]), [1, 2], [])] else [])
+ | (Const (name, _), args) => the_default default (mk_modes name args)
+ | (Var ((name, _), _), args) => the (mk_modes name args)
+ | (Free (name, _), args) => the (mk_modes name args)
+ | _ => default)
end;
datatype indprem = Prem of term list * term | Sidecond of term;
fun select_mode_prem thy modes vs ps =
find_first (is_some o snd) (ps ~~ map
- (fn Prem (us, t) => find_first (fn Mode ((_, is), _) =>
+ (fn Prem (us, t) => find_first (fn Mode (_, is, _) =>
let
val (in_ts, out_ts) = get_args is 1 us;
val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
@@ -239,8 +220,8 @@
term_vs t subset vs andalso
forall is_eqT dupTs
end)
- (modes_of modes t handle Option => [Mode (([], []), [])])
- | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), []))
+ (modes_of modes t handle Option => [Mode (([], []), [], [])])
+ | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
else NONE) ps);
fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) =
@@ -278,12 +259,12 @@
let val y = f x
in if x = y then x else fixp f y end;
-fun infer_modes thy extra_modes factors arg_vs preds = fixp (fn modes =>
+fun infer_modes thy extra_modes arities arg_vs preds = fixp (fn modes =>
map (check_modes_pred thy arg_vs preds (modes @ extra_modes)) modes)
- (map (fn (s, (fs, f)) => (s, cprod (cprods (map
+ (map (fn (s, (ks, k)) => (s, cprod (cprods (map
(fn NONE => [NONE]
- | SOME f' => map SOME (subsets 1 (length f' + 1))) fs),
- subsets 1 (length f + 1)))) factors);
+ | SOME k' => map SOME (subsets 1 k')) ks),
+ subsets 1 k))) arities);
(**** code generation ****)
@@ -296,51 +277,6 @@
List.concat (separate [Pretty.str ",", Pretty.brk 1] (map single xs)) @
[Pretty.str ")"]);
-(* convert nested pairs to n-tuple *)
-
-fun conv_ntuple [_] t ps = ps
- | conv_ntuple [_, _] t ps = ps
- | conv_ntuple us t ps =
- let
- val xs = map (fn i => Pretty.str ("x" ^ string_of_int i))
- (1 upto length us);
- fun ntuple (ys as (x, T) :: xs) U =
- if T = U then (x, xs)
- else
- let
- val Type ("*", [U1, U2]) = U;
- val (p1, ys1) = ntuple ys U1;
- val (p2, ys2) = ntuple ys1 U2
- in (mk_tuple [p1, p2], ys2) end
- in
- [Pretty.str "Seq.map (fn", Pretty.brk 1,
- fst (ntuple (xs ~~ map fastype_of us) (HOLogic.dest_setT (fastype_of t))),
- Pretty.str " =>", Pretty.brk 1, mk_tuple xs, Pretty.str ")",
- Pretty.brk 1, parens (Pretty.block ps)]
- end;
-
-(* convert n-tuple to nested pairs *)
-
-fun conv_ntuple' fs T ps =
- let
- fun mk_x i = Pretty.str ("x" ^ string_of_int i);
- fun conv i js (Type ("*", [T, U])) =
- if js mem fs then
- let
- val (p, i') = conv i (1::js) T;
- val (q, i'') = conv i' (2::js) U
- in (mk_tuple [p, q], i'') end
- else (mk_x i, i+1)
- | conv i js _ = (mk_x i, i+1)
- val (p, i) = conv 1 [] T
- in
- if i > 3 then
- [Pretty.str "Seq.map (fn", Pretty.brk 1,
- mk_tuple (map mk_x (1 upto i-1)), Pretty.str " =>", Pretty.brk 1,
- p, Pretty.str ")", Pretty.brk 1, parens (Pretty.block ps)]
- else ps
- end;
-
fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of
NONE => ((names, (s, [s])::vs), s)
| SOME xs => let val s' = Name.variant names s in
@@ -383,23 +319,37 @@
map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is])))
end;
-fun compile_expr thy defs dep module brack (gr, (NONE, t)) =
+fun mk_funcomp brack s k p = (if brack then parens else I)
+ (Pretty.block [Pretty.block ((if k = 0 then [] else [Pretty.str "("]) @
+ separate (Pretty.brk 1) (Pretty.str s :: replicate k (Pretty.str "|> ???")) @
+ (if k = 0 then [] else [Pretty.str ")"])), Pretty.brk 1, p]);
+
+fun compile_expr thy defs dep module brack modes (gr, (NONE, t)) =
apsnd single (invoke_codegen thy defs dep module brack (gr, t))
- | compile_expr _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) =
+ | compile_expr _ _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) =
(gr, [Pretty.str name])
- | compile_expr thy defs dep module brack (gr, (SOME (Mode (mode, ms)), t)) =
- let
- val (Const (name, _), args) = strip_comb t;
- val (gr', (ps, mode_id)) = foldl_map
- (compile_expr thy defs dep module true) (gr, ms ~~ args) |>>>
- modename module name mode;
- in (gr', (if brack andalso not (null ps) then
- single o parens o Pretty.block else I)
- (List.concat (separate [Pretty.brk 1]
- ([Pretty.str mode_id] :: ps))))
- end;
+ | compile_expr thy defs dep module brack modes (gr, (SOME (Mode (mode, _, ms)), t)) =
+ (case strip_comb t of
+ (Const (name, _), args) =>
+ if name = "op =" orelse AList.defined op = modes name then
+ let
+ val (args1, args2) = chop (length ms) args;
+ val (gr', (ps, mode_id)) = foldl_map
+ (compile_expr thy defs dep module true modes) (gr, ms ~~ args1) |>>>
+ modename module name mode;
+ val (gr'', ps') = foldl_map
+ (invoke_codegen thy defs dep module true) (gr', args2)
+ in (gr', (if brack andalso not (null ps andalso null ps') then
+ single o parens o Pretty.block else I)
+ (List.concat (separate [Pretty.brk 1]
+ ([Pretty.str mode_id] :: ps @ map single ps'))))
+ end
+ else apsnd (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
+ (invoke_codegen thy defs dep module true (gr, t))
+ | _ => apsnd (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
+ (invoke_codegen thy defs dep module true (gr, t)));
-fun compile_clause thy defs gr dep module all_vs arg_vs modes (iss, is) (ts, ps) =
+fun compile_clause thy defs gr dep module all_vs arg_vs modes (iss, is) (ts, ps) inp =
let
val modes' = modes @ List.mapPartial
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
@@ -442,7 +392,7 @@
| compile_prems out_ts vs names gr ps =
let
val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts));
- val SOME (p, mode as SOME (Mode ((_, js), _))) =
+ val SOME (p, mode as SOME (Mode (_, js, _))) =
select_mode_prem thy modes' vs' ps;
val ps' = filter_out (equal p) ps;
val ((names', eqs), out_ts') =
@@ -458,14 +408,14 @@
let
val (in_ts, out_ts''') = get_args js 1 us;
val (gr2, in_ps) = foldl_map
- (invoke_codegen thy defs dep module false) (gr1, in_ts);
+ (invoke_codegen thy defs dep module true) (gr1, in_ts);
val (gr3, ps) = if is_ind t then
- apsnd (fn ps => ps @ [Pretty.brk 1, mk_tuple in_ps])
- (compile_expr thy defs dep module false
+ apsnd (fn ps => ps @ Pretty.brk 1 ::
+ separate (Pretty.brk 1) in_ps)
+ (compile_expr thy defs dep module false modes
(gr2, (mode, t)))
else
- apsnd (fn p => conv_ntuple us t
- [Pretty.str "Seq.of_list", Pretty.brk 1, p])
+ apsnd (fn p => [Pretty.str "Seq.of_list", Pretty.brk 1, p])
(invoke_codegen thy defs dep module true (gr2, t));
val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps';
in
@@ -488,20 +438,24 @@
val (gr', prem_p) = compile_prems in_ts' arg_vs all_vs' gr ps;
in
- (gr', Pretty.block [Pretty.str "Seq.single inp :->", Pretty.brk 1, prem_p])
+ (gr', Pretty.block [Pretty.str "Seq.single", Pretty.brk 1, inp,
+ Pretty.str " :->", Pretty.brk 1, prem_p])
end;
fun compile_pred thy defs gr dep module prfx all_vs arg_vs modes s cls mode =
- let val (gr', (cl_ps, mode_id)) =
- foldl_map (fn (gr, cl) => compile_clause thy defs
- gr dep module all_vs arg_vs modes mode cl) (gr, cls) |>>>
- modename module s mode
+ let
+ val xs = map Pretty.str (Name.variant_list arg_vs
+ (map (fn i => "x" ^ string_of_int i) (snd mode)));
+ val (gr', (cl_ps, mode_id)) =
+ foldl_map (fn (gr, cl) => compile_clause thy defs
+ gr dep module all_vs arg_vs modes mode cl (mk_tuple xs)) (gr, cls) |>>>
+ modename module s mode
in
((gr', "and "), Pretty.block
([Pretty.block (separate (Pretty.brk 1)
(Pretty.str (prfx ^ mode_id) ::
- map Pretty.str arg_vs) @
- [Pretty.str " inp ="]),
+ map Pretty.str arg_vs @ xs) @
+ [Pretty.str " ="]),
Pretty.brk 1] @
List.concat (separate [Pretty.str " ++", Pretty.brk 1] (map single cl_ps))))
end;
@@ -519,17 +473,17 @@
exception Modes of
(string * (int list option list * int list) list) list *
- (string * (int list list option list * int list list)) list;
+ (string * (int option list * int)) list;
fun lookup_modes gr dep = apfst List.concat (apsnd List.concat (ListPair.unzip
(map ((fn (SOME (Modes x), _, _) => x | _ => ([], [])) o get_node gr)
(Graph.all_preds (fst gr) [dep]))));
-fun print_factors factors = message ("Factors:\n" ^
- space_implode "\n" (map (fn (s, (fs, f)) => s ^ ": " ^
+fun print_arities arities = message ("Arities:\n" ^
+ space_implode "\n" (map (fn (s, (ks, k)) => s ^ ": " ^
space_implode " -> " (map
- (fn NONE => "X" | SOME f' => string_of_factors [] f')
- (fs @ [SOME f]))) factors));
+ (fn NONE => "X" | SOME k' => string_of_int k')
+ (ks @ [SOME k]))) arities));
fun prep_intrs intrs = map (rename_term o #prop o rep_thm o standard) intrs;
@@ -543,133 +497,97 @@
if name mem names then gr
else (case get_clauses thy name of
NONE => gr
- | SOME (names, thyname, intrs) =>
+ | SOME (names, thyname, nparms, intrs) =>
mk_ind_def thy defs gr dep names (if_library thyname module)
- [] [] (prep_intrs intrs)))
+ [] (prep_intrs intrs) nparms))
(gr, foldr add_term_consts [] ts)
-and mk_ind_def thy defs gr dep names module modecs factorcs intrs =
+and mk_ind_def thy defs gr dep names module modecs intrs nparms =
add_edge (hd names, dep) gr handle Graph.UNDEF _ =>
let
- val _ $ (_ $ _ $ u) = Logic.strip_imp_concl (hd intrs);
- val (_, args) = strip_comb u;
+ val _ $ u = Logic.strip_imp_concl (hd intrs);
+ val args = List.take (snd (strip_comb u), nparms);
val arg_vs = List.concat (map term_vs args);
- fun dest_prem factors (_ $ (p as (Const ("op :", _) $ t $ u))) =
- (case AList.lookup (op =) factors (case head_of u of
- Const (name, _) => name | Var ((name, _), _) => name) of
- NONE => Prem (full_split_prod t, u)
- | SOME f => Prem (split_prod [] f t, u))
- | dest_prem factors (_ $ ((eq as Const ("op =", _)) $ t $ u)) =
- Prem ([t, u], eq)
- | dest_prem factors (_ $ t) = Sidecond t;
+ fun get_nparms s = if s mem names then SOME nparms else
+ Option.map #3 (get_clauses thy s);
- fun add_clause factors (clauses, intr) =
+ fun dest_prem (_ $ (Const ("op :", _) $ t $ u)) = Prem ([t], u)
+ | dest_prem (_ $ ((eq as Const ("op =", _)) $ t $ u)) = Prem ([t, u], eq)
+ | dest_prem (_ $ t) =
+ (case strip_comb t of
+ (v as Var _, ts) => Prem (ts, v)
+ | (c as Const (s, _), ts) => (case get_nparms s of
+ NONE => Sidecond t
+ | SOME k =>
+ let val (ts1, ts2) = chop k ts
+ in Prem (ts2, list_comb (c, ts1)) end)
+ | _ => Sidecond t);
+
+ fun add_clause intr (clauses, arities) =
let
- val _ $ (_ $ t $ u) = Logic.strip_imp_concl intr;
- val Const (name, _) = head_of u;
- val prems = map (dest_prem factors) (Logic.strip_imp_prems intr);
+ val _ $ t = Logic.strip_imp_concl intr;
+ val (Const (name, T), ts) = strip_comb t;
+ val (ts1, ts2) = chop nparms ts;
+ val prems = map dest_prem (Logic.strip_imp_prems intr);
+ val (Ts, Us) = chop nparms (binder_types T)
in
- AList.update (op =) (name, ((these o AList.lookup (op =) clauses) name) @
- [(split_prod [] ((the o AList.lookup (op =) factors) name) t, prems)]) clauses
+ (AList.update op = (name, these (AList.lookup op = clauses name) @
+ [(ts2, prems)]) clauses,
+ AList.update op = (name, (map (fn U => (case strip_type U of
+ (Rs as _ :: _, Type ("bool", [])) => SOME (length Rs)
+ | _ => NONE)) Ts,
+ length Us)) arities)
end;
- fun check_set (Const (s, _)) = s mem names orelse is_some (get_clauses thy s)
- | check_set (Var ((s, _), _)) = s mem arg_vs
- | check_set _ = false;
-
- fun add_prod_factors extra_fs (fs, _ $ (Const ("op :", _) $ t $ u)) =
- if check_set (head_of u)
- then infer_factors (sign_of thy) extra_fs
- (fs, (SOME (FVar (prod_factors [] t)), u))
- else fs
- | add_prod_factors _ (fs, _) = fs;
-
val gr' = mk_extra_defs thy defs
(add_edge (hd names, dep)
(new_node (hd names, (NONE, "", "")) gr)) (hd names) names module intrs;
- val (extra_modes, extra_factors) = lookup_modes gr' (hd names);
- val fs = constrain factorcs (map (apsnd dest_factors)
- (Library.foldl (add_prod_factors extra_factors) ([], List.concat (map (fn t =>
- Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs))));
- val factors = List.mapPartial (fn (name, f) =>
- if name mem arg_vs then NONE
- else SOME (name, (map (AList.lookup (op =) fs) arg_vs, f))) fs;
- val clauses =
- Library.foldl (add_clause (fs @ map (apsnd snd) extra_factors)) ([], intrs);
+ val (extra_modes, extra_arities) = lookup_modes gr' (hd names);
+ val (clauses, arities) = fold add_clause intrs ([], []);
val modes = constrain modecs
- (infer_modes thy extra_modes factors arg_vs clauses);
- val _ = print_factors factors;
+ (infer_modes thy extra_modes arities arg_vs clauses);
+ val _ = print_arities arities;
val _ = print_modes modes;
val (gr'', s) = compile_preds thy defs gr' (hd names) module (terms_vs intrs)
arg_vs (modes @ extra_modes) clauses;
in
(map_node (hd names)
- (K (SOME (Modes (modes, factors)), module, s)) gr'')
+ (K (SOME (Modes (modes, arities)), module, s)) gr'')
end;
-fun find_mode gr dep s u modes is = (case find_first (fn Mode ((_, js), _) => is=js)
+fun find_mode gr dep s u modes is = (case find_first (fn Mode (_, js, _) => is=js)
(modes_of modes u handle Option => []) of
NONE => codegen_error gr dep
("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
| mode => mode);
-fun mk_ind_call thy defs gr dep module t u is_query = (case head_of u of
- Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
- (NONE, _) => NONE
- | (SOME (names, thyname, intrs), NONE) =>
- let
- fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) =
- ((ts, mode), i+1)
- | mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1);
+fun mk_ind_call thy defs gr dep module is_query s T ts names thyname k intrs =
+ let
+ val (ts1, ts2) = chop k ts;
+ val u = list_comb (Const (s, T), ts1);
+
+ fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) =
+ ((ts, mode), i+1)
+ | mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1);
- val module' = if_library thyname module;
- val gr1 = mk_extra_defs thy defs
- (mk_ind_def thy defs gr dep names module'
- [] [] (prep_intrs intrs)) dep names module' [u];
- val (modes, factors) = lookup_modes gr1 dep;
- val ts = split_prod [] ((snd o the o AList.lookup (op =) factors) s) t;
- val (ts', is) = if is_query then
- fst (Library.foldl mk_mode ((([], []), 1), ts))
- else (ts, 1 upto length ts);
- val mode = find_mode gr1 dep s u modes is;
- val (gr2, in_ps) = foldl_map
- (invoke_codegen thy defs dep module false) (gr1, ts');
- val (gr3, ps) =
- compile_expr thy defs dep module false (gr2, (mode, u))
- in
- SOME (gr3, Pretty.block
- (ps @ [Pretty.brk 1, mk_tuple in_ps]))
- end
- | _ => NONE)
- | _ => NONE);
-
-fun list_of_indset thy defs gr dep module brack u = (case head_of u of
- Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
- (NONE, _) => NONE
- | (SOME (names, thyname, intrs), NONE) =>
- let
- val module' = if_library thyname module;
- val gr1 = mk_extra_defs thy defs
- (mk_ind_def thy defs gr dep names module'
- [] [] (prep_intrs intrs)) dep names module' [u];
- val (modes, factors) = lookup_modes gr1 dep;
- val mode = find_mode gr1 dep s u modes [];
- val (gr2, ps) =
- compile_expr thy defs dep module false (gr1, (mode, u));
- val (gr3, _) =
- invoke_tycodegen thy defs dep module false (gr2, body_type T)
- in
- SOME (gr3, (if brack then parens else I)
- (Pretty.block ([Pretty.str "Seq.list_of", Pretty.brk 1,
- Pretty.str "("] @
- conv_ntuple' (snd (valOf (AList.lookup (op =) factors s)))
- (HOLogic.dest_setT (fastype_of u))
- (ps @ [Pretty.brk 1, Pretty.str "()"]) @
- [Pretty.str ")"])))
- end
- | _ => NONE)
- | _ => NONE);
+ val module' = if_library thyname module;
+ val gr1 = mk_extra_defs thy defs
+ (mk_ind_def thy defs gr dep names module'
+ [] (prep_intrs intrs) k) dep names module' [u];
+ val (modes, _) = lookup_modes gr1 dep;
+ val (ts', is) = if is_query then
+ fst (Library.foldl mk_mode ((([], []), 1), ts2))
+ else (ts2, 1 upto length (binder_types T) - k);
+ val mode = find_mode gr1 dep s u modes is;
+ val (gr2, in_ps) = foldl_map
+ (invoke_codegen thy defs dep module true) (gr1, ts');
+ val (gr3, ps) =
+ compile_expr thy defs dep module false modes (gr2, (mode, u))
+ in
+ (gr3, Pretty.block (ps @ (if null in_ps then [] else [Pretty.brk 1]) @
+ separate (Pretty.brk 1) in_ps))
+ end;
fun clause_of_eqn eqn =
let
@@ -677,10 +595,8 @@
val (Const (s, T), ts) = strip_comb t;
val (Ts, U) = strip_type T
in
- rename_term
- (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop (HOLogic.mk_mem
- (foldr1 HOLogic.mk_prod (ts @ [u]), Const (s ^ "_aux",
- HOLogic.mk_setT (foldr1 HOLogic.mk_prodT (Ts @ [U])))))))
+ rename_term (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop
+ (list_comb (Const (s ^ "_aux", Ts @ [U] ---> HOLogic.boolT), ts @ [u]))))
end;
fun mk_fun thy defs name eqns dep module module' gr =
@@ -699,44 +615,57 @@
val s = Pretty.string_of (Pretty.block
[mk_app false (Pretty.str ("fun " ^ snd fun_id)) vars, Pretty.str " =",
Pretty.brk 1, Pretty.str "Seq.hd", Pretty.brk 1,
- parens (Pretty.block [Pretty.str mode_id,
- Pretty.brk 1, mk_tuple vars])]) ^ ";\n\n";
+ parens (Pretty.block (separate (Pretty.brk 1) (Pretty.str mode_id ::
+ vars)))]) ^ ";\n\n";
val gr'' = mk_ind_def thy defs (add_edge (name, dep)
(new_node (name, (NONE, module', s)) gr')) name [pname] module'
- [(pname, [([], mode)])]
- [(pname, map (fn i => replicate i 2) (0 upto arity-1))]
- clauses;
+ [(pname, [([], mode)])] clauses 0;
val (modes, _) = lookup_modes gr'' dep;
- val _ = find_mode gr'' dep pname (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
- (Logic.strip_imp_concl (hd clauses))))) modes mode
+ val _ = find_mode gr'' dep pname (head_of (HOLogic.dest_Trueprop
+ (Logic.strip_imp_concl (hd clauses)))) modes mode
in (gr'', mk_qual_id module fun_id) end
| SOME _ =>
(add_edge (name, dep) gr, mk_qual_id module (get_const_id name gr));
-fun inductive_codegen thy defs gr dep module brack (Const ("op :", _) $ t $ u) =
- ((case mk_ind_call thy defs gr dep module (Term.no_dummy_patterns t) u false of
- NONE => NONE
- | SOME (gr', call_p) => SOME (gr', (if brack then parens else I)
- (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"])))
- handle TERM _ => mk_ind_call thy defs gr dep module t u true)
- | inductive_codegen thy defs gr dep module brack t = (case strip_comb t of
- (Const (s, _), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy)) s of
- NONE => list_of_indset thy defs gr dep module brack t
- | SOME eqns =>
- let
- val (_, (_, thyname)) = split_last eqns;
- val (gr', id) = mk_fun thy defs s (preprocess thy (map fst eqns))
- dep module (if_library thyname module) gr;
- val (gr'', ps) = foldl_map
- (invoke_codegen thy defs dep module true) (gr', ts);
- in SOME (gr'', mk_app brack (Pretty.str id) ps)
- end)
- | _ => NONE);
+fun inductive_codegen thy defs gr dep module brack t = (case strip_comb t of
+ (Const ("Collect", Type (_, [_, Type (_, [U])])), [u]) => (case strip_comb u of
+ (Const (s, T), ts) => (case (get_clauses thy s, get_assoc_code thy s T) of
+ (SOME (names, thyname, k, intrs), NONE) =>
+ let val (gr', call_p) = mk_ind_call thy defs gr dep module true
+ s T (ts @ [Term.dummy_pattern U]) names thyname k intrs
+ in SOME (gr', (if brack then parens else I) (Pretty.block
+ [Pretty.str "Seq.list_of", Pretty.brk 1, Pretty.str "(",
+ call_p, Pretty.str ")"]))
+ end
+ | _ => NONE)
+ | _ => NONE)
+ | (Const (s, T), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy)) s of
+ NONE => (case (get_clauses thy s, get_assoc_code thy s T) of
+ (SOME (names, thyname, k, intrs), NONE) =>
+ if length ts < k then NONE else SOME
+ (let val (gr', call_p) = mk_ind_call thy defs gr dep module false
+ s T (map Term.no_dummy_patterns ts) names thyname k intrs
+ in (gr', mk_funcomp brack "?!"
+ (length (binder_types T) - length ts) (parens call_p))
+ end handle TERM _ => mk_ind_call thy defs gr dep module true
+ s T ts names thyname k intrs)
+ | _ => NONE)
+ | SOME eqns =>
+ let
+ val (_, (_, thyname)) = split_last eqns;
+ val (gr', id) = mk_fun thy defs s (preprocess thy (map fst eqns))
+ dep module (if_library thyname module) gr;
+ val (gr'', ps) = foldl_map
+ (invoke_codegen thy defs dep module true) (gr', ts);
+ in SOME (gr'', mk_app brack (Pretty.str id) ps)
+ end)
+ | _ => NONE);
val setup =
add_codegen "inductive" inductive_codegen #>
CodegenData.init #>
- add_attribute "ind" (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add);
+ add_attribute "ind" (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
+ Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add);
end;
@@ -752,6 +681,8 @@
fun ?? b = if b then Seq.single () else Seq.empty;
+fun ??? f g = f o g;
+
fun ?! s = is_some (Seq.pull s);
fun equal__1 x = Seq.single x;
--- a/src/HOL/Tools/inductive_realizer.ML Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Feb 07 17:44:07 2007 +0100
@@ -15,51 +15,103 @@
structure InductiveRealizer : INDUCTIVE_REALIZER =
struct
+(* FIXME: LocalTheory.note should return theorems with proper names! *)
+fun name_of_thm thm = (case Proofterm.strip_combt (fst (Proofterm.strip_combP
+ (Proofterm.rewrite_proof (theory_of_thm thm) ([], []) (proof_of thm)))) of
+ (PThm (name, _, _, _), _) => name
+ | _ => error "name_of_thm: bad proof");
+
+(* infer order of variables in intro rules from order of quantifiers in elim rule *)
+fun infer_intro_vars elim arity intros =
+ let
+ val thy = theory_of_thm elim;
+ val _ :: cases = prems_of elim;
+ val used = map (fst o fst) (Term.add_vars (prop_of elim) []);
+ fun mtch (t, u) =
+ let
+ val params = Logic.strip_params t;
+ val vars = map (Var o apfst (rpair 0))
+ (Name.variant_list used (map fst params) ~~ map snd params);
+ val ts = map (curry subst_bounds (rev vars))
+ (List.drop (Logic.strip_assums_hyp t, arity));
+ val us = Logic.strip_imp_prems u;
+ val tab = fold (Pattern.first_order_match thy) (ts ~~ us)
+ (Vartab.empty, Vartab.empty);
+ in
+ map (Envir.subst_vars tab) vars
+ end
+ in
+ map (mtch o apsnd prop_of) (cases ~~ intros)
+ end;
+
+(* read off arities of inductive predicates from raw induction rule *)
+fun arities_of induct =
+ map (fn (_ $ t $ u) =>
+ (fst (dest_Const (head_of t)), length (snd (strip_comb u))))
+ (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
+
+(* read off parameters of inductive predicate from raw induction rule *)
+fun params_of induct =
+ let
+ val (_ $ t $ u :: _) =
+ HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
+ val (_, ts) = strip_comb t;
+ val (_, us) = strip_comb u
+ in
+ List.take (ts, length ts - length us)
+ end;
+
val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
fun prf_of thm =
let val {sign, prop, der = (_, prf), ...} = rep_thm thm
- in Reconstruct.reconstruct_proof sign prop prf end;
+ in Reconstruct.expand_proof sign [("", NONE)] (Reconstruct.reconstruct_proof sign prop prf) end; (* FIXME *)
fun forall_intr_prf (t, prf) =
let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
+fun forall_intr_term (t, u) =
+ let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
+ in all T $ Abs (a, T, abstract_over (t, u)) end;
+
fun subsets [] = [[]]
| subsets (x::xs) =
let val ys = subsets xs
in ys @ map (cons x) ys end;
-val set_of = fst o dest_Const o head_of o snd o HOLogic.dest_mem;
+val pred_of = fst o dest_Const o head_of;
-fun strip_all t =
- let
- fun strip used (Const ("all", _) $ Abs (s, T, t)) =
- let val s' = Name.variant used s
- in strip (s'::used) (subst_bound (Free (s', T), t)) end
- | strip used ((t as Const ("==>", _) $ P) $ Q) = t $ strip used Q
- | strip _ t = t;
- in strip (add_term_free_names (t, [])) t end;
+fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
+ let val (s', names') = (case names of
+ [] => (Name.variant used s, [])
+ | name :: names' => (name, names'))
+ in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
+ | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
+ t $ strip_all' used names Q
+ | strip_all' _ _ t = t;
+
+fun strip_all t = strip_all' (add_term_free_names (t, [])) [] t;
+
+fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
+ (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
+ | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
fun relevant_vars prop = foldr (fn
(Var ((a, i), T), vs) => (case strip_type T of
- (_, Type (s, _)) => if s mem ["bool", "set"] then (a, T) :: vs else vs
+ (_, Type (s, _)) => if s mem ["bool"] then (a, T) :: vs else vs
| _ => vs)
| (_, vs) => vs) [] (term_vars prop);
-fun params_of intr = map (fst o fst o dest_Var) (term_vars
- (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
- (Logic.strip_imp_concl intr)))));
-
-fun dt_of_intrs thy vs intrs =
+fun dt_of_intrs thy vs nparms intrs =
let
val iTs = term_tvars (prop_of (hd intrs));
val Tvs = map TVar iTs;
- val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
- val (Const (s, _), ts) = strip_comb S;
- val params = map dest_Var ts;
+ val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
+ (Logic.strip_imp_concl (prop_of (hd intrs))));
+ val params = map dest_Var (Library.take (nparms, ts));
val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
- fun constr_of_intr intr = (Sign.base_name (Thm.get_name intr),
+ fun constr_of_intr intr = (Sign.base_name (name_of_thm intr),
map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
filter_out (equal Extraction.nullT) (map
(Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
@@ -70,43 +122,40 @@
fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT);
-(** turn "P" into "%r x. realizes r (P x)" or "%r x. realizes r (x : P)" **)
+(** turn "P" into "%r x. realizes r (P x)" **)
fun gen_rvar vs (t as Var ((a, 0), T)) =
- let val U = TVar (("'" ^ a, 0), HOLogic.typeS)
- in case try HOLogic.dest_setT T of
- NONE => if body_type T <> HOLogic.boolT then t else
- let
- val Ts = binder_types T;
- val i = length Ts;
- val xs = map (pair "x") Ts;
- val u = list_comb (t, map Bound (i - 1 downto 0))
- in
- if a mem vs then
- list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
- else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
- end
- | SOME T' => if a mem vs then
- Abs ("r", U, Abs ("x", T', mk_rlz U $ Bound 1 $
- (HOLogic.mk_mem (Bound 0, t))))
- else Abs ("x", T', mk_rlz Extraction.nullT $ Extraction.nullt $
- (HOLogic.mk_mem (Bound 0, t)))
- end
+ if body_type T <> HOLogic.boolT then t else
+ let
+ val U = TVar (("'" ^ a, 0), HOLogic.typeS)
+ val Ts = binder_types T;
+ val i = length Ts;
+ val xs = map (pair "x") Ts;
+ val u = list_comb (t, map Bound (i - 1 downto 0))
+ in
+ if a mem vs then
+ list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
+ else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
+ end
| gen_rvar _ t = t;
-fun mk_realizes_eqn n vs intrs =
+fun mk_realizes_eqn n vs nparms intrs =
let
- val iTs = term_tvars (prop_of (hd intrs));
+ val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
+ val iTs = term_tvars concl;
val Tvs = map TVar iTs;
- val _ $ (_ $ _ $ S) = concl_of (hd intrs);
- val (Const (s, T), ts') = strip_comb S;
- val setT = body_type T;
- val elT = HOLogic.dest_setT setT;
- val x = Var (("x", 0), elT);
+ val (h as Const (s, T), us) = strip_comb concl;
+ val params = List.take (us, nparms);
+ val elTs = List.drop (binder_types T, nparms);
+ val predT = elTs ---> HOLogic.boolT;
+ val used = map (fst o fst o dest_Var) params;
+ val xs = map (Var o apfst (rpair 0))
+ (Name.variant_list used (replicate (length elTs) "x") ~~ elTs);
val rT = if n then Extraction.nullT
else Type (space_implode "_" (s ^ "T" :: vs),
map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT);
+ val S = list_comb (h, params @ xs);
val rvs = relevant_vars S;
val vs' = map fst rvs \\ vs;
val rname = space_implode "_" (s ^ "R" :: vs);
@@ -119,23 +168,20 @@
end;
val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
- val ts = map (gen_rvar vs) ts';
+ val ts = map (gen_rvar vs) params;
val argTs = map fastype_of ts;
- in ((prems, (Const ("typeof", setT --> Type ("Type", [])) $ S,
+ in ((prems, (Const ("typeof", HOLogic.boolT --> Type ("Type", [])) $ S,
Extraction.mk_typ rT)),
- (prems, (mk_rlz rT $ r $ HOLogic.mk_mem (x, S),
- if n then
- HOLogic.mk_mem (x, list_comb (Const (rname, argTs ---> setT), ts))
- else HOLogic.mk_mem (HOLogic.mk_prod (r, x), list_comb (Const (rname,
- argTs ---> HOLogic.mk_setT (HOLogic.mk_prodT (rT, elT))), ts)))))
+ (prems, (mk_rlz rT $ r $ S,
+ if n then list_comb (Const (rname, argTs ---> predT), ts @ xs)
+ else list_comb (Const (rname, argTs @ [rT] ---> predT), ts @ [r] @ xs))))
end;
-fun fun_of_prem thy rsets vs params rule intr =
+fun fun_of_prem thy rsets vs params rule ivs intr =
let
- (* add_term_vars and Term.add_vars may return variables in different order *)
- val args = map (Free o apfst fst o dest_Var)
- (add_term_vars (prop_of intr, []) \\ map Var params);
+ val ctxt = ProofContext.init thy
+ val args = map (Free o apfst fst o dest_Var) ivs;
val args' = map (Free o apfst fst)
(Term.add_vars (prop_of intr) [] \\ params);
val rule' = strip_all rule;
@@ -146,7 +192,9 @@
fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
| is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
- | is_meta (Const ("Trueprop", _) $ (Const ("op :", _) $ _ $ _)) = true
+ | is_meta (Const ("Trueprop", _) $ t) = (case head_of t of
+ Const (s, _) => can (InductivePackage.the_inductive ctxt) s
+ | _ => true)
| is_meta _ = false;
fun fun_of ts rts args used (prem :: prems) =
@@ -189,50 +237,42 @@
in if conclT = Extraction.nullT
then list_abs_free (map dest_Free xs, HOLogic.unit)
else list_abs_free (map dest_Free xs, list_comb
- (Free ("r" ^ Sign.base_name (Thm.get_name intr),
+ (Free ("r" ^ Sign.base_name (name_of_thm intr),
map fastype_of (rev args) ---> conclT), rev args))
end
in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end;
-fun find_first f = Library.find_first f;
-
fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
let
val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
val premss = List.mapPartial (fn (s, rs) => if s mem rsets then
- SOME (map (fn r => List.nth (prems_of raw_induct,
+ SOME (rs, map (fn (_, r) => List.nth (prems_of raw_induct,
find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss;
- val concls' = List.mapPartial (fn (s, _) => if s mem rsets then
- find_first (fn concl => s mem term_consts concl) concls
- else NONE) rss;
- val fs = List.concat (snd (foldl_map (fn (intrs, (prems, dummy)) =>
+ val fs = maps (fn ((intrs, prems), dummy) =>
let
- val (intrs1, intrs2) = chop (length prems) intrs;
- val fs = map (fn (rule, intr) =>
- fun_of_prem thy rsets vs params rule intr) (prems ~~ intrs1)
- in (intrs2, if dummy then Const ("arbitrary",
+ val fs = map (fn (rule, (ivs, intr)) =>
+ fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs)
+ in if dummy then Const ("arbitrary",
HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
- else fs)
- end) (intrs, (premss ~~ dummies))));
+ else fs
+ end) (premss ~~ dummies);
val frees = fold Term.add_frees fs [];
val Ts = map fastype_of fs;
- val rlzs = List.mapPartial (fn (a, concl) =>
+ fun name_of_fn intr = "r" ^ Sign.base_name (name_of_thm intr)
+ in
+ fst (fold_map (fn concl => fn names =>
let val T = Extraction.etype_of thy vs [] concl
- in if T = Extraction.nullT then NONE
- else SOME (list_comb (Const (a, Ts ---> T), fs))
- end) (rec_names ~~ concls')
- in if null rlzs then Extraction.nullt else
- let
- val r = foldr1 HOLogic.mk_prod rlzs;
- val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct)));
- fun name_of_fn intr = "r" ^ Sign.base_name (Thm.get_name intr);
- val r' = list_abs_free (List.mapPartial (fn intr =>
- Option.map (pair (name_of_fn intr)) (AList.lookup (op =) frees (name_of_fn intr))) intrs,
- if length concls = 1 then r $ x else r)
- in
- if length concls = 1 then lambda x r' else r'
- end
+ in if T = Extraction.nullT then (Extraction.nullt, names) else
+ let
+ val Type ("fun", [U, _]) = T;
+ val a :: names' = names
+ in (list_abs_free (("x", U) :: List.mapPartial (fn intr =>
+ Option.map (pair (name_of_fn intr))
+ (AList.lookup (op =) frees (name_of_fn intr))) intrs,
+ list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
+ end
+ end) concls rec_names)
end;
fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
@@ -254,48 +294,47 @@
|> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
end;
-fun mk_realizer thy vs params ((rule, rrule), rt) =
+fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
let
- val prems = prems_of rule ~~ prems_of rrule;
val rvs = map fst (relevant_vars (prop_of rule));
val xs = rev (Term.add_vars (prop_of rule) []);
val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
val rlzvs = rev (Term.add_vars (prop_of rrule) []);
val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
- val rs = subtract (op = o pairself fst) xs rlzvs;
-
- fun mk_prf _ [] prf = prf
- | mk_prf rs ((prem, rprem) :: prems) prf =
- if Extraction.etype_of thy vs [] prem = Extraction.nullT
- then AbsP ("H", SOME rprem, mk_prf rs prems prf)
- else forall_intr_prf (Var (hd rs), AbsP ("H", SOME rprem,
- mk_prf (tl rs) prems prf));
-
- in (Thm.get_name rule, (vs,
+ val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
+ val rlz' = foldr forall_intr_term (prop_of rrule) (vs2 @ rs);
+ val rlz'' = foldr forall_intr_term rlz vs2
+ in (name, (vs,
if rt = Extraction.nullt then rt else
foldr (uncurry lambda) rt vs1,
- foldr forall_intr_prf (mk_prf rs prems (Proofterm.proof_combP
- (prf_of rrule, map PBound (length prems - 1 downto 0)))) vs2))
+ ProofRewriteRules.un_hhf_proof rlz' rlz''
+ (foldr forall_intr_prf (prf_of rrule) (vs2 @ rs))))
end;
-fun add_rule r rss =
+fun partition_rules induct intrs =
let
- val _ $ (_ $ _ $ S) = concl_of r;
- val (Const (s, _), _) = strip_comb S;
+ fun name_of t = fst (dest_Const (head_of t));
+ val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
+ val sets = map (name_of o fst o HOLogic.dest_imp) ts;
in
- rss
- |> AList.default (op =) (s, [])
- |> AList.map_entry (op =) s (fn rs => rs @ [r])
+ map (fn s => (s, filter
+ (equal s o name_of o HOLogic.dest_Trueprop o concl_of) intrs)) sets
end;
fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
let
+ val qualifier = NameSpace.qualifier (name_of_thm induct);
+ val inducts = PureThy.get_thms thy (Name
+ (NameSpace.qualified qualifier "inducts"));
val iTs = term_tvars (prop_of (hd intrs));
val ar = length vs + length iTs;
- val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
- val (_, params) = strip_comb S;
+ val params = params_of raw_induct;
+ val arities = arities_of raw_induct;
+ val nparms = length params;
val params' = map dest_Var params;
- val rss = [] |> fold add_rule intrs;
+ val rss = partition_rules raw_induct intrs;
+ val rss' = map (fn (((s, rs), (_, arity)), elim) =>
+ (s, (infer_intro_vars elim arity rs ~~ rs))) (rss ~~ arities ~~ elims);
val (prfx, _) = split_last (NameSpace.explode (fst (hd rss)));
val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
@@ -303,7 +342,7 @@
Theory.root_path |>
Theory.add_path (NameSpace.implode prfx);
val (ty_eqs, rlz_eqs) = split_list
- (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
+ (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss);
val thy1' = thy1 |>
Theory.copy |>
@@ -312,7 +351,7 @@
(s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
Extraction.add_typeof_eqns_i ty_eqs;
val dts = List.mapPartial (fn (s, rs) => if s mem rsets then
- SOME (dt_of_intrs thy1' vs rs) else NONE) rss;
+ SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
(** datatype representing computational content of inductive set **)
@@ -338,51 +377,89 @@
((get #rec_thms dt_info, dummies), rss);
val rintrs = map (fn (intr, c) => Envir.eta_contract
(Extraction.realizes_of thy2 vs
- c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var)
- (rev (Term.add_vars (prop_of intr) []) \\ params')) intr))))
- (intrs ~~ List.concat constrss);
- val rlzsets = distinct (op =) (map (fn rintr => snd (HOLogic.dest_mem
- (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)))) rintrs);
+ (if c = Extraction.nullt then c else list_comb (c, map Var (rev
+ (Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
+ (maps snd rss ~~ List.concat constrss);
+ val (rlzpreds, rlzpreds') = split_list
+ (distinct (op = o pairself (#1 o #1)) (map (fn rintr =>
+ let
+ val Const (s, T) = head_of (HOLogic.dest_Trueprop
+ (Logic.strip_assums_concl rintr));
+ val s' = Sign.base_name s;
+ val T' = Logic.unvarifyT T
+ in ((s', SOME T', NoSyn),
+ (Const (s, T'), Free (s', T')))
+ end) rintrs));
+ val rlzparams = map (fn Var ((s, _), T) => (s, SOME (Logic.unvarifyT T)))
+ (List.take (snd (strip_comb
+ (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
(** realizability predicate **)
- val (thy3', ind_info) = thy2 |>
- OldInductivePackage.add_inductive_i false true "" false false false
- (map Logic.unvarify rlzsets) (map (fn (rintr, intr) =>
- ((Sign.base_name (Thm.get_name intr), strip_all
- (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>>
+ val (ind_info, thy3') = thy2 |>
+ TheoryTarget.init NONE |>
+ InductivePackage.add_inductive_i false "" false false false
+ rlzpreds rlzparams (map (fn (rintr, intr) =>
+ ((Sign.base_name (name_of_thm intr), []),
+ subst_atomic rlzpreds' (Logic.unvarify rintr)))
+ (rintrs ~~ maps snd rss)) [] ||>
+ ProofContext.theory_of o LocalTheory.exit ||>
Theory.absolute_path;
val thy3 = PureThy.hide_thms false
- (map Thm.get_name (#intrs ind_info)) thy3';
+ (map name_of_thm (#intrs ind_info)) thy3';
(** realizer for induction rule **)
- val Ps = List.mapPartial (fn _ $ M $ P => if set_of M mem rsets then
+ val Ps = List.mapPartial (fn _ $ M $ P => if pred_of M mem rsets then
SOME (fst (fst (dest_Var (head_of P)))) else NONE)
(HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
fun add_ind_realizer (thy, Ps) =
let
- val r = indrule_realizer thy induct raw_induct rsets params'
- (vs @ Ps) rec_names rss intrs dummies;
- val rlz = strip_all (Logic.unvarify
- (Extraction.realizes_of thy (vs @ Ps) r (prop_of induct)));
+ val rs = indrule_realizer thy induct raw_induct rsets params'
+ (vs @ Ps) rec_names rss' intrs dummies;
+ val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs @ Ps) r
+ (prop_of ind)) (rs ~~ inducts);
+ val used = foldr add_term_free_names [] rlzs;
+ val rnames = Name.variant_list used (replicate (length inducts) "r");
+ val rnames' = Name.variant_list
+ (used @ rnames) (replicate (length intrs) "s");
+ val rlzs' as (prems, _, _) :: _ = map (fn (rlz, name) =>
+ let
+ val (P, Q) = strip_one name (Logic.unvarify rlz);
+ val Q' = strip_all' [] rnames' Q
+ in
+ (Logic.strip_imp_prems Q', P, Logic.strip_imp_concl Q')
+ end) (rlzs ~~ rnames);
+ val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
+ (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
val rews = map mk_meta_eq
(fst_conv :: snd_conv :: get #rec_thms dt_info);
- val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
- [if length rss = 1 then
- cut_facts_tac [hd prems] 1 THEN etac (#induct ind_info) 1
- else EVERY [rewrite_goals_tac (rews @ all_simps),
- REPEAT (rtac allI 1), rtac (#induct ind_info) 1],
+ val thm = Goal.prove_global thy [] prems concl (fn prems => EVERY
+ [rtac (#raw_induct ind_info) 1,
rewrite_goals_tac rews,
REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
[K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
val (thm', thy') = PureThy.store_thm ((space_implode "_"
- (Thm.get_name induct :: vs @ Ps @ ["correctness"]), thm), []) thy
+ (NameSpace.qualified qualifier "induct" :: vs @ Ps @
+ ["correctness"]), thm), []) thy;
+ val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
+ (DatatypeAux.split_conj_thm thm');
+ val ([thms'], thy'') = PureThy.add_thmss
+ [((space_implode "_"
+ (NameSpace.qualified qualifier "inducts" :: vs @ Ps @
+ ["correctness"]), thms), [])] thy';
+ val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
in
Extraction.add_realizers_i
- [mk_realizer thy' (vs @ Ps) params' ((induct, thm'), r)] thy'
+ (map (fn (((ind, corr), rlz), r) =>
+ mk_realizer thy' (vs @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
+ realizers @ (case realizers of
+ [(((ind, corr), rlz), r)] =>
+ [mk_realizer thy' (vs @ Ps) (NameSpace.qualified qualifier "induct",
+ ind, corr, rlz, r)]
+ | _ => [])) thy''
end;
(** realizer for elimination rules **)
@@ -394,15 +471,13 @@
(((((elim, elimR), intrs), case_thms), case_name), dummy) thy =
let
val (prem :: prems) = prems_of elim;
- fun reorder1 (p, intr) =
+ fun reorder1 (p, (_, intr)) =
Library.foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t)
(strip_all p, Term.add_vars (prop_of intr) [] \\ params');
- fun reorder2 (intr, i) =
- let
- val fs1 = term_vars (prop_of intr) \\ params;
- val fs2 = Term.add_vars (prop_of intr) [] \\ params'
+ fun reorder2 ((ivs, intr), i) =
+ let val fs = Term.add_vars (prop_of intr) [] \\ params'
in Library.foldl (fn (t, x) => lambda (Var x) t)
- (list_comb (Bound (i + length fs1), fs1), fs2)
+ (list_comb (Bound (i + length ivs), ivs), fs)
end;
val p = Logic.list_implies
(map reorder1 (prems ~~ intrs) @ [prem], concl_of elim);
@@ -416,37 +491,36 @@
else []) @
map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
[Bound (length prems)]));
- val rlz = strip_all (Logic.unvarify
- (Extraction.realizes_of thy (vs @ Ps) r (prop_of elim)));
+ val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
+ val rlz' = strip_all (Logic.unvarify rlz);
val rews = map mk_meta_eq case_thms;
- val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
+ val thm = Goal.prove_global thy []
+ (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn prems => EVERY
[cut_facts_tac [hd prems] 1,
etac elimR 1,
- ALLGOALS (EVERY' [etac Pair_inject, asm_simp_tac HOL_basic_ss]),
+ ALLGOALS (asm_simp_tac HOL_basic_ss),
rewrite_goals_tac rews,
REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
val (thm', thy') = PureThy.store_thm ((space_implode "_"
- (Thm.get_name elim :: vs @ Ps @ ["correctness"]), thm), []) thy
+ (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
in
Extraction.add_realizers_i
- [mk_realizer thy' (vs @ Ps) params' ((elim, thm'), r)] thy'
+ [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
end;
(** add realizers to theory **)
- val rintr_thms = List.concat (map (fn (_, rs) => map (fn r => List.nth
- (#intrs ind_info, find_index (fn th => eq_thm (th, r)) intrs)) rs) rss);
val thy4 = Library.foldl add_ind_realizer (thy3, subsets Ps);
val thy5 = Extraction.add_realizers_i
- (map (mk_realizer thy4 vs params')
- (map (fn ((rule, rrule), c) => ((rule, rrule), list_comb (c,
- map Var (rev (Term.add_vars (prop_of rule) []) \\ params'))))
- (List.concat (map snd rss) ~~ rintr_thms ~~ List.concat constrss))) thy4;
- val elimps = List.mapPartial (fn (s, intrs) => if s mem rsets then
- Option.map (rpair intrs) (find_first (fn (thm, _) =>
- s mem term_consts (hd (prems_of thm))) (elims ~~ #elims ind_info))
- else NONE) rss;
+ (map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
+ (name_of_thm rule, rule, rrule, rlz,
+ list_comb (c, map Var (rev (Term.add_vars (prop_of rule) []) \\ params'))))
+ (List.concat (map snd rss) ~~ #intrs ind_info ~~ rintrs ~~
+ List.concat constrss))) thy4;
+ val elimps = List.mapPartial (fn ((s, intrs), p) =>
+ if s mem rsets then SOME (p, intrs) else NONE)
+ (rss' ~~ (elims ~~ #elims ind_info));
val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
(HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
@@ -457,12 +531,9 @@
fun add_ind_realizers name rsets thy =
let
val (_, {intrs, induct, raw_induct, elims, ...}) =
- (case OldInductivePackage.get_inductive thy name of
- NONE => error ("Unknown inductive set " ^ quote name)
- | SOME info => info);
- val _ $ (_ $ _ $ S) = concl_of (hd intrs);
+ InductivePackage.the_inductive (ProofContext.init thy) name;
val vss = sort (int_ord o pairself length)
- (subsets (map fst (relevant_vars S)))
+ (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
in
Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
end
@@ -472,8 +543,8 @@
fun err () = error "ind_realizer: bad rule";
val sets =
(case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
- [_] => [set_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
- | xs => map (set_of o fst o HOLogic.dest_imp) xs)
+ [_] => [pred_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
+ | xs => map (pred_of o fst o HOLogic.dest_imp) xs)
handle TERM _ => err () | Empty => err ();
in
add_ind_realizers (hd sets)