File TypeRel.ML

open TypeRel;

Goalw [implmt1_def]
"\<And>G. G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>(sc,is,rest)\<in>class G C: I\<in>set is)";
b y Auto_tac;
qed "implmt1D";

qed_goal "implmtD" thy "\<And>G. G\<turnstile>C\<leadsto>J \<Longrightarrow> (\<exists>I. G\<turnstile>C\<leadsto>1I \<and> G\<turnstile>I\<preceq>I J) \<or> \
\ (\<exists>D. G\<turnstile>C\<prec>C1D \<and> G\<turnstile>D\<leadsto>J)" (K [
	etac implmt.induct 1,
	 ALLGOALS Fast_tac]);


bind_thm ("subcls_direct", subcls1I RS r_into_rtrancl);

Goal "\<lbrakk>is_class G C; ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>C\<preceq>C Object";
b y eatac ws_subcls1_induct 1 1;
b y Clarsimp_tac 1;
b y case_tac "C = Object" 1;
b y  ALLGOALS (fast_tac (claset() addIs [r_into_rtrancl RS rtrancl_trans]));
qed "subcls_ObjectI";

Goal "G\<turnstile>Object\<preceq>C C \<Longrightarrow> C = Object";
b y etac rtrancl_induct 1;
b y  Auto_tac;
b y dtac subcls1D 1;
b y Auto_tac;
qed "subcls_ObjectD";
AddSDs[subcls_ObjectD];

Goal "G\<turnstile>Object\<leadsto>I \<Longrightarrow> R";
b y    auto_tac (claset() addSDs [implmtD, implmt1D,subcls1D], simpset());
qed "implmt_ObjectE";
AddSEs[implmt_ObjectE];


fun prove_typerel_lemma drules indrule s = prove_goal thy s (fn prems => [
	rtac (hd prems RS indrule) 1, (* sic! *)
	auto_tac (claset() addDs drules, simpset())]);

fun qed_typerel n s lemmata = qed_goal n thy s (fn prems => [
	cut_facts_tac prems 1, (* sic! *)
	auto_tac (claset() addDs lemmata, simpset())]);


Goal "G\<turnstile>A\<preceq>C B \<Longrightarrow> G\<turnstile>B\<leadsto>K \<longrightarrow> G\<turnstile>A\<leadsto>K";
b y etac rtrancl_induct 1;
b y  Auto_tac;
b y fast_tac (claset() addIs [implmt.subcls1]) 1;
qed_spec_mp "subcls_implmt";

bind_thm ("implmt_subint2", prove_typerel_lemma  
		[implmt.subint, rtrancl_trans, implmt.subcls1] implmt.induct 
			"G\<turnstile>A\<leadsto>J \<Longrightarrow> G\<turnstile>J\<preceq>I K \<longrightarrow> G\<turnstile>A\<leadsto>K" RS mp);

qed_goal "implmt_is_class" thy 
     "\<And>X. G\<turnstile>C\<leadsto>I \<Longrightarrow> is_class G C" (K [
	etac implmt.induct 1,
	  ALLGOALS (fast_tac (claset() addDs [implmt1D,subcls1D]))]);


section "widen";

AddSIs [widen.refl];
Addsimps (widen.refl::tl widen.intrs);

Goal  "\<lbrakk>class G (SXcpt xn) = Some (if xn = Throwable then ?Object else \
\ SXcpt Throwable, rest)\<rbrakk> \<Longrightarrow> G\<turnstile>SXcpt xn\<preceq>C SXcpt Throwable";
b y case_tac "xn = Throwable" 1;
b y  ALLGOALS Asm_full_simp_tac;
b y etac subcls_direct 1;
b y Simp_tac 1;
qed "SXcpt_subcls_Throwable_lemma";

val prove_widen_lemma = prove_typerel_lemma [] widen.elim;


