# HG changeset patch # User haftmann # Date 1248071527 -7200 # Node ID e8e0fb5da77ae26715f00bd3b652f2b3b0d16319 # Parent db50e76b0046374c050f005522514e19f0e134d1# Parent 76d6ba08a05f7cff95191b1aac5be092f3863167 merged diff -r 76d6ba08a05f -r e8e0fb5da77a src/CCL/CCL.thy --- a/src/CCL/CCL.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/CCL/CCL.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/CCL/Hered.thy --- a/src/CCL/Hered.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/CCL/Hered.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/CCL/Term.thy --- a/src/CCL/Term.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/CCL/Term.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/CCL/Type.thy --- a/src/CCL/Type.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/CCL/Type.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/FOL/simpdata.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Algebra/abstract/Ring2.thy --- a/src/HOL/Algebra/abstract/Ring2.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Algebra/abstract/Ring2.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Divides.thy --- a/src/HOL/Divides.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Divides.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Fact.thy --- a/src/HOL/Fact.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Fact.thy Mon Jul 20 08:32:07 2009 +0200 @@ -2,25 +2,266 @@ Author : Jacques D. Fleuriot Copyright : 1998 University of Cambridge Conversion to Isar and new proofs by Lawrence C Paulson, 2004 + The integer version of factorial and other additions by Jeremy Avigad. *) header{*Factorial Function*} theory Fact -imports Main +imports NatTransfer begin -consts fact :: "nat => nat" -primrec - fact_0: "fact 0 = 1" - fact_Suc: "fact (Suc n) = (Suc n) * fact n" +class fact = + +fixes + fact :: "'a \ 'a" + +instantiation nat :: fact + +begin + +fun + fact_nat :: "nat \ nat" +where + fact_0_nat: "fact_nat 0 = Suc 0" +| fact_Suc: "fact_nat (Suc x) = Suc x * fact x" + +instance proof qed + +end + +(* definitions for the integers *) + +instantiation int :: fact + +begin + +definition + fact_int :: "int \ int" +where + "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)" + +instance proof qed + +end + + +subsection {* Set up Transfer *} + +lemma transfer_nat_int_factorial: + "(x::int) >= 0 \ fact (nat x) = nat (fact x)" + unfolding fact_int_def + by auto + + +lemma transfer_nat_int_factorial_closure: + "x >= (0::int) \ fact x >= 0" + by (auto simp add: fact_int_def) + +declare TransferMorphism_nat_int[transfer add return: + transfer_nat_int_factorial transfer_nat_int_factorial_closure] + +lemma transfer_int_nat_factorial: + "fact (int x) = int (fact x)" + unfolding fact_int_def by auto + +lemma transfer_int_nat_factorial_closure: + "is_nat x \ fact x >= 0" + by (auto simp add: fact_int_def) + +declare TransferMorphism_int_nat[transfer add return: + transfer_int_nat_factorial transfer_int_nat_factorial_closure] -lemma fact_gt_zero [simp]: "0 < fact n" -by (induct n) auto +subsection {* Factorial *} + +lemma fact_0_int [simp]: "fact (0::int) = 1" + by (simp add: fact_int_def) + +lemma fact_1_nat [simp]: "fact (1::nat) = 1" + by simp + +lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0" + by simp + +lemma fact_1_int [simp]: "fact (1::int) = 1" + by (simp add: fact_int_def) + +lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n" + by simp + +lemma fact_plus_one_int: + assumes "n >= 0" + shows "fact ((n::int) + 1) = (n + 1) * fact n" + + using prems unfolding fact_int_def + by (simp add: nat_add_distrib algebra_simps int_mult) + +lemma fact_reduce_nat: "(n::nat) > 0 \ fact n = n * fact (n - 1)" + apply (subgoal_tac "n = Suc (n - 1)") + apply (erule ssubst) + apply (subst fact_Suc) + apply simp_all +done + +lemma fact_reduce_int: "(n::int) > 0 \ fact n = n * fact (n - 1)" + apply (subgoal_tac "n = (n - 1) + 1") + apply (erule ssubst) + apply (subst fact_plus_one_int) + apply simp_all +done + +lemma fact_nonzero_nat [simp]: "fact (n::nat) \ 0" + apply (induct n) + apply (auto simp add: fact_plus_one_nat) +done + +lemma fact_nonzero_int [simp]: "n >= 0 \ fact (n::int) ~= 0" + by (simp add: fact_int_def) + +lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0" + by (insert fact_nonzero_nat [of n], arith) + +lemma fact_gt_zero_int [simp]: "n >= 0 \ fact (n :: int) > 0" + by (auto simp add: fact_int_def) + +lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1" + by (insert fact_nonzero_nat [of n], arith) + +lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0" + by (insert fact_nonzero_nat [of n], arith) + +lemma fact_ge_one_int [simp]: "n >= 0 \ fact (n :: int) >= 1" + apply (auto simp add: fact_int_def) + apply (subgoal_tac "1 = int 1") + apply (erule ssubst) + apply (subst zle_int) + apply auto +done + +lemma dvd_fact_nat [rule_format]: "1 <= m \ m <= n \ m dvd fact (n::nat)" + apply (induct n) + apply force + apply (auto simp only: fact_Suc) + apply (subgoal_tac "m = Suc n") + apply (erule ssubst) + apply (rule dvd_triv_left) + apply auto +done + +lemma dvd_fact_int [rule_format]: "1 <= m \ m <= n \ m dvd fact (n::int)" + apply (case_tac "1 <= n") + apply (induct n rule: int_ge_induct) + apply (auto simp add: fact_plus_one_int) + apply (subgoal_tac "m = i + 1") + apply auto +done + +lemma interval_plus_one_nat: "(i::nat) <= j + 1 \ + {i..j+1} = {i..j} Un {j+1}" + by auto + +lemma interval_Suc: "i <= Suc j \ {i..Suc j} = {i..j} Un {Suc j}" + by auto + +lemma interval_plus_one_int: "(i::int) <= j + 1 \ {i..j+1} = {i..j} Un {j+1}" + by auto -lemma fact_not_eq_zero [simp]: "fact n \ 0" -by simp +lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)" + apply (induct n) + apply force + apply (subst fact_Suc) + apply (subst interval_Suc) + apply auto +done + +lemma fact_altdef_int: "n >= 0 \ fact (n::int) = (PROD i:{1..n}. i)" + apply (induct n rule: int_ge_induct) + apply force + apply (subst fact_plus_one_int, assumption) + apply (subst interval_plus_one_int) + apply auto +done + +lemma fact_mono_nat: "(m::nat) \ n \ fact m \ fact n" +apply (drule le_imp_less_or_eq) +apply (auto dest!: less_imp_Suc_add) +apply (induct_tac k, auto) +done + +lemma fact_neg_int [simp]: "m < (0::int) \ fact m = 0" + unfolding fact_int_def by auto + +lemma fact_ge_zero_int [simp]: "fact m >= (0::int)" + apply (case_tac "m >= 0") + apply auto + apply (frule fact_gt_zero_int) + apply arith +done + +lemma fact_mono_int_aux [rule_format]: "k >= (0::int) \ + fact (m + k) >= fact m" + apply (case_tac "m < 0") + apply auto + apply (induct k rule: int_ge_induct) + apply auto + apply (subst add_assoc [symmetric]) + apply (subst fact_plus_one_int) + apply auto + apply (erule order_trans) + apply (subst mult_le_cancel_right1) + apply (subgoal_tac "fact (m + i) >= 0") + apply arith + apply auto +done + +lemma fact_mono_int: "(m::int) <= n \ fact m <= fact n" + apply (insert fact_mono_int_aux [of "n - m" "m"]) + apply auto +done + +text{*Note that @{term "fact 0 = fact 1"}*} +lemma fact_less_mono_nat: "[| (0::nat) < m; m < n |] ==> fact m < fact n" +apply (drule_tac m = m in less_imp_Suc_add, auto) +apply (induct_tac k, auto) +done + +lemma fact_less_mono_int_aux: "k >= 0 \ (0::int) < m \ + fact m < fact ((m + 1) + k)" + apply (induct k rule: int_ge_induct) + apply (simp add: fact_plus_one_int) + apply (subst mult_less_cancel_right1) + apply (insert fact_gt_zero_int [of m], arith) + apply (subst (2) fact_reduce_int) + apply (auto simp add: add_ac) + apply (erule order_less_le_trans) + apply (subst mult_le_cancel_right1) + apply auto + apply (subgoal_tac "fact (i + (1 + m)) >= 0") + apply force + apply (rule fact_ge_zero_int) +done + +lemma fact_less_mono_int: "(0::int) < m \ m < n \ fact m < fact n" + apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"]) + apply auto +done + +lemma fact_num_eq_if_nat: "fact (m::nat) = + (if m=0 then 1 else m * fact (m - 1))" +by (cases m) auto + +lemma fact_add_num_eq_if_nat: + "fact ((m::nat) + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))" +by (cases "m + n") auto + +lemma fact_add_num_eq_if2_nat: + "fact ((m::nat) + n) = + (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))" +by (cases m) auto + + +subsection {* @{term fact} and @{term of_nat} *} lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \ (0::'a::semiring_char_0)" by auto @@ -33,46 +274,10 @@ lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \ of_nat(fact n)" by simp -lemma fact_ge_one [simp]: "1 \ fact n" -by (induct n) auto - -lemma fact_mono: "m \ n ==> fact m \ fact n" -apply (drule le_imp_less_or_eq) -apply (auto dest!: less_imp_Suc_add) -apply (induct_tac k, auto) -done - -text{*Note that @{term "fact 0 = fact 1"}*} -lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n" -apply (drule_tac m = m in less_imp_Suc_add, auto) -apply (induct_tac k, auto) -done - lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::ordered_field) < inverse (of_nat (fact n))" by (auto simp add: positive_imp_inverse_positive) lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::ordered_field) \ inverse (of_nat (fact n))" by (auto intro: order_less_imp_le) -lemma fact_diff_Suc [rule_format]: - "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)" -apply (induct n arbitrary: m) -apply auto -apply (drule_tac x = "m - Suc 0" in meta_spec, auto) -done - -lemma fact_num0: "fact 0 = 1" -by auto - -lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))" -by (cases m) auto - -lemma fact_add_num_eq_if: - "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))" -by (cases "m + n") auto - -lemma fact_add_num_eq_if2: - "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))" -by (cases m) auto - end diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Finite_Set.thy Mon Jul 20 08:32:07 2009 +0200 @@ -93,6 +93,7 @@ qed qed + text{* A finite choice principle. Does not need the SOME choice operator. *} lemma finite_set_choice: "finite A \ ALL x:A. (EX y. P x y) \ EX f. ALL x:A. P x (f x)" @@ -2122,6 +2123,18 @@ \ x \ \ F = {}" by auto +lemma finite_psubset_induct[consumes 1, case_names psubset]: + assumes "finite A" and "!!A. finite A \ (!!B. finite B \ B \ A \ P(B)) \ P(A)" shows "P A" +using assms(1) +proof (induct A rule: measure_induct_rule[where f=card]) + case (less A) + show ?case + proof(rule assms(2)[OF less(2)]) + fix B assume "finite B" "B \ A" + show "P B" by(rule less(1)[OF psubset_card_mono[OF less(2) `B \ A`] `finite B`]) + qed +qed + text{* main cardinality theorem *} lemma card_partition [rule_format]: "finite C ==> @@ -3252,13 +3265,13 @@ by (simp add: Max fold1_antimono [folded dual_max]) qed -lemma finite_linorder_induct[consumes 1, case_names empty insert]: +lemma finite_linorder_max_induct[consumes 1, case_names empty insert]: "finite A \ P {} \ (!!A b. finite A \ ALL a:A. a < b \ P A \ P(insert b A)) \ P A" -proof (induct A rule: measure_induct_rule[where f=card]) +proof (induct rule: finite_psubset_induct) fix A :: "'a set" - assume IH: "!! B. card B < card A \ finite B \ P {} \ + assume IH: "!! B. finite B \ B < A \ P {} \ (!!A b. finite A \ (\a\A. a P A \ P (insert b A)) \ P B" and "finite A" and "P {}" @@ -3271,16 +3284,17 @@ assume "A \ {}" with `finite A` have "Max A : A" by auto hence A: "?A = A" using insert_Diff_single insert_absorb by auto - note card_Diff1_less[OF `finite A` `Max A : A`] moreover have "finite ?B" using `finite A` by simp ultimately have "P ?B" using `P {}` step IH by blast - moreover have "\a\?B. a < Max A" - using Max_ge [OF `finite A`] by fastsimp - ultimately show "P A" - using A insert_Diff_single step[OF `finite ?B`] by fastsimp + moreover have "\a\?B. a < Max A" using Max_ge [OF `finite A`] by fastsimp + ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastsimp qed qed +lemma finite_linorder_min_induct[consumes 1, case_names empty insert]: + "\finite A; P {}; \A b. \finite A; \a\A. b < a; P A\ \ P (insert b A)\ \ P A" +by(rule linorder.finite_linorder_max_induct[OF dual_linorder]) + end context ordered_ab_semigroup_add diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/GCD.thy --- a/src/HOL/GCD.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/GCD.thy Mon Jul 20 08:32:07 2009 +0200 @@ -20,6 +20,9 @@ the congruence relations on the integers. The notion was extended to the natural numbers by Chiaeb. +Jeremy Avigad combined all of these, made everything uniform for the +natural numbers and the integers, and added a number of new theorems. + Tobias Nipkow cleaned up a lot. *) @@ -27,7 +30,7 @@ header {* GCD *} theory GCD -imports NatTransfer +imports Fact begin declare One_nat_def [simp del] @@ -159,7 +162,6 @@ transfer_int_nat_gcd transfer_int_nat_gcd_closures] - subsection {* GCD *} (* was gcd_induct *) @@ -1553,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) @@ -1625,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) @@ -1652,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" @@ -1751,4 +1780,42 @@ ultimately show ?thesis by blast qed +subsection {* Infinitely many primes *} + +lemma next_prime_bound: "\(p::nat). prime p \ n < p \ p <= fact n + 1" +proof- + have f1: "fact n + 1 \ 1" using fact_ge_one_nat [of n] by arith + from prime_factor_nat [OF f1] + obtain p where "prime p" and "p dvd fact n + 1" by auto + hence "p \ fact n + 1" + by (intro dvd_imp_le, auto) + {assume "p \ n" + from `prime p` have "p \ 1" + by (cases p, simp_all) + with `p <= n` have "p dvd fact n" + by (intro dvd_fact_nat) + with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n" + by (rule dvd_diff_nat) + hence "p dvd 1" by simp + hence "p <= 1" by auto + moreover from `prime p` have "p > 1" by auto + ultimately have False by auto} + hence "n < p" by arith + with `prime p` and `p <= fact n + 1` show ?thesis by auto +qed + +lemma bigger_prime: "\p. prime p \ p > (n::nat)" +using next_prime_bound by auto + +lemma primes_infinite: "\ (finite {(p::nat). prime p})" +proof + assume "finite {(p::nat). prime p}" + with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))" + by auto + then obtain b where "ALL (x::nat). prime x \ x <= b" + by auto + with bigger_prime [of b] show False by auto +qed + + end diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/IntDiv.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Lambda/WeakNorm.thy --- a/src/HOL/Lambda/WeakNorm.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Lambda/WeakNorm.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Library/Binomial.thy --- a/src/HOL/Library/Binomial.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Library/Binomial.thy Mon Jul 20 08:32:07 2009 +0200 @@ -243,14 +243,8 @@ ultimately show ?thesis by blast qed -lemma fact_setprod: "fact n = setprod id {1 .. n}" - apply (induct n, simp) - apply (simp only: fact_Suc atLeastAtMostSuc_conv) - apply (subst setprod_insert) - by simp_all - lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n" - unfolding fact_setprod + unfolding fact_altdef_nat apply (cases n, simp_all add: of_nat_setprod pochhammer_Suc_setprod) apply (rule setprod_reindex_cong[where f=Suc]) @@ -347,7 +341,7 @@ assumes kn: "k \ n" shows "(of_nat (n choose k) :: 'a::field_char_0) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))" using binomial_fact_lemma[OF kn] - by (simp add: field_simps fact_not_eq_zero of_nat_mult[symmetric]) + by (simp add: field_simps of_nat_mult[symmetric]) lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k" proof- @@ -377,7 +371,7 @@ have ?thesis using kn apply (simp add: binomial_fact[OF kn, where ?'a = 'a] gbinomial_pochhammer field_simps pochhammer_Suc_setprod) - apply (simp add: pochhammer_Suc_setprod fact_setprod h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc) + apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc) unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \ 'a"] eq[unfolded h] unfolding mult_assoc[symmetric] unfolding setprod_timesf[symmetric] diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Mon Jul 20 08:32:07 2009 +0200 @@ -2530,8 +2530,8 @@ apply (induct n) apply simp unfolding th - using fact_gt_zero - apply (simp add: field_simps del: of_nat_Suc fact.simps) + using fact_gt_zero_nat + apply (simp add: field_simps del: of_nat_Suc fact_Suc) apply (drule sym) by (simp add: ring_simps of_nat_mult power_Suc)} note th' = this @@ -2747,9 +2747,6 @@ finally show ?thesis . qed -lemma fact_1 [simp]: "fact 1 = 1" -unfolding One_nat_def fact_Suc by simp - lemma divide_eq_iff: "a \ (0::'a::field) \ x / a = y \ x = y * a" by auto diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Library/reflection.ML --- a/src/HOL/Library/reflection.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Library/reflection.ML Mon Jul 20 08:32:07 2009 +0200 @@ -153,8 +153,8 @@ val certy = ctyp_of thy val (tyenv, tmenv) = Pattern.match thy - ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t) - (Envir.type_env (Envir.empty 0), Vartab.empty) + ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t) + (Vartab.empty, Vartab.empty) val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv) val (fts,its) = (map (snd o snd) fnvs, @@ -204,11 +204,9 @@ val xns_map = (fst (split_list nths)) ~~ xns val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map val rhs_P = subst_free subst rhs - val (tyenv, tmenv) = Pattern.match - thy (rhs_P, t) - (Envir.type_env (Envir.empty 0), Vartab.empty) - val sbst = Envir.subst_vars (tyenv, tmenv) - val sbsT = Envir.typ_subst_TVars tyenv + val (tyenv, tmenv) = Pattern.match thy (rhs_P, t) (Vartab.empty, Vartab.empty) + val sbst = Envir.subst_term (tyenv, tmenv) + val sbsT = Envir.subst_type tyenv val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t)) (Vartab.dest tyenv) val tml = Vartab.dest tmenv diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/List.thy --- a/src/HOL/List.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/List.thy Mon Jul 20 08:32:07 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; @@ -2268,6 +2268,8 @@ -- {* simp does not terminate! *} by (induct j) auto +lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n", standard] + lemma upt_conv_Nil [simp]: "j <= i ==> [i..int. i+1)" +successor_int_def[simp]: "successor = (%i\int. i+1)" instance by intro_classes (simp_all add: successor_int_def) @@ -3202,6 +3204,8 @@ lemma upto_rec2_int: "(i::int) \ j \ [i..j+1] = [i..j] @ [j+1]" by(rule upto_rec2[where 'a = int, simplified successor_int_def]) +lemmas upto_rec_number_of_int[simp] = upto_rec[of "number_of m :: int" "number_of n", standard] + subsubsection {* @{text lists}: the list-forming operator over sets *} diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Ln.thy --- a/src/HOL/Ln.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Ln.thy Mon Jul 20 08:32:07 2009 +0200 @@ -31,13 +31,13 @@ qed lemma aux1: assumes a: "0 <= x" and b: "x <= 1" - shows "inverse (real (fact (n + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)" + shows "inverse (real (fact ((n::nat) + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)" proof (induct n) - show "inverse (real (fact (0 + 2))) * x ^ (0 + 2) <= + show "inverse (real (fact ((0::nat) + 2))) * x ^ (0 + 2) <= x ^ 2 / 2 * (1 / 2) ^ 0" by (simp add: real_of_nat_Suc power2_eq_square) next - fix n + fix n :: nat assume c: "inverse (real (fact (n + 2))) * x ^ (n + 2) <= x ^ 2 / 2 * (1 / 2) ^ n" show "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2) diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/MacLaurin.thy --- a/src/HOL/MacLaurin.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/MacLaurin.thy Mon Jul 20 08:32:07 2009 +0200 @@ -27,6 +27,10 @@ lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))" by arith +lemma fact_diff_Suc [rule_format]: + "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)" + by (subst fact_reduce_nat, auto) + lemma Maclaurin_lemma2: assumes diff: "\m t. m < n \ 0\t \ t\h \ DERIV (diff m) t :> diff (Suc m) t" assumes n: "n = Suc k" @@ -47,7 +51,9 @@ apply (rule_tac [2] DERIV_quotient) apply (rule_tac [3] DERIV_const) apply (rule_tac [2] DERIV_pow) - prefer 3 apply (simp add: fact_diff_Suc) + prefer 3 + +apply (simp add: fact_diff_Suc) prefer 2 apply simp apply (frule less_iff_Suc_add [THEN iffD1], clarify) apply (simp del: setsum_op_ivl_Suc) diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Modelcheck/EindhovenSyn.thy --- a/src/HOL/Modelcheck/EindhovenSyn.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Modelcheck/MuckeSyn.thy --- a/src/HOL/Modelcheck/MuckeSyn.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Modelcheck/MuckeSyn.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/NewNumberTheory/Binomial.thy --- a/src/HOL/NewNumberTheory/Binomial.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/NewNumberTheory/Binomial.thy Mon Jul 20 08:32:07 2009 +0200 @@ -2,7 +2,7 @@ Authors: Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow -Defines factorial and the "choose" function, and establishes basic properties. +Defines the "choose" function, and establishes basic properties. The original theory "Binomial" was by Lawrence C. Paulson, based on the work of Andy Gordon and Florian Kammueller. The approach here, @@ -16,7 +16,7 @@ header {* Binomial *} theory Binomial -imports Cong +imports Cong Fact begin @@ -25,7 +25,6 @@ class binomial = fixes - fact :: "'a \ 'a" and binomial :: "'a \ 'a \ 'a" (infixl "choose" 65) (* definitions for the natural numbers *) @@ -35,13 +34,6 @@ begin fun - fact_nat :: "nat \ nat" -where - "fact_nat x = - (if x = 0 then 1 else - x * fact(x - 1))" - -fun binomial_nat :: "nat \ nat \ nat" where "binomial_nat n k = @@ -60,11 +52,6 @@ begin definition - fact_int :: "int \ int" -where - "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)" - -definition binomial_int :: "int => int \ int" where "binomial_int n k = (if n \ 0 \ k \ 0 then int (binomial (nat n) (nat k)) @@ -76,182 +63,29 @@ subsection {* Set up Transfer *} - lemma transfer_nat_int_binomial: - "(x::int) >= 0 \ fact (nat x) = nat (fact x)" "(n::int) >= 0 \ k >= 0 \ binomial (nat n) (nat k) = nat (binomial n k)" - unfolding fact_int_def binomial_int_def + unfolding binomial_int_def by auto - -lemma transfer_nat_int_binomial_closures: - "x >= (0::int) \ fact x >= 0" +lemma transfer_nat_int_binomial_closure: "n >= (0::int) \ k >= 0 \ binomial n k >= 0" - by (auto simp add: fact_int_def binomial_int_def) + by (auto simp add: binomial_int_def) declare TransferMorphism_nat_int[transfer add return: - transfer_nat_int_binomial transfer_nat_int_binomial_closures] + transfer_nat_int_binomial transfer_nat_int_binomial_closure] lemma transfer_int_nat_binomial: - "fact (int x) = int (fact x)" "binomial (int n) (int k) = int (binomial n k)" unfolding fact_int_def binomial_int_def by auto -lemma transfer_int_nat_binomial_closures: - "is_nat x \ fact x >= 0" +lemma transfer_int_nat_binomial_closure: "is_nat n \ is_nat k \ binomial n k >= 0" - by (auto simp add: fact_int_def binomial_int_def) + by (auto simp add: binomial_int_def) declare TransferMorphism_int_nat[transfer add return: - transfer_int_nat_binomial transfer_int_nat_binomial_closures] - - -subsection {* Factorial *} - -lemma fact_zero_nat [simp]: "fact (0::nat) = 1" - by simp - -lemma fact_zero_int [simp]: "fact (0::int) = 1" - by (simp add: fact_int_def) - -lemma fact_one_nat [simp]: "fact (1::nat) = 1" - by simp - -lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0" - by (simp add: One_nat_def) - -lemma fact_one_int [simp]: "fact (1::int) = 1" - by (simp add: fact_int_def) - -lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n" - by simp - -lemma fact_Suc_nat: "fact (Suc n) = (Suc n) * fact n" - by (simp add: One_nat_def) - -lemma fact_plus_one_int: - assumes "n >= 0" - shows "fact ((n::int) + 1) = (n + 1) * fact n" - - using prems by (rule fact_plus_one_nat [transferred]) - -lemma fact_reduce_nat: "(n::nat) > 0 \ fact n = n * fact (n - 1)" - by simp - -lemma fact_reduce_int: - assumes "(n::int) > 0" - shows "fact n = n * fact (n - 1)" - - using prems apply (subst tsub_eq [symmetric], auto) - apply (rule fact_reduce_nat [transferred]) - using prems apply auto -done - -declare fact_nat.simps [simp del] - -lemma fact_nonzero_nat [simp]: "fact (n::nat) \ 0" - apply (induct n rule: induct'_nat) - apply (auto simp add: fact_plus_one_nat) -done - -lemma fact_nonzero_int [simp]: "n >= 0 \ fact (n::int) ~= 0" - by (simp add: fact_int_def) - -lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0" - by (insert fact_nonzero_nat [of n], arith) - -lemma fact_gt_zero_int [simp]: "n >= 0 \ fact (n :: int) > 0" - by (auto simp add: fact_int_def) - -lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1" - by (insert fact_nonzero_nat [of n], arith) - -lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0" - by (insert fact_nonzero_nat [of n], arith) - -lemma fact_ge_one_int [simp]: "n >= 0 \ fact (n :: int) >= 1" - apply (auto simp add: fact_int_def) - apply (subgoal_tac "1 = int 1") - apply (erule ssubst) - apply (subst zle_int) - apply auto -done - -lemma dvd_fact_nat [rule_format]: "1 <= m \ m <= n \ m dvd fact (n::nat)" - apply (induct n rule: induct'_nat) - apply (auto simp add: fact_plus_one_nat) - apply (subgoal_tac "m = n + 1") - apply auto -done - -lemma dvd_fact_int [rule_format]: "1 <= m \ m <= n \ m dvd fact (n::int)" - apply (case_tac "1 <= n") - apply (induct n rule: int_ge_induct) - apply (auto simp add: fact_plus_one_int) - apply (subgoal_tac "m = i + 1") - apply auto -done - -lemma interval_plus_one_nat: "(i::nat) <= j + 1 \ - {i..j+1} = {i..j} Un {j+1}" - by auto - -lemma interval_plus_one_int: "(i::int) <= j + 1 \ {i..j+1} = {i..j} Un {j+1}" - by auto - -lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)" - apply (induct n rule: induct'_nat) - apply force - apply (subst fact_plus_one_nat) - apply (subst interval_plus_one_nat) - apply auto -done - -lemma fact_altdef_int: "n >= 0 \ fact (n::int) = (PROD i:{1..n}. i)" - apply (induct n rule: int_ge_induct) - apply force - apply (subst fact_plus_one_int, assumption) - apply (subst interval_plus_one_int) - apply auto -done - -subsection {* Infinitely many primes *} - -lemma next_prime_bound: "\(p::nat). prime p \ n < p \ p <= fact n + 1" -proof- - have f1: "fact n + 1 \ 1" using fact_ge_one_nat [of n] by arith - from prime_factor_nat [OF f1] - obtain p where "prime p" and "p dvd fact n + 1" by auto - hence "p \ fact n + 1" - by (intro dvd_imp_le, auto) - {assume "p \ n" - from `prime p` have "p \ 1" - by (cases p, simp_all) - with `p <= n` have "p dvd fact n" - by (intro dvd_fact_nat) - with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n" - by (rule dvd_diff_nat) - hence "p dvd 1" by simp - hence "p <= 1" by auto - moreover from `prime p` have "p > 1" by auto - ultimately have False by auto} - hence "n < p" by arith - with `prime p` and `p <= fact n + 1` show ?thesis by auto -qed - -lemma bigger_prime: "\p. prime p \ p > (n::nat)" -using next_prime_bound by auto - -lemma primes_infinite: "\ (finite {(p::nat). prime p})" -proof - assume "finite {(p::nat). prime p}" - with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))" - by auto - then obtain b where "ALL (x::nat). prime x \ x <= b" - by auto - with bigger_prime [of b] show False by auto -qed + transfer_int_nat_binomial transfer_int_nat_binomial_closure] subsection {* Binomial coefficients *} diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Nominal/Examples/Fsub.thy --- a/src/HOL/Nominal/Examples/Fsub.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Nominal/Examples/Fsub.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Mon Jul 20 08:32:07 2009 +0200 @@ -342,7 +342,7 @@ val env = Pattern.first_order_match thy (ihypt, prop_of ihyp) (Vartab.empty, Vartab.empty); val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy)) - (map (Envir.subst_vars env) vs ~~ + (map (Envir.subst_term env) vs ~~ map (fold_rev (NominalDatatype.mk_perm []) (rev pis' @ pis)) params' @ [z])) ihyp; fun mk_pi th = diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Jul 20 08:32:07 2009 +0200 @@ -147,7 +147,7 @@ let val env = Pattern.first_order_match thy (p, prop_of th) (Vartab.empty, Vartab.empty) in Thm.instantiate ([], - map (Envir.subst_vars env #> cterm_of thy) vs ~~ cts) th + map (Envir.subst_term env #> cterm_of thy) vs ~~ cts) th end; fun prove_strong_ind s avoids ctxt = diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/OrderedGroup.thy --- a/src/HOL/OrderedGroup.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/OrderedGroup.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Product_Type.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Prolog/prolog.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Set.thy --- a/src/HOL/Set.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Set.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/SetInterval.thy Mon Jul 20 08:32:07 2009 +0200 @@ -425,7 +425,7 @@ proof cases assume "finite A" thus "PROP ?P" - proof(induct A rule:finite_linorder_induct) + proof(induct A rule:finite_linorder_max_induct) case empty thus ?case by auto next case (insert A b) diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Statespace/DistinctTreeProver.thy --- a/src/HOL/Statespace/DistinctTreeProver.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Statespace/DistinctTreeProver.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Statespace/state_fun.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Mon Jul 20 08:32:07 2009 +0200 @@ -293,7 +293,7 @@ end; fun make_case tab ctxt = gen_make_case - (match_type (ProofContext.theory_of ctxt)) Envir.subst_TVars fastype_of tab ctxt; + (match_type (ProofContext.theory_of ctxt)) Envir.subst_term_types fastype_of tab ctxt; val make_case_untyped = gen_make_case (K (K Vartab.empty)) (K (Term.map_types (K dummyT))) (K dummyT); diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/Function/context_tree.ML --- a/src/HOL/Tools/Function/context_tree.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/Function/context_tree.ML Mon Jul 20 08:32:07 2009 +0200 @@ -116,8 +116,9 @@ val (c, subs) = (concl_of r, prems_of r) val subst = Pattern.match (ProofContext.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty) - val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs - val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_vars subst (Var v)))) (Term.add_vars c []) + val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_term subst) subs + val inst = map (fn v => + (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) (Term.add_vars c []) in (cterm_instantiate inst r, dep, branches) end diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/Function/fundef_core.ML --- a/src/HOL/Tools/Function/fundef_core.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/Function/fundef_core.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/Function/fundef_datatype.ML --- a/src/HOL/Tools/Function/fundef_datatype.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/Function/fundef_datatype.ML Mon Jul 20 08:32:07 2009 +0200 @@ -102,7 +102,8 @@ fun inst_constrs_of thy (T as Type (name, _)) = - map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) + map (fn (Cn,CT) => + Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) (the (Datatype.get_constrs thy name)) | inst_constrs_of thy _ = raise Match diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/Function/mutual.ML Mon Jul 20 08:32:07 2009 +0200 @@ -100,7 +100,7 @@ val (caTss, resultTs) = split_list (map curried_types fs) val argTs = map (foldr1 HOLogic.mk_prodT) caTss - val dresultTs = distinct (Type.eq_type Vartab.empty) resultTs + val dresultTs = distinct (op =) resultTs val n' = length dresultTs val RST = BalancedTree.make (uncurry SumTree.mk_sumT) dresultTs @@ -114,7 +114,7 @@ fun define (fvar as (n, T)) caTs resultT i = let val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *) - val i' = find_index (fn Ta => Type.eq_type Vartab.empty (Ta, resultT)) dresultTs + 1 + val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp) diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/Function/pattern_split.ML --- a/src/HOL/Tools/Function/pattern_split.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/Function/pattern_split.ML Mon Jul 20 08:32:07 2009 +0200 @@ -39,7 +39,8 @@ (* This is copied from "fundef_datatype.ML" *) fun inst_constrs_of thy (T as Type (name, _)) = - map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) + map (fn (Cn,CT) => + Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) (the (Datatype.get_constrs thy name)) | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], []) diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/TFL/casesplit.ML --- a/src/HOL/Tools/TFL/casesplit.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/TFL/casesplit.ML Mon Jul 20 08:32:07 2009 +0200 @@ -129,8 +129,8 @@ | _ => error "not a valid case thm"; val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T)) (Vartab.dest type_insts); - val cPv = ctermify (Envir.subst_TVars type_insts Pv); - val cDv = ctermify (Envir.subst_TVars type_insts Dv); + val cPv = ctermify (Envir.subst_term_types type_insts Pv); + val cDv = ctermify (Envir.subst_term_types type_insts Dv); in (beta_eta_contract (case_thm diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/TFL/thry.ML --- a/src/HOL/Tools/TFL/thry.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/TFL/thry.ML Mon Jul 20 08:32:07 2009 +0200 @@ -35,7 +35,7 @@ fun match_term thry pat ob = let val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty); - fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t) + fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.subst_type ty_theta T), t) in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta)) end; diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/inductive.ML Mon Jul 20 08:32:07 2009 +0200 @@ -922,7 +922,7 @@ val tab = fold (Pattern.first_order_match thy) (ts ~~ us) (Vartab.empty, Vartab.empty); in - map (Envir.subst_vars tab) vars + map (Envir.subst_term tab) vars end in map (mtch o apsnd prop_of) (cases ~~ intros) diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/inductive_set.ML Mon Jul 20 08:32:07 2009 +0200 @@ -324,7 +324,7 @@ fun to_pred_proc thy rules t = case lookup_rule thy I rules t of NONE => NONE | SOME (lhs, rhs) => - SOME (Envir.subst_vars + SOME (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rhs); fun to_pred thms ctxt thm = diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/meson.ML Mon Jul 20 08:32:07 2009 +0200 @@ -87,14 +87,12 @@ fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty); fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t); -val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0 - (*FIXME: currently does not "rename variables apart"*) fun first_order_resolve thA thB = let val thy = theory_of_thm thA val tmA = concl_of thA val Const("==>",_) $ tmB $ _ = prop_of thB - val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0) + val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty) val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) in thA RS (cterm_instantiate ct_pairs thB) end handle _ => raise THM ("first_order_resolve", 0, [thA,thB]); (* FIXME avoid handle _ *) @@ -104,8 +102,8 @@ [] => th | pairs => let val thy = theory_of_thm th - val (tyenv,tenv) = - List.foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs + val (tyenv, tenv) = + fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) val t_pairs = map term_pair_of (Vartab.dest tenv) val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th in th' end diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/metis_tools.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/nat_arith.ML --- a/src/HOL/Tools/nat_arith.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/nat_arith.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/nat_numeral_simprocs.ML --- a/src/HOL/Tools/nat_numeral_simprocs.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/numeral.ML --- a/src/HOL/Tools/numeral.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/numeral.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/res_axioms.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/rewrite_hol_proof.ML --- a/src/HOL/Tools/rewrite_hol_proof.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/sat_funcs.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Tools/simpdata.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOL/Transcendental.thy Mon Jul 20 08:32:07 2009 +0200 @@ -621,19 +621,19 @@ subsection{* Some properties of factorials *} -lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \ 0" +lemma real_of_nat_fact_not_zero [simp]: "real (fact (n::nat)) \ 0" by auto -lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)" +lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact (n::nat))" by auto -lemma real_of_nat_fact_ge_zero [simp]: "0 \ real(fact n)" +lemma real_of_nat_fact_ge_zero [simp]: "0 \ real(fact (n::nat))" by simp -lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))" +lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact (n::nat)))" by (auto simp add: positive_imp_inverse_positive) -lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \ inverse (real (fact n))" +lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \ inverse (real (fact (n::nat)))" by (auto intro: order_less_imp_le) subsection {* Derivability of power series *} @@ -1670,7 +1670,7 @@ apply (rule_tac y = "\n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))" in order_less_trans) -apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc) +apply (simp (no_asm) add: fact_num_eq_if_nat realpow_num_eq_if del: fact_Suc) apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc) apply (rule sumr_pos_lt_pair) apply (erule sums_summable, safe) @@ -1687,7 +1687,7 @@ apply (rule_tac [3] real_of_nat_ge_zero) prefer 2 apply force apply (rule real_of_nat_less_iff [THEN iffD2]) -apply (rule fact_less_mono, auto) +apply (rule fact_less_mono_nat, auto) done lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq] diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOLCF/Tools/adm_tac.ML --- a/src/HOLCF/Tools/adm_tac.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOLCF/Tools/adm_tac.ML Mon Jul 20 08:32:07 2009 +0200 @@ -117,8 +117,8 @@ val tye' = Sign.typ_match thy (PT, #T (rep_cterm Pt)) tye; val ctye = map (fn (ixn, (S, T)) => (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)) (Vartab.dest tye'); - val tv = cterm_of thy (Var (("t", j), Envir.typ_subst_TVars tye' tT)); - val Pv = cterm_of thy (Var (("P", j), Envir.typ_subst_TVars tye' PT)); + val tv = cterm_of thy (Var (("t", j), Envir.subst_type tye' tT)); + val Pv = cterm_of thy (Var (("P", j), Envir.subst_type tye' PT)); val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule in rule' end; diff -r 76d6ba08a05f -r e8e0fb5da77a src/HOLCF/holcf_logic.ML --- a/src/HOLCF/holcf_logic.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/HOLCF/holcf_logic.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/Concurrent/future.ML Mon Jul 20 08:32:07 2009 +0200 @@ -133,7 +133,7 @@ val ws = ! workers; val m = string_of_int (length ws); val n = string_of_int (length (filter #2 ws)); - in Multithreading.tracing 1 (fn () => "SCHEDULE: " ^ m ^ " workers, " ^ n ^ " active") end; + in Multithreading.tracing 2 (fn () => "SCHEDULE: " ^ m ^ " workers, " ^ n ^ " active") end; fun change_active active = (*requires SYNCHRONIZED*) change workers (AList.update Thread.equal (Thread.self (), active)); @@ -188,6 +188,15 @@ fun scheduler_next () = (*requires SYNCHRONIZED*) let + (*queue status*) + val _ = Multithreading.tracing 1 (fn () => + let val {ready, pending, running} = Task_Queue.status (! queue) in + "SCHEDULE: " ^ + string_of_int ready ^ " ready, " ^ + string_of_int pending ^ " pending, " ^ + string_of_int running ^ " running" + end); + (*worker threads*) val _ = (case List.partition (Thread.isActive o #1) (! workers) of @@ -277,8 +286,8 @@ fun get_result x = the_default (Exn.Exn (SYS_ERROR "unfinished future")) (peek x); fun join_wait x = - while not (is_finished x) - do SYNCHRONIZED "join_wait" (fn () => wait ()); + if SYNCHRONIZED "join_wait" (fn () => is_finished x orelse (wait (); false)) + then () else join_wait x; fun join_next x = (*requires SYNCHRONIZED*) if is_finished x then NONE diff -r 76d6ba08a05f -r e8e0fb5da77a src/Pure/Concurrent/simple_thread.ML --- a/src/Pure/Concurrent/simple_thread.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/Concurrent/simple_thread.ML Mon Jul 20 08:32:07 2009 +0200 @@ -25,13 +25,16 @@ fun synchronized name lock e = Exn.release (uninterruptible (fn restore_attributes => fn () => let - val _ = - if Mutex.trylock lock then () + val immediate = + if Mutex.trylock lock then true else (Multithreading.tracing 3 (fn () => name ^ ": locking ..."); Mutex.lock lock; - Multithreading.tracing 3 (fn () => name ^ ": ... locked")); + Multithreading.tracing 3 (fn () => name ^ ": locked"); + false); val result = Exn.capture (restore_attributes e) (); + val _ = + if immediate then () else Multithreading.tracing 3 (fn () => name ^ ": unlocking ..."); val _ = Mutex.unlock lock; in result end) ()); diff -r 76d6ba08a05f -r e8e0fb5da77a src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/Concurrent/task_queue.ML Mon Jul 20 08:32:07 2009 +0200 @@ -11,6 +11,7 @@ val pri_of_task: task -> int val str_of_task: task -> string type group + val group_id: group -> int val eq_group: group * group -> bool val new_group: unit -> group val is_valid: group -> bool @@ -19,6 +20,7 @@ type queue val empty: queue val is_empty: queue -> bool + val status: queue -> {ready: int, pending: int, running: int} val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> task * queue val extend: task -> (bool -> bool) -> queue -> queue option val dequeue: queue -> (task * group * (bool -> bool) list) option * queue @@ -47,6 +49,8 @@ (* groups *) datatype group = Group of serial * bool ref; + +fun group_id (Group (gid, _)) = gid; fun eq_group (Group (gid1, _), Group (gid2, _)) = gid1 = gid2; fun new_group () = Group (serial (), ref true); @@ -89,6 +93,19 @@ fun is_empty (Queue {jobs, ...}) = Task_Graph.is_empty jobs; +(* status *) + +fun status (Queue {jobs, ...}) = + let + val (x, y, z) = + Task_Graph.fold (fn (task, ((_, job), (deps, _))) => fn (x, y, z) => + (case job of + Job _ => if null deps then (x + 1, y, z) else (x, y + 1, z) + | Running _ => (x, y, z + 1))) + jobs (0, 0, 0); + in {ready = x, pending = y, running = z} end; + + (* enqueue *) fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, cache}) = diff -r 76d6ba08a05f -r e8e0fb5da77a src/Pure/General/same.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/same.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/IsaMakefile Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/Isar/overloading.ML Mon Jul 20 08:32:07 2009 +0200 @@ -76,7 +76,7 @@ | _ => I) | accumulate_improvements _ = I; val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty; - val ts' = (map o map_types) (Envir.typ_subst_TVars improvements) ts; + val ts' = (map o map_types) (Envir.subst_type improvements) ts; fun apply_subst t = Envir.expand_term (fn Const (c, ty) => (case subst (c, ty) of SOME (ty', t') => if Type.typ_instance tsig (ty, ty') diff -r 76d6ba08a05f -r e8e0fb5da77a src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/Isar/proof_context.ML Mon Jul 20 08:32:07 2009 +0200 @@ -779,7 +779,7 @@ fun simult_matches ctxt (t, pats) = (case Seq.pull (Unify.matchers (theory_of ctxt) (map (rpair t) pats)) of NONE => error "Pattern match failed!" - | SOME (env, _) => map (apsnd snd) (Envir.alist_of env)); + | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []); (* bind_terms *) diff -r 76d6ba08a05f -r e8e0fb5da77a src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/Isar/theory_target.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/Proof/extraction.ML Mon Jul 20 08:32:07 2009 +0200 @@ -103,11 +103,10 @@ fun ren t = the_default t (Term.rename_abs tm1 tm t); val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1); val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty); - val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems; + val prems' = map (pairself (Envir.subst_term env o inc o ren)) prems; val env' = Envir.Envir - {maxidx = Library.foldl Int.max - (~1, map (Int.max o pairself maxidx_of_term) prems'), - iTs = Tenv, asol = tenv}; + {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1, + tenv = tenv, tyenv = Tenv}; val env'' = fold (Pattern.unify thy o pairself (lookup rew)) prems' env'; in SOME (Envir.norm_term env'' (inc (ren tm2))) end handle Pattern.MATCH => NONE | Pattern.Unif => NONE) diff -r 76d6ba08a05f -r e8e0fb5da77a src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/Proof/reconstruct.ML Mon Jul 20 08:32:07 2009 +0200 @@ -35,12 +35,6 @@ fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf (vars_of prop @ frees_of prop) prf; -fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1}) - (Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) = - Envir.Envir {asol=Vartab.merge (op =) (asol1, asol2), - iTs=Vartab.merge (op =) (iTs1, iTs2), - maxidx=Int.max (maxidx1, maxidx2)}; - (**** generate constraints for proof term ****) @@ -48,31 +42,32 @@ let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T) in (env', list_comb (v, map Bound (length Ts - 1 downto 0))) end; -fun mk_tvar (Envir.Envir {iTs, asol, maxidx}, s) = - (Envir.Envir {iTs = iTs, asol = asol, maxidx = maxidx+1}, - TVar (("'t", maxidx+1), s)); +fun mk_tvar (Envir.Envir {maxidx, tenv, tyenv}, s) = + (Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}, + TVar (("'t", maxidx + 1), s)); val mk_abs = fold (fn T => fn u => Abs ("", T, u)); fun unifyT thy env T U = let - val Envir.Envir {asol, iTs, maxidx} = env; - val (iTs', maxidx') = Sign.typ_unify thy (T, U) (iTs, maxidx) - in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end - handle Type.TUNIFY => error ("Non-unifiable types:\n" ^ - Syntax.string_of_typ_global thy T ^ "\n\n" ^ Syntax.string_of_typ_global thy U); + val Envir.Envir {maxidx, tenv, tyenv} = env; + val (tyenv', maxidx') = Sign.typ_unify thy (T, U) (tyenv, maxidx); + in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end; -fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar ixnS) = - (case Type.lookup iTs ixnS of NONE => T | SOME T' => chaseT env T') +fun chaseT env (T as TVar v) = + (case Type.lookup (Envir.type_env env) v of + NONE => T + | SOME T' => chaseT env T') | chaseT _ T = T; -fun infer_type thy (env as Envir.Envir {maxidx, asol, iTs}) Ts vTs - (t as Const (s, T)) = if T = dummyT then (case Sign.const_type thy s of +fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) Ts vTs + (t as Const (s, T)) = if T = dummyT then + (case Sign.const_type thy s of NONE => error ("reconstruct_proof: No such constant: " ^ quote s) | SOME T => let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T) in (Const (s, T'), T', vTs, - Envir.Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs}) + Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}) end) else (t, T, vTs, env) | infer_type thy env Ts vTs (t as Free (s, T)) = @@ -236,21 +231,23 @@ fun upd_constrs env cs = let - val Envir.Envir {asol, iTs, ...} = env; + val tenv = Envir.term_env env; + val tyenv = Envir.type_env env; val dom = [] - |> Vartab.fold (cons o #1) asol - |> Vartab.fold (cons o #1) iTs; + |> Vartab.fold (cons o #1) tenv + |> Vartab.fold (cons o #1) tyenv; val vran = [] - |> Vartab.fold (Term.add_var_names o #2 o #2) asol - |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) iTs; + |> Vartab.fold (Term.add_var_names o #2 o #2) tenv + |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) tyenv; fun check_cs [] = [] - | check_cs ((u, p, vs)::ps) = - let val vs' = subtract (op =) dom vs; - in if vs = vs' then (u, p, vs)::check_cs ps - else (true, p, fold (insert (op =)) vs' vran)::check_cs ps - end + | check_cs ((u, p, vs) :: ps) = + let val vs' = subtract (op =) dom vs in + if vs = vs' then (u, p, vs) :: check_cs ps + else (true, p, fold (insert op =) vs' vran) :: check_cs ps + end; in check_cs cs end; + (**** solution of constraints ****) fun solve _ [] bigenv = bigenv @@ -280,7 +277,7 @@ val Envir.Envir {maxidx, ...} = bigenv; val (env, cs') = search (Envir.empty maxidx) cs; in - solve thy (upd_constrs env cs') (merge_envs bigenv env) + solve thy (upd_constrs env cs') (Envir.merge (bigenv, env)) end; @@ -353,8 +350,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 +360,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 76d6ba08a05f -r e8e0fb5da77a src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/ROOT.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/Pure/defs.ML --- a/src/Pure/defs.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/defs.ML Mon Jul 20 08:32:07 2009 +0200 @@ -10,10 +10,10 @@ val pretty_const: Pretty.pp -> string * typ list -> Pretty.T val plain_args: typ list -> bool type T + val all_specifications_of: T -> (string * {is_def: bool, name: string, + lhs: typ list, rhs: (string * typ list) list} list) list val specifications_of: T -> string -> {is_def: bool, name: string, lhs: typ list, rhs: (string * typ list) list} list - val all_specifications_of: T -> (string * {is_def: bool, name: string, - lhs: typ list, rhs: (string * typ list) list} list) list val dest: T -> {restricts: ((string * typ list) * string) list, reducts: ((string * typ list) * (string * typ list) list) list} @@ -46,7 +46,7 @@ handle Type.TUNIFY => true); fun match_args (Ts, Us) = - Option.map Envir.typ_subst_TVars + Option.map Envir.subst_type (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE); @@ -75,9 +75,11 @@ SOME (def: def) => which def | NONE => []); +fun all_specifications_of (Defs defs) = + (map o apsnd) (map snd o Inttab.dest o #specs) (Symtab.dest defs); + fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs; -fun all_specifications_of (Defs defs) = - ((map o apsnd) (map snd o Inttab.dest o #specs) o Symtab.dest) defs; + val restricts_of = lookup_list #restricts; val reducts_of = lookup_list #reducts; diff -r 76d6ba08a05f -r e8e0fb5da77a src/Pure/envir.ML --- a/src/Pure/envir.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/envir.ML Mon Jul 20 08:32:07 2009 +0200 @@ -1,249 +1,275 @@ (* Title: Pure/envir.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory -Environments. The type of a term variable / sort of a type variable is -part of its name. The lookup function must apply type substitutions, +Free-form environments. The type of a term variable / sort of a type variable is +part of its name. The lookup function must apply type substitutions, since they may change the identity of a variable. *) signature ENVIR = sig - type tenv - datatype env = Envir of {asol: tenv, iTs: Type.tyenv, maxidx: int} + type tenv = (typ * term) Vartab.table + datatype env = Envir of {maxidx: int, tenv: tenv, tyenv: Type.tyenv} + val maxidx_of: env -> int + val term_env: env -> tenv val type_env: env -> Type.tyenv + val is_empty: env -> bool + val empty: int -> env + val merge: env * env -> env 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 val lookup': tenv * (indexname * typ) -> term option val update: ((indexname * typ) * term) * env -> env - val empty: int -> env - val is_empty: env -> bool val above: env -> int -> bool val vupdate: ((indexname * typ) * term) * env -> env - val alist_of: env -> (indexname * (typ * term)) list + 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_term_same: env -> term Same.operation val norm_term: env -> term -> term - val norm_term_same: env -> term -> term - 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 beta_norm: term -> term val head_norm: env -> term -> term val eta_contract: term -> term val beta_eta_contract: term -> term val fastype: env -> typ list -> term -> typ - val typ_subst_TVars: Type.tyenv -> typ -> typ - val subst_TVars: Type.tyenv -> term -> term - val subst_Vars: tenv -> term -> term - val subst_vars: Type.tyenv * tenv -> term -> term + val subst_type_same: Type.tyenv -> typ Same.operation + val subst_term_types_same: Type.tyenv -> term Same.operation + val subst_term_same: Type.tyenv * tenv -> term Same.operation + val subst_type: Type.tyenv -> typ -> typ + val subst_term_types: Type.tyenv -> term -> term + val subst_term: Type.tyenv * tenv -> term -> term val expand_atom: typ -> typ * term -> term val expand_term: (term -> (typ * term) option) -> term -> term val expand_term_frees: ((string * typ) * term) list -> term -> term end; -structure Envir : ENVIR = +structure Envir: ENVIR = struct -(*updating can destroy environment in 2 ways!! - (1) variables out of range (2) circular assignments +(** datatype env **) + +(*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, (*upper bound of maximum index of vars*) + tenv: tenv, (*assignments to Vars*) + tyenv: Type.tyenv}; (*assignments to TVars*) + +fun make_env (maxidx, tenv, tyenv) = Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv}; +fun map_env f (Envir {maxidx, tenv, tyenv}) = make_env (f (maxidx, tenv, tyenv)); + +fun maxidx_of (Envir {maxidx, ...}) = maxidx; +fun term_env (Envir {tenv, ...}) = tenv; +fun type_env (Envir {tyenv, ...}) = tyenv; + +fun is_empty env = + Vartab.is_empty (term_env env) andalso + Vartab.is_empty (type_env env); -fun type_env (Envir {iTs, ...}) = iTs; + +(* build env *) + +fun empty maxidx = make_env (maxidx, Vartab.empty, Vartab.empty); -(*NB: type unification may invent new sorts*) +fun merge + (Envir {maxidx = maxidx1, tenv = tenv1, tyenv = tyenv1}, + Envir {maxidx = maxidx2, tenv = tenv2, tyenv = tyenv2}) = + make_env (Int.max (maxidx1, maxidx2), + Vartab.merge (op =) (tenv1, tenv2), + Vartab.merge (op =) (tyenv1, tyenv2)); + + +(*NB: type unification may invent new sorts*) (* FIXME tenv!? *) val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) o type_env; (*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; +fun genvars name (Envir {maxidx, tenv, tyenv}, 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, tenv = tenv, tyenv = tyenv}, 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], []); +fun var_clash xi T T' = + raise TYPE ("Variable " ^ quote (Term.string_of_vname xi) ^ " 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); +fun lookup_check check tenv (xi, T) = + (case Vartab.lookup tenv xi of + NONE => NONE + | SOME (U, t) => if check (T, U) then SOME t else var_clash xi T U); (* When dealing with environments produced by matching instead *) (* of unification, there is no need to chase assigned TVars. *) (* In this case, we can simply ignore the type substitution *) (* and use = instead of eq_type. *) -fun lookup' (asol, p) = gen_lookup op = asol p; +fun lookup' (tenv, p) = lookup_check (op =) tenv p; -fun lookup2 (iTs, asol) p = - if Vartab.is_empty iTs then lookup' (asol, p) - else gen_lookup (Type.eq_type iTs) asol p; - -fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p; +fun lookup2 (tyenv, tenv) = + lookup_check (Type.eq_type tyenv) tenv; -fun update (((xname, T), t), Envir {maxidx, asol, iTs}) = - Envir{maxidx=maxidx, asol=Vartab.update_new (xname, (T, t)) asol, iTs=iTs}; +fun lookup (Envir {tenv, tyenv, ...}, p) = lookup2 (tyenv, tenv) p; -(*The empty environment. New variables will start with the given index+1.*) -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; +fun update (((xi, T), t), Envir {maxidx, tenv, tyenv}) = + Envir {maxidx = maxidx, tenv = Vartab.update_new (xi, (T, t)) tenv, tyenv = tyenv}; (*Determine if the least index updated exceeds lim*) -fun above (Envir {asol, iTs, ...}) lim = - (case Vartab.min_key asol of SOME (_, i) => i > lim | NONE => true) andalso - (case Vartab.min_key iTs of SOME (_, i) => i > lim | NONE => true); +fun above (Envir {tenv, tyenv, ...}) lim = + (case Vartab.min_key tenv of SOME (_, i) => i > lim | NONE => true) andalso + (case Vartab.min_key tyenv of SOME (_, i) => i > lim | NONE => true); (*Update, checking Var-Var assignments: try to suppress higher indexes*) -fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of - Var (nT as (name', T)) => - if a = name' then env (*cycle!*) - else if TermOrd.indexname_ord (a, name') = LESS then - (case lookup (env, nT) of (*if already assigned, chase*) - NONE => update ((nT, Var (a, T)), env) - | SOME u => vupdate ((aU, u), env)) - else update ((aU, t), env) - | _ => update ((aU, t), env); +fun vupdate ((aU as (a, U), t), env as Envir {tyenv, ...}) = + (case t of + Var (nT as (name', T)) => + if a = name' then env (*cycle!*) + else if TermOrd.indexname_ord (a, name') = LESS then + (case lookup (env, nT) of (*if already assigned, chase*) + NONE => update ((nT, Var (a, T)), env) + | SOME u => vupdate ((aU, u), env)) + else update ((aU, t), env) + | _ => update ((aU, t), env)); -(*Convert environment to alist*) -fun alist_of (Envir{asol,...}) = Vartab.dest asol; - -(*** Beta normal form for terms (not eta normal form). - Chases variables in env; Does not exploit sharing of variable bindings - Does not check types, so could loop. ***) +(** beta normalization wrt. environment **) -(*raised when norm has no effect on a term, to do sharing instead of copying*) -exception SAME; +(*Chases variables in env. Does not exploit sharing of variable bindings + Does not check types, so could loop.*) + +local -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_type0 tyenv : 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 tyenv v of + SOME U => Same.commit norm U + | NONE => raise Same.SAME); + in norm end; + +fun norm_term1 tenv : term Same.operation = + let + fun norm (Var v) = + (case lookup' (tenv, 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 tenv tyenv : term Same.operation = + let + val normT = norm_type0 tyenv; + fun norm (Const (a, T)) = Const (a, normT T) + | norm (Free (a, T)) = Free (a, normT T) + | norm (Var (xi, T)) = + (case lookup2 (tyenv, tenv) (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 tyenv T = + if Vartab.is_empty tyenv then raise Same.SAME + else norm_type0 tyenv 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 tyenv Ts = + if Vartab.is_empty tyenv then raise Same.SAME + else Same.map (norm_type0 tyenv) Ts; + +fun norm_type tyenv T = norm_type_same tyenv 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 {tenv, tyenv, ...}) = + if Vartab.is_empty tyenv then norm_term1 tenv + else norm_term2 tenv tyenv; +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; @@ -252,64 +278,89 @@ (*finds type of term without checking that combinations are consistent Ts holds types of bound variables*) -fun fastype (Envir {iTs, ...}) = -let val funerr = "fastype: expected function type"; +fun fastype (Envir {tyenv, ...}) = + let + val funerr = "fastype: expected function type"; fun fast Ts (f $ u) = - (case fast Ts f of - Type ("fun", [_, T]) => T - | TVar ixnS => - (case Type.lookup iTs ixnS of - SOME (Type ("fun", [_, T])) => T - | _ => raise TERM (funerr, [f $ u])) - | _ => raise TERM (funerr, [f $ u])) + (case fast Ts f of + Type ("fun", [_, T]) => T + | TVar v => + (case Type.lookup tyenv v of + SOME (Type ("fun", [_, T])) => T + | _ => raise TERM (funerr, [f $ u])) + | _ => raise TERM (funerr, [f $ u])) | fast Ts (Const (_, T)) = T | fast Ts (Free (_, T)) = T | fast Ts (Bound i) = - (nth Ts i - handle Subscript => raise TERM ("fastype: Bound", [Bound i])) + (nth Ts i handle Subscript => raise TERM ("fastype: Bound", [Bound i])) | fast Ts (Var (_, T)) = T - | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u -in fast end; + | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u; + in fast end; + -(*Substitute for type Vars in a type*) -fun typ_subst_TVars iTs T = if Vartab.is_empty iTs then T else - let fun subst(Type(a, Ts)) = Type(a, map subst Ts) - | subst(T as TFree _) = T - | subst(T as TVar ixnS) = - (case Type.lookup iTs ixnS of NONE => T | SOME(U) => U) - in subst T end; +(** plain substitution -- without variable chasing **) + +local -(*Substitute for type Vars in a term*) -val subst_TVars = map_types o typ_subst_TVars; +fun subst_type0 tyenv = Term_Subst.map_atypsT_same + (fn TVar v => + (case Type.lookup tyenv v of + SOME U => U + | NONE => raise Same.SAME) + | _ => raise Same.SAME); -(*Substitute for Vars in a term *) -fun subst_Vars itms t = if Vartab.is_empty itms then t else - let fun subst (v as Var ixnT) = the_default v (lookup' (itms, ixnT)) - | subst (Abs (a, T, t)) = Abs (a, T, subst t) - | subst (f $ t) = subst f $ subst t - | subst t = t - in subst t end; +fun subst_term1 tenv = Term_Subst.map_aterms_same + (fn Var v => + (case lookup' (tenv, v) of + SOME u => u + | NONE => raise Same.SAME) + | _ => raise Same.SAME); -(*Substitute for type/term Vars in a term *) -fun subst_vars (iTs, itms) = - if Vartab.is_empty iTs then subst_Vars itms else - let fun subst (Const (a, T)) = Const(a, typ_subst_TVars iTs T) - | subst (Free (a, T)) = Free (a, typ_subst_TVars iTs T) - | subst (Var (ixn, T)) = (case lookup' (itms, (ixn, T)) of - NONE => Var (ixn, typ_subst_TVars iTs T) - | SOME t => t) - | subst (b as Bound _) = b - | subst (Abs (a, T, t)) = Abs(a, typ_subst_TVars iTs T, subst t) - | subst (f $ t) = subst f $ subst t +fun subst_term2 tenv tyenv : term Same.operation = + let + val substT = subst_type0 tyenv; + fun subst (Const (a, T)) = Const (a, substT T) + | subst (Free (a, T)) = Free (a, substT T) + | subst (Var (xi, T)) = + (case lookup' (tenv, (xi, T)) of + SOME u => u + | NONE => Var (xi, substT T)) + | subst (Bound _) = raise Same.SAME + | subst (Abs (a, T, t)) = + (Abs (a, substT T, Same.commit subst t) + handle Same.SAME => Abs (a, T, subst t)) + | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u); in subst end; +in -(* expand defined atoms -- with local beta reduction *) +fun subst_type_same tyenv T = + if Vartab.is_empty tyenv then raise Same.SAME + else subst_type0 tyenv T; + +fun subst_term_types_same tyenv t = + if Vartab.is_empty tyenv then raise Same.SAME + else Term_Subst.map_types_same (subst_type0 tyenv) t; + +fun subst_term_same (tyenv, tenv) = + if Vartab.is_empty tenv then subst_term_types_same tyenv + else if Vartab.is_empty tyenv then subst_term1 tenv + else subst_term2 tenv tyenv; + +fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T; +fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t; +fun subst_term envs t = subst_term_same envs t handle Same.SAME => t; + +end; + + + +(** expand defined atoms -- with local beta reduction **) fun expand_atom T (U, u) = - subst_TVars (Type.raw_match (U, T) Vartab.empty) u - handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]); + subst_term_types (Type.raw_match (U, T) Vartab.empty) u + handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]); fun expand_term get = let @@ -322,10 +373,9 @@ (case head of Abs (x, T, t) => comb (Abs (x, T, expand t)) | _ => - (case get head of - SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args') - | NONE => comb head) - | _ => comb head) + (case get head of + SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args') + | NONE => comb head)) end; in expand end; diff -r 76d6ba08a05f -r e8e0fb5da77a src/Pure/logic.ML --- a/src/Pure/logic.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/logic.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/Pure/pattern.ML --- a/src/Pure/pattern.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/pattern.ML Mon Jul 20 08:32:07 2009 +0200 @@ -141,8 +141,10 @@ | split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts) | split_type _ = error("split_type"); -fun type_of_G (env as Envir.Envir {iTs, ...}) (T,n,is) = - let val (Ts, U) = split_type (Envir.norm_type iTs T, n, []) +fun type_of_G env (T, n, is) = + let + val tyenv = Envir.type_env env; + val (Ts, U) = split_type (Envir.norm_type tyenv T, n, []); in map (nth Ts) is ---> U end; fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js)); @@ -225,11 +227,12 @@ end; in if TermOrd.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end -fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) = - if T=U then env - else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx) - in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end - handle Type.TUNIFY => (typ_clash thy (iTs,T,U); raise Unif); +fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) = + if T = U then env + else + let val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx) + in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end + handle Type.TUNIFY => (typ_clash thy (tyenv, T, U); raise Unif); fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) => @@ -351,7 +354,7 @@ Abs(ns,Ts,ts) => (case obj of Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (ts,tt) env - | _ => let val Tt = Envir.typ_subst_TVars iTs Ts + | _ => let val Tt = Envir.subst_type iTs Ts in mtch((ns,Tt)::binders) (ts,(incr obj)$Bound(0)) env end) | _ => (case obj of Abs(nt,Tt,tt) => @@ -425,7 +428,7 @@ fun match_rew thy tm (tm1, tm2) = let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in - SOME (Envir.subst_vars (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm) + SOME (Envir.subst_term (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm) handle MATCH => NONE end; diff -r 76d6ba08a05f -r e8e0fb5da77a src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/proofterm.ML Mon Jul 20 08:32:07 2009 +0200 @@ -43,6 +43,7 @@ val proof_of: proof_body -> proof val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a + val join_bodies: proof_body list -> unit val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool} val oracle_ord: oracle * oracle -> order @@ -88,6 +89,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 +129,6 @@ structure Proofterm : PROOFTERM = struct -open Envir; - - (***** datatype proof *****) datatype proof = @@ -187,6 +186,8 @@ in (f (name, prop, body') x', seen') end); in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end; +fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies (); + fun status_of bodies = let fun status (PBody {oracles, thms, ...}) x = @@ -269,47 +270,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 +353,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 +379,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 +442,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 +450,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 +458,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) *****) @@ -490,9 +492,8 @@ | remove_types (Const (s, _)) = Const (s, dummyT) | remove_types t = t; -fun remove_types_env (Envir.Envir {iTs, asol, maxidx}) = - Envir.Envir {iTs = iTs, asol = Vartab.map (apsnd remove_types) asol, - maxidx = maxidx}; +fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) = + Envir.Envir {maxidx = maxidx, tenv = Vartab.map (apsnd remove_types) tenv, tyenv = tyenv}; fun norm_proof' env prf = norm_proof (remove_types_env env) prf; @@ -503,40 +504,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 +599,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 +626,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 +707,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 +750,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 *****) @@ -1082,34 +1090,47 @@ fun prf_subst (pinst, (tyinsts, insts)) = let - val substT = Envir.typ_subst_TVars tyinsts; + val substT = Envir.subst_type_same tyinsts; + val substTs = Same.map substT; - fun subst' lev (t as Var (ixn, _)) = (case AList.lookup (op =) insts ixn of - NONE => t + fun subst' lev (Var (xi, _)) = + (case AList.lookup (op =) insts xi of + NONE => raise Same.SAME | SOME u => incr_boundvars lev u) - | subst' lev (Const (s, T)) = Const (s, substT T) - | subst' lev (Free (s, T)) = Free (s, substT T) - | subst' lev (Abs (a, T, body)) = Abs (a, substT T, subst' (lev+1) body) - | subst' lev (f $ t) = subst' lev f $ subst' lev t - | subst' _ t = t; + | subst' _ (Const (s, T)) = Const (s, substT T) + | subst' _ (Free (s, T)) = Free (s, substT T) + | subst' lev (Abs (a, T, body)) = + (Abs (a, substT T, Same.commit (subst' (lev + 1)) body) + handle Same.SAME => Abs (a, T, subst' (lev + 1) body)) + | subst' lev (f $ t) = + (subst' lev f $ Same.commit (subst' lev) t + handle Same.SAME => f $ subst' lev t) + | subst' _ _ = raise Same.SAME; fun subst plev tlev (AbsP (a, t, body)) = - AbsP (a, Option.map (subst' tlev) t, subst (plev+1) tlev body) + (AbsP (a, Same.map_option (subst' tlev) t, Same.commit (subst (plev + 1) tlev) body) + handle Same.SAME => AbsP (a, t, subst (plev + 1) tlev body)) | subst plev tlev (Abst (a, T, body)) = - Abst (a, Option.map substT T, subst plev (tlev+1) body) - | subst plev tlev (prf %% prf') = subst plev tlev prf %% subst plev tlev prf' - | subst plev tlev (prf % t) = subst plev tlev prf % Option.map (subst' tlev) t - | subst plev tlev (prf as Hyp (Var (ixn, _))) = (case AList.lookup (op =) pinst ixn of - NONE => prf - | SOME prf' => incr_pboundvars plev tlev prf') - | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Option.map (map substT) Ts) + (Abst (a, Same.map_option substT T, Same.commit (subst plev (tlev + 1)) body) + handle Same.SAME => Abst (a, T, subst plev (tlev + 1) body)) + | subst plev tlev (prf %% prf') = + (subst plev tlev prf %% Same.commit (subst plev tlev) prf' + handle Same.SAME => prf %% subst plev tlev prf') + | subst plev tlev (prf % t) = + (subst plev tlev prf % Same.commit (Same.map_option (subst' tlev)) t + handle Same.SAME => prf % Same.map_option (subst' tlev) t) + | subst plev tlev (Hyp (Var (xi, _))) = + (case AList.lookup (op =) pinst xi of + NONE => raise Same.SAME + | SOME prf' => incr_pboundvars plev tlev prf') + | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts) | subst _ _ (OfClass (T, c)) = OfClass (substT T, c) - | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Option.map (map substT) Ts) - | subst _ _ (Promise (i, prop, Ts)) = Promise (i, prop, (map substT) Ts) + | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts) + | subst _ _ (Promise (i, prop, Ts)) = Promise (i, prop, substTs Ts) | subst _ _ (PThm (i, ((id, prop, Ts), body))) = - PThm (i, ((id, prop, Option.map (map substT) Ts), body)) - | subst _ _ t = t; - in subst 0 0 end; + PThm (i, ((id, prop, Same.map_option substTs Ts), body)) + | subst _ _ _ = raise Same.SAME; + in fn t => subst 0 0 t handle Same.SAME => t end; (*A fast unification filter: true unless the two terms cannot be unified. Terms must be NORMAL. Treats all Vars as distinct. *) @@ -1210,7 +1231,7 @@ (case skel of AbsP (_, _, skel') => skel' | _ => skel0) prf of SOME prf' => SOME (AbsP (s, t, prf')) | NONE => NONE) - | rew2 _ _ _ = NONE + | rew2 _ _ _ = NONE; in the_default prf (rew1 [] skel0 prf) end; diff -r 76d6ba08a05f -r e8e0fb5da77a src/Pure/term.ML --- a/src/Pure/term.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/term.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/Pure/term_subst.ML --- a/src/Pure/term_subst.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/term_subst.ML Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/Pure/thm.ML --- a/src/Pure/thm.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/thm.ML Mon Jul 20 08:32:07 2009 +0200 @@ -317,7 +317,7 @@ (Ctyp {T = TVar ((a, i), S), thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts}, Ctyp {T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}); fun mk_ctinst ((x, i), (T, t)) = - let val T = Envir.typ_subst_TVars Tinsts T in + let val T = Envir.subst_type Tinsts T in (Cterm {t = Var ((x, i), T), T = T, thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts}, Cterm {t = t, T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}) @@ -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, @@ -1247,12 +1247,12 @@ val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state; val thy = Theory.deref thy_ref; val (tpairs, Bs, Bi, C) = dest_state (state, i); - fun newth n (env as Envir.Envir {maxidx, ...}, tpairs) = + fun newth n (env, tpairs) = Thm (deriv_rule1 ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o Pt.assumption_proof Bs Bi n) der, {tags = [], - maxidx = maxidx, + maxidx = Envir.maxidx_of env, shyps = Envir.insert_sorts env shyps, hyps = hyps, tpairs = @@ -1465,15 +1465,15 @@ (*Faster normalization: skip assumptions that were lifted over*) fun norm_term_skip env 0 t = Envir.norm_term env t - | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) = - let val Envir.Envir{iTs, ...} = env - val T' = Envir.typ_subst_TVars iTs T - (*Must instantiate types of parameters because they are flattened; - this could be a NEW parameter*) - in Term.all T' $ Abs(a, T', norm_term_skip env n t) end - | norm_term_skip env n (Const("==>", _) $ A $ B) = - Logic.mk_implies (A, norm_term_skip env (n-1) B) - | norm_term_skip env n t = error"norm_term_skip: too few assumptions??"; + | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) = + let + val T' = Envir.subst_type (Envir.type_env env) T + (*Must instantiate types of parameters because they are flattened; + this could be a NEW parameter*) + in Term.all T' $ Abs (a, T', norm_term_skip env n t) end + | norm_term_skip env n (Const ("==>", _) $ A $ B) = + Logic.mk_implies (A, norm_term_skip env (n - 1) B) + | norm_term_skip env n t = error "norm_term_skip: too few assumptions??"; (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) @@ -1495,7 +1495,7 @@ and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0) val thy = Theory.deref (merge_thys2 state orule); (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **) - fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) = + fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) = let val normt = Envir.norm_term env; (*perform minimal copying here by examining env*) val (ntpairs, normp) = @@ -1520,7 +1520,7 @@ curry op oo (Pt.norm_proof' env)) (Pt.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder, {tags = [], - maxidx = maxidx, + maxidx = Envir.maxidx_of env, shyps = Envir.insert_sorts env (Sorts.union rshyps sshyps), hyps = union_hyps rhyps shyps, tpairs = ntpairs, diff -r 76d6ba08a05f -r e8e0fb5da77a src/Pure/type.ML --- a/src/Pure/type.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/type.ML Mon Jul 20 08:32:07 2009 +0200 @@ -494,12 +494,15 @@ (*equality with respect to a type environment*) -fun eq_type tye (T, T') = +fun equal_type tye (T, T') = (case (devar tye T, devar tye T') of (Type (s, Ts), Type (s', Ts')) => - s = s' andalso ListPair.all (eq_type tye) (Ts, Ts') + s = s' andalso ListPair.all (equal_type tye) (Ts, Ts') | (U, U') => U = U'); +fun eq_type tye = + if Vartab.is_empty tye then op = else equal_type tye; + (** extend and merge type signatures **) diff -r 76d6ba08a05f -r e8e0fb5da77a src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/type_infer.ML Mon Jul 20 08:32:07 2009 +0200 @@ -402,7 +402,7 @@ (*convert to preterms*) val ts = burrow_types check_typs raw_ts; - val (ts', (vps, ps)) = + val (ts', _) = fold_map (preterm_of const_type is_param o constrain_vars) ts (Vartab.empty, Vartab.empty); (*do type inference*) diff -r 76d6ba08a05f -r e8e0fb5da77a src/Pure/unify.ML --- a/src/Pure/unify.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Pure/unify.ML Mon Jul 20 08:32:07 2009 +0200 @@ -52,36 +52,48 @@ type dpair = binderlist * term * term; -fun body_type(Envir.Envir{iTs,...}) = -let fun bT(Type("fun",[_,T])) = bT T - | bT(T as TVar ixnS) = (case Type.lookup iTs ixnS of - NONE => T | SOME(T') => bT T') - | bT T = T -in bT end; +fun body_type env = + let + val tyenv = Envir.type_env env; + fun bT (Type ("fun", [_, T])) = bT T + | bT (T as TVar v) = + (case Type.lookup tyenv v of + NONE => T + | SOME T' => bT T') + | bT T = T; + in bT end; -fun binder_types(Envir.Envir{iTs,...}) = -let fun bTs(Type("fun",[T,U])) = T :: bTs U - | bTs(T as TVar ixnS) = (case Type.lookup iTs ixnS of - NONE => [] | SOME(T') => bTs T') - | bTs _ = [] -in bTs end; +fun binder_types env = + let + val tyenv = Envir.type_env env; + fun bTs (Type ("fun", [T, U])) = T :: bTs U + | bTs (T as TVar v) = + (case Type.lookup tyenv v of + NONE => [] + | SOME T' => bTs T') + | bTs _ = []; + in bTs end; fun strip_type env T = (binder_types env T, body_type env T); fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t; -(*Eta normal form*) -fun eta_norm(env as Envir.Envir{iTs,...}) = - let fun etif (Type("fun",[T,U]), t) = - Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0)) - | etif (TVar ixnS, t) = - (case Type.lookup iTs ixnS of - NONE => t | SOME(T) => etif(T,t)) - | etif (_,t) = t; - fun eta_nm (rbinder, Abs(a,T,body)) = - Abs(a, T, eta_nm ((a,T)::rbinder, body)) - | eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t) +(* eta normal form *) + +fun eta_norm env = + let + val tyenv = Envir.type_env env; + fun etif (Type ("fun", [T, U]), t) = + Abs ("", T, etif (U, incr_boundvars 1 t $ Bound 0)) + | etif (TVar v, t) = + (case Type.lookup tyenv v of + NONE => t + | SOME T => etif (T, t)) + | etif (_, t) = t; + fun eta_nm (rbinder, Abs (a, T, body)) = + Abs (a, T, eta_nm ((a, T) :: rbinder, body)) + | eta_nm (rbinder, t) = etif (fastype env (rbinder, t), t); in eta_nm end; @@ -186,11 +198,14 @@ exception ASSIGN; (*Raised if not an assignment*) -fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) = - if T=U then env - else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx) - in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end - handle Type.TUNIFY => raise CANTUNIFY; +fun unify_types thy (T, U, env) = + if T = U then env + else + let + val Envir.Envir {maxidx, tenv, tyenv} = env; + val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx); + in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end + handle Type.TUNIFY => raise CANTUNIFY; fun test_unify_types thy (args as (T,U,_)) = let val str_of = Syntax.string_of_typ_global thy; @@ -636,9 +651,9 @@ (*Pattern matching*) -fun first_order_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) = +fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) = let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv) - in Seq.single (Envir.Envir {asol = tenv', iTs = tyenv', maxidx = maxidx}) end + in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end handle Pattern.MATCH => Seq.empty; (*General matching -- keeps variables disjoint*) @@ -661,10 +676,12 @@ Term.map_aterms (fn t as Var ((x, i), T) => if i > maxidx then Var ((x, i - offset), T) else t | t => t); - fun norm_tvar (Envir.Envir {iTs = tyenv, ...}) ((x, i), S) = - ((x, i - offset), (S, decr_indexesT (Envir.norm_type tyenv (TVar ((x, i), S))))); - fun norm_var (env as Envir.Envir {iTs = tyenv, ...}) ((x, i), T) = + fun norm_tvar env ((x, i), S) = + ((x, i - offset), + (S, decr_indexesT (Envir.norm_type (Envir.type_env env) (TVar ((x, i), S))))); + fun norm_var env ((x, i), T) = let + val tyenv = Envir.type_env env; val T' = Envir.norm_type tyenv T; val t' = Envir.norm_term env (Var ((x, i), T')); in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end; @@ -672,8 +689,8 @@ fun result env = if Envir.above env maxidx then (* FIXME proper handling of generated vars!? *) SOME (Envir.Envir {maxidx = maxidx, - iTs = Vartab.make (map (norm_tvar env) pat_tvars), - asol = Vartab.make (map (norm_var env) pat_vars)}) + tyenv = Vartab.make (map (norm_tvar env) pat_tvars), + tenv = Vartab.make (map (norm_var env) pat_vars)}) else NONE; val empty = Envir.empty maxidx'; diff -r 76d6ba08a05f -r e8e0fb5da77a src/Tools/Compute_Oracle/linker.ML --- a/src/Tools/Compute_Oracle/linker.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Tools/Compute_Oracle/linker.ML Mon Jul 20 08:32:07 2009 +0200 @@ -341,7 +341,7 @@ let val (newsubsts, instances) = Linker.add_instances thy instances monocs val _ = if not (null newsubsts) then changed := true else () - val newpats = map (fn subst => Envir.subst_TVars subst p) newsubsts + val newpats = map (fn subst => Envir.subst_term_types subst p) newsubsts in PolyPattern (p, instances, instancepats@newpats) end diff -r 76d6ba08a05f -r e8e0fb5da77a src/Tools/coherent.ML --- a/src/Tools/coherent.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Tools/coherent.ML Mon Jul 20 08:32:07 2009 +0200 @@ -131,7 +131,7 @@ let val seq = Seq.of_list rules |> Seq.maps (fn (th, ps, cs) => valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) => let val cs' = map (fn (Ts, ts) => - (map (Envir.typ_subst_TVars tye) Ts, map (Envir.subst_vars env) ts)) cs + (map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs in inst_extra_vars ctxt dom cs' |> Seq.map_filter (fn (inst, cs'') => @@ -184,7 +184,7 @@ (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T)) (Vartab.dest tye), map (fn (ixn, (T, t)) => - (Thm.cterm_of thy (Var (ixn, Envir.typ_subst_TVars tye T)), + (Thm.cterm_of thy (Var (ixn, Envir.subst_type tye T)), Thm.cterm_of thy t)) (Vartab.dest env) @ map (fn (ixnT, t) => (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th) diff -r 76d6ba08a05f -r e8e0fb5da77a src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Tools/eqsubst.ML Mon Jul 20 08:32:07 2009 +0200 @@ -231,9 +231,9 @@ or should I be using them somehow? *) fun mk_insts env = (Vartab.dest (Envir.type_env env), - Envir.alist_of env); - val initenv = Envir.Envir {asol = Vartab.empty, - iTs = typinsttab, maxidx = ix2}; + Vartab.dest (Envir.term_env env)); + val initenv = + Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab}; val useq = Unify.smash_unifiers thry [a] initenv handle UnequalLengths => Seq.empty | Term.TERM _ => Seq.empty; diff -r 76d6ba08a05f -r e8e0fb5da77a src/Tools/induct.ML --- a/src/Tools/induct.ML Wed Jul 15 18:20:08 2009 +0200 +++ b/src/Tools/induct.ML Mon Jul 20 08:32:07 2009 +0200 @@ -423,14 +423,15 @@ local -fun dest_env thy (env as Envir.Envir {iTs, ...}) = +fun dest_env thy env = let val cert = Thm.cterm_of thy; val certT = Thm.ctyp_of thy; - val pairs = Envir.alist_of env; + val pairs = Vartab.dest (Envir.term_env env); + val types = Vartab.dest (Envir.type_env env); val ts = map (cert o Envir.norm_term env o #2 o #2) pairs; val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts); - in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end; + in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) types, xs ~~ ts) end; in @@ -450,8 +451,7 @@ val rule' = Thm.incr_indexes (maxidx + 1) rule; val concl = Logic.strip_assums_concl goal; in - Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] - (Envir.empty (#maxidx (Thm.rep_thm rule'))) + Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule')) |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule') end end handle Subscript => Seq.empty; diff -r 76d6ba08a05f -r e8e0fb5da77a src/ZF/Datatype_ZF.thy --- a/src/ZF/Datatype_ZF.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/ZF/Datatype_ZF.thy Mon Jul 20 08:32:07 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 76d6ba08a05f -r e8e0fb5da77a src/ZF/OrdQuant.thy --- a/src/ZF/OrdQuant.thy Wed Jul 15 18:20:08 2009 +0200 +++ b/src/ZF/OrdQuant.thy Mon Jul 20 08:32:07 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;