File BiAbstr.ML

(*
      File: BiAbstr.thy
    Author: Simon Ambler (sja4@mcs.le.ac.uk)
 Copyright: Leicester University, 2001.
Time-stamp: <2002-04-08 17:03:24 sja4>

	Abstraction of two variables

*)

Addsimps (ext_simps);

val abstSet_Es =
  let
	val rbt = rule_by_tactic (ALLGOALS Full_simp_tac);
  in
	map (rbt o abstSet.mk_cases) [
		"abst i (% x. BND j)",
		"abst i (% x. f x $$ g x)",
		"abst i (% x. ABS (e x))"
	 ]
  end;

Delsimps (ext_simps);


val prems = Goalw [abstr_def]
  "[| abstr (% x. e x $$ f x); \
	\ [| abstr (% x. e x); abstr (% x. f x) |] ==> P |] ==> P";
by (cut_facts_tac prems 1);
bes abstSet_Es 1;
brs prems 1;
ba 1;
ba 1;
qed "abstr_APP_E";


Goalw [abstr_def] "abstr (% x. BND j) ==> P";
bes abstSet_Es 1;
be less_zeroE 1;
qed "abstr_BND_E";


Goal "abst i e ==> ordinary e";
be abstSet.induct 1;
by (ALLGOALS (fast_tac (claset() addIs ordinaryIs
	addss simpset())));
qed "abst_ordinary";


Goalw [abstr_def] "abstr e ==> ordinary e";
br abst_ordinary 1;
ba 1;
qed "abstr_ordinary";


Goal "! i. insts i [s] t = inst i s t";
by (induct_tac "t" 1);
by Auto_tac;
qed_spec_mp "insts_inst";


Goalw [lambda_def]
  "abst 1 f ==> (% x. ABS (f x)) = (% x. LAM y. insts 0 [y,x] (lbind 1 f))";
br ext 1;
by (simp_tac (simpset() addsimps [insts_lbind RS sym]) 1);
by (asm_simp_tac (simpset() addsimps [insts_inst, abst_inst_lbind RS cong]) 1);
qed "ABS_LAM_insts";


Goalw [rank_def] "abst i e \
	\ ==> !j. rank (% x. inst j (VAR n) (e x)) = rank e";
be abstSet.induct 1;
by Auto_tac;
qed_spec_mp "rank_inst";


Goalw [rank_def] "level i s \
	\ ==> !j. rank (% x. insts j [VAR n, x] s) = size s";
be levelSet.induct 1;
by Auto_tac;
be less_SucE 1;
be less_SucE 1;
by (ALLGOALS Asm_simp_tac);
qed_spec_mp "rank_insts1";


Goalw [rank_def] "level i s \
	\ ==> !j. rank (% x. insts j [x, VAR n] s) = size s";
be levelSet.induct 1;
by Auto_tac;
be less_SucE 1;
be less_SucE 1;
by (ALLGOALS Asm_simp_tac);
qed_spec_mp "rank_insts2";


Goal "level i s ==> ! j. i = Suc (Suc j) \
	\ --> abst j (% x. insts j [VAR n, x] s)";
be levelSet.induct 1;
by (ALLGOALS (fast_tac (claset()
	addIs abstSet.intrs
	addEs [less_SucE] addss simpset())));
val lemma = result();

Goal "level (Suc (Suc j)) s ==> abst j (% x. insts j [VAR n, x] s)";
bd lemma 1;
by Auto_tac;
qed "level_abst_insts1";


Goal "level i s ==> ! j. i = Suc (Suc j) \
	\ --> abst j (% x. insts j [x, VAR n] s)";
be levelSet.induct 1;
by (ALLGOALS (fast_tac (claset()
	addIs abstSet.intrs
	addEs [less_SucE] addss simpset())));
val lemma = result();

Goal "level (Suc (Suc j)) s ==> abst j (% x. insts j [x, VAR n] s)";
bd lemma 1;
by Auto_tac;
qed "level_abst_insts2";


