# HG changeset patch # User berghofe # Date 1247818035 -7200 # Node ID efc5f4806cd540368a078f18abdc5378a1e16c46 # Parent 47122b809e3785a06d4091cc7c072351173d428d# Parent 64a12f353c576dc70208f16eb73b0aa445d0664c merged diff -r 64a12f353c57 -r efc5f4806cd5 src/CCL/CCL.thy --- 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 [= ", "~ [= true", "~ true [= lam x. f(x)","~ lam x. f(x) [= true", diff -r 64a12f353c57 -r efc5f4806cd5 src/CCL/Hered.thy --- 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 |] ==> : HTTgen(R)", diff -r 64a12f353c57 -r efc5f4806cd5 src/CCL/Term.thy --- 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'", diff -r 64a12f353c57 -r efc5f4806cd5 src/CCL/Type.thy --- 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}) [" : POgen(R)", " : POgen(R)", "[| : R; : R |] ==> <,> : 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}) [" : EQgen(R)", " : EQgen(R)", "[| : R; : R |] ==> <,> : EQgen(R)", diff -r 64a12f353c57 -r efc5f4806cd5 src/FOL/simpdata.ML --- 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; diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Algebra/abstract/Ring2.thy --- 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; *} diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Divides.thy --- 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]; diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/GCD.thy --- 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) \ \ p dvd n \ 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) \ ~ p dvd a \ - 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<.. 1 & (list_all (%n. ~ n dvd p) [2.. 1 & (ALL n : {1<.. 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) \ ~ p dvd a \ 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) \ ~ p dvd a \ - coprime a (p^m)" +lemma prime_imp_power_coprime_int: "prime (p::int) \ ~ p dvd a \ 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) \ prime q \ p ~= q \ - coprime (p^m) (q^n)" +lemma primes_imp_powers_coprime_nat: "prime (p::nat) \ prime q \ p ~= q \ coprime (p^m) (q^n)" by (rule coprime_exp2_nat, rule primes_coprime_nat) -lemma primes_imp_powers_coprime_int: "prime (p::int) \ prime q \ p ~= q \ - coprime (p^m) (q^n)" +lemma primes_imp_powers_coprime_int: "prime (p::int) \ prime q \ p ~= q \ coprime (p^m) (q^n)" by (rule coprime_exp2_int, rule primes_coprime_int) lemma prime_factor_nat: "n \ (1::nat) \ \ p. prime p \ p dvd n" diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/IntDiv.thy --- 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]; diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Lambda/WeakNorm.thy --- 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 diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/List.thy --- 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\int. i+1)" +successor_int_def[simp]: "successor = (%i\int. i+1)" instance by intro_classes (simp_all add: successor_int_def) diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Modelcheck/EindhovenSyn.thy --- 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 = diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Modelcheck/MuckeSyn.thy --- 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]; diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Nominal/Examples/Fsub.thy --- 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 \ tyvrs set" @@ -108,16 +108,16 @@ by auto consts - "ty_domain" :: "env \ tyvrs set" + "ty_dom" :: "env \ tyvrs set" primrec - "ty_domain [] = {}" - "ty_domain (X#\) = (tyvrs_of X)\(ty_domain \)" + "ty_dom [] = {}" + "ty_dom (X#\) = (tyvrs_of X)\(ty_dom \)" consts - "trm_domain" :: "env \ vrs set" + "trm_dom" :: "env \ vrs set" primrec - "trm_domain [] = {}" - "trm_domain (X#\) = (vrs_of X)\(trm_domain \)" + "trm_dom [] = {}" + "trm_dom (X#\) = (vrs_of X)\(trm_dom \)" lemma vrs_of_eqvt[eqvt]: fixes pi ::"tyvrs prm" @@ -128,13 +128,13 @@ and "pi'\(vrs_of x) = vrs_of (pi'\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 \(ty_domain \) = ty_domain (pi\\)" - and "pi'\(ty_domain \) = ty_domain (pi'\\)" - and "pi \(trm_domain \) = trm_domain (pi\\)" - and "pi'\(trm_domain \) = trm_domain (pi'\\)" + shows "pi \(ty_dom \) = ty_dom (pi\\)" + and "pi'\(ty_dom \) = ty_dom (pi'\\)" + and "pi \(trm_dom \) = trm_dom (pi\\)" + and "pi'\(trm_dom \) = trm_dom (pi'\\)" by (induct \) (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 \)" - and "finite (trm_domain \)" +lemma finite_doms: + shows "finite (ty_dom \)" + and "finite (trm_dom \)" by (induct \, auto simp add: finite_vrs) -lemma ty_domain_supp: - shows "(supp (ty_domain \)) = (ty_domain \)" - and "(supp (trm_domain \)) = (trm_domain \)" -by (simp only: at_fin_set_supp at_tyvrs_inst at_vrs_inst finite_domains)+ +lemma ty_dom_supp: + shows "(supp (ty_dom \)) = (ty_dom \)" + and "(supp (trm_dom \)) = (trm_dom \)" +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)\set \" - shows "X\(ty_domain \)" + shows "X\(ty_dom \)" using a by (induct \, 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\(ty_domain \)" +lemma ty_dom_existence: + assumes a: "X\(ty_dom \)" shows "\T.(TVarB X T)\set \" using a apply (induct \, auto) @@ -173,9 +173,9 @@ apply (auto simp add: ty_binding_existence) done -lemma domains_append: - shows "ty_domain (\@\) = ((ty_domain \) \ (ty_domain \))" - and "trm_domain (\@\) = ((trm_domain \) \ (trm_domain \))" +lemma doms_append: + shows "ty_dom (\@\) = ((ty_dom \) \ (ty_dom \))" + and "trm_dom (\@\) = ((trm_dom \) \ (trm_dom \))" by (induct \, auto) lemma ty_vrs_prm_simp: @@ -184,15 +184,15 @@ shows "pi\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\(ty_domain (Y#\)) = (X\(tyvrs_of Y) \ X\(ty_domain \))" + shows "X\(ty_dom (Y#\)) = (X\(tyvrs_of Y) \ X\(ty_dom \))" 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\\" - shows "X\(ty_domain \)" + shows "X\(ty_dom \)" using a apply(induct \) 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#\"} all free variables of @{term "S"} must be - in the @{term "ty_domain"} of @{term "\"}, that is @{term "S"} must be @{text "closed"} + in the @{term "ty_dom"} of @{term "\"}, that is @{term "S"} must be @{text "closed"} in @{term "\"}. The set of free variables of @{term "S"} is the @{text "support"} of @{term "S"}. *} constdefs "closed_in" :: "ty \ env \ bool" ("_ closed'_in _" [100,100] 100) - "S closed_in \ \ (supp S)\(ty_domain \)" + "S closed_in \ \ (supp S)\(ty_dom \)" lemma closed_in_eqvt[eqvt]: fixes pi::"tyvrs prm" @@ -251,10 +251,10 @@ shows "x \ 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 \::"env" - shows "(ty_domain (pi\\)) = (ty_domain \)" + shows "(ty_dom (pi\\)) = (ty_dom \)" apply(induct \) apply (simp add: eqvts) apply(simp add: tyvrs_vrs_prm_simp) @@ -265,7 +265,7 @@ assumes a: "S closed_in \" shows "(pi\S) closed_in (pi\\)" 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\ trm_domain \ = x\\" + shows "x\ trm_dom \ = x\\" by (induct \) (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) \ ty_domain \ \ T closed_in \ \ X \ T" - by (auto simp add: closed_in_def fresh_def ty_domain_supp) +lemma closed_in_fresh: "(X::tyvrs) \ ty_dom \ \ T closed_in \ \ X \ 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 \ bool" ("\ _ ok" [100] 100) where valid_nil[simp]: "\ [] ok" -| valid_consT[simp]: "\\ \ ok; X\(ty_domain \); T closed_in \\ \ \ (TVarB X T#\) ok" -| valid_cons [simp]: "\\ \ ok; x\(trm_domain \); T closed_in \\ \ \ (VarB x T#\) ok" +| valid_consT[simp]: "\\ \ ok; X\(ty_dom \); T closed_in \\ \ \ (TVarB X T#\) ok" +| valid_cons [simp]: "\\ \ ok; x\(trm_dom \); T closed_in \\ \ \ (VarB x T#\) ok" equivariance valid_rel declare binding.inject [simp add] declare trm.inject [simp add] -inductive_cases validE[elim]: "\ (TVarB X T#\) ok" "\ (VarB x T#\) ok" "\ (b#\) ok" +inductive_cases validE[elim]: + "\ (TVarB X T#\) ok" + "\ (VarB x T#\) ok" + "\ (b#\) ok" declare binding.inject [simp del] declare trm.inject [simp del] @@ -321,12 +324,12 @@ using a b proof(induct \) 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 \') 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 \ X' T') moreover { fix \'::"env" - assume a: "X'\(ty_domain \')" + assume a: "X'\(ty_dom \')" have "\(\T.(TVarB X' T)\(set \'))" using a proof (induct \') case (Cons Y \') thus "\ (\T.(TVarB X' T)\set(Y#\'))" - 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 \ x' T') moreover { fix \'::"env" - assume a: "x'\(trm_domain \')" + assume a: "x'\(trm_dom \')" have "\(\T.(VarB x' T)\(set \'))" using a proof (induct \') case (Cons y \') thus "\ (\T.(VarB x' T)\set(y#\'))" 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 \ T]\<^sub>\ = (if X=Y then T else Tvar X)" | "(Top)[Y \ T]\<^sub>\ = Top" | "(T\<^isub>1 \ T\<^isub>2)[Y \ T]\<^sub>\ = T\<^isub>1[Y \ T]\<^sub>\ \ T\<^isub>2[Y \ T]\<^sub>\" -| "\X\(Y,T); X\T\<^isub>1\ \ (\X<:T\<^isub>1. T\<^isub>2)[Y \ T]\<^sub>\ = (\X<:T\<^isub>1[Y \ T]\<^sub>\. T\<^isub>2[Y \ T]\<^sub>\)" +| "X\(Y,T,T\<^isub>1) \ (\X<:T\<^isub>1. T\<^isub>2)[Y \ T]\<^sub>\ = (\X<:T\<^isub>1[Y \ T]\<^sub>\. T\<^isub>2[Y \ T]\<^sub>\)" apply (finite_guess)+ apply (rule TrueI)+ apply (simp add: abs_fresh) @@ -424,8 +427,8 @@ lemma type_subst_fresh: fixes X::"tyvrs" - assumes "X \ T" and "X \ P" - shows "X \ T[Y \ P]\<^sub>\" + assumes "X\T" and "X\P" + shows "X\T[Y \ P]\<^sub>\" 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 \ T \ T[X \ U]\<^sub>\ = T" +lemma type_subst_identity: + "X\T \ T[X \ U]\<^sub>\ = T" by (nominal_induct T avoiding: X U rule: ty.strong_induct) (simp_all add: fresh_atm abs_fresh) lemma type_substitution_lemma: - "X \ Y \ X \ L \ M[X \ N]\<^sub>\[Y \ L]\<^sub>\ = M[Y \ L]\<^sub>\[X \ N[Y \ L]\<^sub>\]\<^sub>\" + "X \ Y \ X\L \ M[X \ N]\<^sub>\[Y \ L]\<^sub>\ = M[Y \ L]\<^sub>\[X \ N[Y \ L]\<^sub>\]\<^sub>\" 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 \ T \ ([(Y, X)] \ T)[Y \ U]\<^sub>\ = T[X \ U]\<^sub>\" + "Y\T \ ([(Y,X)]\T)[Y \ U]\<^sub>\ = T[X \ U]\<^sub>\" 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 \ a" - and "X \ P" - shows "X \ a[Y \ P]\<^sub>b" + assumes "X\a" + and "X\P" + shows "X\a[Y \ 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 \ B \ B[X \ U]\<^sub>b = B" + shows "X\B \ B[X \ 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 \ \" - and "X \ P" - shows "X \ \[Y \ P]\<^sub>e" + assumes "X\\" + and "X\P" + shows "X\\[Y \ P]\<^sub>e" using assms by (induct \) (auto simp add: fresh_list_cons binding_subst_fresh) @@ -494,7 +498,7 @@ lemma ctxt_subst_mem_VarB: "VarB x T \ set \ \ VarB x (T[Y \ U]\<^sub>\) \ set (\[Y \ U]\<^sub>e)" by (induct \) auto -lemma ctxt_subst_identity: "X \ \ \ \[X \ U]\<^sub>e = \" +lemma ctxt_subst_identity: "X\\ \ \[X \ U]\<^sub>e = \" by (induct \) (simp_all add: fresh_list_cons binding_subst_identity) lemma ctxt_subst_append: "(\ @ \)[X \ T]\<^sub>e = \[X \ T]\<^sub>e @ \[X \ T]\<^sub>e" @@ -515,11 +519,13 @@ done lemma subst_trm_fresh_tyvar: - "(X::tyvrs) \ t \ X \ u \ X \ t[x \ u]" + fixes X::"tyvrs" + shows "X\t \ X\u \ X\t[x \ 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 \ u \ x \ t[x \ u]" +lemma subst_trm_fresh_var: + "x\u \ x\t[x \ 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 \ t \ ([(y, x)] \ t)[y \ u] = t[x \ u]" + "y\t \ ([(y, x)] \ t)[y \ u] = t[x \ 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) \ t \ X \ T \ X \ t[Y \\<^sub>\ T]" + fixes X::"tyvrs" + shows "X\t \ X\T \ X\t[Y \\<^sub>\ 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 \ T \ X \ t[X \\<^sub>\ T]" + "X\T \ X\t[X \\<^sub>\ 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 \ t \ ([(Y, X)] \ t)[Y \\<^sub>\ U] = t[X \\<^sub>\ U]" + "Y\t \ ([(Y, X)] \ t)[Y \\<^sub>\ U] = t[X \\<^sub>\ 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 \ ty \ ty \ bool" ("_\_<:_" [100,100,100] 100) where SA_Top[intro]: "\\ \ ok; S closed_in \\ \ \ \ S <: Top" -| SA_refl_TVar[intro]: "\\ \ ok; X \ ty_domain \\\ \ \ Tvar X <: Tvar X" +| SA_refl_TVar[intro]: "\\ \ ok; X \ ty_dom \\\ \ \ Tvar X <: Tvar X" | SA_trans_TVar[intro]: "\(TVarB X S) \ set \; \ \ S <: T\ \ \ \ (Tvar X) <: T" | SA_arrow[intro]: "\\ \ T\<^isub>1 <: S\<^isub>1; \ \ S\<^isub>2 <: T\<^isub>2\ \ \ \ (S\<^isub>1 \ S\<^isub>2) <: (T\<^isub>1 \ T\<^isub>2)" | SA_all[intro]: "\\ \ T\<^isub>1 <: S\<^isub>1; ((TVarB X T\<^isub>1)#\) \ S\<^isub>2 <: T\<^isub>2\ \ \ \ (\X<:S\<^isub>1. S\<^isub>2) <: (\X<:T\<^isub>1. T\<^isub>2)" @@ -623,7 +630,7 @@ next case (SA_trans_TVar X S \ T) have "(TVarB X S)\set \" by fact - hence "X \ ty_domain \" by (rule ty_domain_inclusion) + hence "X \ ty_dom \" by (rule ty_dom_inclusion) hence "(Tvar X) closed_in \" by (simp add: closed_in_def ty.supp supp_atm) moreover have "S closed_in \ \ T closed_in \" by fact @@ -638,23 +645,23 @@ shows "X\S \ X\T" proof - from a1 have "\ \ ok" by (rule subtype_implies_ok) - with a2 have "X\ty_domain(\)" by (simp add: fresh_domain) + with a2 have "X\ty_dom(\)" by (simp add: fresh_dom) moreover from a1 have "S closed_in \ \ T closed_in \" by (rule subtype_implies_closed) - hence "supp S \ ((supp (ty_domain \))::tyvrs set)" - and "supp T \ ((supp (ty_domain \))::tyvrs set)" by (simp_all add: ty_domain_supp closed_in_def) + hence "supp S \ ((supp (ty_dom \))::tyvrs set)" + and "supp T \ ((supp (ty_dom \))::tyvrs set)" by (simp_all add: ty_dom_supp closed_in_def) ultimately show "X\S \ X\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: "\ \ ok" - shows "X\(ty_domain \) = X\\" + shows "X\(ty_dom \) = X\\" 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: "\\. \\ \ ok; T\<^isub>1 closed_in \\ \ \ \ T\<^isub>1 <: T\<^isub>1" by fact have ih_T\<^isub>2: "\\. \\ \ ok; T\<^isub>2 closed_in \\ \ \ \ T\<^isub>2 <: T\<^isub>2" by fact have fresh_cond: "X\\" by fact - hence fresh_ty_domain: "X\(ty_domain \)" by (simp add: fresh_domain) + hence fresh_ty_dom: "X\(ty_dom \)" by (simp add: fresh_dom) have "(\X<:T\<^isub>2. T\<^isub>1) closed_in \" by fact hence closed\<^isub>T\<^isub>2: "T\<^isub>2 closed_in \" and closed\<^isub>T\<^isub>1: "T\<^isub>1 closed_in ((TVarB X T\<^isub>2)#\)" by (auto simp add: closed_in_def ty.supp abs_supp) have ok: "\ \ ok" by fact - hence ok': "\ ((TVarB X T\<^isub>2)#\) ok" using closed\<^isub>T\<^isub>2 fresh_ty_domain by simp + hence ok': "\ ((TVarB X T\<^isub>2)#\) ok" using closed\<^isub>T\<^isub>2 fresh_ty_dom by simp have "\ \ 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)#\) \ 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)#\" 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 \ env \ bool" ("_ extends _" [100,100] 100) "\ extends \ \ \X Q. (TVarB X Q)\set \ \ (TVarB X Q)\set \" -lemma extends_ty_domain: +lemma extends_ty_dom: assumes a: "\ extends \" - shows "ty_domain \ \ ty_domain \" + shows "ty_dom \ \ ty_dom \" 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: "\ extends \" shows "T closed_in \" 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: "\ extends \" @@ -763,18 +770,18 @@ ultimately show "\ \ Tvar X <: T" using ok by force next case (SA_refl_TVar \ X) - have lh_drv_prem: "X \ ty_domain \" by fact + have lh_drv_prem: "X \ ty_dom \" by fact have "\ \ ok" by fact moreover have "\ extends \" by fact - hence "X \ ty_domain \" using lh_drv_prem by (force dest: extends_ty_domain) + hence "X \ ty_dom \" using lh_drv_prem by (force dest: extends_ty_dom) ultimately show "\ \ Tvar X <: Tvar X" by force next case (SA_arrow \ T\<^isub>1 S\<^isub>1 S\<^isub>2 T\<^isub>2) thus "\ \ S\<^isub>1 \ S\<^isub>2 <: T\<^isub>1 \ T\<^isub>2" by blast next case (SA_all \ T\<^isub>1 S\<^isub>1 X S\<^isub>2 T\<^isub>2) have fresh_cond: "X\\" by fact - hence fresh_domain: "X\(ty_domain \)" by (simp add: fresh_domain) + hence fresh_dom: "X\(ty_dom \)" by (simp add: fresh_dom) have ih\<^isub>1: "\\. \ \ ok \ \ extends \ \ \ \ T\<^isub>1 <: S\<^isub>1" by fact have ih\<^isub>2: "\\. \ \ ok \ \ extends ((TVarB X T\<^isub>1)#\) \ \ \ S\<^isub>2 <: T\<^isub>2" by fact have lh_drv_prem: "\ \ T\<^isub>1 <: S\<^isub>1" by fact @@ -782,7 +789,7 @@ have ok: "\ \ ok" by fact have ext: "\ extends \" by fact have "T\<^isub>1 closed_in \" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed) - hence "\ ((TVarB X T\<^isub>1)#\) ok" using fresh_domain ok by force + hence "\ ((TVarB X T\<^isub>1)#\) ok" using fresh_dom ok by force moreover have "((TVarB X T\<^isub>1)#\) extends ((TVarB X T\<^isub>1)#\)" using ext by (force simp add: extends_def) ultimately have "((TVarB X T\<^isub>1)#\) \ S\<^isub>2 <: T\<^isub>2" using ih\<^isub>2 by simp @@ -802,7 +809,7 @@ proof (nominal_induct \ S T avoiding: \ rule: subtype_of.strong_induct) case (SA_all \ T\<^isub>1 S\<^isub>1 X S\<^isub>2 T\<^isub>2) have fresh_cond: "X\\" by fact - hence fresh_domain: "X\(ty_domain \)" by (simp add: fresh_domain) + hence fresh_dom: "X\(ty_dom \)" by (simp add: fresh_dom) have ih\<^isub>1: "\\. \ \ ok \ \ extends \ \ \ \ T\<^isub>1 <: S\<^isub>1" by fact have ih\<^isub>2: "\\. \ \ ok \ \ extends ((TVarB X T\<^isub>1)#\) \ \ \ S\<^isub>2 <: T\<^isub>2" by fact have lh_drv_prem: "\ \ T\<^isub>1 <: S\<^isub>1" by fact @@ -810,14 +817,14 @@ have ok: "\ \ ok" by fact have ext: "\ extends \" by fact have "T\<^isub>1 closed_in \" using ext closed\<^isub>T\<^isub>1 by (simp only: extends_closed) - hence "\ ((TVarB X T\<^isub>1)#\) ok" using fresh_domain ok by force + hence "\ ((TVarB X T\<^isub>1)#\) ok" using fresh_dom ok by force moreover have "((TVarB X T\<^isub>1)#\) extends ((TVarB X T\<^isub>1)#\)" using ext by (force simp add: extends_def) ultimately have "((TVarB X T\<^isub>1)#\) \ S\<^isub>2 <: T\<^isub>2" using ih\<^isub>2 by simp moreover have "\ \ T\<^isub>1 <: S\<^isub>1" using ok ext ih\<^isub>1 by simp ultimately show "\ \ (\X<:S\<^isub>1. S\<^isub>2) <: (\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 "\\ \ (\X<:S\<^isub>1. S\<^isub>2) <: T; X\\; X\S\<^isub>1\ + shows "\\ \ (\X<:S\<^isub>1. S\<^isub>2) <: T; X\\; X\S\<^isub>1; X\T\ \ T = Top \ (\T\<^isub>1 T\<^isub>2. T = (\X<:T\<^isub>1. T\<^isub>2) \ \ \ T\<^isub>1 <: S\<^isub>1 \ ((TVarB X T\<^isub>1)#\) \ S\<^isub>2 <: T\<^isub>2)" - apply(frule subtype_implies_ok) - apply(ind_cases "\ \ (\X<:S\<^isub>1. S\<^isub>2) <: T") - apply(auto simp add: ty.inject alpha) - apply(rule_tac x="[(X,Xa)]\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 \="((TVarB Xa T\<^isub>1)#\)" in subtype_implies_closed)+ - apply(simp add: closed_in_def) - apply(drule fresh_domain)+ - apply(simp add: fresh_def) - apply(subgoal_tac "X \ (insert Xa (ty_domain \))")(*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 \="TVarB Xa T\<^isub>1 # \" 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: "(\@[(TVarB X Q)]@\)\M<:N \ \\P<:Q \ (\@[(TVarB X P)]@\)\M<:N" proof (induct Q arbitrary: \ S T \ 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: "\Q' \ S T. \size_ty Q' < size_ty Q; \\S<:Q'; \\Q'<:T\ \ \\S<:T" by fact have IH_narrow: "\Q' \ \ X M N P. \size_ty Q' < size_ty Q; (\@[(TVarB X Q')]@\)\M<:N; \\P<:Q'\ \ (\@[(TVarB X P)]@\)\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: - "\\ S T. \\ \ S <: Q; \ \ Q <: T\ \ \ \ S <: T" - proof - - fix \' S' T - assume "\' \ S' <: Q" --{* left-hand derivation *} - and "\' \ Q <: T" --{* right-hand derivation *} - thus "\' \ S' <: T" - proof (nominal_induct \' S' Q\Q rule: subtype_of.strong_induct) + + { fix \ S T + have "\\ \ S <: Q; \ \ Q <: T\ \ \ \ S <: T" + proof (induct \ S Q\Q rule: subtype_of.induct) case (SA_Top \ S) - --{* \begin{minipage}[t]{0.9\textwidth} - In this case the left-hand derivation is @{term "\ \ S <: Top"}, giving - us @{term "\ \ ok"} and @{term "S closed_in \"}. This case is straightforward, - because the right-hand derivation must be of the form @{term "\ \ Top <: Top"} - giving us the equation @{term "T = Top"}.\end{minipage}*} - hence rh_drv: "\ \ Top <: T" by simp - hence T_inst: "T = Top" by (auto elim: S_TopE) + then have rh_drv: "\ \ Top <: T" by simp + then have T_inst: "T = Top" by (auto elim: S_TopE) from `\ \ ok` and `S closed_in \` - have "\ \ S <: Top" by (simp add: subtype_of.SA_Top) - thus "\ \ S <: T" using T_inst by simp + have "\ \ S <: Top" by auto + then show "\ \ S <: T" using T_inst by simp next case (SA_trans_TVar Y U \) - -- {* \begin{minipage}[t]{0.9\textwidth} - In this case the left-hand derivation is @{term "\ \ Tvar Y <: Q"} - with @{term "S = Tvar Y"}. We have therefore @{term "(Y,U)"} - is in @{term "\"} and by inner induction hypothesis that @{term "\ \ U <: T"}. - By @{text "S_Var"} follows @{term "\ \ Tvar Y <: T"}.\end{minipage}*} - hence IH_inner: "\ \ U <: T" by simp + then have IH_inner: "\ \ U <: T" by simp have "(TVarB Y U) \ set \" by fact - with IH_inner show "\ \ Tvar Y <: T" by (simp add: subtype_of.SA_trans_TVar) + with IH_inner show "\ \ Tvar Y <: T" by auto next case (SA_refl_TVar \ X) - --{* \begin{minipage}[t]{0.9\textwidth} - In this case the left-hand derivation is @{term "\\(Tvar X) <: (Tvar X)"} with - @{term "Q=Tvar X"}. The goal then follows immediately from the right-hand - derivation.\end{minipage}*} - thus "\ \ Tvar X <: T" by simp + then show "\ \ Tvar X <: T" by simp next case (SA_arrow \ 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 "\ \ S\<^isub>1 \ S\<^isub>2 <: Q\<^isub>1 \ Q\<^isub>2"} with - @{term "S\<^isub>1\S\<^isub>2=S"} and @{term "Q\<^isub>1\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 "\\Q\<^isub>1<:S\<^isub>1"} and @{term "\\S\<^isub>2<:Q\<^isub>2"}. - The right-hand derivation is @{term "\ \ Q\<^isub>1 \ Q\<^isub>2 <: T"}. There exist types - @{text "T\<^isub>1,T\<^isub>2"} such that @{term "T=Top \ T=T\<^isub>1\T\<^isub>2"}. The @{term "Top"}-case is - straightforward once we know @{term "(S\<^isub>1 \ S\<^isub>2) closed_in \"} and @{term "\ \ ok"}. - In the other case we have the sub-derivations @{term "\\T\<^isub>1<:Q\<^isub>1"} and @{term "\\Q\<^isub>2<:T\<^isub>2"}. - Using the outer induction hypothesis for transitivity we can derive @{term "\\T\<^isub>1<:S\<^isub>1"} - and @{term "\\S\<^isub>2<:T\<^isub>2"}. By rule @{text "S_Arrow"} follows @{term "\ \ S\<^isub>1 \ S\<^isub>2 <: T\<^isub>1 \ T\<^isub>2"}, - which is @{term "\ \ S\<^isub>1 \ S\<^isub>2 <: T\<^isub>"}.\end{minipage}*} - hence rh_drv: "\ \ Q\<^isub>1 \ Q\<^isub>2 <: T" by simp + then have rh_drv: "\ \ Q\<^isub>1 \ Q\<^isub>2 <: T" by simp from `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" by auto have lh_drv_prm\<^isub>1: "\ \ Q\<^isub>1 <: S\<^isub>1" by fact have lh_drv_prm\<^isub>2: "\ \ S\<^isub>2 <: Q\<^isub>2" by fact from rh_drv have "T=Top \ (\T\<^isub>1 T\<^isub>2. T=T\<^isub>1\T\<^isub>2 \ \\T\<^isub>1<:Q\<^isub>1 \ \\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 \" and "S\<^isub>2 closed_in \" using lh_drv_prm\<^isub>1 lh_drv_prm\<^isub>2 by (simp_all add: subtype_implies_closed) @@ -974,7 +917,7 @@ moreover have "\ \ ok" using rh_drv by (rule subtype_implies_ok) moreover - { assume "\T\<^isub>1 T\<^isub>2. T=T\<^isub>1\T\<^isub>2 \ \\T\<^isub>1<:Q\<^isub>1 \ \\Q\<^isub>2<:T\<^isub>2" + { assume "\T\<^isub>1 T\<^isub>2. T = T\<^isub>1\T\<^isub>2 \ \ \ T\<^isub>1 <: Q\<^isub>1 \ \ \ Q\<^isub>2 <: T\<^isub>2" then obtain T\<^isub>1 T\<^isub>2 where T_inst: "T = T\<^isub>1 \ T\<^isub>2" and rh_drv_prm\<^isub>1: "\ \ T\<^isub>1 <: Q\<^isub>1" @@ -984,46 +927,26 @@ moreover from IH_trans[of "Q\<^isub>2"] have "\ \ 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 "\ \ S\<^isub>1 \ S\<^isub>2 <: T\<^isub>1 \ T\<^isub>2" by (simp add: subtype_of.SA_arrow) - hence "\ \ S\<^isub>1 \ S\<^isub>2 <: T" using T_inst by simp + ultimately have "\ \ S\<^isub>1 \ S\<^isub>2 <: T\<^isub>1 \ T\<^isub>2" by auto + then have "\ \ S\<^isub>1 \ S\<^isub>2 <: T" using T_inst by simp } ultimately show "\ \ S\<^isub>1 \ S\<^isub>2 <: T" by blast next case (SA_all \ 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 "\\(\X<:S\<^isub>1. S\<^isub>2) <: (\X<:Q\<^isub>1. Q\<^isub>2)"} with - @{term "(\X<:S\<^isub>1. S\<^isub>2)=S"} and @{term "(\X<:Q\<^isub>1. Q\<^isub>2)=Q"}. We therefore have the sub-derivations - @{term "\\Q\<^isub>1<:S\<^isub>1"} and @{term "((TVarB X Q\<^isub>1)#\)\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\\"} and @{term "X\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 "\ \ (\X<:Q\<^isub>1. Q\<^isub>2) <: T"}. Since @{term "X\\"} - and @{term "X\Q\<^isub>1"} there exists types @{text "T\<^isub>1,T\<^isub>2"} such that - @{term "T=Top \ T=(\X<:T\<^isub>1. T\<^isub>2)"}. The @{term "Top"}-case is straightforward once we know - @{term "(\X<:S\<^isub>1. S\<^isub>2) closed_in \"} and @{term "\ \ ok"}. In the other case we have - the sub-derivations @{term "\\T\<^isub>1<:Q\<^isub>1"} and @{term "((TVarB X T\<^isub>1)#\)\Q\<^isub>2<:T\<^isub>2"}. Using the outer - induction hypothesis for transitivity we can derive @{term "\\T\<^isub>1<:S\<^isub>1"}. From the outer - induction for narrowing we get @{term "((TVarB X T\<^isub>1)#\) \ S\<^isub>2 <: Q\<^isub>2"} and then using again - induction for transitivity we obtain @{term "((TVarB X T\<^isub>1)#\) \ S\<^isub>2 <: T\<^isub>2"}. By rule - @{text "S_Forall"} and the freshness condition @{term "X\\"} follows - @{term "\ \ (\X<:S\<^isub>1. S\<^isub>2) <: (\X<:T\<^isub>1. T\<^isub>2)"}, which is @{term "\ \ (\X<:S\<^isub>1. S\<^isub>2) <: T\<^isub>"}. - \end{minipage}*} - hence rh_drv: "\ \ (\X<:Q\<^isub>1. Q\<^isub>2) <: T" by simp + then have rh_drv: "\ \ (\X<:Q\<^isub>1. Q\<^isub>2) <: T" by simp have lh_drv_prm\<^isub>1: "\ \ Q\<^isub>1 <: S\<^isub>1" by fact have lh_drv_prm\<^isub>2: "((TVarB X Q\<^isub>1)#\) \ S\<^isub>2 <: Q\<^isub>2" by fact - then have "X\\" by (force dest: subtype_implies_ok simp add: valid_ty_domain_fresh) - then have fresh_cond: "X\\" "X\Q\<^isub>1" using lh_drv_prm\<^isub>1 by (simp_all add: subtype_implies_fresh) - from `(\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\\" by (force dest: subtype_implies_ok simp add: valid_ty_dom_fresh) + then have fresh_cond: "X\\" "X\Q\<^isub>1" "X\T" using rh_drv lh_drv_prm\<^isub>1 + by (simp_all add: subtype_implies_fresh) from rh_drv - have "T=Top \ (\T\<^isub>1 T\<^isub>2. T=(\X<:T\<^isub>1. T\<^isub>2) \ \\T\<^isub>1<:Q\<^isub>1 \ ((TVarB X T\<^isub>1)#\)\Q\<^isub>2<:T\<^isub>2)" + have "T = Top \ + (\T\<^isub>1 T\<^isub>2. T = (\X<:T\<^isub>1. T\<^isub>2) \ \ \ T\<^isub>1 <: Q\<^isub>1 \ ((TVarB X T\<^isub>1)#\) \ Q\<^isub>2 <: T\<^isub>2)" using fresh_cond by (simp add: S_ForallE_left) moreover have "S\<^isub>1 closed_in \" and "S\<^isub>2 closed_in ((TVarB X Q\<^isub>1)#\)" using lh_drv_prm\<^isub>1 lh_drv_prm\<^isub>2 by (simp_all add: subtype_implies_closed) - hence "(\X<:S\<^isub>1. S\<^isub>2) closed_in \" by (force simp add: closed_in_def ty.supp abs_supp) + then have "(\X<:S\<^isub>1. S\<^isub>2) closed_in \" by (force simp add: closed_in_def ty.supp abs_supp) moreover have "\ \ ok" using rh_drv by (rule subtype_implies_ok) moreover @@ -1032,6 +955,9 @@ where T_inst: "T = (\X<:T\<^isub>1. T\<^isub>2)" and rh_drv_prm\<^isub>1: "\ \ T\<^isub>1 <: Q\<^isub>1" and rh_drv_prm\<^isub>2:"((TVarB X T\<^isub>1)#\) \ Q\<^isub>2 <: T\<^isub>2" by force + have "(\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 "\ \ 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 "\ \ (\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 `\ \ S <: Q` and `\ \ Q <: T` - show "\ \ S <: T" by (rule transitivity_aux) + show "\ \ S <: T" by (rule transitivity_lemma) next - --{* The narrowing proof proceeds by an induction over @{term "(\@[(TVarB X Q)]@\) \ M <: N"}. *} case 2 - from `(\@[(TVarB X Q)]@\) \ M <: N` --{* left-hand derivation *} - and `\ \ P<:Q` --{* right-hand derivation *} + from `(\@[(TVarB X Q)]@\) \ M <: N` + and `\ \ P<:Q` show "(\@[(TVarB X P)]@\) \ M <: N" - proof (nominal_induct \\"\@[(TVarB X Q)]@\" M N avoiding: \ \ X rule: subtype_of.strong_induct) - case (SA_Top _ S \ \ X) - --{* \begin{minipage}[t]{0.9\textwidth} - In this case the left-hand derivation is @{term "(\@[(TVarB X Q)]@\) \ S <: Top"}. We show - that the context @{term "\@[(TVarB X P)]@\"} is ok and that @{term S} is closed in - @{term "\@[(TVarB X P)]@\"}. Then we can apply the @{text "S_Top"}-rule.\end{minipage}*} - hence lh_drv_prm\<^isub>1: "\ (\@[(TVarB X Q)]@\) ok" + proof (induct \\"\@[(TVarB X Q)]@\" M N arbitrary: \ X \ rule: subtype_of.induct) + case (SA_Top _ S \ X \) + then have lh_drv_prm\<^isub>1: "\ (\@[(TVarB X Q)]@\) ok" and lh_drv_prm\<^isub>2: "S closed_in (\@[(TVarB X Q)]@\)" by simp_all have rh_drv: "\ \ P <: Q" by fact hence "P closed_in \" by (simp add: subtype_implies_closed) with lh_drv_prm\<^isub>1 have "\ (\@[(TVarB X P)]@\) ok" by (simp add: replace_type) moreover from lh_drv_prm\<^isub>2 have "S closed_in (\@[(TVarB X P)]@\)" - by (simp add: closed_in_def domains_append) + by (simp add: closed_in_def doms_append) ultimately show "(\@[(TVarB X P)]@\) \ S <: Top" by (simp add: subtype_of.SA_Top) next - case (SA_trans_TVar Y S _ N \ \ X) - --{* \begin{minipage}[t]{0.9\textwidth} - In this case the left-hand derivation is @{term "(\@[(TVarB X Q)]@\) \ Tvar Y <: N"} and - by inner induction hypothesis we have @{term "(\@[(TVarB X P)]@\) \ S <: N"}. We therefore - know that the contexts @{term "\@[(TVarB X Q)]@\"} and @{term "\@[(TVarB X P)]@\"} are ok, and that - @{term "(Y,S)"} is in @{term "\@[(TVarB X Q)]@\"}. We need to show that - @{term "(\@[(TVarB X P)]@\) \ Tvar Y <: N"} holds. In case @{term "X\Y"} we know that - @{term "(Y,S)"} is in @{term "\@[(TVarB X P)]@\"} 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 "(\@[(TVarB X P)]@\) extends \"} and therefore - by @{text "weakening"} that @{term "(\@[(TVarB X P)]@\) \ P <: Q"} holds. By transitivity we - obtain then @{term "(\@[(TVarB X P)]@\) \ P <: N"} and can conclude by applying rule - @{text "S_Var"}.\end{minipage}*} - hence IH_inner: "(\@[(TVarB X P)]@\) \ S <: N" + case (SA_trans_TVar Y S _ N \ X \) + then have IH_inner: "(\@[(TVarB X P)]@\) \ S <: N" and lh_drv_prm: "(TVarB Y S) \ set (\@[(TVarB X Q)]@\)" and rh_drv: "\ \ P<:Q" and ok\<^isub>Q: "\ (\@[(TVarB X Q)]@\) ok" by (simp_all add: subtype_implies_ok) - hence ok\<^isub>P: "\ (\@[(TVarB X P)]@\) ok" by (simp add: subtype_implies_ok) + then have ok\<^isub>P: "\ (\@[(TVarB X P)]@\) ok" by (simp add: subtype_implies_ok) show "(\@[(TVarB X P)]@\) \ Tvar Y <: N" proof (cases "X=Y") case False @@ -1107,48 +1016,28 @@ moreover have "(\@[(TVarB X P)]@\) extends \" by (simp add: extends_def) hence "(\@[(TVarB X P)]@\) \ P <: Q" using rh_drv ok\<^isub>P by (simp only: weakening) - ultimately have "(\@[(TVarB X P)]@\) \ P <: N" by (simp add: transitivity_aux) - thus "(\@[(TVarB X P)]@\) \ Tvar Y <: N" using memb\<^isub>X\<^isub>P eq by (simp only: subtype_of.SA_trans_TVar) + ultimately have "(\@[(TVarB X P)]@\) \ P <: N" by (simp add: transitivity_lemma) + then show "(\@[(TVarB X P)]@\) \ Tvar Y <: N" using memb\<^isub>X\<^isub>P eq by auto qed next - case (SA_refl_TVar _ Y \ \ X) - --{* \begin{minipage}[t]{0.9\textwidth} - In this case the left-hand derivation is @{term "(\@[(TVarB X Q)]@\) \ Tvar Y <: Tvar Y"} and we - therefore know that @{term "\@[(TVarB X Q)]@\"} is ok and that @{term "Y"} is in - the domain of @{term "\@[(TVarB X Q)]@\"}. We therefore know that @{term "\@[(TVarB X P)]@\"} is ok - and that @{term Y} is in the domain of @{term "\@[(TVarB X P)]@\"}. We can conclude by applying - rule @{text "S_Refl"}.\end{minipage}*} - hence lh_drv_prm\<^isub>1: "\ (\@[(TVarB X Q)]@\) ok" - and lh_drv_prm\<^isub>2: "Y \ ty_domain (\@[(TVarB X Q)]@\)" by simp_all + case (SA_refl_TVar _ Y \ X \) + then have lh_drv_prm\<^isub>1: "\ (\@[(TVarB X Q)]@\) ok" + and lh_drv_prm\<^isub>2: "Y \ ty_dom (\@[(TVarB X Q)]@\)" by simp_all have "\ \ P <: Q" by fact hence "P closed_in \" by (simp add: subtype_implies_closed) with lh_drv_prm\<^isub>1 have "\ (\@[(TVarB X P)]@\) ok" by (simp add: replace_type) moreover - from lh_drv_prm\<^isub>2 have "Y \ ty_domain (\@[(TVarB X P)]@\)" by (simp add: domains_append) + from lh_drv_prm\<^isub>2 have "Y \ ty_dom (\@[(TVarB X P)]@\)" by (simp add: doms_append) ultimately show "(\@[(TVarB X P)]@\) \ 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 \ \ X) - --{* \begin{minipage}[t]{0.9\textwidth} - In this case the left-hand derivation is @{term "(\@[(TVarB X Q)]@\) \ Q\<^isub>1 \ Q\<^isub>2 <: S\<^isub>1 \ S\<^isub>2"} - and the proof is trivial.\end{minipage}*} - thus "(\@[(TVarB X P)]@\) \ Q\<^isub>1 \ Q\<^isub>2 <: S\<^isub>1 \ S\<^isub>2" by blast + case (SA_arrow _ S\<^isub>1 Q\<^isub>1 Q\<^isub>2 S\<^isub>2 \ X \) + then show "(\@[(TVarB X P)]@\) \ Q\<^isub>1 \ Q\<^isub>2 <: S\<^isub>1 \ S\<^isub>2" by blast next - case (SA_all \' T\<^isub>1 S\<^isub>1 Y S\<^isub>2 T\<^isub>2 \ \ X) - --{* \begin{minipage}[t]{0.9\textwidth} - In this case the left-hand derivation is @{term "(\@[(TVarB X Q)]@\) \ (\Y<:S\<^isub>1. S\<^isub>2) <: (\Y<:T\<^isub>1. T\<^isub>2)"} - and therfore we know that the binder @{term Y} is fresh for @{term "\@[(TVarB X Q)]@\"}. By - the inner induction hypothesis we have that @{term "(\@[(TVarB X P)]@\) \ T\<^isub>1 <: S\<^isub>1"} and - @{term "((TVarB Y T\<^isub>1)#\@[(TVarB X P)]@\) \ 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 "\@[(TVarB X P)]@\"}. We can then conclude by applying rule @{text "S_Forall"}. - \end{minipage}*} - hence rh_drv: "\ \ P <: Q" - and IH_inner\<^isub>1: "(\@[(TVarB X P)]@\) \ T\<^isub>1 <: S\<^isub>1" - and "TVarB Y T\<^isub>1 # \' = ((TVarB Y T\<^isub>1)#\) @ [TVarB X Q] @ \" by auto - moreover have " \\\P<:Q; TVarB Y T\<^isub>1 # \' = ((TVarB Y T\<^isub>1)#\) @ [TVarB X Q] @ \\ \ (((TVarB Y T\<^isub>1)#\) @ [TVarB X P] @ \)\S\<^isub>2<:T\<^isub>2" by fact - ultimately have IH_inner\<^isub>2: "(((TVarB Y T\<^isub>1)#\) @ [TVarB X P] @ \)\S\<^isub>2<:T\<^isub>2" by auto - with IH_inner\<^isub>1 IH_inner\<^isub>2 - show "(\@[(TVarB X P)]@\) \ (\Y<:S\<^isub>1. S\<^isub>2) <: (\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 \ X \) + from SA_all(2,4,5,6) + have IH_inner\<^isub>1: "(\@[(TVarB X P)]@\) \ T\<^isub>1 <: S\<^isub>1" + and IH_inner\<^isub>2: "(((TVarB Y T\<^isub>1)#\)@[(TVarB X P)]@\) \ S\<^isub>2 <: T\<^isub>2" by force+ + then show "(\@[(TVarB X P)]@\) \ (\Y<:S\<^isub>1. S\<^isub>2) <: (\Y<:T\<^isub>1. T\<^isub>2)" by auto qed } qed @@ -1163,7 +1052,7 @@ | T_Abs[intro]: "\ VarB x T\<^isub>1 # \ \ t\<^isub>2 : T\<^isub>2 \ \ \ \ (\x:T\<^isub>1. t\<^isub>2) : T\<^isub>1 \ T\<^isub>2" | T_Sub[intro]: "\ \ \ t : S; \ \ S <: T \ \ \ \ t : T" | T_TAbs[intro]:"\ TVarB X T\<^isub>1 # \ \ t\<^isub>2 : T\<^isub>2 \ \ \ \ (\X<:T\<^isub>1. t\<^isub>2) : (\X<:T\<^isub>1. T\<^isub>2)" -| T_TApp[intro]:"\ X \ (\, t\<^isub>1, T\<^isub>2); \ \ t\<^isub>1 : (\X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2); \ \ T\<^isub>2 <: T\<^isub>1\<^isub>1 \ \ \ \ t\<^isub>1 \\<^sub>\ T\<^isub>2 : (T\<^isub>1\<^isub>2[X \ T\<^isub>2]\<^sub>\)" +| T_TApp[intro]:"\X\(\,t\<^isub>1,T\<^isub>2); \ \ t\<^isub>1 : (\X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2); \ \ T\<^isub>2 <: T\<^isub>1\<^isub>1\ \ \ \ t\<^isub>1 \\<^sub>\ T\<^isub>2 : (T\<^isub>1\<^isub>2[X \ T\<^isub>2]\<^sub>\)" 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: "\ \ ok" @@ -1200,19 +1089,19 @@ lemma tyvrs_of_subst: "tyvrs_of (B[X \ T]\<^sub>b) = tyvrs_of B" by (nominal_induct B rule: binding.strong_induct) simp_all -lemma ty_domain_subst: "ty_domain (\[X \ T]\<^sub>e) = ty_domain \" +lemma ty_dom_subst: "ty_dom (\[X \ T]\<^sub>e) = ty_dom \" by (induct \) (simp_all add: tyvrs_of_subst) lemma vrs_of_subst: "vrs_of (B[X \ T]\<^sub>b) = vrs_of B" by (nominal_induct B rule: binding.strong_induct) simp_all -lemma trm_domain_subst: "trm_domain (\[X \ T]\<^sub>e) = trm_domain \" +lemma trm_dom_subst: "trm_dom (\[X \ T]\<^sub>e) = trm_dom \" by (induct \) (simp_all add: vrs_of_subst) lemma subst_closed_in: "T closed_in (\ @ TVarB X S # \) \ U closed_in \ \ T[X \ U]\<^sub>\ closed_in (\[X \ U]\<^sub>e @ \)" apply (nominal_induct T avoiding: X U \ 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) # \" 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 @@ "(\x:T. t) \ t'" "(\X<:T. t) \ t'" -lemma ty_domain_cons: - shows "ty_domain (\@[VarB X Q]@\) = ty_domain (\@\)" +lemma ty_dom_cons: + shows "ty_dom (\@[VarB X Q]@\) = ty_dom (\@\)" by (induct \, auto) lemma closed_in_cons: assumes "S closed_in (\ @ VarB X Q # \)" shows "S closed_in (\@\)" -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 (\ @ \) \ T closed_in (\ @ B # \)" - 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 \ \ T closed_in (\ @ \)" - by (auto simp add: closed_in_def domains_append) + by (auto simp add: closed_in_def doms_append) lemma valid_subst: assumes ok: "\ (\ @ TVarB X Q # \) 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 "\ (bs @ \) ok" by simp - moreover from Cons and valid_consT have "X \ ty_domain (bs @ \)" - by (simp add: domains_append) + moreover from Cons and valid_consT have "X \ ty_dom (bs @ \)" + by (simp add: doms_append) moreover from Cons and valid_consT have "T closed_in (bs @ \)" - by (simp add: closed_in_def domains_append) + by (simp add: closed_in_def doms_append) ultimately have "\ (TVarB X T # bs @ \) 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 "\ (bs @ \) ok" by simp - moreover from Cons and valid_cons have "x \ trm_domain (bs @ \)" - by (simp add: domains_append finite_domains + moreover from Cons and valid_cons have "x \ trm_dom (bs @ \)" + 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 @ \)" - by (simp add: closed_in_def domains_append) + by (simp add: closed_in_def doms_append) ultimately have "\ (VarB x T # bs @ \) ok" by (rule valid_rel.valid_cons) with Cons and valid_cons show ?thesis by simp @@ -1439,10 +1328,10 @@ have "\ (VarB y T\<^isub>1 # \ @ B # \) 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 "\ (TVarB X T\<^isub>1 # \ @ B # \) 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 "\ (G' @ VarB x Q # \) ok" by simp then have h1:"\ (G' @ \) ok" by (auto dest: valid_cons') - have "X' \ ty_domain (G' @ VarB x Q # \)" using SA_refl_TVar by auto - then have h2:"X' \ ty_domain (G' @ \)" using ty_domain_vrs by auto + have "X' \ ty_dom (G' @ VarB x Q # \)" using SA_refl_TVar by auto + then have h2:"X' \ ty_dom (G' @ \)" 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 \ t2 : T2` have "X \ 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 \ 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 \ set G" by simp with G_ok have QS: "Q = S" using `TVarB Y S \ set G` by (rule uniqueness_of_ctxt) - from X\_ok have "X \ ty_domain \" and "Q closed_in \" by auto + from X\_ok have "X \ ty_dom \" and "Q closed_in \" by auto then have XQ: "X \ Q" by (rule closed_in_fresh) note `\\P<:Q` moreover from ST have "\ (D[X \ P]\<^sub>e @ \) ok" by (rule subtype_implies_ok) @@ -1652,8 +1541,8 @@ with neq and ST show ?thesis by auto next assume Y: "TVarB Y S \ set \" - from X\_ok have "X \ ty_domain \" and "\ \ ok" by auto - then have "X \ \" by (simp add: valid_ty_domain_fresh) + from X\_ok have "X \ ty_dom \" and "\ \ ok" by auto + then have "X \ \" by (simp add: valid_ty_dom_fresh) with Y have "X \ S" by (induct \) (auto simp add: fresh_list_nil fresh_list_cons) with ST have "(D[X \ P]\<^sub>e @ \)\S<:T[X \ P]\<^sub>\" @@ -1677,8 +1566,8 @@ by (auto intro: subtype_reflexivity) next assume neq: "X \ Y" - with SA_refl_TVar have "Y \ ty_domain (D[X \ P]\<^sub>e @ \)" - by (simp add: ty_domain_subst domains_append) + with SA_refl_TVar have "Y \ ty_dom (D[X \ P]\<^sub>e @ \)" + 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 \ ty_domain (D @ TVarB X Q # \)" - by (auto dest: subtype_implies_ok intro: fresh_domain) + then have Y: "Y \ ty_dom (D @ TVarB X Q # \)" + by (auto dest: subtype_implies_ok intro: fresh_dom) moreover from SA_all have "S1 closed_in (D @ TVarB X Q # \)" by (auto dest: subtype_implies_closed) ultimately have S1: "Y \ S1" by (rule closed_in_fresh) @@ -1722,8 +1611,8 @@ next assume x: "VarB x T \ set G" from T_Var have ok: "\ G ok" by (auto dest: subtype_implies_ok) - then have "X \ ty_domain G" using T_Var by (auto dest: validE_append) - with ok have "X \ G" by (simp add: valid_ty_domain_fresh) + then have "X \ ty_dom G" using T_Var by (auto dest: validE_append) + with ok have "X \ G" by (simp add: valid_ty_dom_fresh) moreover from x have "VarB x T \ set (D' @ G)" by simp then have "VarB x (T[X \ P]\<^sub>\) \ set ((D' @ G)[X \ 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' \ ty_domain (D' @ TVarB X Q # G)" + then have "X' \ ty_dom (D' @ TVarB X Q # G)" and "G' closed_in (D' @ TVarB X Q # G)" by (auto dest: typing_ok) then have "X' \ 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' \ ty_domain (D' @ TVarB X Q # G)" - by (simp add: fresh_domain) + then have "X' \ 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' \ T11" by (rule closed_in_fresh) @@ -1783,7 +1672,7 @@ then have "[(y, x)] \ (VarB y S # \) \ [(y, x)] \ [(y, x)] \ s : [(y, x)] \ T\<^isub>2" by (rule typing.eqvt) moreover from T_Abs have "y \ \" - 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 # \ \ 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 \ t \ "\X<:S. s" T avoiding: X U U' S arbitrary: s rule: typing.strong_induct) case (T_TAbs Y T\<^isub>1 \ t\<^isub>2 T\<^isub>2) from `TVarB Y T\<^isub>1 # \ \ t\<^isub>2 : T\<^isub>2` have Y: "Y \ \" - by (auto dest!: typing_ok simp add: valid_ty_domain_fresh) + by (auto dest!: typing_ok simp add: valid_ty_dom_fresh) from `Y \ U'` and `Y \ X` have "(\X<:U. U') = (\Y<:U. [(Y, X)] \ U')" by (simp add: ty.inject alpha' fresh_atm) @@ -1907,7 +1796,7 @@ with T_TApp have "\ \ (\X<:T\<^isub>1\<^isub>1'. t\<^isub>1\<^isub>2) : (\X<:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2)" and "X \ \" and "X \ T\<^isub>1\<^isub>1'" by (simp_all add: trm.inject) moreover from `\\T\<^isub>2<:T\<^isub>1\<^isub>1` and `X \ \` have "X \ 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 # \ \ t\<^isub>1\<^isub>2 : S'" and "(TVarB X T\<^isub>1\<^isub>1 # \) \ S' <: T\<^isub>1\<^isub>2" diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Nominal/nominal_datatype.ML --- 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 \ (pi2 \ x)"] perm_simproc'; + Simplifier.simproc @{theory} "perm_simp" ["pi1 \ (pi2 \ x)"] perm_simproc'; val meta_spec = thm "meta_spec"; diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Nominal/nominal_permeq.ML --- 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 = diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/OrderedGroup.thy --- 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; diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Product_Type.thy --- 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]; diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Prolog/prolog.ML --- 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))" *) diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Set.thy --- 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; diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Statespace/DistinctTreeProver.thy --- 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'; *} diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Statespace/state_fun.ML --- 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 diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Tools/Datatype/datatype_realizer.ML --- 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]))))); diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Tools/Function/fundef_core.ML --- 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 diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Tools/metis_tools.ML --- 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 diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Tools/nat_arith.ML --- 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)]; diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Tools/nat_numeral_simprocs.ML --- 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*) diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Tools/numeral.ML --- 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)], []); diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Tools/res_axioms.ML --- 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 = diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Tools/rewrite_hol_proof.ML --- 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 **) diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Tools/sat_funcs.ML --- 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, *) diff -r 64a12f353c57 -r efc5f4806cd5 src/HOL/Tools/simpdata.ML --- 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; diff -r 64a12f353c57 -r efc5f4806cd5 src/HOLCF/holcf_logic.ML --- 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); diff -r 64a12f353c57 -r efc5f4806cd5 src/Pure/General/same.ML --- /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; diff -r 64a12f353c57 -r efc5f4806cd5 src/Pure/IsaMakefile --- 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 \ diff -r 64a12f353c57 -r efc5f4806cd5 src/Pure/Isar/theory_target.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 ? diff -r 64a12f353c57 -r efc5f4806cd5 src/Pure/Proof/reconstruct.ML --- 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; diff -r 64a12f353c57 -r efc5f4806cd5 src/Pure/ROOT.ML --- 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"; diff -r 64a12f353c57 -r efc5f4806cd5 src/Pure/envir.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; diff -r 64a12f353c57 -r efc5f4806cd5 src/Pure/logic.ML --- 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 *) diff -r 64a12f353c57 -r efc5f4806cd5 src/Pure/proofterm.ML --- 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 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 *****) diff -r 64a12f353c57 -r efc5f4806cd5 src/Pure/term.ML --- 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 = diff -r 64a12f353c57 -r efc5f4806cd5 src/Pure/term_subst.ML --- 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; diff -r 64a12f353c57 -r efc5f4806cd5 src/Pure/thm.ML --- 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, diff -r 64a12f353c57 -r efc5f4806cd5 src/ZF/Datatype_ZF.thy --- 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; diff -r 64a12f353c57 -r efc5f4806cd5 src/ZF/OrdQuant.thy --- 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;