--- a/src/HOL/Bali/AxCompl.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Bali/AxCompl.thy Tue Sep 09 20:51:36 2014 +0200
@@ -1027,7 +1027,7 @@
"G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}" and
"G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" and
"G,A\<turnstile>{=:n} \<langle>es\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
- proof (induct rule: var_expr_stmt.inducts)
+ proof (induct rule: compat_var.induct compat_expr.induct compat_stmt.induct compat_expr_list.induct)
case (LVar v)
show "G,A\<turnstile>{=:n} \<langle>LVar v\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
apply (rule MGFn_NormalI)
@@ -1318,7 +1318,7 @@
show "G,A\<turnstile>{=:n} \<langle>Init C\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
by (rule MGFn_Init)
next
- case Nil_expr
+ case Nil
show "G,A\<turnstile>{=:n} \<langle>[]\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
apply -
apply (rule MGFn_NormalI)
@@ -1326,7 +1326,7 @@
apply (fastforce intro: eval.Nil)
done
next
- case (Cons_expr e es)
+ case (Cons e es)
thus "G,A\<turnstile>{=:n} \<langle>e# es\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
apply -
apply (rule MGFn_NormalI)
--- a/src/HOL/Bali/DefiniteAssignment.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Tue Sep 09 20:51:36 2014 +0200
@@ -236,8 +236,8 @@
\<Longrightarrow> P (b? e1 : e2)"
shows "P e"
proof -
- have "True" and "\<And> v. constVal e = Some v \<Longrightarrow> P e" and "True" and "True"
- proof (induct "x::var" and e and "s::stmt" and "es::expr list")
+ have "\<And> v. constVal e = Some v \<Longrightarrow> P e"
+ proof (induct e)
case Lit
show ?case by (rule hyp_Lit)
next
@@ -264,7 +264,7 @@
with Cond show ?thesis using v bv
by (auto intro: hyp_CondR)
qed
- qed (simp_all)
+ qed (simp_all add: hyp_Lit)
with const
show ?thesis
by blast
@@ -334,8 +334,8 @@
assumes boolConst: "constVal e = Some (Bool b)" (is "?Const b e")
shows "assigns_if b e = {}" (is "?Ass b e")
proof -
- have "True" and "\<And> b. ?Const b e \<Longrightarrow> ?Ass b e" and "True" and "True"
- proof (induct _ and e and _ and _ rule: var_expr_stmt.inducts)
+ have "\<And> b. ?Const b e \<Longrightarrow> ?Ass b e"
+ proof (induct e)
case Lit
thus ?case by simp
next
@@ -382,8 +382,8 @@
assumes boolConst: "constVal e = Some (Bool b)" (is "?Const b e")
shows "assigns_if (\<not>b) e = UNIV" (is "?Ass b e")
proof -
- have True and "\<And> b. ?Const b e \<Longrightarrow> ?Ass b e" and True and True
- proof (induct _ and e and _ and _ rule: var_expr_stmt.inducts)
+ have "\<And> b. ?Const b e \<Longrightarrow> ?Ass b e"
+ proof (induct e)
case Lit
thus ?case by simp
next
@@ -949,8 +949,10 @@
assumes boolEx: "E\<turnstile>e\<Colon>-PrimT Boolean" (is "?Boolean e")
shows "assignsE e \<subseteq> assigns_if True e \<inter> assigns_if False e" (is "?Incl e")
proof -
- have True and "?Boolean e \<Longrightarrow> ?Incl e" and True and True
- proof (induct _ and e and _ and _ rule: var_expr_stmt.inducts)
+ obtain vv where ex_lit: "E\<turnstile>Lit vv\<Colon>- PrimT Boolean"
+ using typeof.simps(2) wt.Lit by blast
+ have "?Boolean e \<Longrightarrow> ?Incl e"
+ proof (induct e)
case (Cast T e)
have "E\<turnstile>e\<Colon>- (PrimT Boolean)"
proof -
@@ -1011,7 +1013,10 @@
with Some show ?thesis using hyp_e2 boolean_e2 by auto
qed
qed
- qed simp_all
+ next
+ show "\<And>x. E\<turnstile>Lit vv\<Colon>-PrimT Boolean"
+ by (rule ex_lit)
+ qed (simp_all add: ex_lit)
with boolEx
show ?thesis
by blast
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Tue Sep 09 20:51:36 2014 +0200
@@ -102,8 +102,7 @@
proof -
have True and True and
"\<And> jmps' jmps. \<lbrakk>jumpNestingOkS jmps' c; jmps' \<subseteq> jmps\<rbrakk> \<Longrightarrow> jumpNestingOkS jmps c"
- and True
- proof (induct rule: var_expr_stmt.inducts)
+ proof (induct rule: var.induct expr.induct stmt.induct)
case (Lab j c jmps' jmps)
note jmpOk = `jumpNestingOkS jmps' (j\<bullet> c)`
note jmps = `jmps' \<subseteq> jmps`
@@ -2008,8 +2007,8 @@
have True and
"\<And> c v s0 s. \<lbrakk> constVal e = Some c; G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s\<rbrakk>
\<Longrightarrow> v = c \<and> normal s"
- and True and True
- proof (induct rule: var_expr_stmt.inducts)
+ and True
+ proof (induct rule: var.induct expr.induct stmt.induct)
case NewC hence False by simp thus ?case ..
next
case NewA hence False by simp thus ?case ..
@@ -2156,8 +2155,8 @@
have True and
"\<And> c. \<lbrakk>constVal e = Some c;Env\<turnstile>e\<Colon>-PrimT Boolean\<rbrakk>
\<Longrightarrow> typeof empty_dt c = Some (PrimT Boolean)"
- and True and True
- proof (induct rule: var_expr_stmt.inducts)
+ and True
+ proof (induct rule: var.induct expr.induct stmt.induct)
case NewC hence False by simp thus ?case ..
next
case NewA hence False by simp thus ?case ..
--- a/src/HOL/Bali/Eval.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Bali/Eval.thy Tue Sep 09 20:51:36 2014 +0200
@@ -833,7 +833,7 @@
apply (erule eval_cases)
apply auto
apply (induct_tac "t")
-apply (induct_tac "a")
+apply (rename_tac a, induct_tac "a")
apply auto
done
--- a/src/HOL/Bali/Evaln.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Bali/Evaln.thy Tue Sep 09 20:51:36 2014 +0200
@@ -245,7 +245,7 @@
| In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
apply (erule evaln_cases , auto)
apply (induct_tac "t")
-apply (induct_tac "a")
+apply (rename_tac a, induct_tac "a")
apply auto
done
--- a/src/HOL/Bali/Term.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Bali/Term.thy Tue Sep 09 20:51:36 2014 +0200
@@ -217,6 +217,8 @@
--{* technical term for smallstep sem.) *}
| Init qtname --{* class initialization *}
+datatype_compat var expr stmt
+
text {*
The expressions Methd and Body are artificial program constructs, in the
@@ -421,7 +423,7 @@
\<lbrakk>\<And> v. P \<langle>v\<rangle>\<^sub>v; \<And> e. P \<langle>e\<rangle>\<^sub>e;\<And> c. P \<langle>c\<rangle>\<^sub>s;\<And> l. P \<langle>l\<rangle>\<^sub>l\<rbrakk>
\<Longrightarrow> P t"
apply (cases t)
- apply (case_tac a)
+ apply (rename_tac a, case_tac a)
apply auto
done