Goalw [rank_def] "abst i e ==> ! j. size (lbind j e) = rank e";
be abstSet.induct 1;
by (ALLGOALS (asm_simp_tac (simpset() addsimps lbind_simps)));
qed_spec_mp "size_lbind";


Goal "biAbst j e ==> biAbst j (% x y. e y x)";
be biAbstSet.induct 1;
by (ALLGOALS (fast_tac (claset()
	addIs biAbstSet.intrs)));
qed "biAbst_swap";


Goalw [biAbstr_def] "biAbstr f ==> biAbstr (% x y. f y x)";
br biAbst_swap 1;
ba 1;
qed "biAbstr_swap";


Goalw [proper_def] "biAbst i e ==> ! s. proper s --> abst i (e s)";
be biAbstSet.induct 1;
by (ALLGOALS (fast_tac (claset()
	addIs abstSet.intrs @ [level_abst_const]
	addss simpset())));
qed_spec_mp "biAbst_proper_abst";


Goalw [biAbstr_def, abstr_def]
 "[| biAbstr e; proper s |] ==> abstr (e s)";
br biAbst_proper_abst 1;
ba 1;
ba 1;
qed "biAbstr_proper_abstr1";


Goalw [biAbstr_def, abstr_def]
 "[| biAbstr e; proper s |] ==> abstr (% x. e x s)";
br (biAbst_swap RS biAbst_proper_abst) 1;
ba 1;
ba 1;
qed "biAbstr_proper_abstr2";


Goalw [biAbstr_def, abstr_def, lambda_def]
  "biAbstr f ==> abstr (% x. LAM y. f x y)";
be biAbstSet.induct 1;
by (ALLGOALS (fast_tac (claset()
	addIs abstSet.intrs
	addEs abstSet_Es
	addss (simpset() addsimps lbind_simps))));
qed "biAbstr_abstr_LAM1";


Goal "biAbstr f ==> abstr (% y. LAM x. f x y)";
br (biAbstr_swap RS biAbstr_abstr_LAM1) 1;
ba 1;
qed "biAbstr_abstr_LAM2";


val abstrIs = [abstr_VAR, abstr_id, abstr_APP, biAbstr_abstr_LAM1];


Goal "level i s ==> ! j. i = Suc (Suc j) \
	\ --> biAbst j (% x y. insts j [x, y] s)";
be levelSet.induct 1;
by (ALLGOALS (fast_tac (claset()
	addIs biAbstSet.intrs
	addEs [less_SucE] addss simpset())));
val lemma = result();

Goal "level (Suc (Suc j)) s ==> biAbst j (% x y. insts j [x, y] s)";
bd lemma 1;
by Auto_tac;
qed "level_biAbst_insts";


val prems = Goalw [abstr_def, biAbstr_def]
	"[| abstr e; \
	\     !! a. P (% x. CON a); \
	\     !! j. P (% x. VAR j); \
	\           P (% x. x); \
	\   !! f g. [| abstr f; P f; abstr g; P g |] ==> P (% x. f x $$ g x); \
	\     !! f. [| biAbstr f; ! n. P (% x. f x (VAR n)); \
				\ ! n. P (% x. f (VAR n) x) |] \
			\ ==> P (% x. LAM y. f x y) \
	\ |] ==> P e";

by (res_inst_tac [("P","abst 0 e"), ("Q", "P e")] mp  1);
brs prems 2;
by (res_inst_tac [("P","% e. abst 0 e --> P e"), ("f","rank")]
	measure_induct 1);
by (case_tac "ordinary x" 1);
by (fast_tac (claset() addIs prems @ [abst_ordinary]
	addss simpset()) 2);

bw ordinary_def;
by Safe_tac;

(* ABS case *)

