# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID b13e5c3497f588c38980c23c3474742d21f63dc9
# Parent  bf4188deabb20e091f7c8e19baaff2f1930d9b4e
ported Bali to new datatypes

diff -r bf4188deabb2 -r b13e5c3497f5 src/HOL/Bali/AxCompl.thy
--- 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)
diff -r bf4188deabb2 -r b13e5c3497f5 src/HOL/Bali/DefiniteAssignment.thy
--- 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
diff -r bf4188deabb2 -r b13e5c3497f5 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- 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 ..
diff -r bf4188deabb2 -r b13e5c3497f5 src/HOL/Bali/Eval.thy
--- 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
 
diff -r bf4188deabb2 -r b13e5c3497f5 src/HOL/Bali/Evaln.thy
--- 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
 
diff -r bf4188deabb2 -r b13e5c3497f5 src/HOL/Bali/Term.thy
--- 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