--- a/src/CCL/CCL.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/CCL/CCL.thy Fri Jul 17 10:07:15 2009 +0200
@@ -1,5 +1,4 @@
(* Title: CCL/CCL.thy
- ID: $Id$
Author: Martin Coen
Copyright 1993 University of Cambridge
*)
@@ -249,13 +248,13 @@
ML {*
-val caseB_lemmas = mk_lemmas (thms "caseBs")
+val caseB_lemmas = mk_lemmas @{thms caseBs}
val ccl_dstncts =
let fun mk_raw_dstnct_thm rls s =
- prove_goal (the_context ()) s (fn _=> [rtac notI 1,eresolve_tac rls 1])
+ prove_goal @{theory} s (fn _=> [rtac notI 1,eresolve_tac rls 1])
in map (mk_raw_dstnct_thm caseB_lemmas)
- (mk_dstnct_rls (the_context ()) ["bot","true","false","pair","lambda"]) end
+ (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end
fun mk_dstnct_thms thy defs inj_rls xs =
let fun mk_dstnct_thm rls s = prove_goalw thy defs s
@@ -273,9 +272,9 @@
val XH_to_Ds = map XH_to_D
val XH_to_Es = map XH_to_E;
-bind_thms ("ccl_rews", thms "caseBs" @ ccl_injs @ ccl_dstncts);
+bind_thms ("ccl_rews", @{thms caseBs} @ ccl_injs @ ccl_dstncts);
bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [notE]);
-bind_thms ("ccl_injDs", XH_to_Ds (thms "ccl_injs"));
+bind_thms ("ccl_injDs", XH_to_Ds @{thms ccl_injs});
*}
lemmas [simp] = ccl_rews
@@ -388,13 +387,13 @@
ML {*
local
- fun mk_thm s = prove_goal (the_context ()) s (fn _ =>
- [rtac notI 1,dtac (thm "case_pocong") 1,etac rev_mp 5,
+ fun mk_thm s = prove_goal @{theory} s (fn _ =>
+ [rtac notI 1, dtac @{thm case_pocong} 1, etac rev_mp 5,
ALLGOALS (simp_tac @{simpset}),
- REPEAT (resolve_tac [thm "po_refl", thm "npo_lam_bot"] 1)])
+ REPEAT (resolve_tac [@{thm po_refl}, @{thm npo_lam_bot}] 1)])
in
-val npo_rls = [thm "npo_pair_lam", thm "npo_lam_pair"] @ map mk_thm
+val npo_rls = [@{thm npo_pair_lam}, @{thm npo_lam_pair}] @ map mk_thm
["~ true [= false", "~ false [= true",
"~ true [= <a,b>", "~ <a,b> [= true",
"~ true [= lam x. f(x)","~ lam x. f(x) [= true",
--- a/src/CCL/Hered.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/CCL/Hered.thy Fri Jul 17 10:07:15 2009 +0200
@@ -1,5 +1,4 @@
(* Title: CCL/Hered.thy
- ID: $Id$
Author: Martin Coen
Copyright 1993 University of Cambridge
*)
@@ -113,7 +112,7 @@
res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
val HTTgenIs =
- map (mk_genIs (the_context ()) @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
+ map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
["true : HTTgen(R)",
"false : HTTgen(R)",
"[| a : R; b : R |] ==> <a,b> : HTTgen(R)",
--- a/src/CCL/Term.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/CCL/Term.thy Fri Jul 17 10:07:15 2009 +0200
@@ -1,5 +1,4 @@
(* Title: CCL/Term.thy
- ID: $Id$
Author: Martin Coen
Copyright 1993 University of Cambridge
*)
@@ -274,8 +273,9 @@
ML {*
-bind_thms ("term_injs", map (mk_inj_rl (the_context ())
- [thm "applyB", thm "splitB", thm "whenBinl", thm "whenBinr", thm "ncaseBsucc", thm "lcaseBcons"])
+bind_thms ("term_injs", map (mk_inj_rl @{theory}
+ [@{thm applyB}, @{thm splitB}, @{thm whenBinl}, @{thm whenBinr},
+ @{thm ncaseBsucc}, @{thm lcaseBcons}])
["(inl(a) = inl(a')) <-> (a=a')",
"(inr(a) = inr(a')) <-> (a=a')",
"(succ(a) = succ(a')) <-> (a=a')",
@@ -287,7 +287,7 @@
ML {*
bind_thms ("term_dstncts",
- mkall_dstnct_thms (the_context ()) (thms "data_defs") (thms "ccl_injs" @ thms "term_injs")
+ mkall_dstnct_thms @{theory} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs})
[["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
*}
@@ -297,8 +297,8 @@
ML {*
local
- fun mk_thm s = prove_goalw (the_context ()) (thms "data_defs") s (fn _ =>
- [simp_tac (@{simpset} addsimps (thms "ccl_porews")) 1])
+ fun mk_thm s = prove_goalw @{theory} @{thms data_defs} s (fn _ =>
+ [simp_tac (@{simpset} addsimps @{thms ccl_porews}) 1])
in
val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
"inr(b) [= inr(b') <-> b [= b'",
--- a/src/CCL/Type.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/CCL/Type.thy Fri Jul 17 10:07:15 2009 +0200
@@ -428,7 +428,7 @@
ML {*
-val POgenIs = map (mk_genIs (the_context ()) (thms "data_defs") (thm "POgenXH") (thm "POgen_mono"))
+val POgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm POgenXH} @{thm POgen_mono})
["<true,true> : POgen(R)",
"<false,false> : POgen(R)",
"[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)",
@@ -443,9 +443,9 @@
fun POgen_tac ctxt (rla,rlb) i =
SELECT_GOAL (safe_tac (local_claset_of ctxt)) i THEN
- rtac (rlb RS (rla RS (thm "ssubst_pair"))) i THEN
- (REPEAT (resolve_tac (POgenIs @ [thm "PO_refl" RS (thm "POgen_mono" RS ci3_AI)] @
- (POgenIs RL [thm "POgen_mono" RS ci3_AgenI]) @ [thm "POgen_mono" RS ci3_RI]) i));
+ rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN
+ (REPEAT (resolve_tac (POgenIs @ [@{thm PO_refl} RS (@{thm POgen_mono} RS ci3_AI)] @
+ (POgenIs RL [@{thm POgen_mono} RS ci3_AgenI]) @ [@{thm POgen_mono} RS ci3_RI]) i));
*}
@@ -458,7 +458,7 @@
ML {*
-val EQgenIs = map (mk_genIs (the_context ()) (thms "data_defs") (thm "EQgenXH") (thm "EQgen_mono"))
+val EQgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm EQgenXH} @{thm EQgen_mono})
["<true,true> : EQgen(R)",
"<false,false> : EQgen(R)",
"[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)",
--- a/src/FOL/simpdata.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/FOL/simpdata.ML Fri Jul 17 10:07:15 2009 +0200
@@ -85,11 +85,11 @@
end);
val defEX_regroup =
- Simplifier.simproc (the_context ())
+ Simplifier.simproc @{theory}
"defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
val defALL_regroup =
- Simplifier.simproc (the_context ())
+ Simplifier.simproc @{theory}
"defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
--- a/src/HOL/Algebra/abstract/Ring2.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Fri Jul 17 10:07:15 2009 +0200
@@ -286,7 +286,7 @@
else SOME rew
end;
in
- val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss (K proc);
+ val ring_simproc = Simplifier.simproc @{theory} "ring" lhss (K proc);
end;
*}
--- a/src/HOL/Divides.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Divides.thy Fri Jul 17 10:07:15 2009 +0200
@@ -655,7 +655,7 @@
in
-val cancel_div_mod_nat_proc = Simplifier.simproc (the_context ())
+val cancel_div_mod_nat_proc = Simplifier.simproc @{theory}
"cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
val _ = Addsimprocs [cancel_div_mod_nat_proc];
--- a/src/HOL/GCD.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/GCD.thy Fri Jul 17 10:07:15 2009 +0200
@@ -162,7 +162,6 @@
transfer_int_nat_gcd transfer_int_nat_gcd_closures]
-
subsection {* GCD *}
(* was gcd_induct *)
@@ -1556,32 +1555,6 @@
apply (case_tac "p >= 0")
by (blast, auto simp add: prime_ge_0_int)
-(* To do: determine primality of any numeral *)
-
-lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
- by (simp add: prime_nat_def)
-
-lemma zero_not_prime_int [simp]: "~prime (0::int)"
- by (simp add: prime_int_def)
-
-lemma one_not_prime_nat [simp]: "~prime (1::nat)"
- by (simp add: prime_nat_def)
-
-lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
- by (simp add: prime_nat_def One_nat_def)
-
-lemma one_not_prime_int [simp]: "~prime (1::int)"
- by (simp add: prime_int_def)
-
-lemma two_is_prime_nat [simp]: "prime (2::nat)"
- apply (auto simp add: prime_nat_def)
- apply (case_tac m)
- apply (auto dest!: dvd_imp_le)
- done
-
-lemma two_is_prime_int [simp]: "prime (2::int)"
- by (rule two_is_prime_nat [transferred direction: nat "op <= (0::int)"])
-
lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
apply (unfold prime_nat_def)
apply (metis gcd_dvd1_nat gcd_dvd2_nat)
@@ -1628,15 +1601,70 @@
apply auto
done
-lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
- coprime a (p^m)"
+subsubsection{* Make prime naively executable *}
+
+lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
+ by (simp add: prime_nat_def)
+
+lemma zero_not_prime_int [simp]: "~prime (0::int)"
+ by (simp add: prime_int_def)
+
+lemma one_not_prime_nat [simp]: "~prime (1::nat)"
+ by (simp add: prime_nat_def)
+
+lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
+ by (simp add: prime_nat_def One_nat_def)
+
+lemma one_not_prime_int [simp]: "~prime (1::int)"
+ by (simp add: prime_int_def)
+
+lemma prime_nat_code[code]:
+ "prime(p::nat) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))"
+apply(simp add: Ball_def)
+apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
+done
+
+lemma prime_nat_simp:
+ "prime(p::nat) = (p > 1 & (list_all (%n. ~ n dvd p) [2..<p]))"
+apply(simp only:prime_nat_code list_ball_code greaterThanLessThan_upt)
+apply(simp add:nat_number One_nat_def)
+done
+
+lemmas prime_nat_simp_number_of[simp] = prime_nat_simp[of "number_of m", standard]
+
+lemma prime_int_code[code]:
+ "prime(p::int) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))" (is "?L = ?R")
+proof
+ assume "?L" thus "?R"
+ by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
+next
+ assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
+qed
+
+lemma prime_int_simp:
+ "prime(p::int) = (p > 1 & (list_all (%n. ~ n dvd p) [2..p - 1]))"
+apply(simp only:prime_int_code list_ball_code greaterThanLessThan_upto)
+apply simp
+done
+
+lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard]
+
+declare successor_int_def[simp]
+
+lemma two_is_prime_nat [simp]: "prime (2::nat)"
+by simp
+
+lemma two_is_prime_int [simp]: "prime (2::int)"
+by simp
+
+
+lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
apply (rule coprime_exp_nat)
apply (subst gcd_commute_nat)
apply (erule (1) prime_imp_coprime_nat)
done
-lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
- coprime a (p^m)"
+lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
apply (rule coprime_exp_int)
apply (subst gcd_commute_int)
apply (erule (1) prime_imp_coprime_int)
@@ -1655,12 +1683,10 @@
apply auto
done
-lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
- coprime (p^m) (q^n)"
+lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
by (rule coprime_exp2_nat, rule primes_coprime_nat)
-lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
- coprime (p^m) (q^n)"
+lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
by (rule coprime_exp2_int, rule primes_coprime_int)
lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
--- a/src/HOL/IntDiv.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/IntDiv.thy Fri Jul 17 10:07:15 2009 +0200
@@ -266,7 +266,7 @@
in
-val cancel_div_mod_int_proc = Simplifier.simproc (the_context ())
+val cancel_div_mod_int_proc = Simplifier.simproc @{theory}
"cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
val _ = Addsimprocs [cancel_div_mod_int_proc];
--- a/src/HOL/Lambda/WeakNorm.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Fri Jul 17 10:07:15 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Lambda/WeakNorm.thy
- ID: $Id$
Author: Stefan Berghofer
Copyright 2003 TU Muenchen
*)
@@ -430,11 +429,11 @@
val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct1));
-val ct1' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct1)) dB1);
+val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2));
-val ct2' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct2)) dB2);
+val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
*}
text {*
@@ -505,11 +504,11 @@
ML {*
val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1));
-val ct1' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct1)) dB1);
+val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
-val ct2' = cterm_of (the_context ()) (term_of_dB [] (#T (rep_cterm ct2)) dB2);
+val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
*}
end
--- a/src/HOL/List.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/List.thy Fri Jul 17 10:07:15 2009 +0200
@@ -679,7 +679,7 @@
in
val list_eq_simproc =
- Simplifier.simproc (the_context ()) "list_eq" ["(xs::'a list) = ys"] (K list_eq);
+ Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
end;
@@ -3190,7 +3190,7 @@
begin
definition
-successor_int_def: "successor = (%i\<Colon>int. i+1)"
+successor_int_def[simp]: "successor = (%i\<Colon>int. i+1)"
instance
by intro_classes (simp_all add: successor_int_def)
--- a/src/HOL/Modelcheck/EindhovenSyn.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy Fri Jul 17 10:07:15 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Modelcheck/EindhovenSyn.thy
- ID: $Id$
Author: Olaf Mueller, Jan Philipps, Robert Sandner
Copyright 1997 TU Muenchen
*)
@@ -70,7 +69,7 @@
val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
val pair_eta_expand_proc =
- Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
+ Simplifier.simproc @{theory} "pair_eta_expand" ["f::'a*'b=>'c"]
(fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
val Eindhoven_ss =
--- a/src/HOL/Modelcheck/MuckeSyn.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy Fri Jul 17 10:07:15 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Modelcheck/MuckeSyn.thy
- ID: $Id$
Author: Tobias Hamberger
Copyright 1999 TU Muenchen
*)
@@ -119,7 +118,7 @@
local
- val move_thm = prove_goal (the_context ()) "[| a = b ==> P a; a = b |] ==> P b"
+ val move_thm = prove_goal @{theory} "[| a = b ==> P a; a = b |] ==> P b"
(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
REPEAT (resolve_tac prems 1)]);
@@ -214,7 +213,7 @@
val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
val pair_eta_expand_proc =
- Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
+ Simplifier.simproc @{theory} "pair_eta_expand" ["f::'a*'b=>'c"]
(fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
val Mucke_ss = @{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
--- a/src/HOL/Nominal/Examples/Fsub.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy Fri Jul 17 10:07:15 2009 +0200
@@ -91,7 +91,7 @@
pairs of type-variables and types (this is sufficient for Part 1A). *}
text {* In order to state validity-conditions for typing-contexts, the notion of
- a @{text "domain"} of a typing-context is handy. *}
+ a @{text "dom"} of a typing-context is handy. *}
nominal_primrec
"tyvrs_of" :: "binding \<Rightarrow> tyvrs set"
@@ -108,16 +108,16 @@
by auto
consts
- "ty_domain" :: "env \<Rightarrow> tyvrs set"
+ "ty_dom" :: "env \<Rightarrow> tyvrs set"
primrec
- "ty_domain [] = {}"
- "ty_domain (X#\<Gamma>) = (tyvrs_of X)\<union>(ty_domain \<Gamma>)"
+ "ty_dom [] = {}"
+ "ty_dom (X#\<Gamma>) = (tyvrs_of X)\<union>(ty_dom \<Gamma>)"
consts
- "trm_domain" :: "env \<Rightarrow> vrs set"
+ "trm_dom" :: "env \<Rightarrow> vrs set"
primrec
- "trm_domain [] = {}"
- "trm_domain (X#\<Gamma>) = (vrs_of X)\<union>(trm_domain \<Gamma>)"
+ "trm_dom [] = {}"
+ "trm_dom (X#\<Gamma>) = (vrs_of X)\<union>(trm_dom \<Gamma>)"
lemma vrs_of_eqvt[eqvt]:
fixes pi ::"tyvrs prm"
@@ -128,13 +128,13 @@
and "pi'\<bullet>(vrs_of x) = vrs_of (pi'\<bullet>x)"
by (nominal_induct x rule: binding.strong_induct) (simp_all add: tyvrs_of.simps eqvts)
-lemma domains_eqvt[eqvt]:
+lemma doms_eqvt[eqvt]:
fixes pi::"tyvrs prm"
and pi'::"vrs prm"
- shows "pi \<bullet>(ty_domain \<Gamma>) = ty_domain (pi\<bullet>\<Gamma>)"
- and "pi'\<bullet>(ty_domain \<Gamma>) = ty_domain (pi'\<bullet>\<Gamma>)"
- and "pi \<bullet>(trm_domain \<Gamma>) = trm_domain (pi\<bullet>\<Gamma>)"
- and "pi'\<bullet>(trm_domain \<Gamma>) = trm_domain (pi'\<bullet>\<Gamma>)"
+ shows "pi \<bullet>(ty_dom \<Gamma>) = ty_dom (pi\<bullet>\<Gamma>)"
+ and "pi'\<bullet>(ty_dom \<Gamma>) = ty_dom (pi'\<bullet>\<Gamma>)"
+ and "pi \<bullet>(trm_dom \<Gamma>) = trm_dom (pi\<bullet>\<Gamma>)"
+ and "pi'\<bullet>(trm_dom \<Gamma>) = trm_dom (pi'\<bullet>\<Gamma>)"
by (induct \<Gamma>) (simp_all add: eqvts)
lemma finite_vrs:
@@ -142,19 +142,19 @@
and "finite (vrs_of x)"
by (nominal_induct rule:binding.strong_induct, auto)
-lemma finite_domains:
- shows "finite (ty_domain \<Gamma>)"
- and "finite (trm_domain \<Gamma>)"
+lemma finite_doms:
+ shows "finite (ty_dom \<Gamma>)"
+ and "finite (trm_dom \<Gamma>)"
by (induct \<Gamma>, auto simp add: finite_vrs)
-lemma ty_domain_supp:
- shows "(supp (ty_domain \<Gamma>)) = (ty_domain \<Gamma>)"
- and "(supp (trm_domain \<Gamma>)) = (trm_domain \<Gamma>)"
-by (simp only: at_fin_set_supp at_tyvrs_inst at_vrs_inst finite_domains)+
+lemma ty_dom_supp:
+ shows "(supp (ty_dom \<Gamma>)) = (ty_dom \<Gamma>)"
+ and "(supp (trm_dom \<Gamma>)) = (trm_dom \<Gamma>)"
+by (simp only: at_fin_set_supp at_tyvrs_inst at_vrs_inst finite_doms)+
-lemma ty_domain_inclusion:
+lemma ty_dom_inclusion:
assumes a: "(TVarB X T)\<in>set \<Gamma>"
- shows "X\<in>(ty_domain \<Gamma>)"
+ shows "X\<in>(ty_dom \<Gamma>)"
using a by (induct \<Gamma>, auto)
lemma ty_binding_existence:
@@ -163,8 +163,8 @@
using assms
by (nominal_induct a rule: binding.strong_induct, auto)
-lemma ty_domain_existence:
- assumes a: "X\<in>(ty_domain \<Gamma>)"
+lemma ty_dom_existence:
+ assumes a: "X\<in>(ty_dom \<Gamma>)"
shows "\<exists>T.(TVarB X T)\<in>set \<Gamma>"
using a
apply (induct \<Gamma>, auto)
@@ -173,9 +173,9 @@
apply (auto simp add: ty_binding_existence)
done
-lemma domains_append:
- shows "ty_domain (\<Gamma>@\<Delta>) = ((ty_domain \<Gamma>) \<union> (ty_domain \<Delta>))"
- and "trm_domain (\<Gamma>@\<Delta>) = ((trm_domain \<Gamma>) \<union> (trm_domain \<Delta>))"
+lemma doms_append:
+ shows "ty_dom (\<Gamma>@\<Delta>) = ((ty_dom \<Gamma>) \<union> (ty_dom \<Delta>))"
+ and "trm_dom (\<Gamma>@\<Delta>) = ((trm_dom \<Gamma>) \<union> (trm_dom \<Delta>))"
by (induct \<Gamma>, auto)
lemma ty_vrs_prm_simp:
@@ -184,15 +184,15 @@
shows "pi\<bullet>S = S"
by (induct S rule: ty.induct) (auto simp add: calc_atm)
-lemma fresh_ty_domain_cons:
+lemma fresh_ty_dom_cons:
fixes X::"tyvrs"
- shows "X\<sharp>(ty_domain (Y#\<Gamma>)) = (X\<sharp>(tyvrs_of Y) \<and> X\<sharp>(ty_domain \<Gamma>))"
+ shows "X\<sharp>(ty_dom (Y#\<Gamma>)) = (X\<sharp>(tyvrs_of Y) \<and> X\<sharp>(ty_dom \<Gamma>))"
apply (nominal_induct rule:binding.strong_induct)
apply (auto)
apply (simp add: fresh_def supp_def eqvts)
- apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_domains)
+ apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms)
apply (simp add: fresh_def supp_def eqvts)
- apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_domains)+
+ apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms)+
done
lemma tyvrs_fresh:
@@ -206,26 +206,26 @@
apply (fresh_guess)+
done
-lemma fresh_domain:
+lemma fresh_dom:
fixes X::"tyvrs"
assumes a: "X\<sharp>\<Gamma>"
- shows "X\<sharp>(ty_domain \<Gamma>)"
+ shows "X\<sharp>(ty_dom \<Gamma>)"
using a
apply(induct \<Gamma>)
apply(simp add: fresh_set_empty)
-apply(simp only: fresh_ty_domain_cons)
+apply(simp only: fresh_ty_dom_cons)
apply(auto simp add: fresh_prod fresh_list_cons tyvrs_fresh)
done
text {* Not all lists of type @{typ "env"} are well-formed. One condition
requires that in @{term "TVarB X S#\<Gamma>"} all free variables of @{term "S"} must be
- in the @{term "ty_domain"} of @{term "\<Gamma>"}, that is @{term "S"} must be @{text "closed"}
+ in the @{term "ty_dom"} of @{term "\<Gamma>"}, that is @{term "S"} must be @{text "closed"}
in @{term "\<Gamma>"}. The set of free variables of @{term "S"} is the
@{text "support"} of @{term "S"}. *}
constdefs
"closed_in" :: "ty \<Rightarrow> env \<Rightarrow> bool" ("_ closed'_in _" [100,100] 100)
- "S closed_in \<Gamma> \<equiv> (supp S)\<subseteq>(ty_domain \<Gamma>)"
+ "S closed_in \<Gamma> \<equiv> (supp S)\<subseteq>(ty_dom \<Gamma>)"
lemma closed_in_eqvt[eqvt]:
fixes pi::"tyvrs prm"
@@ -251,10 +251,10 @@
shows "x \<sharp> T"
by (simp add: fresh_def supp_def ty_vrs_prm_simp)
-lemma ty_domain_vrs_prm_simp:
+lemma ty_dom_vrs_prm_simp:
fixes pi::"vrs prm"
and \<Gamma>::"env"
- shows "(ty_domain (pi\<bullet>\<Gamma>)) = (ty_domain \<Gamma>)"
+ shows "(ty_dom (pi\<bullet>\<Gamma>)) = (ty_dom \<Gamma>)"
apply(induct \<Gamma>)
apply (simp add: eqvts)
apply(simp add: tyvrs_vrs_prm_simp)
@@ -265,7 +265,7 @@
assumes a: "S closed_in \<Gamma>"
shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)"
using a
-by (simp add: closed_in_def ty_domain_vrs_prm_simp ty_vrs_prm_simp)
+by (simp add: closed_in_def ty_dom_vrs_prm_simp ty_vrs_prm_simp)
lemma fresh_vrs_of:
fixes x::"vrs"
@@ -273,16 +273,16 @@
by (nominal_induct b rule: binding.strong_induct)
(simp_all add: fresh_singleton [OF pt_vrs_inst at_vrs_inst] fresh_set_empty ty_vrs_fresh fresh_atm)
-lemma fresh_trm_domain:
+lemma fresh_trm_dom:
fixes x::"vrs"
- shows "x\<sharp> trm_domain \<Gamma> = x\<sharp>\<Gamma>"
+ shows "x\<sharp> trm_dom \<Gamma> = x\<sharp>\<Gamma>"
by (induct \<Gamma>)
(simp_all add: fresh_set_empty fresh_list_cons
fresh_fin_union [OF pt_vrs_inst at_vrs_inst fs_vrs_inst]
- finite_domains finite_vrs fresh_vrs_of fresh_list_nil)
+ finite_doms finite_vrs fresh_vrs_of fresh_list_nil)
-lemma closed_in_fresh: "(X::tyvrs) \<sharp> ty_domain \<Gamma> \<Longrightarrow> T closed_in \<Gamma> \<Longrightarrow> X \<sharp> T"
- by (auto simp add: closed_in_def fresh_def ty_domain_supp)
+lemma closed_in_fresh: "(X::tyvrs) \<sharp> ty_dom \<Gamma> \<Longrightarrow> T closed_in \<Gamma> \<Longrightarrow> X \<sharp> T"
+ by (auto simp add: closed_in_def fresh_def ty_dom_supp)
text {* Now validity of a context is a straightforward inductive definition. *}
@@ -290,15 +290,18 @@
valid_rel :: "env \<Rightarrow> bool" ("\<turnstile> _ ok" [100] 100)
where
valid_nil[simp]: "\<turnstile> [] ok"
-| valid_consT[simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; X\<sharp>(ty_domain \<Gamma>); T closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<turnstile> (TVarB X T#\<Gamma>) ok"
-| valid_cons [simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; x\<sharp>(trm_domain \<Gamma>); T closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<turnstile> (VarB x T#\<Gamma>) ok"
+| valid_consT[simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; X\<sharp>(ty_dom \<Gamma>); T closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<turnstile> (TVarB X T#\<Gamma>) ok"
+| valid_cons [simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; x\<sharp>(trm_dom \<Gamma>); T closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<turnstile> (VarB x T#\<Gamma>) ok"
equivariance valid_rel
declare binding.inject [simp add]
declare trm.inject [simp add]
-inductive_cases validE[elim]: "\<turnstile> (TVarB X T#\<Gamma>) ok" "\<turnstile> (VarB x T#\<Gamma>) ok" "\<turnstile> (b#\<Gamma>) ok"
+inductive_cases validE[elim]:
+ "\<turnstile> (TVarB X T#\<Gamma>) ok"
+ "\<turnstile> (VarB x T#\<Gamma>) ok"
+ "\<turnstile> (b#\<Gamma>) ok"
declare binding.inject [simp del]
declare trm.inject [simp del]
@@ -321,12 +324,12 @@
using a b
proof(induct \<Delta>)
case Nil
- then show ?case by (auto elim: validE intro: valid_cons simp add: domains_append closed_in_def)
+ then show ?case by (auto elim: validE intro: valid_cons simp add: doms_append closed_in_def)
next
case (Cons a \<Gamma>')
then show ?case
by (nominal_induct a rule:binding.strong_induct)
- (auto elim: validE intro!: valid_cons simp add: domains_append closed_in_def)
+ (auto elim: validE intro!: valid_cons simp add: doms_append closed_in_def)
qed
text {* Well-formed contexts have a unique type-binding for a type-variable. *}
@@ -342,14 +345,14 @@
case (valid_consT \<Gamma> X' T')
moreover
{ fix \<Gamma>'::"env"
- assume a: "X'\<sharp>(ty_domain \<Gamma>')"
+ assume a: "X'\<sharp>(ty_dom \<Gamma>')"
have "\<not>(\<exists>T.(TVarB X' T)\<in>(set \<Gamma>'))" using a
proof (induct \<Gamma>')
case (Cons Y \<Gamma>')
thus "\<not> (\<exists>T.(TVarB X' T)\<in>set(Y#\<Gamma>'))"
- by (simp add: fresh_ty_domain_cons
+ by (simp add: fresh_ty_dom_cons
fresh_fin_union[OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst]
- finite_vrs finite_domains,
+ finite_vrs finite_doms,
auto simp add: fresh_atm fresh_singleton [OF pt_tyvrs_inst at_tyvrs_inst])
qed (simp)
}
@@ -367,13 +370,13 @@
case (valid_cons \<Gamma> x' T')
moreover
{ fix \<Gamma>'::"env"
- assume a: "x'\<sharp>(trm_domain \<Gamma>')"
+ assume a: "x'\<sharp>(trm_dom \<Gamma>')"
have "\<not>(\<exists>T.(VarB x' T)\<in>(set \<Gamma>'))" using a
proof (induct \<Gamma>')
case (Cons y \<Gamma>')
thus "\<not> (\<exists>T.(VarB x' T)\<in>set(y#\<Gamma>'))"
by (simp add: fresh_fin_union[OF pt_vrs_inst at_vrs_inst fs_vrs_inst]
- finite_vrs finite_domains,
+ finite_vrs finite_doms,
auto simp add: fresh_atm fresh_singleton [OF pt_vrs_inst at_vrs_inst])
qed (simp)
}
@@ -401,7 +404,7 @@
"(Tvar X)[Y \<mapsto> T]\<^sub>\<tau> = (if X=Y then T else Tvar X)"
| "(Top)[Y \<mapsto> T]\<^sub>\<tau> = Top"
| "(T\<^isub>1 \<rightarrow> T\<^isub>2)[Y \<mapsto> T]\<^sub>\<tau> = T\<^isub>1[Y \<mapsto> T]\<^sub>\<tau> \<rightarrow> T\<^isub>2[Y \<mapsto> T]\<^sub>\<tau>"
-| "\<lbrakk>X\<sharp>(Y,T); X\<sharp>T\<^isub>1\<rbrakk> \<Longrightarrow> (\<forall>X<:T\<^isub>1. T\<^isub>2)[Y \<mapsto> T]\<^sub>\<tau> = (\<forall>X<:T\<^isub>1[Y \<mapsto> T]\<^sub>\<tau>. T\<^isub>2[Y \<mapsto> T]\<^sub>\<tau>)"
+| "X\<sharp>(Y,T,T\<^isub>1) \<Longrightarrow> (\<forall>X<:T\<^isub>1. T\<^isub>2)[Y \<mapsto> T]\<^sub>\<tau> = (\<forall>X<:T\<^isub>1[Y \<mapsto> T]\<^sub>\<tau>. T\<^isub>2[Y \<mapsto> T]\<^sub>\<tau>)"
apply (finite_guess)+
apply (rule TrueI)+
apply (simp add: abs_fresh)
@@ -424,8 +427,8 @@
lemma type_subst_fresh:
fixes X::"tyvrs"
- assumes "X \<sharp> T" and "X \<sharp> P"
- shows "X \<sharp> T[Y \<mapsto> P]\<^sub>\<tau>"
+ assumes "X\<sharp>T" and "X\<sharp>P"
+ shows "X\<sharp>T[Y \<mapsto> P]\<^sub>\<tau>"
using assms
by (nominal_induct T avoiding: X Y P rule:ty.strong_induct)
(auto simp add: abs_fresh)
@@ -437,17 +440,18 @@
by (nominal_induct T avoiding: X T' rule: ty.strong_induct)
(auto simp add: fresh_atm abs_fresh fresh_nat)
-lemma type_subst_identity: "X \<sharp> T \<Longrightarrow> T[X \<mapsto> U]\<^sub>\<tau> = T"
+lemma type_subst_identity:
+ "X\<sharp>T \<Longrightarrow> T[X \<mapsto> U]\<^sub>\<tau> = T"
by (nominal_induct T avoiding: X U rule: ty.strong_induct)
(simp_all add: fresh_atm abs_fresh)
lemma type_substitution_lemma:
- "X \<noteq> Y \<Longrightarrow> X \<sharp> L \<Longrightarrow> M[X \<mapsto> N]\<^sub>\<tau>[Y \<mapsto> L]\<^sub>\<tau> = M[Y \<mapsto> L]\<^sub>\<tau>[X \<mapsto> N[Y \<mapsto> L]\<^sub>\<tau>]\<^sub>\<tau>"
+ "X \<noteq> Y \<Longrightarrow> X\<sharp>L \<Longrightarrow> M[X \<mapsto> N]\<^sub>\<tau>[Y \<mapsto> L]\<^sub>\<tau> = M[Y \<mapsto> L]\<^sub>\<tau>[X \<mapsto> N[Y \<mapsto> L]\<^sub>\<tau>]\<^sub>\<tau>"
by (nominal_induct M avoiding: X Y N L rule: ty.strong_induct)
(auto simp add: type_subst_fresh type_subst_identity)
lemma type_subst_rename:
- "Y \<sharp> T \<Longrightarrow> ([(Y, X)] \<bullet> T)[Y \<mapsto> U]\<^sub>\<tau> = T[X \<mapsto> U]\<^sub>\<tau>"
+ "Y\<sharp>T \<Longrightarrow> ([(Y,X)]\<bullet>T)[Y \<mapsto> U]\<^sub>\<tau> = T[X \<mapsto> U]\<^sub>\<tau>"
by (nominal_induct T avoiding: X Y U rule: ty.strong_induct)
(simp_all add: fresh_atm calc_atm abs_fresh fresh_aux)
@@ -460,15 +464,15 @@
lemma binding_subst_fresh:
fixes X::"tyvrs"
- assumes "X \<sharp> a"
- and "X \<sharp> P"
- shows "X \<sharp> a[Y \<mapsto> P]\<^sub>b"
+ assumes "X\<sharp>a"
+ and "X\<sharp>P"
+ shows "X\<sharp>a[Y \<mapsto> P]\<^sub>b"
using assms
by (nominal_induct a rule: binding.strong_induct)
(auto simp add: type_subst_fresh)
lemma binding_subst_identity:
- shows "X \<sharp> B \<Longrightarrow> B[X \<mapsto> U]\<^sub>b = B"
+ shows "X\<sharp>B \<Longrightarrow> B[X \<mapsto> U]\<^sub>b = B"
by (induct B rule: binding.induct)
(simp_all add: fresh_atm type_subst_identity)
@@ -481,9 +485,9 @@
lemma ctxt_subst_fresh':
fixes X::"tyvrs"
- assumes "X \<sharp> \<Gamma>"
- and "X \<sharp> P"
- shows "X \<sharp> \<Gamma>[Y \<mapsto> P]\<^sub>e"
+ assumes "X\<sharp>\<Gamma>"
+ and "X\<sharp>P"
+ shows "X\<sharp>\<Gamma>[Y \<mapsto> P]\<^sub>e"
using assms
by (induct \<Gamma>)
(auto simp add: fresh_list_cons binding_subst_fresh)
@@ -494,7 +498,7 @@
lemma ctxt_subst_mem_VarB: "VarB x T \<in> set \<Gamma> \<Longrightarrow> VarB x (T[Y \<mapsto> U]\<^sub>\<tau>) \<in> set (\<Gamma>[Y \<mapsto> U]\<^sub>e)"
by (induct \<Gamma>) auto
-lemma ctxt_subst_identity: "X \<sharp> \<Gamma> \<Longrightarrow> \<Gamma>[X \<mapsto> U]\<^sub>e = \<Gamma>"
+lemma ctxt_subst_identity: "X\<sharp>\<Gamma> \<Longrightarrow> \<Gamma>[X \<mapsto> U]\<^sub>e = \<Gamma>"
by (induct \<Gamma>) (simp_all add: fresh_list_cons binding_subst_identity)
lemma ctxt_subst_append: "(\<Delta> @ \<Gamma>)[X \<mapsto> T]\<^sub>e = \<Delta>[X \<mapsto> T]\<^sub>e @ \<Gamma>[X \<mapsto> T]\<^sub>e"
@@ -515,11 +519,13 @@
done
lemma subst_trm_fresh_tyvar:
- "(X::tyvrs) \<sharp> t \<Longrightarrow> X \<sharp> u \<Longrightarrow> X \<sharp> t[x \<mapsto> u]"
+ fixes X::"tyvrs"
+ shows "X\<sharp>t \<Longrightarrow> X\<sharp>u \<Longrightarrow> X\<sharp>t[x \<mapsto> u]"
by (nominal_induct t avoiding: x u rule: trm.strong_induct)
(auto simp add: trm.fresh abs_fresh)
-lemma subst_trm_fresh_var: "x \<sharp> u \<Longrightarrow> x \<sharp> t[x \<mapsto> u]"
+lemma subst_trm_fresh_var:
+ "x\<sharp>u \<Longrightarrow> x\<sharp>t[x \<mapsto> u]"
by (nominal_induct t avoiding: x u rule: trm.strong_induct)
(simp_all add: abs_fresh fresh_atm ty_vrs_fresh)
@@ -538,7 +544,7 @@
(perm_simp add: fresh_left)+
lemma subst_trm_rename:
- "y \<sharp> t \<Longrightarrow> ([(y, x)] \<bullet> t)[y \<mapsto> u] = t[x \<mapsto> u]"
+ "y\<sharp>t \<Longrightarrow> ([(y, x)] \<bullet> t)[y \<mapsto> u] = t[x \<mapsto> u]"
by (nominal_induct t avoiding: x y u rule: trm.strong_induct)
(simp_all add: fresh_atm calc_atm abs_fresh fresh_aux ty_vrs_fresh perm_fresh_fresh)
@@ -558,12 +564,13 @@
done
lemma subst_trm_ty_fresh:
- "(X::tyvrs) \<sharp> t \<Longrightarrow> X \<sharp> T \<Longrightarrow> X \<sharp> t[Y \<mapsto>\<^sub>\<tau> T]"
+ fixes X::"tyvrs"
+ shows "X\<sharp>t \<Longrightarrow> X\<sharp>T \<Longrightarrow> X\<sharp>t[Y \<mapsto>\<^sub>\<tau> T]"
by (nominal_induct t avoiding: Y T rule: trm.strong_induct)
(auto simp add: abs_fresh type_subst_fresh)
lemma subst_trm_ty_fresh':
- "X \<sharp> T \<Longrightarrow> X \<sharp> t[X \<mapsto>\<^sub>\<tau> T]"
+ "X\<sharp>T \<Longrightarrow> X\<sharp>t[X \<mapsto>\<^sub>\<tau> T]"
by (nominal_induct t avoiding: X T rule: trm.strong_induct)
(simp_all add: abs_fresh fresh_type_subst_fresh fresh_atm)
@@ -582,7 +589,7 @@
(perm_simp add: fresh_left subst_eqvt')+
lemma subst_trm_ty_rename:
- "Y \<sharp> t \<Longrightarrow> ([(Y, X)] \<bullet> t)[Y \<mapsto>\<^sub>\<tau> U] = t[X \<mapsto>\<^sub>\<tau> U]"
+ "Y\<sharp>t \<Longrightarrow> ([(Y, X)] \<bullet> t)[Y \<mapsto>\<^sub>\<tau> U] = t[X \<mapsto>\<^sub>\<tau> U]"
by (nominal_induct t avoiding: X Y U rule: trm.strong_induct)
(simp_all add: fresh_atm calc_atm abs_fresh fresh_aux type_subst_rename)
@@ -599,7 +606,7 @@
subtype_of :: "env \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_<:_" [100,100,100] 100)
where
SA_Top[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
-| SA_refl_TVar[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; X \<in> ty_domain \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Tvar X <: Tvar X"
+| SA_refl_TVar[intro]: "\<lbrakk>\<turnstile> \<Gamma> ok; X \<in> ty_dom \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Tvar X <: Tvar X"
| SA_trans_TVar[intro]: "\<lbrakk>(TVarB X S) \<in> set \<Gamma>; \<Gamma> \<turnstile> S <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Tvar X) <: T"
| SA_arrow[intro]: "\<lbrakk>\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (S\<^isub>1 \<rightarrow> S\<^isub>2) <: (T\<^isub>1 \<rightarrow> T\<^isub>2)"
| SA_all[intro]: "\<lbrakk>\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1; ((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: (\<forall>X<:T\<^isub>1. T\<^isub>2)"
@@ -623,7 +630,7 @@
next
case (SA_trans_TVar X S \<Gamma> T)
have "(TVarB X S)\<in>set \<Gamma>" by fact
- hence "X \<in> ty_domain \<Gamma>" by (rule ty_domain_inclusion)
+ hence "X \<in> ty_dom \<Gamma>" by (rule ty_dom_inclusion)
hence "(Tvar X) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp supp_atm)
moreover
have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by fact
@@ -638,23 +645,23 @@
shows "X\<sharp>S \<and> X\<sharp>T"
proof -
from a1 have "\<turnstile> \<Gamma> ok" by (rule subtype_implies_ok)
- with a2 have "X\<sharp>ty_domain(\<Gamma>)" by (simp add: fresh_domain)
+ with a2 have "X\<sharp>ty_dom(\<Gamma>)" by (simp add: fresh_dom)
moreover
from a1 have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by (rule subtype_implies_closed)
- hence "supp S \<subseteq> ((supp (ty_domain \<Gamma>))::tyvrs set)"
- and "supp T \<subseteq> ((supp (ty_domain \<Gamma>))::tyvrs set)" by (simp_all add: ty_domain_supp closed_in_def)
+ hence "supp S \<subseteq> ((supp (ty_dom \<Gamma>))::tyvrs set)"
+ and "supp T \<subseteq> ((supp (ty_dom \<Gamma>))::tyvrs set)" by (simp_all add: ty_dom_supp closed_in_def)
ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp add: supp_prod fresh_def)
qed
-lemma valid_ty_domain_fresh:
+lemma valid_ty_dom_fresh:
fixes X::"tyvrs"
assumes valid: "\<turnstile> \<Gamma> ok"
- shows "X\<sharp>(ty_domain \<Gamma>) = X\<sharp>\<Gamma>"
+ shows "X\<sharp>(ty_dom \<Gamma>) = X\<sharp>\<Gamma>"
using valid
apply induct
apply (simp add: fresh_list_nil fresh_set_empty)
apply (simp_all add: binding.fresh fresh_list_cons
- fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_domains fresh_atm)
+ fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms fresh_atm)
apply (auto simp add: closed_in_fresh)
done
@@ -662,7 +669,7 @@
nominal_inductive subtype_of
apply (simp_all add: abs_fresh)
- apply (fastsimp simp add: valid_ty_domain_fresh dest: subtype_implies_ok)
+ apply (fastsimp simp add: valid_ty_dom_fresh dest: subtype_implies_ok)
apply (force simp add: closed_in_fresh dest: subtype_implies_closed subtype_implies_ok)+
done
@@ -678,12 +685,12 @@
have ih_T\<^isub>1: "\<And>\<Gamma>. \<lbrakk>\<turnstile> \<Gamma> ok; T\<^isub>1 closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>1 <: T\<^isub>1" by fact
have ih_T\<^isub>2: "\<And>\<Gamma>. \<lbrakk>\<turnstile> \<Gamma> ok; T\<^isub>2 closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" by fact
have fresh_cond: "X\<sharp>\<Gamma>" by fact
- hence fresh_ty_domain: "X\<sharp>(ty_domain \<Gamma>)" by (simp add: fresh_domain)
+ hence fresh_ty_dom: "X\<sharp>(ty_dom \<Gamma>)" by (simp add: fresh_dom)
have "(\<forall>X<:T\<^isub>2. T\<^isub>1) closed_in \<Gamma>" by fact
hence closed\<^isub>T\<^isub>2: "T\<^isub>2 closed_in \<Gamma>" and closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in ((TVarB X T\<^isub>2)#\<Gamma>)"
by (auto simp add: closed_in_def ty.supp abs_supp)
have ok: "\<turnstile> \<Gamma> ok" by fact
- hence ok': "\<turnstile> ((TVarB X T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T\<^isub>2 fresh_ty_domain by simp
+ hence ok': "\<turnstile> ((TVarB X T\<^isub>2)#\<Gamma>) ok" using closed\<^isub>T\<^isub>2 fresh_ty_dom by simp
have "\<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" using ih_T\<^isub>2 closed\<^isub>T\<^isub>2 ok by simp
moreover
have "((TVarB X T\<^isub>2)#\<Gamma>) \<turnstile> T\<^isub>1 <: T\<^isub>1" using ih_T\<^isub>1 closed\<^isub>T\<^isub>1 ok' by simp
@@ -702,7 +709,7 @@
\isakeyword{auto}; \isakeyword{blast} would find it if we had not used
an explicit definition for @{text "closed_in_def"}. *}
apply(drule_tac x="(TVarB tyvrs ty2)#\<Gamma>" in meta_spec)
-apply(force dest: fresh_domain simp add: closed_in_def)
+apply(force dest: fresh_dom simp add: closed_in_def)
done
section {* Weakening *}
@@ -715,13 +722,13 @@
extends :: "env \<Rightarrow> env \<Rightarrow> bool" ("_ extends _" [100,100] 100)
"\<Delta> extends \<Gamma> \<equiv> \<forall>X Q. (TVarB X Q)\<in>set \<Gamma> \<longrightarrow> (TVarB X Q)\<in>set \<Delta>"
-lemma extends_ty_domain:
+lemma extends_ty_dom:
assumes a: "\<Delta> extends \<Gamma>"
- shows "ty_domain \<Gamma> \<subseteq> ty_domain \<Delta>"
+ shows "ty_dom \<Gamma> \<subseteq> ty_dom \<Delta>"
using a
apply (auto simp add: extends_def)
- apply (drule ty_domain_existence)
- apply (force simp add: ty_domain_inclusion)
+ apply (drule ty_dom_existence)
+ apply (force simp add: ty_dom_inclusion)
done
lemma extends_closed:
@@ -729,7 +736,7 @@
and a2: "\<Delta> extends \<Gamma>"
shows "T closed_in \<Delta>"
using a1 a2
- by (auto dest: extends_ty_domain simp add: closed_in_def)
+ by (auto dest: extends_ty_dom simp add: closed_in_def)
lemma extends_memb:
assumes a: "\<Delta> extends \<Gamma>"
@@ -763,18 +770,18 @@
ultimately show "\<Delta> \<turnstile> Tvar X <: T" using ok by force
next
case (SA_refl_TVar \<Gamma> X)
- have lh_drv_prem: "X \<in> ty_domain \<Gamma>" by fact
+ have lh_drv_prem: "X \<in> ty_dom \<Gamma>" by fact
have "\<turnstile> \<Delta> ok" by fact
moreover
have "\<Delta> extends \<Gamma>" by fact
- hence "X \<in> ty_domain \<Delta>" using lh_drv_prem by (force dest: extends_ty_domain)
+ hence "X \<in> ty_dom \<Delta>" using lh_drv_prem by (force dest: extends_ty_dom)
ultimately show "\<Delta> \<turnstile> Tvar X <: Tvar X" by force
next
case (SA_arrow \<Gamma> T\<^isub>1 S\<^isub>1 S\<^isub>2 T\<^isub>2) thus "\<Delta> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2" by blast
next
case (SA_all \<Gamma> T\<^isub>1 S\<^isub>1 X S\<^isub>2 T\<^isub>2)
have fresh_cond: "X\<sharp>\<Delta>" by fact
- hence fresh_domain: "X\<sharp>(ty_domain \<Delta>)" by (simp add: fresh_domain)
+ hence fresh_dom: "X\<sharp>(ty_dom \<Delta>)" by (simp add: fresh_dom)
have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
have ih\<^isub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((TVarB X T\<^isub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^isub>2 <: T\<^isub>2" by fact
have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
@@ -782,7 +789,7 @@
have ok: "\<turnstile> \<Delta> ok" by fact
have ext: "\<Delta> extends \<Gamma>" by fact
have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed)
- hence "\<turnstile> ((TVarB X T\<^isub>1)#\<Delta>) ok" using fresh_domain ok by force
+ hence "\<turnstile> ((TVarB X T\<^isub>1)#\<Delta>) ok" using fresh_dom ok by force
moreover
have "((TVarB X T\<^isub>1)#\<Delta>) extends ((TVarB X T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
ultimately have "((TVarB X T\<^isub>1)#\<Delta>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using ih\<^isub>2 by simp
@@ -802,7 +809,7 @@
proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of.strong_induct)
case (SA_all \<Gamma> T\<^isub>1 S\<^isub>1 X S\<^isub>2 T\<^isub>2)
have fresh_cond: "X\<sharp>\<Delta>" by fact
- hence fresh_domain: "X\<sharp>(ty_domain \<Delta>)" by (simp add: fresh_domain)
+ hence fresh_dom: "X\<sharp>(ty_dom \<Delta>)" by (simp add: fresh_dom)
have ih\<^isub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
have ih\<^isub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((TVarB X T\<^isub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^isub>2 <: T\<^isub>2" by fact
have lh_drv_prem: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" by fact
@@ -810,14 +817,14 @@
have ok: "\<turnstile> \<Delta> ok" by fact
have ext: "\<Delta> extends \<Gamma>" by fact
have "T\<^isub>1 closed_in \<Delta>" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed)
- hence "\<turnstile> ((TVarB X T\<^isub>1)#\<Delta>) ok" using fresh_domain ok by force
+ hence "\<turnstile> ((TVarB X T\<^isub>1)#\<Delta>) ok" using fresh_dom ok by force
moreover
have "((TVarB X T\<^isub>1)#\<Delta>) extends ((TVarB X T\<^isub>1)#\<Gamma>)" using ext by (force simp add: extends_def)
ultimately have "((TVarB X T\<^isub>1)#\<Delta>) \<turnstile> S\<^isub>2 <: T\<^isub>2" using ih\<^isub>2 by simp
moreover
have "\<Delta> \<turnstile> T\<^isub>1 <: S\<^isub>1" using ok ext ih\<^isub>1 by simp
ultimately show "\<Delta> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: (\<forall>X<:T\<^isub>1. T\<^isub>2)" using ok by (force intro: SA_all)
-qed (blast intro: extends_closed extends_memb dest: extends_ty_domain)+
+qed (blast intro: extends_closed extends_memb dest: extends_ty_dom)+
section {* Transitivity and Narrowing *}
@@ -831,38 +838,11 @@
declare ty.inject [simp del]
lemma S_ForallE_left:
- shows "\<lbrakk>\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: T; X\<sharp>\<Gamma>; X\<sharp>S\<^isub>1\<rbrakk>
+ shows "\<lbrakk>\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: T; X\<sharp>\<Gamma>; X\<sharp>S\<^isub>1; X\<sharp>T\<rbrakk>
\<Longrightarrow> T = Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T = (\<forall>X<:T\<^isub>1. T\<^isub>2) \<and> \<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<and> ((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2)"
- apply(frule subtype_implies_ok)
- apply(ind_cases "\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: T")
- apply(auto simp add: ty.inject alpha)
- apply(rule_tac x="[(X,Xa)]\<bullet>T\<^isub>2" in exI)
- apply(rule conjI)
- apply(rule sym)
- apply(rule pt_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst])
- apply(rule pt_tyvrs3)
- apply(simp)
- apply(rule at_ds5[OF at_tyvrs_inst])
- apply(rule conjI)
- apply(simp add: pt_fresh_left[OF pt_tyvrs_inst, OF at_tyvrs_inst] calc_atm)
- apply(drule_tac \<Gamma>="((TVarB Xa T\<^isub>1)#\<Gamma>)" in subtype_implies_closed)+
- apply(simp add: closed_in_def)
- apply(drule fresh_domain)+
- apply(simp add: fresh_def)
- apply(subgoal_tac "X \<notin> (insert Xa (ty_domain \<Gamma>))")(*A*)
- apply(force)
- (*A*)apply(simp add: at_fin_set_supp[OF at_tyvrs_inst, OF finite_domains(1)])
- (* 2nd conjunct *)apply(frule_tac X="X" in subtype_implies_fresh)
- apply(assumption)
- apply (frule_tac \<Gamma>="TVarB Xa T\<^isub>1 # \<Gamma>" in subtype_implies_ok)
- apply (erule validE)
- apply (simp add: valid_ty_domain_fresh)
- apply(drule_tac X="Xa" in subtype_implies_fresh)
- apply(assumption)
- apply(drule_tac pi="[(X,Xa)]" in subtype_of.eqvt(2))
- apply(simp add: calc_atm)
- apply(simp add: pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst])
- done
+apply(erule subtype_of.strong_cases[where X="X"])
+apply(auto simp add: abs_fresh ty.inject alpha)
+done
text {* Next we prove the transitivity and narrowing for the subtyping-relation.
The POPLmark-paper says the following:
@@ -898,75 +878,38 @@
and subtype_narrow: "(\<Delta>@[(TVarB X Q)]@\<Gamma>)\<turnstile>M<:N \<Longrightarrow> \<Gamma>\<turnstile>P<:Q \<Longrightarrow> (\<Delta>@[(TVarB X P)]@\<Gamma>)\<turnstile>M<:N"
proof (induct Q arbitrary: \<Gamma> S T \<Delta> X P M N taking: "size_ty" rule: measure_induct_rule)
case (less Q)
- --{* \begin{minipage}[t]{0.9\textwidth}
- First we mention the induction hypotheses of the outer induction for later
- reference:\end{minipage}*}
have IH_trans:
"\<And>Q' \<Gamma> S T. \<lbrakk>size_ty Q' < size_ty Q; \<Gamma>\<turnstile>S<:Q'; \<Gamma>\<turnstile>Q'<:T\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>S<:T" by fact
have IH_narrow:
"\<And>Q' \<Delta> \<Gamma> X M N P. \<lbrakk>size_ty Q' < size_ty Q; (\<Delta>@[(TVarB X Q')]@\<Gamma>)\<turnstile>M<:N; \<Gamma>\<turnstile>P<:Q'\<rbrakk>
\<Longrightarrow> (\<Delta>@[(TVarB X P)]@\<Gamma>)\<turnstile>M<:N" by fact
- --{* \begin{minipage}[t]{0.9\textwidth}
- We proceed with the transitivity proof as an auxiliary lemma, because it needs
- to be referenced in the narrowing proof.\end{minipage}*}
- have transitivity_aux:
- "\<And>\<Gamma> S T. \<lbrakk>\<Gamma> \<turnstile> S <: Q; \<Gamma> \<turnstile> Q <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
- proof -
- fix \<Gamma>' S' T
- assume "\<Gamma>' \<turnstile> S' <: Q" --{* left-hand derivation *}
- and "\<Gamma>' \<turnstile> Q <: T" --{* right-hand derivation *}
- thus "\<Gamma>' \<turnstile> S' <: T"
- proof (nominal_induct \<Gamma>' S' Q\<equiv>Q rule: subtype_of.strong_induct)
+
+ { fix \<Gamma> S T
+ have "\<lbrakk>\<Gamma> \<turnstile> S <: Q; \<Gamma> \<turnstile> Q <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T"
+ proof (induct \<Gamma> S Q\<equiv>Q rule: subtype_of.induct)
case (SA_Top \<Gamma> S)
- --{* \begin{minipage}[t]{0.9\textwidth}
- In this case the left-hand derivation is @{term "\<Gamma> \<turnstile> S <: Top"}, giving
- us @{term "\<turnstile> \<Gamma> ok"} and @{term "S closed_in \<Gamma>"}. This case is straightforward,
- because the right-hand derivation must be of the form @{term "\<Gamma> \<turnstile> Top <: Top"}
- giving us the equation @{term "T = Top"}.\end{minipage}*}
- hence rh_drv: "\<Gamma> \<turnstile> Top <: T" by simp
- hence T_inst: "T = Top" by (auto elim: S_TopE)
+ then have rh_drv: "\<Gamma> \<turnstile> Top <: T" by simp
+ then have T_inst: "T = Top" by (auto elim: S_TopE)
from `\<turnstile> \<Gamma> ok` and `S closed_in \<Gamma>`
- have "\<Gamma> \<turnstile> S <: Top" by (simp add: subtype_of.SA_Top)
- thus "\<Gamma> \<turnstile> S <: T" using T_inst by simp
+ have "\<Gamma> \<turnstile> S <: Top" by auto
+ then show "\<Gamma> \<turnstile> S <: T" using T_inst by simp
next
case (SA_trans_TVar Y U \<Gamma>)
- -- {* \begin{minipage}[t]{0.9\textwidth}
- In this case the left-hand derivation is @{term "\<Gamma> \<turnstile> Tvar Y <: Q"}
- with @{term "S = Tvar Y"}. We have therefore @{term "(Y,U)"}
- is in @{term "\<Gamma>"} and by inner induction hypothesis that @{term "\<Gamma> \<turnstile> U <: T"}.
- By @{text "S_Var"} follows @{term "\<Gamma> \<turnstile> Tvar Y <: T"}.\end{minipage}*}
- hence IH_inner: "\<Gamma> \<turnstile> U <: T" by simp
+ then have IH_inner: "\<Gamma> \<turnstile> U <: T" by simp
have "(TVarB Y U) \<in> set \<Gamma>" by fact
- with IH_inner show "\<Gamma> \<turnstile> Tvar Y <: T" by (simp add: subtype_of.SA_trans_TVar)
+ with IH_inner show "\<Gamma> \<turnstile> Tvar Y <: T" by auto
next
case (SA_refl_TVar \<Gamma> X)
- --{* \begin{minipage}[t]{0.9\textwidth}
- In this case the left-hand derivation is @{term "\<Gamma>\<turnstile>(Tvar X) <: (Tvar X)"} with
- @{term "Q=Tvar X"}. The goal then follows immediately from the right-hand
- derivation.\end{minipage}*}
- thus "\<Gamma> \<turnstile> Tvar X <: T" by simp
+ then show "\<Gamma> \<turnstile> Tvar X <: T" by simp
next
case (SA_arrow \<Gamma> Q\<^isub>1 S\<^isub>1 S\<^isub>2 Q\<^isub>2)
- --{* \begin{minipage}[t]{0.9\textwidth}
- In this case the left-hand derivation is @{term "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: Q\<^isub>1 \<rightarrow> Q\<^isub>2"} with
- @{term "S\<^isub>1\<rightarrow>S\<^isub>2=S"} and @{term "Q\<^isub>1\<rightarrow>Q\<^isub>2=Q"}. We know that the @{text "size_ty"} of
- @{term Q\<^isub>1} and @{term Q\<^isub>2} is smaller than that of @{term Q};
- so we can apply the outer induction hypotheses for @{term Q\<^isub>1} and @{term Q\<^isub>2}.
- We also have the sub-derivations @{term "\<Gamma>\<turnstile>Q\<^isub>1<:S\<^isub>1"} and @{term "\<Gamma>\<turnstile>S\<^isub>2<:Q\<^isub>2"}.
- The right-hand derivation is @{term "\<Gamma> \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: T"}. There exist types
- @{text "T\<^isub>1,T\<^isub>2"} such that @{term "T=Top \<or> T=T\<^isub>1\<rightarrow>T\<^isub>2"}. The @{term "Top"}-case is
- straightforward once we know @{term "(S\<^isub>1 \<rightarrow> S\<^isub>2) closed_in \<Gamma>"} and @{term "\<turnstile> \<Gamma> ok"}.
- In the other case we have the sub-derivations @{term "\<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1"} and @{term "\<Gamma>\<turnstile>Q\<^isub>2<:T\<^isub>2"}.
- Using the outer induction hypothesis for transitivity we can derive @{term "\<Gamma>\<turnstile>T\<^isub>1<:S\<^isub>1"}
- and @{term "\<Gamma>\<turnstile>S\<^isub>2<:T\<^isub>2"}. By rule @{text "S_Arrow"} follows @{term "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2"},
- which is @{term "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>"}.\end{minipage}*}
- hence rh_drv: "\<Gamma> \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: T" by simp
+ then have rh_drv: "\<Gamma> \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: T" by simp
from `Q\<^isub>1 \<rightarrow> Q\<^isub>2 = Q`
have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q" by auto
have lh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> Q\<^isub>1 <: S\<^isub>1" by fact
have lh_drv_prm\<^isub>2: "\<Gamma> \<turnstile> S\<^isub>2 <: Q\<^isub>2" by fact
from rh_drv have "T=Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2 \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> \<Gamma>\<turnstile>Q\<^isub>2<:T\<^isub>2)"
- by (auto elim: S_ArrowE_left)
+ by (auto elim: S_ArrowE_left)
moreover
have "S\<^isub>1 closed_in \<Gamma>" and "S\<^isub>2 closed_in \<Gamma>"
using lh_drv_prm\<^isub>1 lh_drv_prm\<^isub>2 by (simp_all add: subtype_implies_closed)
@@ -974,7 +917,7 @@
moreover
have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok)
moreover
- { assume "\<exists>T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2 \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> \<Gamma>\<turnstile>Q\<^isub>2<:T\<^isub>2"
+ { assume "\<exists>T\<^isub>1 T\<^isub>2. T = T\<^isub>1\<rightarrow>T\<^isub>2 \<and> \<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1 \<and> \<Gamma> \<turnstile> Q\<^isub>2 <: T\<^isub>2"
then obtain T\<^isub>1 T\<^isub>2
where T_inst: "T = T\<^isub>1 \<rightarrow> T\<^isub>2"
and rh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1"
@@ -984,46 +927,26 @@
moreover
from IH_trans[of "Q\<^isub>2"]
have "\<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2" using Q\<^isub>1\<^isub>2_less rh_drv_prm\<^isub>2 lh_drv_prm\<^isub>2 by simp
- ultimately have "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2" by (simp add: subtype_of.SA_arrow)
- hence "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" using T_inst by simp
+ ultimately have "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2" by auto
+ then have "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" using T_inst by simp
}
ultimately show "\<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T" by blast
next
case (SA_all \<Gamma> Q\<^isub>1 S\<^isub>1 X S\<^isub>2 Q\<^isub>2)
- --{* \begin{minipage}[t]{0.9\textwidth}
- In this case the left-hand derivation is @{term "\<Gamma>\<turnstile>(\<forall>X<:S\<^isub>1. S\<^isub>2) <: (\<forall>X<:Q\<^isub>1. Q\<^isub>2)"} with
- @{term "(\<forall>X<:S\<^isub>1. S\<^isub>2)=S"} and @{term "(\<forall>X<:Q\<^isub>1. Q\<^isub>2)=Q"}. We therefore have the sub-derivations
- @{term "\<Gamma>\<turnstile>Q\<^isub>1<:S\<^isub>1"} and @{term "((TVarB X Q\<^isub>1)#\<Gamma>)\<turnstile>S\<^isub>2<:Q\<^isub>2"}. Since @{term "X"} is a binder, we
- assume that it is sufficiently fresh; in particular we have the freshness conditions
- @{term "X\<sharp>\<Gamma>"} and @{term "X\<sharp>Q\<^isub>1"} (these assumptions are provided by the strong
- induction-rule @{text "subtype_of_induct"}). We know that the @{text "size_ty"} of
- @{term Q\<^isub>1} and @{term Q\<^isub>2} is smaller than that of @{term Q};
- so we can apply the outer induction hypotheses for @{term Q\<^isub>1} and @{term Q\<^isub>2}.
- The right-hand derivation is @{term "\<Gamma> \<turnstile> (\<forall>X<:Q\<^isub>1. Q\<^isub>2) <: T"}. Since @{term "X\<sharp>\<Gamma>"}
- and @{term "X\<sharp>Q\<^isub>1"} there exists types @{text "T\<^isub>1,T\<^isub>2"} such that
- @{term "T=Top \<or> T=(\<forall>X<:T\<^isub>1. T\<^isub>2)"}. The @{term "Top"}-case is straightforward once we know
- @{term "(\<forall>X<:S\<^isub>1. S\<^isub>2) closed_in \<Gamma>"} and @{term "\<turnstile> \<Gamma> ok"}. In the other case we have
- the sub-derivations @{term "\<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1"} and @{term "((TVarB X T\<^isub>1)#\<Gamma>)\<turnstile>Q\<^isub>2<:T\<^isub>2"}. Using the outer
- induction hypothesis for transitivity we can derive @{term "\<Gamma>\<turnstile>T\<^isub>1<:S\<^isub>1"}. From the outer
- induction for narrowing we get @{term "((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2"} and then using again
- induction for transitivity we obtain @{term "((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2"}. By rule
- @{text "S_Forall"} and the freshness condition @{term "X\<sharp>\<Gamma>"} follows
- @{term "\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: (\<forall>X<:T\<^isub>1. T\<^isub>2)"}, which is @{term "\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: T\<^isub>"}.
- \end{minipage}*}
- hence rh_drv: "\<Gamma> \<turnstile> (\<forall>X<:Q\<^isub>1. Q\<^isub>2) <: T" by simp
+ then have rh_drv: "\<Gamma> \<turnstile> (\<forall>X<:Q\<^isub>1. Q\<^isub>2) <: T" by simp
have lh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> Q\<^isub>1 <: S\<^isub>1" by fact
have lh_drv_prm\<^isub>2: "((TVarB X Q\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: Q\<^isub>2" by fact
- then have "X\<sharp>\<Gamma>" by (force dest: subtype_implies_ok simp add: valid_ty_domain_fresh)
- then have fresh_cond: "X\<sharp>\<Gamma>" "X\<sharp>Q\<^isub>1" using lh_drv_prm\<^isub>1 by (simp_all add: subtype_implies_fresh)
- from `(\<forall>X<:Q\<^isub>1. Q\<^isub>2) = Q`
- have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q " using fresh_cond by auto
+ then have "X\<sharp>\<Gamma>" by (force dest: subtype_implies_ok simp add: valid_ty_dom_fresh)
+ then have fresh_cond: "X\<sharp>\<Gamma>" "X\<sharp>Q\<^isub>1" "X\<sharp>T" using rh_drv lh_drv_prm\<^isub>1
+ by (simp_all add: subtype_implies_fresh)
from rh_drv
- have "T=Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T=(\<forall>X<:T\<^isub>1. T\<^isub>2) \<and> \<Gamma>\<turnstile>T\<^isub>1<:Q\<^isub>1 \<and> ((TVarB X T\<^isub>1)#\<Gamma>)\<turnstile>Q\<^isub>2<:T\<^isub>2)"
+ have "T = Top \<or>
+ (\<exists>T\<^isub>1 T\<^isub>2. T = (\<forall>X<:T\<^isub>1. T\<^isub>2) \<and> \<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1 \<and> ((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> Q\<^isub>2 <: T\<^isub>2)"
using fresh_cond by (simp add: S_ForallE_left)
moreover
have "S\<^isub>1 closed_in \<Gamma>" and "S\<^isub>2 closed_in ((TVarB X Q\<^isub>1)#\<Gamma>)"
using lh_drv_prm\<^isub>1 lh_drv_prm\<^isub>2 by (simp_all add: subtype_implies_closed)
- hence "(\<forall>X<:S\<^isub>1. S\<^isub>2) closed_in \<Gamma>" by (force simp add: closed_in_def ty.supp abs_supp)
+ then have "(\<forall>X<:S\<^isub>1. S\<^isub>2) closed_in \<Gamma>" by (force simp add: closed_in_def ty.supp abs_supp)
moreover
have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok)
moreover
@@ -1032,6 +955,9 @@
where T_inst: "T = (\<forall>X<:T\<^isub>1. T\<^isub>2)"
and rh_drv_prm\<^isub>1: "\<Gamma> \<turnstile> T\<^isub>1 <: Q\<^isub>1"
and rh_drv_prm\<^isub>2:"((TVarB X T\<^isub>1)#\<Gamma>) \<turnstile> Q\<^isub>2 <: T\<^isub>2" by force
+ have "(\<forall>X<:Q\<^isub>1. Q\<^isub>2) = Q" by fact
+ then have Q\<^isub>1\<^isub>2_less: "size_ty Q\<^isub>1 < size_ty Q" "size_ty Q\<^isub>2 < size_ty Q"
+ using fresh_cond by auto
from IH_trans[of "Q\<^isub>1"]
have "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1" using lh_drv_prm\<^isub>1 rh_drv_prm\<^isub>1 Q\<^isub>1\<^isub>2_less by blast
moreover
@@ -1045,52 +971,35 @@
}
ultimately show "\<Gamma> \<turnstile> (\<forall>X<:S\<^isub>1. S\<^isub>2) <: T" by blast
qed
- qed
+ } note transitivity_lemma = this
{ --{* The transitivity proof is now by the auxiliary lemma. *}
case 1
from `\<Gamma> \<turnstile> S <: Q` and `\<Gamma> \<turnstile> Q <: T`
- show "\<Gamma> \<turnstile> S <: T" by (rule transitivity_aux)
+ show "\<Gamma> \<turnstile> S <: T" by (rule transitivity_lemma)
next
- --{* The narrowing proof proceeds by an induction over @{term "(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> M <: N"}. *}
case 2
- from `(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> M <: N` --{* left-hand derivation *}
- and `\<Gamma> \<turnstile> P<:Q` --{* right-hand derivation *}
+ from `(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> M <: N`
+ and `\<Gamma> \<turnstile> P<:Q`
show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> M <: N"
- proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@[(TVarB X Q)]@\<Gamma>" M N avoiding: \<Delta> \<Gamma> X rule: subtype_of.strong_induct)
- case (SA_Top _ S \<Delta> \<Gamma> X)
- --{* \begin{minipage}[t]{0.9\textwidth}
- In this case the left-hand derivation is @{term "(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> S <: Top"}. We show
- that the context @{term "\<Delta>@[(TVarB X P)]@\<Gamma>"} is ok and that @{term S} is closed in
- @{term "\<Delta>@[(TVarB X P)]@\<Gamma>"}. Then we can apply the @{text "S_Top"}-rule.\end{minipage}*}
- hence lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok"
+ proof (induct \<Gamma>\<equiv>"\<Delta>@[(TVarB X Q)]@\<Gamma>" M N arbitrary: \<Gamma> X \<Delta> rule: subtype_of.induct)
+ case (SA_Top _ S \<Gamma> X \<Delta>)
+ then have lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok"
and lh_drv_prm\<^isub>2: "S closed_in (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp_all
have rh_drv: "\<Gamma> \<turnstile> P <: Q" by fact
hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
with lh_drv_prm\<^isub>1 have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: replace_type)
moreover
from lh_drv_prm\<^isub>2 have "S closed_in (\<Delta>@[(TVarB X P)]@\<Gamma>)"
- by (simp add: closed_in_def domains_append)
+ by (simp add: closed_in_def doms_append)
ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: Top" by (simp add: subtype_of.SA_Top)
next
- case (SA_trans_TVar Y S _ N \<Delta> \<Gamma> X)
- --{* \begin{minipage}[t]{0.9\textwidth}
- In this case the left-hand derivation is @{term "(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> Tvar Y <: N"} and
- by inner induction hypothesis we have @{term "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: N"}. We therefore
- know that the contexts @{term "\<Delta>@[(TVarB X Q)]@\<Gamma>"} and @{term "\<Delta>@[(TVarB X P)]@\<Gamma>"} are ok, and that
- @{term "(Y,S)"} is in @{term "\<Delta>@[(TVarB X Q)]@\<Gamma>"}. We need to show that
- @{term "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N"} holds. In case @{term "X\<noteq>Y"} we know that
- @{term "(Y,S)"} is in @{term "\<Delta>@[(TVarB X P)]@\<Gamma>"} and can use the inner induction hypothesis
- and rule @{text "S_Var"} to conclude. In case @{term "X=Y"} we can infer that
- @{term "S=Q"}; moreover we have that @{term "(\<Delta>@[(TVarB X P)]@\<Gamma>) extends \<Gamma>"} and therefore
- by @{text "weakening"} that @{term "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: Q"} holds. By transitivity we
- obtain then @{term "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: N"} and can conclude by applying rule
- @{text "S_Var"}.\end{minipage}*}
- hence IH_inner: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: N"
+ case (SA_trans_TVar Y S _ N \<Gamma> X \<Delta>)
+ then have IH_inner: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: N"
and lh_drv_prm: "(TVarB Y S) \<in> set (\<Delta>@[(TVarB X Q)]@\<Gamma>)"
and rh_drv: "\<Gamma> \<turnstile> P<:Q"
and ok\<^isub>Q: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok" by (simp_all add: subtype_implies_ok)
- hence ok\<^isub>P: "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: subtype_implies_ok)
+ then have ok\<^isub>P: "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: subtype_implies_ok)
show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N"
proof (cases "X=Y")
case False
@@ -1107,48 +1016,28 @@
moreover
have "(\<Delta>@[(TVarB X P)]@\<Gamma>) extends \<Gamma>" by (simp add: extends_def)
hence "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: Q" using rh_drv ok\<^isub>P by (simp only: weakening)
- ultimately have "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: N" by (simp add: transitivity_aux)
- thus "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^isub>X\<^isub>P eq by (simp only: subtype_of.SA_trans_TVar)
+ ultimately have "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: N" by (simp add: transitivity_lemma)
+ then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^isub>X\<^isub>P eq by auto
qed
next
- case (SA_refl_TVar _ Y \<Delta> \<Gamma> X)
- --{* \begin{minipage}[t]{0.9\textwidth}
- In this case the left-hand derivation is @{term "(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y"} and we
- therefore know that @{term "\<Delta>@[(TVarB X Q)]@\<Gamma>"} is ok and that @{term "Y"} is in
- the domain of @{term "\<Delta>@[(TVarB X Q)]@\<Gamma>"}. We therefore know that @{term "\<Delta>@[(TVarB X P)]@\<Gamma>"} is ok
- and that @{term Y} is in the domain of @{term "\<Delta>@[(TVarB X P)]@\<Gamma>"}. We can conclude by applying
- rule @{text "S_Refl"}.\end{minipage}*}
- hence lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok"
- and lh_drv_prm\<^isub>2: "Y \<in> ty_domain (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp_all
+ case (SA_refl_TVar _ Y \<Gamma> X \<Delta>)
+ then have lh_drv_prm\<^isub>1: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok"
+ and lh_drv_prm\<^isub>2: "Y \<in> ty_dom (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp_all
have "\<Gamma> \<turnstile> P <: Q" by fact
hence "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
with lh_drv_prm\<^isub>1 have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: replace_type)
moreover
- from lh_drv_prm\<^isub>2 have "Y \<in> ty_domain (\<Delta>@[(TVarB X P)]@\<Gamma>)" by (simp add: domains_append)
+ from lh_drv_prm\<^isub>2 have "Y \<in> ty_dom (\<Delta>@[(TVarB X P)]@\<Gamma>)" by (simp add: doms_append)
ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y" by (simp add: subtype_of.SA_refl_TVar)
next
- case (SA_arrow _ S\<^isub>1 Q\<^isub>1 Q\<^isub>2 S\<^isub>2 \<Delta> \<Gamma> X)
- --{* \begin{minipage}[t]{0.9\textwidth}
- In this case the left-hand derivation is @{term "(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: S\<^isub>1 \<rightarrow> S\<^isub>2"}
- and the proof is trivial.\end{minipage}*}
- thus "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: S\<^isub>1 \<rightarrow> S\<^isub>2" by blast
+ case (SA_arrow _ S\<^isub>1 Q\<^isub>1 Q\<^isub>2 S\<^isub>2 \<Gamma> X \<Delta>)
+ then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Q\<^isub>1 \<rightarrow> Q\<^isub>2 <: S\<^isub>1 \<rightarrow> S\<^isub>2" by blast
next
- case (SA_all \<Gamma>' T\<^isub>1 S\<^isub>1 Y S\<^isub>2 T\<^isub>2 \<Delta> \<Gamma> X)
- --{* \begin{minipage}[t]{0.9\textwidth}
- In this case the left-hand derivation is @{term "(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> (\<forall>Y<:S\<^isub>1. S\<^isub>2) <: (\<forall>Y<:T\<^isub>1. T\<^isub>2)"}
- and therfore we know that the binder @{term Y} is fresh for @{term "\<Delta>@[(TVarB X Q)]@\<Gamma>"}. By
- the inner induction hypothesis we have that @{term "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> T\<^isub>1 <: S\<^isub>1"} and
- @{term "((TVarB Y T\<^isub>1)#\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2"}. Since @{term P} is a subtype of @{term Q}
- we can infer that @{term Y} is fresh for @{term P} and thus also fresh for
- @{term "\<Delta>@[(TVarB X P)]@\<Gamma>"}. We can then conclude by applying rule @{text "S_Forall"}.
- \end{minipage}*}
- hence rh_drv: "\<Gamma> \<turnstile> P <: Q"
- and IH_inner\<^isub>1: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> T\<^isub>1 <: S\<^isub>1"
- and "TVarB Y T\<^isub>1 # \<Gamma>' = ((TVarB Y T\<^isub>1)#\<Delta>) @ [TVarB X Q] @ \<Gamma>" by auto
- moreover have " \<lbrakk>\<Gamma>\<turnstile>P<:Q; TVarB Y T\<^isub>1 # \<Gamma>' = ((TVarB Y T\<^isub>1)#\<Delta>) @ [TVarB X Q] @ \<Gamma>\<rbrakk> \<Longrightarrow> (((TVarB Y T\<^isub>1)#\<Delta>) @ [TVarB X P] @ \<Gamma>)\<turnstile>S\<^isub>2<:T\<^isub>2" by fact
- ultimately have IH_inner\<^isub>2: "(((TVarB Y T\<^isub>1)#\<Delta>) @ [TVarB X P] @ \<Gamma>)\<turnstile>S\<^isub>2<:T\<^isub>2" by auto
- with IH_inner\<^isub>1 IH_inner\<^isub>2
- show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> (\<forall>Y<:S\<^isub>1. S\<^isub>2) <: (\<forall>Y<:T\<^isub>1. T\<^isub>2)" by (simp add: subtype_of.SA_all)
+ case (SA_all _ T\<^isub>1 S\<^isub>1 Y S\<^isub>2 T\<^isub>2 \<Gamma> X \<Delta>)
+ from SA_all(2,4,5,6)
+ have IH_inner\<^isub>1: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> T\<^isub>1 <: S\<^isub>1"
+ and IH_inner\<^isub>2: "(((TVarB Y T\<^isub>1)#\<Delta>)@[(TVarB X P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2" by force+
+ then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> (\<forall>Y<:S\<^isub>1. S\<^isub>2) <: (\<forall>Y<:T\<^isub>1. T\<^isub>2)" by auto
qed
}
qed
@@ -1163,7 +1052,7 @@
| T_Abs[intro]: "\<lbrakk> VarB x T\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>x:T\<^isub>1. t\<^isub>2) : T\<^isub>1 \<rightarrow> T\<^isub>2"
| T_Sub[intro]: "\<lbrakk> \<Gamma> \<turnstile> t : S; \<Gamma> \<turnstile> S <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t : T"
| T_TAbs[intro]:"\<lbrakk> TVarB X T\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>X<:T\<^isub>1. t\<^isub>2) : (\<forall>X<:T\<^isub>1. T\<^isub>2)"
-| T_TApp[intro]:"\<lbrakk> X \<sharp> (\<Gamma>, t\<^isub>1, T\<^isub>2); \<Gamma> \<turnstile> t\<^isub>1 : (\<forall>X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2); \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<cdot>\<^sub>\<tau> T\<^isub>2 : (T\<^isub>1\<^isub>2[X \<mapsto> T\<^isub>2]\<^sub>\<tau>)"
+| T_TApp[intro]:"\<lbrakk>X\<sharp>(\<Gamma>,t\<^isub>1,T\<^isub>2); \<Gamma> \<turnstile> t\<^isub>1 : (\<forall>X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2); \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<cdot>\<^sub>\<tau> T\<^isub>2 : (T\<^isub>1\<^isub>2[X \<mapsto> T\<^isub>2]\<^sub>\<tau>)"
equivariance typing
@@ -1189,8 +1078,8 @@
using assms by (induct, auto)
nominal_inductive typing
-by (auto dest!: typing_ok intro: closed_in_fresh fresh_domain type_subst_fresh
- simp: abs_fresh fresh_type_subst_fresh ty_vrs_fresh valid_ty_domain_fresh fresh_trm_domain)
+by (auto dest!: typing_ok intro: closed_in_fresh fresh_dom type_subst_fresh
+ simp: abs_fresh fresh_type_subst_fresh ty_vrs_fresh valid_ty_dom_fresh fresh_trm_dom)
lemma ok_imp_VarB_closed_in:
assumes ok: "\<turnstile> \<Gamma> ok"
@@ -1200,19 +1089,19 @@
lemma tyvrs_of_subst: "tyvrs_of (B[X \<mapsto> T]\<^sub>b) = tyvrs_of B"
by (nominal_induct B rule: binding.strong_induct) simp_all
-lemma ty_domain_subst: "ty_domain (\<Gamma>[X \<mapsto> T]\<^sub>e) = ty_domain \<Gamma>"
+lemma ty_dom_subst: "ty_dom (\<Gamma>[X \<mapsto> T]\<^sub>e) = ty_dom \<Gamma>"
by (induct \<Gamma>) (simp_all add: tyvrs_of_subst)
lemma vrs_of_subst: "vrs_of (B[X \<mapsto> T]\<^sub>b) = vrs_of B"
by (nominal_induct B rule: binding.strong_induct) simp_all
-lemma trm_domain_subst: "trm_domain (\<Gamma>[X \<mapsto> T]\<^sub>e) = trm_domain \<Gamma>"
+lemma trm_dom_subst: "trm_dom (\<Gamma>[X \<mapsto> T]\<^sub>e) = trm_dom \<Gamma>"
by (induct \<Gamma>) (simp_all add: vrs_of_subst)
lemma subst_closed_in:
"T closed_in (\<Delta> @ TVarB X S # \<Gamma>) \<Longrightarrow> U closed_in \<Gamma> \<Longrightarrow> T[X \<mapsto> U]\<^sub>\<tau> closed_in (\<Delta>[X \<mapsto> U]\<^sub>e @ \<Gamma>)"
apply (nominal_induct T avoiding: X U \<Gamma> rule: ty.strong_induct)
- apply (simp add: closed_in_def ty.supp supp_atm domains_append ty_domain_subst)
+ apply (simp add: closed_in_def ty.supp supp_atm doms_append ty_dom_subst)
apply blast
apply (simp add: closed_in_def ty.supp)
apply (simp add: closed_in_def ty.supp)
@@ -1220,7 +1109,7 @@
apply (drule_tac x = X in meta_spec)
apply (drule_tac x = U in meta_spec)
apply (drule_tac x = "(TVarB tyvrs ty2) # \<Gamma>" in meta_spec)
- apply (simp add: domains_append ty_domain_subst)
+ apply (simp add: doms_append ty_dom_subst)
apply blast
done
@@ -1323,20 +1212,20 @@
"(\<lambda>x:T. t) \<longmapsto> t'"
"(\<lambda>X<:T. t) \<longmapsto> t'"
-lemma ty_domain_cons:
- shows "ty_domain (\<Gamma>@[VarB X Q]@\<Delta>) = ty_domain (\<Gamma>@\<Delta>)"
+lemma ty_dom_cons:
+ shows "ty_dom (\<Gamma>@[VarB X Q]@\<Delta>) = ty_dom (\<Gamma>@\<Delta>)"
by (induct \<Gamma>, auto)
lemma closed_in_cons:
assumes "S closed_in (\<Gamma> @ VarB X Q # \<Delta>)"
shows "S closed_in (\<Gamma>@\<Delta>)"
-using assms ty_domain_cons closed_in_def by auto
+using assms ty_dom_cons closed_in_def by auto
lemma closed_in_weaken: "T closed_in (\<Delta> @ \<Gamma>) \<Longrightarrow> T closed_in (\<Delta> @ B # \<Gamma>)"
- by (auto simp add: closed_in_def domains_append)
+ by (auto simp add: closed_in_def doms_append)
lemma closed_in_weaken': "T closed_in \<Gamma> \<Longrightarrow> T closed_in (\<Delta> @ \<Gamma>)"
- by (auto simp add: closed_in_def domains_append)
+ by (auto simp add: closed_in_def doms_append)
lemma valid_subst:
assumes ok: "\<turnstile> (\<Delta> @ TVarB X Q # \<Gamma>) ok"
@@ -1350,24 +1239,24 @@
apply simp
apply (rule valid_consT)
apply assumption
- apply (simp add: domains_append ty_domain_subst)
- apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_domains)
+ apply (simp add: doms_append ty_dom_subst)
+ apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms)
apply (rule_tac S=Q in subst_closed_in')
- apply (simp add: closed_in_def domains_append ty_domain_subst)
- apply (simp add: closed_in_def domains_append)
+ apply (simp add: closed_in_def doms_append ty_dom_subst)
+ apply (simp add: closed_in_def doms_append)
apply blast
apply simp
apply (rule valid_cons)
apply assumption
- apply (simp add: domains_append trm_domain_subst)
+ apply (simp add: doms_append trm_dom_subst)
apply (rule_tac S=Q in subst_closed_in')
- apply (simp add: closed_in_def domains_append ty_domain_subst)
- apply (simp add: closed_in_def domains_append)
+ apply (simp add: closed_in_def doms_append ty_dom_subst)
+ apply (simp add: closed_in_def doms_append)
apply blast
done
-lemma ty_domain_vrs:
- shows "ty_domain (G @ [VarB x Q] @ D) = ty_domain (G @ D)"
+lemma ty_dom_vrs:
+ shows "ty_dom (G @ [VarB x Q] @ D) = ty_dom (G @ D)"
by (induct G, auto)
lemma valid_cons':
@@ -1389,10 +1278,10 @@
case (Cons b bs)
with valid_consT
have "\<turnstile> (bs @ \<Delta>) ok" by simp
- moreover from Cons and valid_consT have "X \<sharp> ty_domain (bs @ \<Delta>)"
- by (simp add: domains_append)
+ moreover from Cons and valid_consT have "X \<sharp> ty_dom (bs @ \<Delta>)"
+ by (simp add: doms_append)
moreover from Cons and valid_consT have "T closed_in (bs @ \<Delta>)"
- by (simp add: closed_in_def domains_append)
+ by (simp add: closed_in_def doms_append)
ultimately have "\<turnstile> (TVarB X T # bs @ \<Delta>) ok"
by (rule valid_rel.valid_consT)
with Cons and valid_consT show ?thesis by simp
@@ -1407,11 +1296,11 @@
case (Cons b bs)
with valid_cons
have "\<turnstile> (bs @ \<Delta>) ok" by simp
- moreover from Cons and valid_cons have "x \<sharp> trm_domain (bs @ \<Delta>)"
- by (simp add: domains_append finite_domains
+ moreover from Cons and valid_cons have "x \<sharp> trm_dom (bs @ \<Delta>)"
+ by (simp add: doms_append finite_doms
fresh_fin_insert [OF pt_vrs_inst at_vrs_inst fs_vrs_inst])
moreover from Cons and valid_cons have "T closed_in (bs @ \<Delta>)"
- by (simp add: closed_in_def domains_append)
+ by (simp add: closed_in_def doms_append)
ultimately have "\<turnstile> (VarB x T # bs @ \<Delta>) ok"
by (rule valid_rel.valid_cons)
with Cons and valid_cons show ?thesis by simp
@@ -1439,10 +1328,10 @@
have "\<turnstile> (VarB y T\<^isub>1 # \<Delta> @ B # \<Gamma>) ok"
apply (rule valid_cons)
apply (rule T_Abs)
- apply (simp add: domains_append
+ apply (simp add: doms_append
fresh_fin_insert [OF pt_vrs_inst at_vrs_inst fs_vrs_inst]
fresh_fin_union [OF pt_vrs_inst at_vrs_inst fs_vrs_inst]
- finite_domains finite_vrs fresh_vrs_of T_Abs fresh_trm_domain)
+ finite_doms finite_vrs fresh_vrs_of T_Abs fresh_trm_dom)
apply (rule closed_in_weaken)
apply (rule closed)
done
@@ -1467,10 +1356,10 @@
have "\<turnstile> (TVarB X T\<^isub>1 # \<Delta> @ B # \<Gamma>) ok"
apply (rule valid_consT)
apply (rule T_TAbs)
- apply (simp add: domains_append
+ apply (simp add: doms_append
fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst]
fresh_fin_union [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst]
- finite_domains finite_vrs tyvrs_fresh T_TAbs fresh_domain)
+ finite_doms finite_vrs tyvrs_fresh T_TAbs fresh_dom)
apply (rule closed_in_weaken)
apply (rule closed)
done
@@ -1513,8 +1402,8 @@
case (SA_refl_TVar G X' G')
then have "\<turnstile> (G' @ VarB x Q # \<Delta>) ok" by simp
then have h1:"\<turnstile> (G' @ \<Delta>) ok" by (auto dest: valid_cons')
- have "X' \<in> ty_domain (G' @ VarB x Q # \<Delta>)" using SA_refl_TVar by auto
- then have h2:"X' \<in> ty_domain (G' @ \<Delta>)" using ty_domain_vrs by auto
+ have "X' \<in> ty_dom (G' @ VarB x Q # \<Delta>)" using SA_refl_TVar by auto
+ then have h2:"X' \<in> ty_dom (G' @ \<Delta>)" using ty_dom_vrs by auto
show ?case using h1 h2 by auto
next
case (SA_all G T1 S1 X S2 T2 G')
@@ -1592,7 +1481,7 @@
next
case (T_TAbs X T1 G t2 T2 x u D)
from `TVarB X T1 # G \<turnstile> t2 : T2` have "X \<sharp> T1"
- by (auto simp add: valid_ty_domain_fresh dest: typing_ok intro!: closed_in_fresh)
+ by (auto simp add: valid_ty_dom_fresh dest: typing_ok intro!: closed_in_fresh)
with `X \<sharp> u` and T_TAbs show ?case by fastsimp
next
case (T_TApp X G t1 T2 T11 T12 x u D)
@@ -1627,7 +1516,7 @@
assume eq: "X = Y"
from eq and SA_trans_TVar have "TVarB Y Q \<in> set G" by simp
with G_ok have QS: "Q = S" using `TVarB Y S \<in> set G` by (rule uniqueness_of_ctxt)
- from X\<Gamma>_ok have "X \<sharp> ty_domain \<Gamma>" and "Q closed_in \<Gamma>" by auto
+ from X\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "Q closed_in \<Gamma>" by auto
then have XQ: "X \<sharp> Q" by (rule closed_in_fresh)
note `\<Gamma>\<turnstile>P<:Q`
moreover from ST have "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" by (rule subtype_implies_ok)
@@ -1652,8 +1541,8 @@
with neq and ST show ?thesis by auto
next
assume Y: "TVarB Y S \<in> set \<Gamma>"
- from X\<Gamma>_ok have "X \<sharp> ty_domain \<Gamma>" and "\<turnstile> \<Gamma> ok" by auto
- then have "X \<sharp> \<Gamma>" by (simp add: valid_ty_domain_fresh)
+ from X\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "\<turnstile> \<Gamma> ok" by auto
+ then have "X \<sharp> \<Gamma>" by (simp add: valid_ty_dom_fresh)
with Y have "X \<sharp> S"
by (induct \<Gamma>) (auto simp add: fresh_list_nil fresh_list_cons)
with ST have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>S<:T[X \<mapsto> P]\<^sub>\<tau>"
@@ -1677,8 +1566,8 @@
by (auto intro: subtype_reflexivity)
next
assume neq: "X \<noteq> Y"
- with SA_refl_TVar have "Y \<in> ty_domain (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)"
- by (simp add: ty_domain_subst domains_append)
+ with SA_refl_TVar have "Y \<in> ty_dom (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)"
+ by (simp add: ty_dom_subst doms_append)
with neq and ok show ?thesis by auto
qed
next
@@ -1688,8 +1577,8 @@
show ?case using subtype_of.SA_arrow h1 h2 by auto
next
case (SA_all G T1 S1 Y S2 T2 X P D)
- then have Y: "Y \<sharp> ty_domain (D @ TVarB X Q # \<Gamma>)"
- by (auto dest: subtype_implies_ok intro: fresh_domain)
+ then have Y: "Y \<sharp> ty_dom (D @ TVarB X Q # \<Gamma>)"
+ by (auto dest: subtype_implies_ok intro: fresh_dom)
moreover from SA_all have "S1 closed_in (D @ TVarB X Q # \<Gamma>)"
by (auto dest: subtype_implies_closed)
ultimately have S1: "Y \<sharp> S1" by (rule closed_in_fresh)
@@ -1722,8 +1611,8 @@
next
assume x: "VarB x T \<in> set G"
from T_Var have ok: "\<turnstile> G ok" by (auto dest: subtype_implies_ok)
- then have "X \<sharp> ty_domain G" using T_Var by (auto dest: validE_append)
- with ok have "X \<sharp> G" by (simp add: valid_ty_domain_fresh)
+ then have "X \<sharp> ty_dom G" using T_Var by (auto dest: validE_append)
+ with ok have "X \<sharp> G" by (simp add: valid_ty_dom_fresh)
moreover from x have "VarB x T \<in> set (D' @ G)" by simp
then have "VarB x (T[X \<mapsto> P]\<^sub>\<tau>) \<in> set ((D' @ G)[X \<mapsto> P]\<^sub>e)"
by (rule ctxt_subst_mem_VarB)
@@ -1744,15 +1633,15 @@
then show ?case using substT_subtype by force
next
case (T_TAbs X' G' T1 t2 T2 X P D')
- then have "X' \<sharp> ty_domain (D' @ TVarB X Q # G)"
+ then have "X' \<sharp> ty_dom (D' @ TVarB X Q # G)"
and "G' closed_in (D' @ TVarB X Q # G)"
by (auto dest: typing_ok)
then have "X' \<sharp> G'" by (rule closed_in_fresh)
with T_TAbs show ?case by force
next
case (T_TApp X' G' t1 T2 T11 T12 X P D')
- then have "X' \<sharp> ty_domain (D' @ TVarB X Q # G)"
- by (simp add: fresh_domain)
+ then have "X' \<sharp> ty_dom (D' @ TVarB X Q # G)"
+ by (simp add: fresh_dom)
moreover from T_TApp have "T11 closed_in (D' @ TVarB X Q # G)"
by (auto dest: subtype_implies_closed)
ultimately have X': "X' \<sharp> T11" by (rule closed_in_fresh)
@@ -1783,7 +1672,7 @@
then have "[(y, x)] \<bullet> (VarB y S # \<Gamma>) \<turnstile> [(y, x)] \<bullet> [(y, x)] \<bullet> s : [(y, x)] \<bullet> T\<^isub>2"
by (rule typing.eqvt)
moreover from T_Abs have "y \<sharp> \<Gamma>"
- by (auto dest!: typing_ok simp add: fresh_trm_domain)
+ by (auto dest!: typing_ok simp add: fresh_trm_dom)
ultimately have "VarB x S # \<Gamma> \<turnstile> s : T\<^isub>2" using T_Abs
by (perm_simp add: ty_vrs_prm_simp)
with ty1 show ?case using ty2 by (rule T_Abs)
@@ -1819,7 +1708,7 @@
proof (nominal_induct \<Gamma> t \<equiv> "\<lambda>X<:S. s" T avoiding: X U U' S arbitrary: s rule: typing.strong_induct)
case (T_TAbs Y T\<^isub>1 \<Gamma> t\<^isub>2 T\<^isub>2)
from `TVarB Y T\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2` have Y: "Y \<sharp> \<Gamma>"
- by (auto dest!: typing_ok simp add: valid_ty_domain_fresh)
+ by (auto dest!: typing_ok simp add: valid_ty_dom_fresh)
from `Y \<sharp> U'` and `Y \<sharp> X`
have "(\<forall>X<:U. U') = (\<forall>Y<:U. [(Y, X)] \<bullet> U')"
by (simp add: ty.inject alpha' fresh_atm)
@@ -1907,7 +1796,7 @@
with T_TApp have "\<Gamma> \<turnstile> (\<lambda>X<:T\<^isub>1\<^isub>1'. t\<^isub>1\<^isub>2) : (\<forall>X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2)" and "X \<sharp> \<Gamma>" and "X \<sharp> T\<^isub>1\<^isub>1'"
by (simp_all add: trm.inject)
moreover from `\<Gamma>\<turnstile>T\<^isub>2<:T\<^isub>1\<^isub>1` and `X \<sharp> \<Gamma>` have "X \<sharp> T\<^isub>1\<^isub>1"
- by (blast intro: closed_in_fresh fresh_domain dest: subtype_implies_closed)
+ by (blast intro: closed_in_fresh fresh_dom dest: subtype_implies_closed)
ultimately obtain S'
where "TVarB X T\<^isub>1\<^isub>1 # \<Gamma> \<turnstile> t\<^isub>1\<^isub>2 : S'"
and "(TVarB X T\<^isub>1\<^isub>1 # \<Gamma>) \<turnstile> S' <: T\<^isub>1\<^isub>2"
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Jul 17 10:07:15 2009 +0200
@@ -147,7 +147,7 @@
| perm_simproc' thy ss _ = NONE;
val perm_simproc =
- Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
+ Simplifier.simproc @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
val meta_spec = thm "meta_spec";
--- a/src/HOL/Nominal/nominal_permeq.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Fri Jul 17 10:07:15 2009 +0200
@@ -117,7 +117,7 @@
| _ => NONE
end
-val perm_simproc_app = Simplifier.simproc (the_context ()) "perm_simproc_app"
+val perm_simproc_app = Simplifier.simproc @{theory} "perm_simproc_app"
["Nominal.perm pi x"] perm_simproc_app';
(* a simproc that deals with permutation instances in front of functions *)
@@ -137,7 +137,7 @@
| _ => NONE
end
-val perm_simproc_fun = Simplifier.simproc (the_context ()) "perm_simproc_fun"
+val perm_simproc_fun = Simplifier.simproc @{theory} "perm_simproc_fun"
["Nominal.perm pi x"] perm_simproc_fun';
(* function for simplyfying permutations *)
@@ -217,7 +217,7 @@
end
| _ => NONE);
-val perm_compose_simproc = Simplifier.simproc (the_context ()) "perm_compose"
+val perm_compose_simproc = Simplifier.simproc @{theory} "perm_compose"
["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc';
fun perm_compose_tac ss i =
--- a/src/HOL/OrderedGroup.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/OrderedGroup.thy Fri Jul 17 10:07:15 2009 +0200
@@ -1380,7 +1380,7 @@
if termless_agrp (y, x) then SOME ac2 else NONE
| solve_add_ac thy _ _ = NONE
in
- val add_ac_proc = Simplifier.simproc (the_context ())
+ val add_ac_proc = Simplifier.simproc @{theory}
"add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
end;
--- a/src/HOL/Product_Type.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Product_Type.thy Fri Jul 17 10:07:15 2009 +0200
@@ -470,8 +470,8 @@
| NONE => NONE)
| eta_proc _ _ = NONE;
in
- val split_beta_proc = Simplifier.simproc (the_context ()) "split_beta" ["split f z"] (K beta_proc);
- val split_eta_proc = Simplifier.simproc (the_context ()) "split_eta" ["split f"] (K eta_proc);
+ val split_beta_proc = Simplifier.simproc @{theory} "split_beta" ["split f z"] (K beta_proc);
+ val split_eta_proc = Simplifier.simproc @{theory} "split_eta" ["split f"] (K eta_proc);
end;
Addsimprocs [split_beta_proc, split_eta_proc];
--- a/src/HOL/Prolog/prolog.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Prolog/prolog.ML Fri Jul 17 10:07:15 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Prolog/prolog.ML
- ID: $Id$
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
@@ -60,7 +59,7 @@
in map zero_var_indexes (at thm) end;
val atomize_ss =
- Simplifier.theory_context (the_context ()) empty_ss
+ Simplifier.theory_context @{theory} empty_ss
setmksimps (mksimps mksimps_pairs)
addsimps [
all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
--- a/src/HOL/Set.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Set.thy Fri Jul 17 10:07:15 2009 +0200
@@ -478,9 +478,9 @@
fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
in
- val defBEX_regroup = Simplifier.simproc (the_context ())
+ val defBEX_regroup = Simplifier.simproc @{theory}
"defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
- val defBALL_regroup = Simplifier.simproc (the_context ())
+ val defBALL_regroup = Simplifier.simproc @{theory}
"defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
end;
@@ -1014,7 +1014,7 @@
ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
in
- val defColl_regroup = Simplifier.simproc (the_context ())
+ val defColl_regroup = Simplifier.simproc @{theory}
"defined Collect" ["{x. P x & Q x}"]
(Quantifier1.rearrange_Coll Coll_perm_tac)
end;
--- a/src/HOL/Statespace/DistinctTreeProver.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Fri Jul 17 10:07:15 2009 +0200
@@ -676,7 +676,7 @@
ML {*
- val ct' = cterm_of (the_context ()) t';
+ val ct' = cterm_of @{theory} t';
*}
ML {*
@@ -706,7 +706,7 @@
ML {*
-val cdist' = cterm_of (the_context ()) dist';
+val cdist' = cterm_of @{theory} dist';
DistinctTreeProver.distinct_implProver (!da) cdist';
*}
--- a/src/HOL/Statespace/state_fun.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Statespace/state_fun.ML Fri Jul 17 10:07:15 2009 +0200
@@ -115,7 +115,7 @@
Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false));
val lookup_simproc =
- Simplifier.simproc (the_context ()) "lookup_simp" ["lookup d n (update d' c m v s)"]
+ Simplifier.simproc @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
(fn thy => fn ss => fn t =>
(case t of (Const ("StateFun.lookup",lT)$destr$n$
(s as Const ("StateFun.update",uT)$_$_$_$_$_)) =>
@@ -171,7 +171,7 @@
addcongs [thm "block_conj_cong"]);
in
val update_simproc =
- Simplifier.simproc (the_context ()) "update_simp" ["update d c n v s"]
+ Simplifier.simproc @{theory} "update_simp" ["update d c n v s"]
(fn thy => fn ss => fn t =>
(case t of ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) =>
let
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Fri Jul 17 10:07:15 2009 +0200
@@ -180,7 +180,7 @@
val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
val r = Const (case_name, map fastype_of rs ---> T --> rT);
- val y = Var (("y", 0), Logic.legacy_varifyT T);
+ val y = Var (("y", 0), Logic.varifyT T);
val y' = Free ("y", T);
val thm = OldGoals.prove_goalw_cterm [] (cert (Logic.list_implies (prems,
@@ -201,10 +201,10 @@
val P = Var (("P", 0), rT' --> HOLogic.boolT);
val prf = forall_intr_prf (y, forall_intr_prf (P,
List.foldr (fn ((p, r), prf) =>
- forall_intr_prf (Logic.legacy_varify r, AbsP ("H", SOME (Logic.varify p),
+ forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),
prf))) (Proofterm.proof_combP (prf_of thm',
map PBound (length prems - 1 downto 0))) (prems ~~ rs)));
- val r' = Logic.legacy_varify (Abs ("y", Logic.legacy_varifyT T,
+ val r' = Logic.varify (Abs ("y", T,
list_abs (map dest_Free rs, list_comb (r,
map Bound ((length rs - 1 downto 0) @ [length rs])))));
--- a/src/HOL/Tools/Function/fundef_core.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_core.ML Fri Jul 17 10:07:15 2009 +0200
@@ -179,16 +179,17 @@
(* lowlevel term function *)
fun abstract_over_list vs body =
let
- exception SAME;
fun abs lev v tm =
if v aconv tm then Bound lev
else
(case tm of
Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
- | t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u)
- | _ => raise SAME);
+ | t $ u =>
+ (abs lev v t $ (abs lev v u handle Same.SAME => u)
+ handle Same.SAME => t $ abs lev v u)
+ | _ => raise Same.SAME);
in
- fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body
+ fold_index (fn (i, v) => fn t => abs i v t handle Same.SAME => t) vs body
end
--- a/src/HOL/Tools/metis_tools.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Fri Jul 17 10:07:15 2009 +0200
@@ -371,7 +371,7 @@
end;
(* INFERENCE RULE: REFL *)
- val refl_x = cterm_of (the_context ()) (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
+ val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
fun refl_inf ctxt t =
@@ -475,14 +475,14 @@
fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
- val equal_imp_fequal' = cnf_th (the_context ()) (thm"equal_imp_fequal");
- val fequal_imp_equal' = cnf_th (the_context ()) (thm"fequal_imp_equal");
+ val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal};
+ val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal};
- val comb_I = cnf_th (the_context ()) ResHolClause.comb_I;
- val comb_K = cnf_th (the_context ()) ResHolClause.comb_K;
- val comb_B = cnf_th (the_context ()) ResHolClause.comb_B;
- val comb_C = cnf_th (the_context ()) ResHolClause.comb_C;
- val comb_S = cnf_th (the_context ()) ResHolClause.comb_S;
+ val comb_I = cnf_th @{theory} ResHolClause.comb_I;
+ val comb_K = cnf_th @{theory} ResHolClause.comb_K;
+ val comb_B = cnf_th @{theory} ResHolClause.comb_B;
+ val comb_C = cnf_th @{theory} ResHolClause.comb_C;
+ val comb_S = cnf_th @{theory} ResHolClause.comb_S;
fun type_ext thy tms =
let val subs = ResAtp.tfree_classes_of_terms tms
--- a/src/HOL/Tools/nat_arith.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Tools/nat_arith.ML Fri Jul 17 10:07:15 2009 +0200
@@ -91,18 +91,18 @@
end);
val nat_cancel_sums_add =
- [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
+ [Simplifier.simproc @{theory} "nateq_cancel_sums"
["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
(K EqCancelSums.proc),
- Simplifier.simproc (the_context ()) "natless_cancel_sums"
+ Simplifier.simproc @{theory} "natless_cancel_sums"
["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
(K LessCancelSums.proc),
- Simplifier.simproc (the_context ()) "natle_cancel_sums"
+ Simplifier.simproc @{theory} "natle_cancel_sums"
["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
(K LeCancelSums.proc)];
val nat_cancel_sums = nat_cancel_sums_add @
- [Simplifier.simproc (the_context ()) "natdiff_cancel_sums"
+ [Simplifier.simproc @{theory} "natdiff_cancel_sums"
["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
(K DiffCancelSums.proc)];
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Fri Jul 17 10:07:15 2009 +0200
@@ -19,7 +19,7 @@
val numeral_sym_ss = HOL_ss addsimps numeral_syms;
fun rename_numerals th =
- simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
+ simplify numeral_sym_ss (Thm.transfer @{theory} th);
(*Utilities*)
--- a/src/HOL/Tools/numeral.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Tools/numeral.ML Fri Jul 17 10:07:15 2009 +0200
@@ -39,7 +39,7 @@
val oneT = Thm.ctyp_of_term one;
val number_of = @{cpat "number_of"};
-val numberT = Thm.ctyp_of (the_context ()) (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of)));
+val numberT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of)));
fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
--- a/src/HOL/Tools/res_axioms.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Fri Jul 17 10:07:15 2009 +0200
@@ -154,9 +154,9 @@
val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
-val [f_B,g_B] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_B}));
-val [g_C,f_C] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_C}));
-val [f_S,g_S] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_S}));
+val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
+val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
+val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
(*FIXME: requires more use of cterm constructors*)
fun abstract ct =
--- a/src/HOL/Tools/rewrite_hol_proof.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Fri Jul 17 10:07:15 2009 +0200
@@ -15,8 +15,8 @@
open Proofterm;
-val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) true) o
- Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT)
+val rews = map (pairself (ProofSyntax.proof_of_term @{theory} true) o
+ Logic.dest_equals o Logic.varify o ProofSyntax.read_term @{theory} propT)
(** eliminate meta-equality rules **)
--- a/src/HOL/Tools/sat_funcs.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Fri Jul 17 10:07:15 2009 +0200
@@ -66,16 +66,10 @@
val counter = ref 0;
-val resolution_thm = (* "[| ?P ==> False; ~ ?P ==> False |] ==> False" *)
- let
- val cterm = cterm_of (the_context ())
- val Q = Var (("Q", 0), HOLogic.boolT)
- val False = HOLogic.false_const
- in
- Thm.instantiate ([], [(cterm Q, cterm False)]) @{thm case_split}
- end;
+val resolution_thm =
+ @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
-val cP = cterm_of (theory_of_thm resolution_thm) (Var (("P", 0), HOLogic.boolT));
+val cP = cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
(* ------------------------------------------------------------------------- *)
(* lit_ord: an order on integers that considers their absolute values only, *)
--- a/src/HOL/Tools/simpdata.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOL/Tools/simpdata.ML Fri Jul 17 10:07:15 2009 +0200
@@ -181,11 +181,11 @@
in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
val defALL_regroup =
- Simplifier.simproc (the_context ())
+ Simplifier.simproc @{theory}
"defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
val defEX_regroup =
- Simplifier.simproc (the_context ())
+ Simplifier.simproc @{theory}
"defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
--- a/src/HOLCF/holcf_logic.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/HOLCF/holcf_logic.ML Fri Jul 17 10:07:15 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOLCF/holcf_logic.ML
- ID: $Id$
Author: David von Oheimb
Abstract syntax operations for HOLCF.
@@ -10,7 +9,6 @@
signature HOLCF_LOGIC =
sig
val mk_btyp: string -> typ * typ -> typ
- val pcpoC: class
val pcpoS: sort
val mk_TFree: string -> typ
val cfun_arrow: string
@@ -27,8 +25,7 @@
(* sort pcpo *)
-val pcpoC = Sign.intern_class (the_context ()) "pcpo";
-val pcpoS = [pcpoC];
+val pcpoS = @{sort pcpo};
fun mk_TFree s = TFree ("'" ^ s, pcpoS);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/same.ML Fri Jul 17 10:07:15 2009 +0200
@@ -0,0 +1,45 @@
+(* Title: Pure/General/same.ML
+ Author: Makarius
+
+Support for copy-avoiding functions on pure values, at the cost of
+readability.
+*)
+
+signature SAME =
+sig
+ exception SAME
+ type ('a, 'b) function = 'a -> 'b (*exception SAME*)
+ type 'a operation = ('a, 'a) function (*exception SAME*)
+ val same: ('a, 'b) function
+ val commit: 'a operation -> 'a -> 'a
+ val function: ('a -> 'b option) -> ('a, 'b) function
+ val capture: ('a, 'b) function -> 'a -> 'b option
+ val map: 'a operation -> 'a list operation
+ val map_option: ('a, 'b) function -> ('a option, 'b option) function
+end;
+
+structure Same: SAME =
+struct
+
+exception SAME;
+
+type ('a, 'b) function = 'a -> 'b;
+type 'a operation = ('a, 'a) function;
+
+fun same _ = raise SAME;
+fun commit f x = f x handle SAME => x;
+
+fun capture f x = SOME (f x) handle SAME => NONE;
+
+fun function f x =
+ (case f x of
+ NONE => raise SAME
+ | SOME y => y);
+
+fun map f [] = raise SAME
+ | map f (x :: xs) = (f x :: commit (map f) xs handle SAME => x :: map f xs);
+
+fun map_option f NONE = raise SAME
+ | map_option f (SOME x) = SOME (f x);
+
+end;
--- a/src/Pure/IsaMakefile Wed Jul 15 15:09:56 2009 +0200
+++ b/src/Pure/IsaMakefile Fri Jul 17 10:07:15 2009 +0200
@@ -52,12 +52,12 @@
General/long_name.ML General/markup.ML General/name_space.ML \
General/ord_list.ML General/output.ML General/path.ML \
General/position.ML General/pretty.ML General/print_mode.ML \
- General/properties.ML General/queue.ML General/scan.ML \
- General/secure.ML General/seq.ML General/source.ML General/stack.ML \
- General/symbol.ML General/symbol_pos.ML General/table.ML \
- General/url.ML General/xml.ML General/yxml.ML Isar/args.ML \
- Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \
- Isar/class_target.ML Isar/code.ML Isar/constdefs.ML \
+ General/properties.ML General/queue.ML General/same.ML \
+ General/scan.ML General/secure.ML General/seq.ML General/source.ML \
+ General/stack.ML General/symbol.ML General/symbol_pos.ML \
+ General/table.ML General/url.ML General/xml.ML General/yxml.ML \
+ Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML \
+ Isar/class.ML Isar/class_target.ML Isar/code.ML Isar/constdefs.ML \
Isar/context_rules.ML Isar/element.ML Isar/expression.ML \
Isar/isar_cmd.ML Isar/isar_document.ML Isar/isar_syn.ML \
Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \
--- a/src/Pure/Isar/theory_target.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/Pure/Isar/theory_target.ML Fri Jul 17 10:07:15 2009 +0200
@@ -177,7 +177,6 @@
let
val b' = Morphism.binding phi b;
val rhs' = Morphism.term phi rhs;
- val legacy_arg = (b', Term.close_schematic_term (Logic.legacy_varify rhs'));
val arg = (b', Term.close_schematic_term rhs');
val similar_body = Type.similar_types (rhs, rhs');
(* FIXME workaround based on educated guess *)
@@ -188,7 +187,7 @@
in
not (is_class andalso (similar_body orelse class_global)) ?
(Context.mapping_result
- (Sign.add_abbrev PrintMode.internal tags legacy_arg)
+ (Sign.add_abbrev PrintMode.internal tags arg)
(ProofContext.add_abbrev PrintMode.internal tags arg)
#-> (fn (lhs' as Const (d, _), _) =>
similar_body ?
--- a/src/Pure/Proof/reconstruct.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML Fri Jul 17 10:07:15 2009 +0200
@@ -353,8 +353,6 @@
| (b, SOME prop') => a = b andalso prop = prop') thms)
then (maxidx, prfs, prf) else
let
- fun inc i =
- map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i);
val (maxidx', prf, prfs') =
(case AList.lookup (op =) prfs (a, prop) of
NONE =>
@@ -365,11 +363,11 @@
(reconstruct_proof thy prop (join_proof body));
val (maxidx', prfs', prf) = expand
(maxidx_proof prf' ~1) prfs prf'
- in (maxidx' + maxidx + 1, inc (maxidx + 1) prf,
+ in (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf,
((a, prop), (maxidx', prf)) :: prfs')
end
| SOME (maxidx', prf) => (maxidx' + maxidx + 1,
- inc (maxidx + 1) prf, prfs));
+ incr_indexes (maxidx + 1) prf, prfs));
val tfrees = OldTerm.term_tfrees prop;
val tye = map (fn ((s, j), _) => (s, maxidx + 1 + j))
(OldTerm.term_tvars prop) @ map (rpair ~1 o fst) tfrees ~~ Ts;
--- a/src/Pure/ROOT.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/Pure/ROOT.ML Fri Jul 17 10:07:15 2009 +0200
@@ -33,11 +33,12 @@
use "ML/ml_lex.ML";
use "ML/ml_parse.ML";
use "General/secure.ML";
-(*----- basic ML bootstrap finished -----*)
+(*^^^^^ end of basic ML bootstrap ^^^^^*)
use "General/integer.ML";
use "General/stack.ML";
use "General/queue.ML";
use "General/heap.ML";
+use "General/same.ML";
use "General/ord_list.ML";
use "General/balanced_tree.ML";
use "General/graph.ML";
--- a/src/Pure/envir.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/Pure/envir.ML Fri Jul 17 10:07:15 2009 +0200
@@ -8,11 +8,10 @@
signature ENVIR =
sig
- type tenv
+ type tenv = (typ * term) Vartab.table
datatype env = Envir of {asol: tenv, iTs: Type.tyenv, maxidx: int}
val type_env: env -> Type.tyenv
val insert_sorts: env -> sort list -> sort list
- exception SAME
val genvars: string -> env * typ list -> env * term list
val genvar: string -> env * typ -> env * term
val lookup: env * (indexname * typ) -> term option
@@ -23,11 +22,11 @@
val above: env -> int -> bool
val vupdate: ((indexname * typ) * term) * env -> env
val alist_of: env -> (indexname * (typ * term)) list
- val norm_term: env -> term -> term
- val norm_term_same: env -> term -> term
+ val norm_type_same: Type.tyenv -> typ Same.operation
+ val norm_types_same: Type.tyenv -> typ list Same.operation
val norm_type: Type.tyenv -> typ -> typ
- val norm_type_same: Type.tyenv -> typ -> typ
- val norm_types_same: Type.tyenv -> typ list -> typ list
+ val norm_term_same: env -> term Same.operation
+ val norm_term: env -> term -> term
val beta_norm: term -> term
val head_norm: env -> term -> term
val eta_contract: term -> term
@@ -48,12 +47,12 @@
(*updating can destroy environment in 2 ways!!
(1) variables out of range (2) circular assignments
*)
-type tenv = (typ * term) Vartab.table
+type tenv = (typ * term) Vartab.table;
datatype env = Envir of
- {maxidx: int, (*maximum index of vars*)
- asol: tenv, (*table of assignments to Vars*)
- iTs: Type.tyenv} (*table of assignments to TVars*)
+ {maxidx: int, (*maximum index of vars*)
+ asol: tenv, (*assignments to Vars*)
+ iTs: Type.tyenv}; (*assignments to TVars*)
fun type_env (Envir {iTs, ...}) = iTs;
@@ -63,27 +62,27 @@
(*Generate a list of distinct variables.
Increments index to make them distinct from ALL present variables. *)
fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
- let fun genvs (_, [] : typ list) : term list = []
- | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
- | genvs (n, T::Ts) =
- Var((name ^ radixstring(26,"a",n), maxidx+1), T)
- :: genvs(n+1,Ts)
- in (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts)) end;
+ let
+ fun genvs (_, [] : typ list) : term list = []
+ | genvs (n, [T]) = [Var ((name, maxidx + 1), T)]
+ | genvs (n, T :: Ts) =
+ Var ((name ^ radixstring (26, "a" , n), maxidx + 1), T)
+ :: genvs (n + 1, Ts);
+ in (Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs}, genvs (0, Ts)) end;
(*Generate a variable.*)
-fun genvar name (env,T) : env * term =
- let val (env',[v]) = genvars name (env,[T])
- in (env',v) end;
+fun genvar name (env, T) : env * term =
+ let val (env', [v]) = genvars name (env, [T])
+ in (env', v) end;
fun var_clash ixn T T' = raise TYPE ("Variable " ^
- quote (Term.string_of_vname ixn) ^ " has two distinct types",
- [T', T], []);
+ quote (Term.string_of_vname ixn) ^ " has two distinct types",
+ [T', T], []);
fun gen_lookup f asol (xname, T) =
(case Vartab.lookup asol xname of
- NONE => NONE
- | SOME (U, t) => if f (T, U) then SOME t
- else var_clash xname T U);
+ NONE => NONE
+ | SOME (U, t) => if f (T, U) then SOME t else var_clash xname T U);
(* When dealing with environments produced by matching instead *)
(* of unification, there is no need to chase assigned TVars. *)
@@ -99,10 +98,10 @@
fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p;
fun update (((xname, T), t), Envir {maxidx, asol, iTs}) =
- Envir{maxidx=maxidx, asol=Vartab.update_new (xname, (T, t)) asol, iTs=iTs};
+ Envir {maxidx = maxidx, asol = Vartab.update_new (xname, (T, t)) asol, iTs = iTs};
(*The empty environment. New variables will start with the given index+1.*)
-fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
+fun empty m = Envir {maxidx = m, asol = Vartab.empty, iTs = Vartab.empty};
(*Test for empty environment*)
fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
@@ -132,118 +131,123 @@
Chases variables in env; Does not exploit sharing of variable bindings
Does not check types, so could loop. ***)
-(*raised when norm has no effect on a term, to do sharing instead of copying*)
-exception SAME;
+local
+
+fun norm_type0 iTs : typ Same.operation =
+ let
+ fun norm (Type (a, Ts)) = Type (a, Same.map norm Ts)
+ | norm (TFree _) = raise Same.SAME
+ | norm (TVar v) =
+ (case Type.lookup iTs v of
+ SOME U => Same.commit norm U
+ | NONE => raise Same.SAME);
+ in norm end;
-fun norm_term1 same (asol,t) : term =
- let fun norm (Var wT) =
- (case lookup' (asol, wT) of
- SOME u => (norm u handle SAME => u)
- | NONE => raise SAME)
- | norm (Abs(a,T,body)) = Abs(a, T, norm body)
- | norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
- | norm (f $ t) =
- ((case norm f of
- Abs(_,_,body) => normh(subst_bound (t, body))
- | nf => nf $ (norm t handle SAME => t))
- handle SAME => f $ norm t)
- | norm _ = raise SAME
- and normh t = norm t handle SAME => t
- in (if same then norm else normh) t end
+fun norm_term1 asol : term Same.operation =
+ let
+ fun norm (Var v) =
+ (case lookup' (asol, v) of
+ SOME u => Same.commit norm u
+ | NONE => raise Same.SAME)
+ | norm (Abs (a, T, body)) = Abs (a, T, norm body)
+ | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
+ | norm (f $ t) =
+ ((case norm f of
+ Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
+ | nf => nf $ Same.commit norm t)
+ handle Same.SAME => f $ norm t)
+ | norm _ = raise Same.SAME;
+ in norm end;
-fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
- | normT iTs (TFree _) = raise SAME
- | normT iTs (TVar vS) = (case Type.lookup iTs vS of
- SOME U => normTh iTs U
- | NONE => raise SAME)
-and normTh iTs T = ((normT iTs T) handle SAME => T)
-and normTs iTs [] = raise SAME
- | normTs iTs (T :: Ts) =
- ((normT iTs T :: (normTs iTs Ts handle SAME => Ts))
- handle SAME => T :: normTs iTs Ts);
+fun norm_term2 asol iTs : term Same.operation =
+ let
+ val normT = norm_type0 iTs;
+ fun norm (Const (a, T)) = Const (a, normT T)
+ | norm (Free (a, T)) = Free (a, normT T)
+ | norm (Var (xi, T)) =
+ (case lookup2 (iTs, asol) (xi, T) of
+ SOME u => Same.commit norm u
+ | NONE => Var (xi, normT T))
+ | norm (Abs (a, T, body)) =
+ (Abs (a, normT T, Same.commit norm body)
+ handle Same.SAME => Abs (a, T, norm body))
+ | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
+ | norm (f $ t) =
+ ((case norm f of
+ Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
+ | nf => nf $ Same.commit norm t)
+ handle Same.SAME => f $ norm t)
+ | norm _ = raise Same.SAME;
+ in norm end;
-fun norm_term2 same (asol, iTs, t) : term =
- let fun norm (Const (a, T)) = Const(a, normT iTs T)
- | norm (Free (a, T)) = Free(a, normT iTs T)
- | norm (Var (w, T)) =
- (case lookup2 (iTs, asol) (w, T) of
- SOME u => normh u
- | NONE => Var(w, normT iTs T))
- | norm (Abs (a, T, body)) =
- (Abs (a, normT iTs T, normh body) handle SAME => Abs (a, T, norm body))
- | norm (Abs(_, _, body) $ t) = normh (subst_bound (t, body))
- | norm (f $ t) =
- ((case norm f of
- Abs(_, _, body) => normh (subst_bound (t, body))
- | nf => nf $ normh t)
- handle SAME => f $ norm t)
- | norm _ = raise SAME
- and normh t = (norm t) handle SAME => t
- in (if same then norm else normh) t end;
+in
+
+fun norm_type_same iTs T =
+ if Vartab.is_empty iTs then raise Same.SAME
+ else norm_type0 iTs T;
-fun gen_norm_term same (env as Envir{asol,iTs,...}) t : term =
- if Vartab.is_empty iTs then norm_term1 same (asol, t)
- else norm_term2 same (asol, iTs, t);
+fun norm_types_same iTs Ts =
+ if Vartab.is_empty iTs then raise Same.SAME
+ else Same.map (norm_type0 iTs) Ts;
+
+fun norm_type iTs T = norm_type_same iTs T handle Same.SAME => T;
-val norm_term = gen_norm_term false;
-val norm_term_same = gen_norm_term true;
+fun norm_term_same (Envir {asol, iTs, ...}) =
+ if Vartab.is_empty iTs then norm_term1 asol
+ else norm_term2 asol iTs;
+fun norm_term envir t = norm_term_same envir t handle Same.SAME => t;
fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t;
-fun norm_type iTs = normTh iTs;
-fun norm_type_same iTs =
- if Vartab.is_empty iTs then raise SAME else normT iTs;
-
-fun norm_types_same iTs =
- if Vartab.is_empty iTs then raise SAME else normTs iTs;
+end;
(*Put a term into head normal form for unification.*)
-fun head_norm env t =
+fun head_norm env =
let
- fun hnorm (Var vT) = (case lookup (env, vT) of
+ fun norm (Var v) =
+ (case lookup (env, v) of
SOME u => head_norm env u
- | NONE => raise SAME)
- | hnorm (Abs (a, T, body)) = Abs (a, T, hnorm body)
- | hnorm (Abs (_, _, body) $ t) =
- head_norm env (subst_bound (t, body))
- | hnorm (f $ t) = (case hnorm f of
- Abs (_, _, body) => head_norm env (subst_bound (t, body))
- | nf => nf $ t)
- | hnorm _ = raise SAME
- in hnorm t handle SAME => t end;
+ | NONE => raise Same.SAME)
+ | norm (Abs (a, T, body)) = Abs (a, T, norm body)
+ | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
+ | norm (f $ t) =
+ (case norm f of
+ Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
+ | nf => nf $ t)
+ | norm _ = raise Same.SAME;
+ in Same.commit norm end;
(*Eta-contract a term (fully)*)
local
-fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise SAME
+fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME
| decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
- | decr lev (t $ u) = (decr lev t $ decrh lev u handle SAME => t $ decr lev u)
- | decr _ _ = raise SAME
-and decrh lev t = (decr lev t handle SAME => t);
+ | decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u)
+ | decr _ _ = raise Same.SAME
+and decrh lev t = (decr lev t handle Same.SAME => t);
fun eta (Abs (a, T, body)) =
((case eta body of
body' as (f $ Bound 0) =>
if loose_bvar1 (f, 0) then Abs (a, T, body')
else decrh 0 f
- | body' => Abs (a, T, body')) handle SAME =>
+ | body' => Abs (a, T, body')) handle Same.SAME =>
(case body of
f $ Bound 0 =>
- if loose_bvar1 (f, 0) then raise SAME
+ if loose_bvar1 (f, 0) then raise Same.SAME
else decrh 0 f
- | _ => raise SAME))
- | eta (t $ u) = (eta t $ etah u handle SAME => t $ eta u)
- | eta _ = raise SAME
-and etah t = (eta t handle SAME => t);
+ | _ => raise Same.SAME))
+ | eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u)
+ | eta _ = raise Same.SAME;
in
fun eta_contract t =
- if Term.has_abs t then etah t else t;
+ if Term.has_abs t then Same.commit eta t else t;
val beta_eta_contract = eta_contract o beta_norm;
--- a/src/Pure/logic.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/Pure/logic.ML Fri Jul 17 10:07:15 2009 +0200
@@ -54,8 +54,10 @@
val close_form: term -> term
val combound: term * int * int -> term
val rlist_abs: (string * typ) list * term -> term
+ val incr_tvar_same: int -> typ Same.operation
+ val incr_tvar: int -> typ -> typ
+ val incr_indexes_same: typ list * int -> term Same.operation
val incr_indexes: typ list * int -> term -> term
- val incr_tvar: int -> typ -> typ
val lift_abs: int -> term -> term -> term
val lift_all: int -> term -> term -> term
val strip_assums_hyp: term -> term list
@@ -70,8 +72,6 @@
val unvarifyT: typ -> typ
val varify: term -> term
val unvarify: term -> term
- val legacy_varifyT: typ -> typ
- val legacy_varify: term -> term
val get_goal: term -> int -> term
val goal_params: term -> int -> term * term list
val prems_of_goal: term -> int -> term list
@@ -305,45 +305,35 @@
fun rlist_abs ([], body) = body
| rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
-
-local exception SAME in
+fun incr_tvar_same 0 = Same.same
+ | incr_tvar_same k = Term_Subst.map_atypsT_same
+ (fn TVar ((a, i), S) => TVar ((a, i + k), S)
+ | _ => raise Same.SAME);
-fun incrT k =
- let
- fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S)
- | incr (Type (a, Ts)) = Type (a, incrs Ts)
- | incr _ = raise SAME
- and incrs (T :: Ts) =
- (incr T :: (incrs Ts handle SAME => Ts)
- handle SAME => T :: incrs Ts)
- | incrs [] = raise SAME;
- in incr end;
+fun incr_tvar k T = incr_tvar_same k T handle Same.SAME => T;
(*For all variables in the term, increment indexnames and lift over the Us
result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
-fun incr_indexes ([], 0) t = t
- | incr_indexes (Ts, k) t =
- let
- val n = length Ts;
- val incrT = if k = 0 then I else incrT k;
+fun incr_indexes_same ([], 0) = Same.same
+ | incr_indexes_same (Ts, k) =
+ let
+ val n = length Ts;
+ val incrT = incr_tvar_same k;
- fun incr lev (Var ((x, i), T)) =
- combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
- | incr lev (Abs (x, T, body)) =
- (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
- handle SAME => Abs (x, T, incr (lev + 1) body))
- | incr lev (t $ u) =
- (incr lev t $ (incr lev u handle SAME => u)
- handle SAME => t $ incr lev u)
- | incr _ (Const (c, T)) = Const (c, incrT T)
- | incr _ (Free (x, T)) = Free (x, incrT T)
- | incr _ (t as Bound _) = t;
- in incr 0 t handle SAME => t end;
+ fun incr lev (Var ((x, i), T)) =
+ combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n)
+ | incr lev (Abs (x, T, body)) =
+ (Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body)
+ handle Same.SAME => Abs (x, T, incr (lev + 1) body))
+ | incr lev (t $ u) =
+ (incr lev t $ (incr lev u handle Same.SAME => u)
+ handle Same.SAME => t $ incr lev u)
+ | incr _ (Const (c, T)) = Const (c, incrT T)
+ | incr _ (Free (x, T)) = Free (x, incrT T)
+ | incr _ (Bound _) = raise Same.SAME;
+ in incr 0 end;
-fun incr_tvar 0 T = T
- | incr_tvar k T = incrT k T handle SAME => T;
-
-end;
+fun incr_indexes arg t = incr_indexes_same arg t handle Same.SAME => t;
(* Lifting functions from subgoal and increment:
@@ -424,6 +414,8 @@
a $ Abs(c, T, list_rename_params (cs, t))
| list_rename_params (cs, B) = B;
+
+
(*** Treatment of "assume", "erule", etc. ***)
(*Strips assumptions in goal yielding
@@ -440,8 +432,7 @@
strip_assums_imp (nasms-1, H::Hs, B)
| strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
-
-(*Strips OUTER parameters only, unlike similar legacy versions.*)
+(*Strips OUTER parameters only.*)
fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
strip_assums_all ((a,T)::params, t)
| strip_assums_all (params, B) = (params, B);
@@ -474,43 +465,37 @@
fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
-fun varifyT_option ty = ty
- |> Term_Subst.map_atypsT_option
- (fn TFree (a, S) => SOME (TVar ((a, 0), S))
+fun varifyT_same ty = ty
+ |> Term_Subst.map_atypsT_same
+ (fn TFree (a, S) => TVar ((a, 0), S)
| TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
-fun unvarifyT_option ty = ty
- |> Term_Subst.map_atypsT_option
- (fn TVar ((a, 0), S) => SOME (TFree (a, S))
+fun unvarifyT_same ty = ty
+ |> Term_Subst.map_atypsT_same
+ (fn TVar ((a, 0), S) => TFree (a, S)
| TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
| TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
-val varifyT = perhaps varifyT_option;
-val unvarifyT = perhaps unvarifyT_option;
+val varifyT = Same.commit varifyT_same;
+val unvarifyT = Same.commit unvarifyT_same;
fun varify tm = tm
- |> perhaps (Term_Subst.map_aterms_option
- (fn Free (x, T) => SOME (Var ((x, 0), T))
+ |> Same.commit (Term_Subst.map_aterms_same
+ (fn Free (x, T) => Var ((x, 0), T)
| Var (xi, _) => raise TERM (bad_schematic xi, [tm])
- | _ => NONE))
- |> perhaps (Term_Subst.map_types_option varifyT_option)
+ | _ => raise Same.SAME))
+ |> Same.commit (Term_Subst.map_types_same varifyT_same)
handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
fun unvarify tm = tm
- |> perhaps (Term_Subst.map_aterms_option
- (fn Var ((x, 0), T) => SOME (Free (x, T))
+ |> Same.commit (Term_Subst.map_aterms_same
+ (fn Var ((x, 0), T) => Free (x, T)
| Var (xi, _) => raise TERM (bad_schematic xi, [tm])
| Free (x, _) => raise TERM (bad_fixed x, [tm])
- | _ => NONE))
- |> perhaps (Term_Subst.map_types_option unvarifyT_option)
+ | _ => raise Same.SAME))
+ |> Same.commit (Term_Subst.map_types_same unvarifyT_same)
handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
-val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
-
-val legacy_varify =
- Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
- Term.map_types legacy_varifyT;
-
(* goal states *)
--- a/src/Pure/proofterm.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/Pure/proofterm.ML Fri Jul 17 10:07:15 2009 +0200
@@ -88,6 +88,7 @@
val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
-> proof -> proof
val lift_proof: term -> int -> term -> proof -> proof
+ val incr_indexes: int -> proof -> proof
val assumption_proof: term list -> term -> int -> proof -> proof
val bicompose_proof: bool -> term list -> term list -> term list -> term option ->
int -> int -> proof -> proof -> proof
@@ -127,9 +128,6 @@
structure Proofterm : PROOFTERM =
struct
-open Envir;
-
-
(***** datatype proof *****)
datatype proof =
@@ -269,47 +267,40 @@
val mk_Abst = fold_rev (fn (s, T:typ) => fn prf => Abst (s, NONE, prf));
fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
-fun apsome f NONE = raise SAME
- | apsome f (SOME x) = (case f x of NONE => raise SAME | some => some);
-
-fun apsome' f NONE = raise SAME
- | apsome' f (SOME x) = SOME (f x);
-
fun map_proof_terms_option f g =
let
- fun map_typs (T :: Ts) =
- (case g T of
- NONE => T :: map_typs Ts
- | SOME T' => T' :: (map_typs Ts handle SAME => Ts))
- | map_typs [] = raise SAME;
+ val term = Same.function f;
+ val typ = Same.function g;
+ val typs = Same.map typ;
- fun mapp (Abst (s, T, prf)) = (Abst (s, apsome g T, mapph prf)
- handle SAME => Abst (s, T, mapp prf))
- | mapp (AbsP (s, t, prf)) = (AbsP (s, apsome f t, mapph prf)
- handle SAME => AbsP (s, t, mapp prf))
- | mapp (prf % t) = (mapp prf % (apsome f t handle SAME => t)
- handle SAME => prf % apsome f t)
- | mapp (prf1 %% prf2) = (mapp prf1 %% mapph prf2
- handle SAME => prf1 %% mapp prf2)
- | mapp (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (map_typs Ts))
- | mapp (OfClass (T, c)) = OfClass (apsome g (SOME T) |> the, c)
- | mapp (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (map_typs Ts))
- | mapp (Promise (i, prop, Ts)) = Promise (i, prop, map_typs Ts)
- | mapp (PThm (i, ((a, prop, SOME Ts), body))) =
- PThm (i, ((a, prop, SOME (map_typs Ts)), body))
- | mapp _ = raise SAME
- and mapph prf = (mapp prf handle SAME => prf)
-
- in mapph end;
+ fun proof (Abst (s, T, prf)) =
+ (Abst (s, Same.map_option typ T, Same.commit proof prf)
+ handle Same.SAME => Abst (s, T, proof prf))
+ | proof (AbsP (s, t, prf)) =
+ (AbsP (s, Same.map_option term t, Same.commit proof prf)
+ handle Same.SAME => AbsP (s, t, proof prf))
+ | proof (prf % t) =
+ (proof prf % Same.commit (Same.map_option term) t
+ handle Same.SAME => prf % Same.map_option term t)
+ | proof (prf1 %% prf2) =
+ (proof prf1 %% Same.commit proof prf2
+ handle Same.SAME => prf1 %% proof prf2)
+ | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
+ | proof (OfClass (T, c)) = OfClass (typ T, c)
+ | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
+ | proof (Promise (i, prop, Ts)) = Promise (i, prop, typs Ts)
+ | proof (PThm (i, ((a, prop, SOME Ts), body))) = PThm (i, ((a, prop, SOME (typs Ts)), body))
+ | proof _ = raise Same.SAME;
+ in Same.commit proof end;
fun same eq f x =
let val x' = f x
- in if eq (x, x') then raise SAME else x' end;
+ in if eq (x, x') then raise Same.SAME else x' end;
fun map_proof_terms f g =
map_proof_terms_option
- (fn t => SOME (same (op =) f t) handle SAME => NONE)
- (fn T => SOME (same (op =) g T) handle SAME => NONE);
+ (fn t => SOME (same (op =) f t) handle Same.SAME => NONE)
+ (fn T => SOME (same (op =) g T) handle Same.SAME => NONE);
fun fold_proof_terms f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms f g prf
| fold_proof_terms f g (Abst (_, NONE, prf)) = fold_proof_terms f g prf
@@ -359,20 +350,20 @@
fun abst' lev u = if v aconv u then Bound lev else
(case u of
Abs (a, T, t) => Abs (a, T, abst' (lev + 1) t)
- | f $ t => (abst' lev f $ absth' lev t handle SAME => f $ abst' lev t)
- | _ => raise SAME)
- and absth' lev t = (abst' lev t handle SAME => t);
+ | f $ t => (abst' lev f $ absth' lev t handle Same.SAME => f $ abst' lev t)
+ | _ => raise Same.SAME)
+ and absth' lev t = (abst' lev t handle Same.SAME => t);
fun abst lev (AbsP (a, t, prf)) =
- (AbsP (a, apsome' (abst' lev) t, absth lev prf)
- handle SAME => AbsP (a, t, abst lev prf))
+ (AbsP (a, Same.map_option (abst' lev) t, absth lev prf)
+ handle Same.SAME => AbsP (a, t, abst lev prf))
| abst lev (Abst (a, T, prf)) = Abst (a, T, abst (lev + 1) prf)
| abst lev (prf1 %% prf2) = (abst lev prf1 %% absth lev prf2
- handle SAME => prf1 %% abst lev prf2)
+ handle Same.SAME => prf1 %% abst lev prf2)
| abst lev (prf % t) = (abst lev prf % Option.map (absth' lev) t
- handle SAME => prf % apsome' (abst' lev) t)
- | abst _ _ = raise SAME
- and absth lev prf = (abst lev prf handle SAME => prf)
+ handle Same.SAME => prf % Same.map_option (abst' lev) t)
+ | abst _ _ = raise Same.SAME
+ and absth lev prf = (abst lev prf handle Same.SAME => prf);
in absth 0 end;
@@ -385,22 +376,22 @@
fun incr_bv' inct tlev t = incr_bv (inct, tlev, t);
fun prf_incr_bv' incP inct Plev tlev (PBound i) =
- if i >= Plev then PBound (i+incP) else raise SAME
+ if i >= Plev then PBound (i+incP) else raise Same.SAME
| prf_incr_bv' incP inct Plev tlev (AbsP (a, t, body)) =
- (AbsP (a, apsome' (same (op =) (incr_bv' inct tlev)) t,
- prf_incr_bv incP inct (Plev+1) tlev body) handle SAME =>
+ (AbsP (a, Same.map_option (same (op =) (incr_bv' inct tlev)) t,
+ prf_incr_bv incP inct (Plev+1) tlev body) handle Same.SAME =>
AbsP (a, t, prf_incr_bv' incP inct (Plev+1) tlev body))
| prf_incr_bv' incP inct Plev tlev (Abst (a, T, body)) =
Abst (a, T, prf_incr_bv' incP inct Plev (tlev+1) body)
| prf_incr_bv' incP inct Plev tlev (prf %% prf') =
(prf_incr_bv' incP inct Plev tlev prf %% prf_incr_bv incP inct Plev tlev prf'
- handle SAME => prf %% prf_incr_bv' incP inct Plev tlev prf')
+ handle Same.SAME => prf %% prf_incr_bv' incP inct Plev tlev prf')
| prf_incr_bv' incP inct Plev tlev (prf % t) =
(prf_incr_bv' incP inct Plev tlev prf % Option.map (incr_bv' inct tlev) t
- handle SAME => prf % apsome' (same (op =) (incr_bv' inct tlev)) t)
- | prf_incr_bv' _ _ _ _ _ = raise SAME
+ handle Same.SAME => prf % Same.map_option (same (op =) (incr_bv' inct tlev)) t)
+ | prf_incr_bv' _ _ _ _ _ = raise Same.SAME
and prf_incr_bv incP inct Plev tlev prf =
- (prf_incr_bv' incP inct Plev tlev prf handle SAME => prf);
+ (prf_incr_bv' incP inct Plev tlev prf handle Same.SAME => prf);
fun incr_pboundvars 0 0 prf = prf
| incr_pboundvars incP inct prf = prf_incr_bv incP inct 0 0 prf;
@@ -448,7 +439,7 @@
fun del_conflicting_vars env t = Term_Subst.instantiate
(map_filter (fn ixnS as (_, S) =>
- (Type.lookup (type_env env) ixnS; NONE) handle TYPE _ =>
+ (Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
SOME (ixnS, TFree ("'dummy", S))) (OldTerm.term_tvars t),
map_filter (fn Var (ixnT as (_, T)) =>
(Envir.lookup (env, ixnT); NONE) handle TYPE _ =>
@@ -456,7 +447,7 @@
fun norm_proof env =
let
- val envT = type_env env;
+ val envT = Envir.type_env env;
fun msg s = warning ("type conflict in norm_proof:\n" ^ s);
fun htype f t = f env t handle TYPE (s, _, _) =>
(msg s; f env (del_conflicting_vars env t));
@@ -464,23 +455,31 @@
(msg s; f envT (del_conflicting_tvars envT T));
fun htypeTs f Ts = f envT Ts handle TYPE (s, _, _) =>
(msg s; f envT (map (del_conflicting_tvars envT) Ts));
- fun norm (Abst (s, T, prf)) = (Abst (s, apsome' (htypeT norm_type_same) T, normh prf)
- handle SAME => Abst (s, T, norm prf))
- | norm (AbsP (s, t, prf)) = (AbsP (s, apsome' (htype norm_term_same) t, normh prf)
- handle SAME => AbsP (s, t, norm prf))
- | norm (prf % t) = (norm prf % Option.map (htype norm_term) t
- handle SAME => prf % apsome' (htype norm_term_same) t)
- | norm (prf1 %% prf2) = (norm prf1 %% normh prf2
- handle SAME => prf1 %% norm prf2)
- | norm (PAxm (s, prop, Ts)) = PAxm (s, prop, apsome' (htypeTs norm_types_same) Ts)
- | norm (OfClass (T, c)) = OfClass (htypeT norm_type_same T, c)
- | norm (Oracle (s, prop, Ts)) = Oracle (s, prop, apsome' (htypeTs norm_types_same) Ts)
- | norm (Promise (i, prop, Ts)) = Promise (i, prop, htypeTs norm_types_same Ts)
+
+ fun norm (Abst (s, T, prf)) =
+ (Abst (s, Same.map_option (htypeT Envir.norm_type_same) T, Same.commit norm prf)
+ handle Same.SAME => Abst (s, T, norm prf))
+ | norm (AbsP (s, t, prf)) =
+ (AbsP (s, Same.map_option (htype Envir.norm_term_same) t, Same.commit norm prf)
+ handle Same.SAME => AbsP (s, t, norm prf))
+ | norm (prf % t) =
+ (norm prf % Option.map (htype Envir.norm_term) t
+ handle Same.SAME => prf % Same.map_option (htype Envir.norm_term_same) t)
+ | norm (prf1 %% prf2) =
+ (norm prf1 %% Same.commit norm prf2
+ handle Same.SAME => prf1 %% norm prf2)
+ | norm (PAxm (s, prop, Ts)) =
+ PAxm (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
+ | norm (OfClass (T, c)) =
+ OfClass (htypeT Envir.norm_type_same T, c)
+ | norm (Oracle (s, prop, Ts)) =
+ Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
+ | norm (Promise (i, prop, Ts)) =
+ Promise (i, prop, htypeTs Envir.norm_types_same Ts)
| norm (PThm (i, ((s, t, Ts), body))) =
- PThm (i, ((s, t, apsome' (htypeTs norm_types_same) Ts), body))
- | norm _ = raise SAME
- and normh prf = (norm prf handle SAME => prf);
- in normh end;
+ PThm (i, ((s, t, Same.map_option (htypeTs Envir.norm_types_same) Ts), body))
+ | norm _ = raise Same.SAME;
+ in Same.commit norm end;
(***** Remove some types in proof term (to save space) *****)
@@ -503,40 +502,40 @@
let
val n = length args;
fun subst' lev (Bound i) =
- (if i<lev then raise SAME (*var is locally bound*)
+ (if i<lev then raise Same.SAME (*var is locally bound*)
else incr_boundvars lev (nth args (i-lev))
handle Subscript => Bound (i-n)) (*loose: change it*)
| subst' lev (Abs (a, T, body)) = Abs (a, T, subst' (lev+1) body)
| subst' lev (f $ t) = (subst' lev f $ substh' lev t
- handle SAME => f $ subst' lev t)
- | subst' _ _ = raise SAME
- and substh' lev t = (subst' lev t handle SAME => t);
+ handle Same.SAME => f $ subst' lev t)
+ | subst' _ _ = raise Same.SAME
+ and substh' lev t = (subst' lev t handle Same.SAME => t);
- fun subst lev (AbsP (a, t, body)) = (AbsP (a, apsome' (subst' lev) t, substh lev body)
- handle SAME => AbsP (a, t, subst lev body))
+ fun subst lev (AbsP (a, t, body)) = (AbsP (a, Same.map_option (subst' lev) t, substh lev body)
+ handle Same.SAME => AbsP (a, t, subst lev body))
| subst lev (Abst (a, T, body)) = Abst (a, T, subst (lev+1) body)
| subst lev (prf %% prf') = (subst lev prf %% substh lev prf'
- handle SAME => prf %% subst lev prf')
+ handle Same.SAME => prf %% subst lev prf')
| subst lev (prf % t) = (subst lev prf % Option.map (substh' lev) t
- handle SAME => prf % apsome' (subst' lev) t)
- | subst _ _ = raise SAME
- and substh lev prf = (subst lev prf handle SAME => prf)
+ handle Same.SAME => prf % Same.map_option (subst' lev) t)
+ | subst _ _ = raise Same.SAME
+ and substh lev prf = (subst lev prf handle Same.SAME => prf);
in case args of [] => prf | _ => substh 0 prf end;
fun prf_subst_pbounds args prf =
let
val n = length args;
fun subst (PBound i) Plev tlev =
- (if i < Plev then raise SAME (*var is locally bound*)
+ (if i < Plev then raise Same.SAME (*var is locally bound*)
else incr_pboundvars Plev tlev (nth args (i-Plev))
handle Subscript => PBound (i-n) (*loose: change it*))
| subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev)
| subst (Abst (a, T, body)) Plev tlev = Abst (a, T, subst body Plev (tlev+1))
| subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev
- handle SAME => prf %% subst prf' Plev tlev)
+ handle Same.SAME => prf %% subst prf' Plev tlev)
| subst (prf % t) Plev tlev = subst prf Plev tlev % t
- | subst prf _ _ = raise SAME
- and substh prf Plev tlev = (subst prf Plev tlev handle SAME => prf)
+ | subst prf _ _ = raise Same.SAME
+ and substh prf Plev tlev = (subst prf Plev tlev handle Same.SAME => prf)
in case args of [] => prf | _ => substh prf 0 0 end;
@@ -598,14 +597,15 @@
fun implies_intr_proof h prf =
let
- fun abshyp i (Hyp t) = if h aconv t then PBound i else raise SAME
+ fun abshyp i (Hyp t) = if h aconv t then PBound i else raise Same.SAME
| abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf)
- | abshyp i (AbsP (s, t, prf)) = AbsP (s, t, abshyp (i+1) prf)
+ | abshyp i (AbsP (s, t, prf)) = AbsP (s, t, abshyp (i + 1) prf)
| abshyp i (prf % t) = abshyp i prf % t
- | abshyp i (prf1 %% prf2) = (abshyp i prf1 %% abshyph i prf2
- handle SAME => prf1 %% abshyp i prf2)
- | abshyp _ _ = raise SAME
- and abshyph i prf = (abshyp i prf handle SAME => prf)
+ | abshyp i (prf1 %% prf2) =
+ (abshyp i prf1 %% abshyph i prf2
+ handle Same.SAME => prf1 %% abshyp i prf2)
+ | abshyp _ _ = raise Same.SAME
+ and abshyph i prf = (abshyp i prf handle Same.SAME => prf);
in
AbsP ("H", NONE (*h*), abshyph 0 prf)
end;
@@ -624,7 +624,7 @@
(fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
val used = Name.context
|> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
- val fmap = fs ~~ (#1 (Name.variants (map fst fs) used));
+ val fmap = fs ~~ #1 (Name.variants (map fst fs) used);
fun thaw (f as (a, S)) =
(case AList.lookup (op =) fmap f of
NONE => TFree f
@@ -705,30 +705,31 @@
fun lift_proof Bi inc prop prf =
let
- fun lift'' Us Ts t = strip_abs Ts (Logic.incr_indexes (Us, inc) (mk_abs Ts t));
+ fun lift'' Us Ts t =
+ strip_abs Ts (Logic.incr_indexes (Us, inc) (mk_abs Ts t));
fun lift' Us Ts (Abst (s, T, prf)) =
- (Abst (s, apsome' (same (op =) (Logic.incr_tvar inc)) T, lifth' Us (dummyT::Ts) prf)
- handle SAME => Abst (s, T, lift' Us (dummyT::Ts) prf))
+ (Abst (s, Same.map_option (Logic.incr_tvar_same inc) T, lifth' Us (dummyT::Ts) prf)
+ handle Same.SAME => Abst (s, T, lift' Us (dummyT::Ts) prf))
| lift' Us Ts (AbsP (s, t, prf)) =
- (AbsP (s, apsome' (same (op =) (lift'' Us Ts)) t, lifth' Us Ts prf)
- handle SAME => AbsP (s, t, lift' Us Ts prf))
+ (AbsP (s, Same.map_option (same (op =) (lift'' Us Ts)) t, lifth' Us Ts prf)
+ handle Same.SAME => AbsP (s, t, lift' Us Ts prf))
| lift' Us Ts (prf % t) = (lift' Us Ts prf % Option.map (lift'' Us Ts) t
- handle SAME => prf % apsome' (same (op =) (lift'' Us Ts)) t)
+ handle Same.SAME => prf % Same.map_option (same (op =) (lift'' Us Ts)) t)
| lift' Us Ts (prf1 %% prf2) = (lift' Us Ts prf1 %% lifth' Us Ts prf2
- handle SAME => prf1 %% lift' Us Ts prf2)
+ handle Same.SAME => prf1 %% lift' Us Ts prf2)
| lift' _ _ (PAxm (s, prop, Ts)) =
- PAxm (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts)
+ PAxm (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
| lift' _ _ (OfClass (T, c)) =
- OfClass (same (op =) (Logic.incr_tvar inc) T, c)
+ OfClass (Logic.incr_tvar_same inc T, c)
| lift' _ _ (Oracle (s, prop, Ts)) =
- Oracle (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts)
+ Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
| lift' _ _ (Promise (i, prop, Ts)) =
- Promise (i, prop, same (op =) (map (Logic.incr_tvar inc)) Ts)
+ Promise (i, prop, Same.map (Logic.incr_tvar_same inc) Ts)
| lift' _ _ (PThm (i, ((s, prop, Ts), body))) =
- PThm (i, ((s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts), body))
- | lift' _ _ _ = raise SAME
- and lifth' Us Ts prf = (lift' Us Ts prf handle SAME => prf);
+ PThm (i, ((s, prop, (Same.map_option o Same.map) (Logic.incr_tvar inc) Ts), body))
+ | lift' _ _ _ = raise Same.SAME
+ and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf);
val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop);
val k = length ps;
@@ -747,6 +748,11 @@
mk_AbsP (k, lift [] [] 0 0 Bi)
end;
+fun incr_indexes i =
+ map_proof_terms_option
+ (Same.capture (Logic.incr_indexes_same ([], i)))
+ (Same.capture (Logic.incr_tvar_same i));
+
(***** proof by assumption *****)
--- a/src/Pure/term.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/Pure/term.ML Fri Jul 17 10:07:15 2009 +0200
@@ -634,31 +634,31 @@
*)
fun subst_bounds (args: term list, t) : term =
let
- exception SAME;
val n = length args;
fun subst (t as Bound i, lev) =
- (if i < lev then raise SAME (*var is locally bound*)
+ (if i < lev then raise Same.SAME (*var is locally bound*)
else incr_boundvars lev (nth args (i - lev))
handle Subscript => Bound (i - n)) (*loose: change it*)
| subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
| subst (f $ t, lev) =
- (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
- | subst _ = raise SAME;
- in case args of [] => t | _ => (subst (t, 0) handle SAME => t) end;
+ (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
+ handle Same.SAME => f $ subst (t, lev))
+ | subst _ = raise Same.SAME;
+ in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end;
(*Special case: one argument*)
fun subst_bound (arg, t) : term =
let
- exception SAME;
fun subst (Bound i, lev) =
- if i < lev then raise SAME (*var is locally bound*)
+ if i < lev then raise Same.SAME (*var is locally bound*)
else if i = lev then incr_boundvars lev arg
else Bound (i - 1) (*loose: change it*)
| subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
| subst (f $ t, lev) =
- (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
- | subst _ = raise SAME;
- in subst (t, 0) handle SAME => t end;
+ (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
+ handle Same.SAME => f $ subst (t, lev))
+ | subst _ = raise Same.SAME;
+ in subst (t, 0) handle Same.SAME => t end;
(*beta-reduce if possible, else form application*)
fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
@@ -708,15 +708,16 @@
The resulting term is ready to become the body of an Abs.*)
fun abstract_over (v, body) =
let
- exception SAME;
fun abs lev tm =
if v aconv tm then Bound lev
else
(case tm of
Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
- | t $ u => (abs lev t $ (abs lev u handle SAME => u) handle SAME => t $ abs lev u)
- | _ => raise SAME);
- in abs 0 body handle SAME => body end;
+ | t $ u =>
+ (abs lev t $ (abs lev u handle Same.SAME => u)
+ handle Same.SAME => t $ abs lev u)
+ | _ => raise Same.SAME);
+ in abs 0 body handle Same.SAME => body end;
fun lambda v t =
let val x =
--- a/src/Pure/term_subst.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/Pure/term_subst.ML Fri Jul 17 10:07:15 2009 +0200
@@ -1,11 +1,14 @@
(* Title: Pure/term_subst.ML
Author: Makarius
-Efficient type/term substitution -- avoids copying.
+Efficient type/term substitution.
*)
signature TERM_SUBST =
sig
+ val map_atypsT_same: typ Same.operation -> typ Same.operation
+ val map_types_same: typ Same.operation -> term Same.operation
+ val map_aterms_same: term Same.operation -> term Same.operation
val map_atypsT_option: (typ -> typ option) -> typ -> typ option
val map_atyps_option: (typ -> typ option) -> term -> term option
val map_types_option: (typ -> typ option) -> term -> term option
@@ -32,29 +35,12 @@
structure Term_Subst: TERM_SUBST =
struct
-(* indication of same result *)
-
-exception SAME;
-
-fun same_fn f x =
- (case f x of
- NONE => raise SAME
- | SOME y => y);
-
-fun option_fn f x =
- SOME (f x) handle SAME => NONE;
-
-
(* generic mapping *)
-local
-
fun map_atypsT_same f =
let
- fun typ (Type (a, Ts)) = Type (a, typs Ts)
- | typ T = f T
- and typs (T :: Ts) = (typ T :: (typs Ts handle SAME => Ts) handle SAME => T :: typs Ts)
- | typs [] = raise SAME;
+ fun typ (Type (a, Ts)) = Type (a, Same.map typ Ts)
+ | typ T = f T;
in typ end;
fun map_types_same f =
@@ -62,72 +48,64 @@
fun term (Const (a, T)) = Const (a, f T)
| term (Free (a, T)) = Free (a, f T)
| term (Var (v, T)) = Var (v, f T)
- | term (Bound _) = raise SAME
+ | term (Bound _) = raise Same.SAME
| term (Abs (x, T, t)) =
- (Abs (x, f T, term t handle SAME => t)
- handle SAME => Abs (x, T, term t))
- | term (t $ u) = (term t $ (term u handle SAME => u) handle SAME => t $ term u);
+ (Abs (x, f T, Same.commit term t)
+ handle Same.SAME => Abs (x, T, term t))
+ | term (t $ u) = (term t $ Same.commit term u handle Same.SAME => t $ term u);
in term end;
fun map_aterms_same f =
let
fun term (Abs (x, T, t)) = Abs (x, T, term t)
- | term (t $ u) = (term t $ (term u handle SAME => u) handle SAME => t $ term u)
+ | term (t $ u) = (term t $ Same.commit term u handle Same.SAME => t $ term u)
| term a = f a;
in term end;
-in
-
-val map_atypsT_option = option_fn o map_atypsT_same o same_fn;
-val map_atyps_option = option_fn o map_types_same o map_atypsT_same o same_fn;
-val map_types_option = option_fn o map_types_same o same_fn;
-val map_aterms_option = option_fn o map_aterms_same o same_fn;
-
-end;
+val map_atypsT_option = Same.capture o map_atypsT_same o Same.function;
+val map_atyps_option = Same.capture o map_types_same o map_atypsT_same o Same.function;
+val map_types_option = Same.capture o map_types_same o Same.function;
+val map_aterms_option = Same.capture o map_aterms_same o Same.function;
(* generalization of fixed variables *)
local
-fun generalizeT_same [] _ _ = raise SAME
+fun generalizeT_same [] _ _ = raise Same.SAME
| generalizeT_same tfrees idx ty =
let
- fun gen_typ (Type (a, Ts)) = Type (a, gen_typs Ts)
- | gen_typ (TFree (a, S)) =
+ fun gen (Type (a, Ts)) = Type (a, Same.map gen Ts)
+ | gen (TFree (a, S)) =
if member (op =) tfrees a then TVar ((a, idx), S)
- else raise SAME
- | gen_typ _ = raise SAME
- and gen_typs (T :: Ts) =
- (gen_typ T :: (gen_typs Ts handle SAME => Ts)
- handle SAME => T :: gen_typs Ts)
- | gen_typs [] = raise SAME;
- in gen_typ ty end;
+ else raise Same.SAME
+ | gen _ = raise Same.SAME;
+ in gen ty end;
-fun generalize_same ([], []) _ _ = raise SAME
+fun generalize_same ([], []) _ _ = raise Same.SAME
| generalize_same (tfrees, frees) idx tm =
let
val genT = generalizeT_same tfrees idx;
fun gen (Free (x, T)) =
if member (op =) frees x then
- Var (Name.clean_index (x, idx), genT T handle SAME => T)
+ Var (Name.clean_index (x, idx), Same.commit genT T)
else Free (x, genT T)
| gen (Var (xi, T)) = Var (xi, genT T)
| gen (Const (c, T)) = Const (c, genT T)
- | gen (Bound _) = raise SAME
+ | gen (Bound _) = raise Same.SAME
| gen (Abs (x, T, t)) =
- (Abs (x, genT T, gen t handle SAME => t)
- handle SAME => Abs (x, T, gen t))
- | gen (t $ u) = (gen t $ (gen u handle SAME => u) handle SAME => t $ gen u);
+ (Abs (x, genT T, Same.commit gen t)
+ handle Same.SAME => Abs (x, T, gen t))
+ | gen (t $ u) = (gen t $ Same.commit gen u handle Same.SAME => t $ gen u);
in gen tm end;
in
-fun generalize names i tm = generalize_same names i tm handle SAME => tm;
-fun generalizeT names i ty = generalizeT_same names i ty handle SAME => ty;
+fun generalize names i tm = generalize_same names i tm handle Same.SAME => tm;
+fun generalizeT names i ty = generalizeT_same names i ty handle Same.SAME => ty;
-fun generalize_option names i tm = SOME (generalize_same names i tm) handle SAME => NONE;
-fun generalizeT_option names i ty = SOME (generalizeT_same names i ty) handle SAME => NONE;
+fun generalize_option names i tm = SOME (generalize_same names i tm) handle Same.SAME => NONE;
+fun generalizeT_option names i ty = SOME (generalizeT_same names i ty) handle Same.SAME => NONE;
end;
@@ -148,12 +126,12 @@
| subst_typ (TVar ((a, i), S)) =
(case AList.lookup Term.eq_tvar instT ((a, i), S) of
SOME (T, j) => (maxify j; T)
- | NONE => (maxify i; raise SAME))
- | subst_typ _ = raise SAME
+ | NONE => (maxify i; raise Same.SAME))
+ | subst_typ _ = raise Same.SAME
and subst_typs (T :: Ts) =
- (subst_typ T :: (subst_typs Ts handle SAME => Ts)
- handle SAME => T :: subst_typs Ts)
- | subst_typs [] = raise SAME;
+ (subst_typ T :: Same.commit subst_typs Ts
+ handle Same.SAME => T :: subst_typs Ts)
+ | subst_typs [] = raise Same.SAME;
in subst_typ ty end;
fun instantiate_same maxidx (instT, inst) tm =
@@ -164,43 +142,43 @@
fun subst (Const (c, T)) = Const (c, substT T)
| subst (Free (x, T)) = Free (x, substT T)
| subst (Var ((x, i), T)) =
- let val (T', same) = (substT T, false) handle SAME => (T, true) in
+ let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
(case AList.lookup Term.eq_var inst ((x, i), T') of
SOME (t, j) => (maxify j; t)
- | NONE => (maxify i; if same then raise SAME else Var ((x, i), T')))
+ | NONE => (maxify i; if same then raise Same.SAME else Var ((x, i), T')))
end
- | subst (Bound _) = raise SAME
+ | subst (Bound _) = raise Same.SAME
| subst (Abs (x, T, t)) =
- (Abs (x, substT T, subst t handle SAME => t)
- handle SAME => Abs (x, T, subst t))
- | subst (t $ u) = (subst t $ (subst u handle SAME => u) handle SAME => t $ subst u);
+ (Abs (x, substT T, Same.commit subst t)
+ handle Same.SAME => Abs (x, T, subst t))
+ | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
in subst tm end;
in
fun instantiateT_maxidx instT ty i =
let val maxidx = ref i
- in (instantiateT_same maxidx instT ty handle SAME => ty, ! maxidx) end;
+ in (instantiateT_same maxidx instT ty handle Same.SAME => ty, ! maxidx) end;
fun instantiate_maxidx insts tm i =
let val maxidx = ref i
- in (instantiate_same maxidx insts tm handle SAME => tm, ! maxidx) end;
+ in (instantiate_same maxidx insts tm handle Same.SAME => tm, ! maxidx) end;
fun instantiateT [] ty = ty
| instantiateT instT ty =
- (instantiateT_same (ref ~1) (no_indexes1 instT) ty handle SAME => ty);
+ (instantiateT_same (ref ~1) (no_indexes1 instT) ty handle Same.SAME => ty);
fun instantiate ([], []) tm = tm
| instantiate insts tm =
- (instantiate_same (ref ~1) (no_indexes2 insts) tm handle SAME => tm);
+ (instantiate_same (ref ~1) (no_indexes2 insts) tm handle Same.SAME => tm);
fun instantiateT_option [] _ = NONE
| instantiateT_option instT ty =
- (SOME (instantiateT_same (ref ~1) (no_indexes1 instT) ty) handle SAME => NONE);
+ (SOME (instantiateT_same (ref ~1) (no_indexes1 instT) ty) handle Same.SAME => NONE);
fun instantiate_option ([], []) _ = NONE
| instantiate_option insts tm =
- (SOME (instantiate_same (ref ~1) (no_indexes2 insts) tm) handle SAME => NONE);
+ (SOME (instantiate_same (ref ~1) (no_indexes2 insts) tm) handle Same.SAME => NONE);
end;
--- a/src/Pure/thm.ML Wed Jul 15 15:09:56 2009 +0200
+++ b/src/Pure/thm.ML Fri Jul 17 10:07:15 2009 +0200
@@ -1232,7 +1232,7 @@
if i < 0 then raise THM ("negative increment", 0, [thm])
else if i = 0 then thm
else
- Thm (deriv_rule1 (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i)) der,
+ Thm (deriv_rule1 (Pt.incr_indexes i) der,
{thy_ref = thy_ref,
tags = [],
maxidx = maxidx + i,
--- a/src/ZF/Datatype_ZF.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/ZF/Datatype_ZF.thy Fri Jul 17 10:07:15 2009 +0200
@@ -1,8 +1,6 @@
(* Title: ZF/Datatype.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
-
*)
header{*Datatype and CoDatatype Definitions*}
@@ -103,7 +101,7 @@
handle Match => NONE;
- val conv = Simplifier.simproc (the_context ()) "data_free" ["(x::i) = y"] proc;
+ val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc;
end;
--- a/src/ZF/OrdQuant.thy Wed Jul 15 15:09:56 2009 +0200
+++ b/src/ZF/OrdQuant.thy Fri Jul 17 10:07:15 2009 +0200
@@ -1,5 +1,4 @@
(* Title: ZF/AC/OrdQuant.thy
- ID: $Id$
Authors: Krzysztof Grabczewski and L C Paulson
*)
@@ -382,9 +381,9 @@
in
-val defREX_regroup = Simplifier.simproc (the_context ())
+val defREX_regroup = Simplifier.simproc @{theory}
"defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
-val defRALL_regroup = Simplifier.simproc (the_context ())
+val defRALL_regroup = Simplifier.simproc @{theory}
"defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
end;