src/HOL/MicroJava/BV/Altern.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 14981 e73f8140af78
child 16417 9bc16273c2d4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 (*  Title:      HOL/MicroJava/BV/Altern.thy
     2     ID:         $Id$
     3     Author:     Martin Strecker
     4 *)
     5 
     6 
     7 (* Alternative definition of well-typing of bytecode, 
     8    used in compiler type correctness proof *)
     9 
    10 
    11 theory Altern = BVSpec:
    12 
    13 
    14 constdefs
    15   check_type :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool"
    16   "check_type G mxs mxr s \<equiv> s \<in> states G mxs mxr"
    17 
    18   wt_instr_altern :: "[instr,jvm_prog,ty,method_type,nat,nat,p_count,
    19                 exception_table,p_count] \<Rightarrow> bool"
    20   "wt_instr_altern i G rT phi mxs mxr max_pc et pc \<equiv>
    21   app i G mxs rT pc et (phi!pc) \<and>
    22   check_type G mxs mxr (OK (phi!pc)) \<and>
    23   (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
    24 
    25   wt_method_altern :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
    26                  exception_table,method_type] \<Rightarrow> bool"
    27   "wt_method_altern G C pTs rT mxs mxl ins et phi \<equiv>
    28   let max_pc = length ins in
    29   0 < max_pc \<and> 
    30   length phi = length ins \<and>
    31   check_bounded ins et \<and> 
    32   wt_start G C pTs mxl phi \<and>
    33   (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr_altern (ins!pc) G rT phi mxs (1+length pTs+mxl) max_pc et pc)"
    34 
    35 
    36 lemma wt_method_wt_method_altern : 
    37   "wt_method G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method_altern G C pTs rT mxs mxl ins et phi"
    38 apply (simp add: wt_method_def wt_method_altern_def)
    39 apply (intro strip)
    40 apply clarify
    41 apply (drule spec, drule mp, assumption)
    42 apply (simp add: check_types_def wt_instr_def wt_instr_altern_def check_type_def)
    43 apply (auto  intro: imageI)
    44 done
    45 
    46 
    47 lemma check_type_check_types [rule_format]: 
    48   "(\<forall>pc. pc < length phi \<longrightarrow> check_type G mxs mxr (OK (phi ! pc)))
    49   \<longrightarrow> check_types G mxs mxr (map OK phi)"
    50 apply (induct phi)
    51 apply (simp add: check_types_def)
    52 apply (simp add: check_types_def)
    53 apply clarify
    54 apply (frule_tac x=0 in spec)
    55 apply (simp add: check_type_def)
    56 apply auto
    57 done
    58 
    59 lemma wt_method_altern_wt_method [rule_format]: 
    60   "wt_method_altern G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method G C pTs rT mxs mxl ins et phi"
    61 apply (simp add: wt_method_def wt_method_altern_def)
    62 apply (intro strip)
    63 apply clarify
    64 apply (rule conjI)
    65   (* show check_types *)
    66 apply (rule check_type_check_types)
    67 apply (simp add: wt_instr_altern_def)
    68 
    69   (* show wt_instr *)
    70 apply (intro strip)
    71 apply (drule spec, drule mp, assumption)
    72 apply (simp add: wt_instr_def wt_instr_altern_def)
    73 done
    74 
    75 
    76 end