bes abstSet_Es 6;
by (asm_simp_tac (simpset() addsimps [ABS_LAM_insts]) 6);
brs prems 6;
br (abst_level_lbind RS level_biAbst_insts RS biAbst_swap) 6;
ba 6;
br allI 6;
by (eres_inst_tac [("x","% x. insts 0 [VAR n, x] (lbind 1 f)")] allE 6);
bd mp 6;
be mp 7;
br (abst_level_lbind RS rank_insts1 RS ssubst) 6;
ba 6;
br (size_lbind RS ssubst) 6;
ba 6;
brs expr_ranks 6;
br (abst_level_lbind RS level_abst_insts1) 6;
ba 6;

(* 23 *)

br allI 6;
by (eres_inst_tac [("x","% x. insts 0 [x, VAR n] (lbind 1 f)")] allE 6);
bd mp 6;
be mp 7;
br (abst_level_lbind RS rank_insts2 RS ssubst) 6;
ba 6;
br (size_lbind RS ssubst) 6;
ba 6;
brs expr_ranks 6;
br (abst_level_lbind RS level_abst_insts2) 6;
ba 6;

(* ABS case --- End *)

by (ALLGOALS (fast_tac (claset() addIs prems @ expr_ranks
	addEs abstSet_Es
	addss simpset())));

qed "abstr_VAR_induct";


val prems = Goal "[| abstr e; \
	\   !! a.    e = (% x. CON a) ==> P; \
	\            e = (% x. x) ==> P; \
	\   !! n.    e = (% x. VAR n) ==> P; \
	\ !! f g. [| e = (% x. f x $$ g x); abstr f; abstr g |] ==> P; \
	\   !! f. [| e = (% x. LAM y. f x y); biAbstr f |] ==> P |] \
		\ ==> P";
