Cord.ML
Back to theory Cord
(*
File: Cord.ML
Author: Simon Ambler (sja4@mcs.le.ac.uk)
Copyright: Leicester University, 1998.
Time-stamp: <99/08/26 11:57:08 sja4>
Contextual ordering of expressions.
*)
val prems = goalw thy [cord_def]
"env |- s <cord> t ::: a ==> env |- s ::: a";
by (cut_facts_tac prems 1);
by (Fast_tac 1);
qed "typing_cord1";
val prems = goalw thy [cord_def]
"env |- s <cord> t ::: a ==> env |- t ::: a";
by (cut_facts_tac prems 1);
by (Fast_tac 1);
qed "typing_cord2";
val prems = goalw thy [cord_def]
"env |- s ::: a ==> env |- s <cord> s ::: a";
by (cut_facts_tac prems 1);
by (Fast_tac 1);
qed "cord_refl";
val prems = goalw thy [cord_def]
"[| env |- s <cord> t ::: a; env |- t <cord> u ::: a |] \
\ ==> env |- s <cord> u ::: a";
by (cut_facts_tac prems 1);
by (Fast_tac 1);
qed "cord_trans";
val prems = goal thy
"(env1, a, env2) |-- c ::: b \
\ ==> ! s t. (env1 @ env2 |- s <opensim> t ::: a) \
\ --> (env2 |- c s <opensim> c t ::: b)";
by (cut_facts_tac prems 1);
be ctyping.induct 1;
by (ALLGOALS (fast_tac (claset()
addIs ([opensim_cong, opensim_refl]@ compat.intrs)
addss simpset())));
qed_spec_mp "ctyping_opensim_lemma";
val prems = goalw thy [cord_def] "env |- s <opensim> t ::: a \
\ ==> env |- s <cord> t ::: a";
by (cut_facts_tac prems 1);
by Safe_tac;
br opensim_typing1 1;
ba 1;
br opensim_typing2 1;
ba 1;
bd ctyping_opensim_lemma 1;
by (Simp_tac 1);
bes opensimEs 1;
br sim_converges 1;
ba 1;
ba 1;
qed "opensim_cord";
bind_thm ("kleene_cord", kleene_sim RS sim_opensim RS opensim_cord);
val prems = goalw thy [cord_def]
"[| (env1, a, env2) |-- c ::: b; \
\ env1 @ env2 |- s <cord> t ::: a |] \
\ ==> env2 |- c s <cord> c t ::: b";
by (cut_facts_tac prems 1);
by Safe_tac;
by (res_inst_tac [("f","c")] ctyping_lemma 1);
ba 1;
ba 1;
by (res_inst_tac [("f","c")] ctyping_lemma 1);
ba 1;
ba 1;
by (eres_inst_tac [("x","% u. ca (c u)")] allE 1);
by (eres_inst_tac [("x","ba")] allE 1);
be impE 1;
by (rtac ctyping_lemma2 1 THEN atac 1);
by (Simp_tac 1);
by (Fast_tac 1);
qed "cord_context";
val prems = goal thy "[] |- s <cord> t ::: a ==> s <sim> t ::: a";
br sim.coinduct 1;
by (res_inst_tac [("P","% (s,t,a). [] |- s <cord> t ::: a")] CollectI 1);
by (simp_tac (simpset() addsimps prems) 1);
by (REPEAT (eresolve_tac [CollectE, splitE, conjE, exE] 1));
by (hyp_subst_tac 1);
by (exhaust_tac "ya" 1);
by (ALLGOALS (hyp_subst_tac));
by (ALLGOALS (asm_full_simp_tac
(simpset() addsimps [simFun_def,simBool_def,simNum_def,
simPair_def,simList_def,typing_cord1,typing_cord2])));
by Safe_tac;
(* case for zero *)
by (asm_full_simp_tac (simpset() addsimps [cord_def, conv_zero_lemma]) 1);
by (subgoal_tac "([], Num, []) |-- \
\ (% y. Con ncase @@ y @@ Con zero @@ undef) ::: Num" 1);
by (Blast_tac 1);
by (fast_tac (HOL_cs addIs (ctyping.intrs@typing.intrs
@ typeof.intrs@[typing_undef])) 1);
(* Level 13 --- case for succ *)
by (forw_inst_tac [("P","% u. x >> Con succ @@ u")] exI 1);
by (subgoal_tac "? u. xa >> Con succ @@ u" 1);
by (asm_full_simp_tac (simpset() addsimps [cord_def, conv_succ_lemma]) 2);
by (subgoal_tac "([], Num, []) |-- \
\ (% y. Con ncase @@ y @@ undef @@ Lam (Con zero)) ::: Num" 2);
by (Blast_tac 2);
by (fast_tac (HOL_cs addIs (ctyping.intrs@typing.intrs
@ typeof.intrs@[typing_undef])) 2);
(* Level 19 *)
by (eres_inst_tac [("P","% u. xa >> Con succ @@ u")] exE 1);
br exI 1;
br conjI 1;
ba 1;
br disjI1 1;
br (kleene_ncase_lemma RS kleene_sym RS kleene_cord RS cord_trans) 1;
br typing_cord1 1;
ba 1;
ba 1;
br (kleene_ncase_lemma RS kleene_cord RSN (2,cord_trans)) 1;
br typing_cord2 2;
ba 2;
ba 2;
by (res_inst_tac [("c","% u. Con ncase @@ u @@ undef @@ Lam (Var 0)")]
cord_context 1);
by (Simp_tac 2);
by (fast_tac (HOL_cs addIs (ctyping.intrs@typing.intrs
@ typeof.intrs@[typing_undef])
addss simpset()) 1);
(* Level 35 --- tt *)
by (asm_full_simp_tac (simpset() addsimps [cord_def, conv_tt_lemma]) 1);
by (subgoal_tac "([], Bool, []) |-- \
\ (% y. Con cond @@ y @@ Con tt @@ undef) ::: Bool" 1);
by (Blast_tac 1);
by (fast_tac (HOL_cs addIs (ctyping.intrs@typing.intrs
@ typeof.intrs@[typing_undef])) 1);
(* Level 39 --- ff *)
by (asm_full_simp_tac (simpset() addsimps [cord_def, conv_ff_lemma]) 1);
by (subgoal_tac "([], Bool, []) |-- \
\ (% y. Con cond @@ y @@ undef @@ Con tt) ::: Bool" 1);
by (Blast_tac 1);
by (fast_tac (HOL_cs addIs (ctyping.intrs@typing.intrs
@ typeof.intrs@[typing_undef])) 1);
(* Level 43 --- Fun *)
by (subgoal_tac "? v. xa >> v" 1);
by (asm_full_simp_tac (simpset() addsimps [cord_def, converges_def]) 2);
by (fast_tac (HOL_cs addIs ctyping.intrs) 2);
be exE 1;
br exI 1;
br conjI 1;
ba 1;
by (strip_tac 1);
br disjI1 1;
by (res_inst_tac [("c","% u. u @@ p")] cord_context 1);
by (fast_tac (claset() addIs ctyping.intrs) 1);
by (Simp_tac 1);
br (kleene_eval RS kleene_sym RS kleene_cord RS cord_trans) 1;
ba 2;
br typing_cord1 1;
ba 1;
br (kleene_eval RS kleene_cord RSN (2,cord_trans)) 1;
ba 1;
br typing_cord2 1;
ba 1;
ba 1;
(* Level 64 --- pair *)
by (subgoal_tac "? w y. xa >> Con pair @@ w @@ y" 1);
by (asm_full_simp_tac (simpset() addsimps [cord_def, converges_def]) 2);
by (fast_tac (HOL_cs addIs ctyping.intrs addEs [make_elim values_Pair]) 2);
be exE 1;
be exE 1;
br exI 1;
br exI 1;
br conjI 1;
ba 1;
br conjI 1;
br disjI1 1;
br (kleene_pfst RS kleene_sym RS kleene_cord RS cord_trans) 1;
ba 2;
br typing_cord1 1;
ba 1;
br (kleene_pfst RS kleene_cord RSN (2,cord_trans)) 1;
ba 3;
br typing_cord2 2;
ba 2;
by (res_inst_tac [("c","% u. Con pfst @@ u")] cord_context 1);
by (fast_tac (HOL_cs addIs (ctyping.intrs@typing.intrs
@ typeof.intrs@[typing_undef])) 1);
by (Simp_tac 1);
br disjI1 1;
br (kleene_psnd RS kleene_sym RS kleene_cord RS cord_trans) 1;
ba 2;
br typing_cord1 1;
ba 1;
br (kleene_psnd RS kleene_cord RSN (2,cord_trans)) 1;
ba 3;
br typing_cord2 2;
ba 2;
by (res_inst_tac [("c","% u. Con psnd @@ u")] cord_context 1);
by (fast_tac (HOL_cs addIs (ctyping.intrs@typing.intrs
@ typeof.intrs@[typing_undef])) 1);
by (Simp_tac 1);
(* Level 98 --- nil *)
by (forward_tac [typing_cord1 RS conv_nil_lemma] 1);
by (forward_tac [typing_cord2 RS conv_nil_lemma] 1);
by (rotate_tac 2 1);
by (asm_full_simp_tac (simpset() addsimps [cord_def]) 1);
by (subgoal_tac "([], List typ, []) |-- \
\ (% y. Con scase @@ y @@ Con nil @@ undef) ::: List typ" 1);
by (Blast_tac 1);
by (fast_tac (HOL_cs addIs (ctyping.intrs@typing.intrs
@ typeof.intrs@[typing_undef])) 1);
(* Level 105 --- cons *)
by (forw_inst_tac [("P","% l. x >> Con cons @@ h1 @@ l")] exI 1);
by (dres_inst_tac [("P","% u. ? l. x >> Con cons @@ u @@ l")] exI 1);
by (subgoal_tac "? u l. xa >> Con cons @@ u @@ l" 1);
by (forward_tac [typing_cord1 RS conv_cons_lemma] 2);
by (forward_tac [typing_cord2 RS conv_cons_lemma] 2);
by (rotate_tac 4 2);
by (asm_full_simp_tac (simpset() addsimps [cord_def]) 2);
by (subgoal_tac "([], List typ, []) |-- \
\ (% y. Con scase @@ y @@ undef @@ Lam (Lam (Con nil))) \
\ ::: List typ" 2);
by (Blast_tac 2);
by (fast_tac (HOL_cs addIs (ctyping.intrs@typing.intrs
@ typeof.intrs@[typing_undef])) 2);
(* Level 115 *)
by (REPEAT (etac exE 1));
by (REPEAT (rtac exI 1));
br conjI 1;
ba 1;
br conjI 1;
br disjI1 1;
br disjI1 2;
br (kleene_scase_lemma1 RS kleene_sym RS kleene_cord RS cord_trans) 1;
br typing_cord1 1;
ba 1;
ba 1;
br (kleene_scase_lemma1 RS kleene_cord RSN (2,cord_trans)) 1;
br typing_cord2 2;
ba 2;
ba 2;
by (res_inst_tac [("c","% u. Con scase @@ u @@ undef @@ Lam (Lam (Var 1))")]
cord_context 1);
by (Simp_tac 2);
by (fast_tac (HOL_cs addIs (ctyping.intrs@typing.intrs
@ typeof.intrs@[typing_undef])
addss simpset()) 1);
br (kleene_scase_lemma2 RS kleene_sym RS kleene_cord RS cord_trans) 1;
br typing_cord1 1;
ba 1;
ba 1;
br (kleene_scase_lemma2 RS kleene_cord RSN (2,cord_trans)) 1;
br typing_cord2 2;
ba 2;
ba 2;
by (res_inst_tac [("c","% u. Con scase @@ u @@ undef @@ Lam (Lam (Var 0))")]
cord_context 1);
by (Simp_tac 2);
by (fast_tac (HOL_cs addIs (ctyping.intrs@typing.intrs
@ typeof.intrs@[typing_undef])
addss simpset()) 1);
(* Level 144 *)
qed "cord_sim";
val prems = goal thy
"[| b # env |- s <cord> t ::: a; [] |- p ::: b |] \
\ ==> env |- s [p/0] <cord> t [p/0] ::: a";
by (cut_facts_tac prems 1);
br (opensim_beta_conv1 RS opensim_cord RSN (2,cord_trans)) 1;
br (opensim_beta_conv2 RS opensim_cord RSN (1,cord_trans)) 1;
br typing_cord1 1;
ba 1;
br weakening_0 1;
ba 1;
by (res_inst_tac [("c", "% u. Lam u @@ p")] cord_context 1);
by (fast_tac (claset() addIs ctyping.intrs@typing.intrs@[weakening_0]) 1);
by (Simp_tac 1);
br typing_cord2 1;
ba 1;
br weakening_0 1;
ba 1;
qed "cord_subst_0";
val prems = goal thy
"! s t a. (env |- s <cord> t ::: a) \
\--> (env |- s <opensim> t ::: a)";
by (induct_tac "env" 1);
by (fast_tac (claset() addIs [cord_sim RS sim_opensim]) 1);
by (strip_tac 1);
by (forward_tac [typing_cord1] 1);
by (forward_tac [typing_cord2] 1);
by (fast_tac (claset()
addIs opensimIs@[cord_subst_0]) 1);
qed_spec_mp "cord_opensim";
goal thy "cord = opensim";
by Safe_tac;
by (split_all_tac 1);
br cord_opensim 1;
ba 1;
by (split_all_tac 1);
br opensim_cord 1;
ba 1;
qed "cord_eq_opensim";