(* too strong in general
qed_typerel "widen_PrimT" "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x"
 [ prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> S = PrimT x \<longrightarrow> T = PrimT x"];

qed_typerel "widen_PrimT2" "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x"
 [ prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> T = PrimT x \<longrightarrow> S = PrimT x"];
*)

qed_typerel "widen_PrimT" "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> \<exists>y. T = PrimT y"
 [ prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> S = PrimT x \<longrightarrow> (\<exists>y. T = PrimT y)"];

qed_typerel "widen_PrimT2" "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> \<exists>y. S = PrimT y"
 [ prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> T = PrimT x \<longrightarrow> (\<exists>y. S = PrimT y)"];


qed_typerel "widen_RefT" "G\<turnstile>RefT R\<preceq>T \<Longrightarrow> \<exists>t. T=RefT t" 
	[prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> S=RefT R \<longrightarrow> (\<exists>t. T=RefT t)"];

qed_typerel "widen_RefT2" "G\<turnstile>S\<preceq>RefT R \<Longrightarrow> \<exists>t. S=RefT t" 
	[prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> T=RefT R \<longrightarrow> (\<exists>t. S=RefT t)"];


qed_typerel "widen_Iface" 
	"G\<turnstile>Iface I\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>J. T=Iface J)"
[prove_widen_lemma 
"G\<turnstile>S\<preceq>T \<Longrightarrow> S = Iface I \<longrightarrow> T=Class Object \<or> (\<exists>J. T=Iface J)"];

qed_typerel "widen_Iface2" 
	"G\<turnstile>S\<preceq> Iface J \<Longrightarrow> S = NT \<or> (\<exists>I. S = Iface I) \<or> (\<exists>D. S = Class D) "
 [prove_widen_lemma 
   "G\<turnstile>S\<preceq>T \<Longrightarrow> T = Iface J \<longrightarrow> (S = NT \<or> (\<exists>I. S = Iface I))\<or> (\<exists>D. S = Class D)"];

qed_typerel "widen_Iface_Iface" "G\<turnstile>Iface I\<preceq> Iface J \<Longrightarrow> G\<turnstile>I\<preceq>I J"
 [ prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> S = Iface I \<longrightarrow> T = Iface J \<longrightarrow> G\<turnstile>I\<preceq>I J"];

Goal  "G\<turnstile>Iface I\<preceq> Iface J = G\<turnstile>I\<preceq>I J";
b y rtac iffI 1;
b y  etac widen_Iface_Iface 1;
b y etac widen.subint 1;
qed "widen_Iface_Iface_eq";
Addsimps[widen_Iface_Iface_eq];

qed_typerel "widen_Class" "G\<turnstile>Class C\<preceq>T \<Longrightarrow> \
\ (\<exists>D. T=Class D) \<or> (\<exists>I. T=Iface I)"
 [ prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> S = Class C \<longrightarrow> \
\ (\<exists>D. T=Class D) \<or> (\<exists>I. T=Iface I)"];

qed_typerel "widen_Class2" 
	"G\<turnstile>S\<preceq> Class C \<Longrightarrow> C = Object \<or> S = NT \<or> (\<exists>D. S = Class D)"
 [prove_widen_lemma 
	"G\<turnstile>S\<preceq>T \<Longrightarrow> T = Class C \<longrightarrow> (C = Object \<or> S = NT \<or> (\<exists>D. S = Class D))"];
qed_typerel "widen_Class_Class" "G\<turnstile>Class C\<preceq> Class cm \<Longrightarrow> G\<turnstile>C\<preceq>C cm"
[ prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> S = Class C \<longrightarrow> T = Class cm \<longrightarrow> G\<turnstile>C\<preceq>C cm"];

Goal  "G\<turnstile>Class C\<preceq> Class cm = G\<turnstile>C\<preceq>C cm";
b y rtac iffI 1;
b y  etac widen_Class_Class 1;
b y etac widen.subcls 1;
qed "widen_Class_Class_eq";
Addsimps[widen_Class_Class_eq];


qed_typerel "widen_Class_Iface" "G\<turnstile>Class C\<preceq> Iface I \<Longrightarrow> G\<turnstile>C\<leadsto>I"
 [ prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> S = Class C \<longrightarrow> T = Iface I \<longrightarrow> G\<turnstile>C\<leadsto>I"];

Goal  "G\<turnstile>Class C\<preceq> Iface I = G\<turnstile>C\<leadsto>I";
b y rtac iffI 1;
b y  etac widen_Class_Iface 1;
b y etac widen.implmt 1;
qed "widen_Class_Iface_eq";
Addsimps[widen_Class_Iface_eq];

qed_typerel "widen_Array" "G\<turnstile>S.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>T'. T=T'.[] \<and> G\<turnstile>S\<preceq>T')"
[ prove_widen_lemma 
  "G\<turnstile>S\<preceq>T \<Longrightarrow> S = S'.[] \<longrightarrow> T=Class Object \<or> (\<exists>T'. T=T'.[] \<and> G\<turnstile>S'\<preceq>T')"];

qed_typerel
"widen_Array2"            "G\<turnstile>S\<preceq>T.[] \<Longrightarrow> S = NT \<or> (\<exists>S'. S=S'.[] \<and> G\<turnstile>S'\<preceq>T)"
[ prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> T = T'.[] \<longrightarrow> S = NT \<or> (\<exists>S'. S=S'.[] \<and> G\<turnstile>S'\<preceq>T')"];

qed_typerel "widen_ArrayPrimT" "G\<turnstile>PrimT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> T=PrimT t.[]"
[ prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> S = PrimT t.[] \<longrightarrow> T=Class Object \<or> T=PrimT t.[]"];

qed_typerel
"widen_ArrayRefT"          "G\<turnstile>RefT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>s. T=RefT s.[] \<and> G\<turnstile>RefT t\<preceq>RefT s)"
[ prove_widen_lemma 
"G\<turnstile>S\<preceq>T \<Longrightarrow> S = RefT t.[] \<longrightarrow> T=Class Object \<or> (\<exists>s. T=RefT s.[] \<and> G\<turnstile>RefT t\<preceq>RefT s)"
];

qed_goal "widen_ArrayRefT_ArrayRefT_eq" thy 
	"G\<turnstile>RefT T.[]\<preceq>RefT T'.[] = G\<turnstile>RefT T\<preceq>RefT T'" (K [
	rtac iffI 1,
	 etac widen.array 2,
	dtac widen_ArrayRefT 1,
	Asm_full_simp_tac 1]);
Addsimps [widen_ArrayRefT_ArrayRefT_eq];

qed_goal "widen_Array_Array" thy "\<And>X. G\<turnstile>T.[]\<preceq>T'.[] \<Longrightarrow> G\<turnstile>T\<preceq>T'" (K [
	dtac widen_Array 1,
	Auto_tac]);

qed_typerel "widen_NT2" "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT"
 [prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> T = NT \<longrightarrow> S = NT"];

Goal "ws_prog G \<Longrightarrow> is_type G (RefT t) \<longrightarrow> G\<turnstile>RefT t\<preceq> Class Object";
b y EVERY'[rtac (ref_ty_ty.induct RS conjunct1), K Safe_tac, rtac widen.null] 1;
b y       Auto_tac;
b y case_tac "tname=Object" 1;
b y  Asm_simp_tac 1;
b y fast_tac (claset() addIs [widen.subcls,subcls_ObjectI]) 1;
qed_spec_mp "widen_RefT_ObjectI";
AddIs [widen_RefT_ObjectI];

Goal "\<lbrakk>G\<turnstile>S\<preceq>U; \<forall>C. is_class G C \<longrightarrow> G\<turnstile>C\<preceq>C Object\<rbrakk> \<Longrightarrow> \
\ \<forall>T. G\<turnstile>U\<preceq>T \<longrightarrow> G\<turnstile>S\<preceq>T";
b y etac widen.induct 1;
b y        Safe_tac;
b y       EVERY'[dtac widen_RefT, Clarsimp_tac] 5;
b y      ALLGOALS (forward_tac [widen_Class, widen_Iface, widen_Array]);
b y      Safe_tac;
b y            rtac widen.int_obj 1;
b y           EVERY'[dtac implmt_is_class, Asm_simp_tac] 6; (* using premise *)
b y          ALLGOALS (etac thin_rl);
b y          Asm_simp_tac 6;
b y          rtac widen.arr_obj 9;
b y         EVERY'[rotate_tac ~1, ftac widen_RefT] 9;
b y        auto_tac (claset() addSEs 
		[rtrancl_trans,subcls_implmt,implmt_subint2],simpset());
qed_spec_mp "widen_trans_lemma";


Goal "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T; ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T";
b y auto_tac (claset() addIs [widen_trans_lemma,subcls_ObjectI], simpset());
qed "ws_widen_trans";

Goal "\<lbrakk>G\<turnstile>S\<preceq>T; \
\\<forall>I J. G\<turnstile>I\<preceq>I J \<and> G\<turnstile>J\<preceq>I I \<longrightarrow> I = J; \
\\<forall>C D. G\<turnstile>C\<preceq>C D \<and> G\<turnstile>D\<preceq>C C \<longrightarrow> C = D; \
\\<forall>I  . G\<turnstile>Object\<leadsto>I        \<longrightarrow> False\<rbrakk> \<Longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T";
b y etac widen.induct 1;
b y auto_tac (claset() addDs [widen_Iface,widen_NT2,widen_Class], simpset());
qed_spec_mp "widen_antisym_lemma";

bind_thm ("subint_antisym", subint1_acyclic RS acyclic_impl_antisym_rtrancl);
bind_thm ("subcls_antisym", subcls1_acyclic RS acyclic_impl_antisym_rtrancl);

qed_goal "widen_antisym" thy "\<And>X. \<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>T\<preceq>S; ws_prog G\<rbrakk> \<Longrightarrow> S=T" (K [
  fast_tac (claset() addEs [widen_antisym_lemma, subint_antisym RS antisymD, 
	subcls_antisym RS antisymD]) 1]);

Goal "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C";
b y etac rtrancl_induct 1;
b y  dtac subcls1D 2;
b y  Auto_tac;
qed_spec_mp "subcls_is_class"; 

Goal "G\<turnstile>Class Object\<preceq>T \<Longrightarrow> T=Class Object";
b y ftac widen_Class 1;
b y fast_tac (claset() addDs [widen_Class_Class, widen_Class_Iface]) 1;
qed "widen_ObjectD";
AddSDs [widen_ObjectD];

Goalw [widens_def] "G\<turnstile>[][\<preceq>][]";
b y Auto_tac;
qed "widens_Nil";

Goalw [widens_def] "G\<turnstile>(S#Ss)[\<preceq>](T#Ts) = (G\<turnstile>S\<preceq>T \<and> G\<turnstile>Ss[\<preceq>]Ts)";
b y Auto_tac;
qed "widens_Cons";
Addsimps[widens_Nil,widens_Cons];


(** too specific *)
section "narrow";

(*unused*)
qed_typerel "narrow_RefT" "G\<turnstile>RefT R\<succ>T \<Longrightarrow> \<exists>t. T=RefT t" 
	[prove_typerel_lemma [widen_RefT] narrow.elim 
	"G\<turnstile>S\<succ>T \<Longrightarrow> S=RefT R \<longrightarrow> (\<exists>t. T=RefT t)"];

qed_typerel "narrow_RefT2" "G\<turnstile>S\<succ>RefT R \<Longrightarrow> \<exists>t. S=RefT t" 
	[prove_typerel_lemma [widen_RefT2] narrow.elim 
	"G\<turnstile>S\<succ>T \<Longrightarrow> T=RefT R \<longrightarrow> (\<exists>t. S=RefT t)"];

(*unused*)
qed_typerel "narrow_PrimT" "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> \<exists>t. T=PrimT t" 
 	[prove_typerel_lemma [widen_PrimT] narrow.elim
	 "G\<turnstile>S\<succ>T \<Longrightarrow> S=PrimT pt \<longrightarrow> (\<exists>t. T=PrimT t)"];

qed_typerel "narrow_PrimT2" "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow> \
				\ \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt" 
	[prove_typerel_lemma [widen_PrimT2] narrow.elim
	 "G\<turnstile>S\<succ>T \<Longrightarrow> T=PrimT pt \<longrightarrow> (\<exists>t. S=PrimT t \<and> G\<turnstile>S\<preceq>PrimT pt)"];


section "cast";

Goal "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>S\<succ>T\<rbrakk> \<Longrightarrow> R";
(* deferred *)

(*unused*)
qed_typerel "cast_RefT" "G\<turnstile>RefT R\<preceq>? T \<Longrightarrow> \<exists>t. T=RefT t" 
	[prove_typerel_lemma [widen_RefT,narrow_RefT] cast.elim 
	"G\<turnstile>S\<preceq>? T \<Longrightarrow> S=RefT R \<longrightarrow> (\<exists>t. T=RefT t)"];

qed_typerel "cast_RefT2" "G\<turnstile>S\<preceq>? RefT R \<Longrightarrow> \<exists>t. S=RefT t" 
	[prove_typerel_lemma [widen_RefT2,narrow_RefT2] cast.elim 
	"G\<turnstile>S\<preceq>? T \<Longrightarrow> T=RefT R \<longrightarrow> (\<exists>t. S=RefT t)"];

(*unused*)
qed_typerel "cast_PrimT" "G\<turnstile>PrimT pt\<preceq>? T \<Longrightarrow> \<exists>t. T=PrimT t" 
 	[prove_typerel_lemma [widen_PrimT,narrow_PrimT] cast.elim
	 "G\<turnstile>S\<preceq>? T \<Longrightarrow> S=PrimT pt \<longrightarrow> (\<exists>t. T=PrimT t)"];

qed_typerel "cast_PrimT2" "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \
				\ \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt" 
	[prove_typerel_lemma [widen_PrimT2,narrow_PrimT2] cast.elim
	 "G\<turnstile>S\<preceq>? T \<Longrightarrow> T=PrimT pt \<longrightarrow> (\<exists>t. S=PrimT t \<and> G\<turnstile>S\<preceq>PrimT pt)"];
(**)