by (cut_facts_tac prems 1);
by (subgoal_tac "e = e --> P" 1);
be impE 1;
br refl 1;
ba 1;
by (eres_inst_tac [("P","% x. (e=x --> P)")] abstr_VAR_induct 1);
by (ALLGOALS (strip_tac THEN' eresolve_tac prems));
by (ALLGOALS atac);
qed "abstrE";


(*

Goal "abstr e ==> proper t --> proper (e t)";
be abstr_VAR_induct 1;
by (ALLGOALS (fast_tac (claset() addIs properIs @ [biAbstr_proper_abstr1])));
qed_spec_mp "abstr_proper_proper";

*)

Goalw [biRank_def] "biRank f < biRank (% x y. f x y $$ g x y)";
by (Simp_tac 1);
qed "biRank_APP1";

Goalw [biRank_def] "biRank g < biRank (% x y. f x y $$ g x y)";
by (Simp_tac 1);
qed "biRank_APP2";

Goalw [biRank_def] "biRank e < biRank (% x y. ABS (e x y))";
by (Simp_tac 1);
qed "biRank_ABS";


val expr_biRanks = [biRank_APP1, biRank_APP2, biRank_ABS];


val prems = Goal "[| !! a. P (% x y. CON a); \
	\     !! j. P (% x y. VAR j); \
	\           P (% x y. x); \
	\           P (% x y. y); \
	\     !! j. P (% x y. BND j); \
	\   !! f g. [| P f; P g |] ==> P (% x y. f x y $$ g x y); \
	\     !! f. P f ==> P (% x y. ABS (f x y)); \
	\     !! f. ~ biOrdinary f ==> P f |] \
			\ ==> P e";
by (res_inst_tac [("P","P"), ("f", "biRank")]
	measure_induct 1);
by (case_tac "biOrdinary x" 1);
brs prems 2;
ba 2;
bw biOrdinary_def;
by Safe_tac;
by (ALLGOALS (blast_tac (claset()
	addIs prems @ expr_biRanks
	addss simpset())));
qed "biAbstraction_induct";


val ext2_expr_inject = 
  let
	fun prv form = prove_goal thy form
		(fn prs => [fast_tac (claset()
			addss (simpset() addsimps [ext_simp])) 1]);
  in
	map prv [
		"((% x y. CON a) = (% x y. CON b)) = (a = b)",
		"((% x y. VAR j) = (% x y. VAR k)) = (j = k)",
		"((% x y. BND j) = (% x y. BND k)) = (j = k)",
		"((% x y. e x y $$ g x y) = (% x y. f x y $$ h x y)) \
			\ = (e = f & g = h)",
		"((% x y. ABS (e x y)) = (% x y. ABS (f x y))) = (e = f)"
		]
  end;


Goal "(% (x :: 'a expr) (y :: 'a expr). x) ~= (% x y. s)";
by (simp_tac (simpset() addsimps [ext_simp]) 1);
by (res_inst_tac [("x","if VAR 0 = s then VAR 1 else VAR 0")] exI 1);
by (fast_tac (claset()
	addss (simpset() addsplits [split_if_asm])) 1);
qed "proj1_neq_const";


Goal "(% (x :: 'a expr) (y :: 'a expr). y) ~= (% x y. s)";
by (simp_tac (simpset() addsimps [ext_simp]) 1);
by (res_inst_tac [("x","if VAR 0 = s then VAR 1 else VAR 0")] exI 1);
by (fast_tac (claset()
	addss (simpset() addsplits [split_if_asm])) 1);
qed "proj2_neq_const";


Goal "(% (x :: 'a expr) (y :: 'a expr). x) ~= (% x y. y)";
by (simp_tac (simpset() addsimps [ext_simp]) 1);
by (res_inst_tac [("x","VAR 0")] exI 1);
by (res_inst_tac [("x","VAR 1")] exI 1);
by (Simp_tac 1);
qed "proj1_neq_proj2";


Goal "(% (x :: 'a expr) (y :: 'a expr). x) ~= (% x y. f x y $$ g x y)";
by (simp_tac (simpset() addsimps [ext_simp]) 1);
by (res_inst_tac [("x","VAR 0")] exI 1);
by (res_inst_tac [("x","VAR 0")] exI 1);
by (Simp_tac 1);
qed "proj1_neq_APP";


Goal "(% (x :: 'a expr) (y :: 'a expr). y) ~= (% x y. f x y $$ g x y)";
by (simp_tac (simpset() addsimps [ext_simp]) 1);
by (res_inst_tac [("x","VAR 0")] exI 1);
by (res_inst_tac [("x","VAR 0")] exI 1);
by (Simp_tac 1);
qed "proj2_neq_APP";


Goal "(% (x :: 'a expr) (y :: 'a expr). x) ~= (% x y. ABS (e x y))";
by (simp_tac (simpset() addsimps [ext_simp]) 1);
by (res_inst_tac [("x","VAR 0")] exI 1);
by (res_inst_tac [("x","VAR 0")] exI 1);
by (Simp_tac 1);
qed "proj1_neq_ABS";


Goal "(% (x :: 'a expr) (y :: 'a expr). y) ~= (% x y. ABS (e x y))";
by (simp_tac (simpset() addsimps [ext_simp]) 1);
by (res_inst_tac [("x","VAR 0")] exI 1);
by (res_inst_tac [("x","VAR 0")] exI 1);
by (Simp_tac 1);
qed "proj2_neq_ABS";



val ext2_expr_distinct =
  let
	fun prv form = prove_goal thy form
		(fn prs => [simp_tac (simpset() addsimps [ext_simp]) 1]);

	val expr_distinct = [proj1_neq_const, proj1_neq_APP, proj1_neq_ABS,
				proj1_neq_proj2,
				proj2_neq_const, proj2_neq_APP, proj2_neq_ABS]
		@
		map prv [
		"(% x y. CON a) ~= (% x y. VAR n)",
		"(% x y. CON a) ~= (% x y. BND j)",
		"(% x y. CON a) ~= (% x y. f x y $$ g x y)",
		"(% x y. CON a) ~= (% x y. ABS (e x y))",
		"(% x y. VAR n) ~= (% x y. BND j)",
		"(% x y. VAR n) ~= (% x y. f x y $$ g x y)",
		"(% x y. VAR n) ~= (% x y. ABS (e x y))",
		"(% x y. BND j) ~= (% x y. f x y $$ g x y)",
		"(% x y. BND j) ~= (% x y. ABS (e x y))",
		"(% x y. f x y $$ g x y) ~= (% x y. ABS (e x y))"
		]
 
  in
	expr_distinct @ (expr_distinct RL [not_sym])

  end;


val ext2_simps = ext2_expr_inject @ ext2_expr_distinct;


(* BiAbstraction solver --- for goals of the form "biAbstr (% x y. e x y)" *)


local

  (* Will only resolve against goals of the right form *)
  val biAbstr_filter_thm =
	prove_goal thy "biAbstr (% x y. e x y) ==> biAbstr (% x y. e x y)"
		(fn prems => [resolve_tac prems 1]);
in

  fun biAbstr_tac defs prems =
	rtac biAbstr_filter_thm
	THEN'
	 (resolve_tac prems
	  ORELSE'
	  fast_tac (claset()
		addIs biAbstSet.intrs
		addss (simpset()
			addsimps defs @ [biAbstr_def, lambda_def]
					@ lbind_simps)))
end;


fun biAbstr_solver defs = mk_solver "biAbstr"
		(fn prems => biAbstr_tac defs prems);


Goalw [biAbstr_def]
  "biAbstr f ==> ! g n. biAbstr g --> newFor n (f dflt dflt) \
	\ --> newFor n (g dflt dflt) \
	\ --> f (VAR n) = g (VAR n) --> f = g";
be biAbstSet.induct 1;
by (ALLGOALS strip_tac);
by (ALLGOALS (eres_inst_tac [("aa","(i,g)")] biAbstSet.elim));
by (ALLGOALS (fast_tac (claset()
	addss (simpset() addsimps ext_simps @ ext2_simps))));
qed_spec_mp "biAbstr_extensionality";


Goalw [biSubst_def]
  "[| f (VAR n) = e; biAbstr f; newFor n (f dflt dflt) |] \
	\ ==> biSubst e n = f";
br some_equality 1;
by (Fast_tac 1);
by (REPEAT (etac conjE 1));
br biAbstr_extensionality 1;
by Auto_tac;
qed_spec_mp "biAbstr_biSubst";


Goalw [abstr_def, biAbstr_def]
  "abstr e ==> ? f. biAbstr f & newFor n (f dflt dflt) & f (VAR n) = e";
be abstSet.induct 1;
by (case_tac "n=na" 3);
by (res_inst_tac [("x","% x y. CON a")] exI 1);
by (res_inst_tac [("x","% x y. y")] exI 2);
by (res_inst_tac [("x","% x y. x")] exI 3);
by (res_inst_tac [("x","% x y. VAR na")] exI 4);
by (REPEAT (eresolve_tac [exE, conjE] 6));
by (res_inst_tac [("x","% x y. fa x y $$ fb x y")] exI 6);
by (REPEAT (eresolve_tac [exE, conjE] 7));
by (res_inst_tac [("x","% x y. ABS (fa x y)")] exI 7);

by (ALLGOALS (fast_tac (claset()
	addIs biAbstSet.intrs
	addss simpset())));
qed "abstr_biSubst_lemma";


Goalw [biSubst_def] "abstr e ==> biAbstr (biSubst e n)";
br (abstr_biSubst_lemma RS someI_ex RS conjunct1) 1;
ba 1;
qed "abstr_biAbstr_biSubst";


Goalw [biSubst_def] "abstr e ==> biSubst e n (VAR n) = e";
br (abstr_biSubst_lemma RS someI_ex RS conjunct2 RS conjunct2) 1;
ba 1;
qed "abstr_biSubst_id";


Goalw [biSubst_def] "abstr e ==> newFor n (biSubst e n dflt dflt)";
br (abstr_biSubst_lemma RS someI_ex RS conjunct2 RS conjunct1) 1;
ba 1;
qed "abstr_newFor_biSubst";


(*

Goal "subst (CON a) n = (% x. CON a)";
br abstr_subst 1;
br refl 1;
by (abstr_tac [] [] 1);
by (Simp_tac 1);
qed "subst_CON";


Goal "subst (VAR m) n = (if n=m then (% x. x) else (% x. VAR m))";
br abstr_subst 1;
by (Simp_tac 1);
by (abstr_tac [] [] 1);
by (Simp_tac 1);
qed "subst_VAR";


Goal "[| proper s; proper t |] \
	\ ==> subst (s $$ t) n = (% x. subst s n x $$ subst t n x)";
br abstr_subst 1;
by (asm_simp_tac (simpset() addsimps [proper_subst_id]) 1);
br abstr_APP 1;
be proper_abstr_subst 1;
be proper_abstr_subst 1;
by (asm_simp_tac (simpset() addsimps [proper_newFor_subst]) 1);
qed "subst_APP";

*)

Goal "abstr e ==> subst (LAM y. e y) n = (% x. LAM y. biSubst e n x y)";
br abstr_subst 1;
by (asm_simp_tac (simpset()
	addsimps [abstr_LAM_simp, abstr_biSubst_id,
		abstr_biAbstr_biSubst RS biAbstr_abstr_LAM1]) 1);

br (abstr_biAbstr_biSubst RS biAbstr_abstr_LAM1) 1;
ba 1;

by (asm_simp_tac (simpset()
	addsimps [newFor_LAM, abstr_newFor_biSubst,
		abstr_biAbstr_biSubst RS biAbstr_proper_abstr1,
		proper_dflt]) 1);

qed "subst_LAM";


Goal "biAbst i f ==> ! e. abst i e --> abst i (% x. f x (e x))";
be biAbstSet.induct 1;
by (strip_tac 7);
bd ((le_refl RS le_SucI) RSN (2, abst_le_abst)) 7;
by (ALLGOALS (fast_tac (claset() addIs abstSet.intrs)));
qed_spec_mp "biAbst_abst_compose";


Goalw [biAbstr_def, abstr_def]
  "[| biAbstr f; abstr e |] ==> abstr (% x. f x (e x))";
be biAbst_abst_compose 1;
ba 1;
qed "biAbstr_abstr_compose";


Goalw [biAbstr_def] "biAbstr f ==> ! s t. proper s --> proper t \
	\ --> newFor n s --> newFor n t --> newFor n (f dflt dflt) \
	\ --> newFor n (f s t)";
be biAbstSet.induct 1;
by (ALLGOALS (fast_tac (claset() addss simpset())));
qed_spec_mp "biAbstr_newFor_apply";


Goal "[| abstr e; proper u; proper t |] \
	\ ==> biSubst e n u (subst t n u) = subst (e t) n u";

by (res_inst_tac [("f", "% x. biSubst e n x (subst t n x)")]
	(refl RSN (2, cong)) 1);
br (abstr_subst RS sym) 1;
by (asm_simp_tac (simpset()
	addsimps [subst_VAR_id, abstr_biSubst_id]) 1);
by (res_inst_tac [("f","biSubst e n"), ("e","subst t n")]
	biAbstr_abstr_compose 1);
br abstr_biAbstr_biSubst 1;
ba 1;
br proper_abstr_subst 1;
ba 1;
by (res_inst_tac [("f","biSubst e n")] biAbstr_newFor_apply 1);
br abstr_biAbstr_biSubst 1;
ba 1;
br proper_dflt 1;
br (proper_abstr_subst RS abstr_proper_proper) 1;
ba 1;
br proper_dflt 1;
by (Simp_tac 1);
by (simp_tac (simpset() addsimps [newFor_subst]) 1);
br abstr_newFor_biSubst 1;
ba 1;
qed "biSubst_subst_simp";