src/HOL/Bali/Trans.thy
changeset 13354 8c8eafb63746
parent 13337 f75dfc606ac7
child 13384 a34e38154413
equal deleted inserted replaced
13353:1800e7134d2e 13354:8c8eafb63746
     8 
     8 
     9 PRELIMINARY!!!!!!!!
     9 PRELIMINARY!!!!!!!!
    10 *)
    10 *)
    11 
    11 
    12 theory Trans = Evaln:
    12 theory Trans = Evaln:
    13 (*
    13 
    14 constdefs inj_stmt:: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 83)
       
    15     "\<langle>s\<rangle>\<^sub>s \<equiv> In1r s"
       
    16 
       
    17 constdefs inj_expr:: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 83)
       
    18     "\<langle>e\<rangle>\<^sub>e \<equiv> In1l e"
       
    19 *)
       
    20 axclass inj_term < "type"
       
    21 consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83)
       
    22 
       
    23 instance stmt::inj_term ..
       
    24 
       
    25 defs (overloaded)
       
    26 stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
       
    27 
       
    28 lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
       
    29 by (simp add: stmt_inj_term_def)
       
    30 
       
    31 instance expr::inj_term ..
       
    32 
       
    33 defs (overloaded)
       
    34 expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
       
    35 
       
    36 lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
       
    37 by (simp add: expr_inj_term_def)
       
    38 
       
    39 instance var::inj_term ..
       
    40 
       
    41 defs (overloaded)
       
    42 var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
       
    43 
       
    44 lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
       
    45 by (simp add: var_inj_term_def)
       
    46 
       
    47 instance "list":: (type) inj_term ..
       
    48 
       
    49 defs (overloaded)
       
    50 expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
       
    51 
       
    52 lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
       
    53 by (simp add: expr_list_inj_term_def)
       
    54 
    14 
    55 constdefs groundVar:: "var \<Rightarrow> bool"
    15 constdefs groundVar:: "var \<Rightarrow> bool"
    56 "groundVar v \<equiv> (case v of
    16 "groundVar v \<equiv> (case v of
    57                    LVar ln \<Rightarrow> True
    17                    LVar ln \<Rightarrow> True
    58                  | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
    18                  | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a