src/HOL/MicroJava/BV/Convert.ML

minor adjustments in branch and method invocation for completeness of LBV

(*  Title:      HOL/MicroJava/BV/Convert.ML
    ID:         $Id$
    Author:     Cornelia Pusch
    Copyright   1999 Technische Universitaet Muenchen
*)


Goalw[sup_ty_opt_def] "G \\<turnstile> t <=o t";
by (exhaust_tac "t" 1);
by Auto_tac;
qed "sup_ty_opt_refl";
Addsimps [sup_ty_opt_refl];

Goalw[sup_loc_def] "G \\<turnstile> t <=l t";
by (induct_tac "t" 1);
by Auto_tac;
qed "sup_loc_refl";
Addsimps [sup_loc_refl];

Goalw[sup_state_def] "G \\<turnstile> s <=s s";
by Auto_tac;
qed "sup_state_refl";
Addsimps [sup_state_refl];

val widen_PrimT_conv1 =
 prove_typerel "(G \\<turnstile> PrimT x \\<preceq> T) = (T = PrimT x)"
 [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = PrimT x"];
Addsimps [widen_PrimT_conv1];

Goalw [sup_ty_opt_def] "(G \\<turnstile> None <=o any) = (any = None)";
by(simp_tac (simpset() addsplits [option.split]) 1);
qed "anyConvNone";
Addsimps [anyConvNone];

Goalw [sup_ty_opt_def] "(G \\<turnstile> Some ty' <=o Some ty) = (G \\<turnstile> ty' \\<preceq> ty)";
by(Simp_tac 1);
qed "SomeanyConvSome";
Addsimps [SomeanyConvSome];

Goal
"(G \\<turnstile> Some(PrimT Integer) <=o X) = (X=None \\<or> (X=Some(PrimT Integer)))";
by (simp_tac (simpset() setloop (split_tac [ty.split,option.split]) addsimps [sup_ty_opt_def]) 1);
qed "sup_PTS_eq";



Goalw [sup_loc_def] "CFS \\<turnstile> [] <=l XT = (XT=[])";
by(Simp_tac 1);
qed "sup_loc_Nil";
AddIffs [sup_loc_Nil];


Goalw [sup_loc_def]
"CFS \\<turnstile> (Y#YT) <=l XT = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> Y <=o X \\<and> CFS \\<turnstile> YT <=l XT')";
by(simp_tac (simpset() addsimps [list_all2_Cons1]) 1);
qed "sup_loc_Cons";
AddIffs [sup_loc_Cons];