# HG changeset patch # User wenzelm # Date 1415736859 -3600 # Node ID 51890cb80b305359491a21d536a76f2212e53ef9 # Parent 2f65dcd32a5910d92dee4882a26a39ebafba358f# Parent 162a4c2e97bc222b21c0281f4e3a6d0800ac27db merged diff -r 2f65dcd32a59 -r 51890cb80b30 src/CCL/CCL.thy --- a/src/CCL/CCL.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CCL/CCL.thy Tue Nov 11 21:14:19 2014 +0100 @@ -27,18 +27,18 @@ consts (*** Evaluation Judgement ***) - Eval :: "[i,i]=>prop" (infixl "--->" 20) + Eval :: "[i,i]\prop" (infixl "--->" 20) (*** Bisimulations for pre-order and equality ***) - po :: "['a,'a]=>o" (infixl "[=" 50) + po :: "['a,'a]\o" (infixl "[=" 50) (*** Term Formers ***) true :: "i" false :: "i" - pair :: "[i,i]=>i" ("(1<_,/_>)") - lambda :: "(i=>i)=>i" (binder "lam " 55) - "case" :: "[i,i,i,[i,i]=>i,(i=>i)=>i]=>i" - "apply" :: "[i,i]=>i" (infixl "`" 56) + pair :: "[i,i]\i" ("(1<_,/_>)") + lambda :: "(i\i)\i" (binder "lam " 55) + "case" :: "[i,i,i,[i,i]\i,(i\i)\i]\i" + "apply" :: "[i,i]\i" (infixl "`" 56) bot :: "i" (******* EVALUATION SEMANTICS *******) @@ -53,23 +53,23 @@ pairV: " ---> " and lamV: "\b. lam x. b(x) ---> lam x. b(x)" and - caseVtrue: "[| t ---> true; d ---> c |] ==> case(t,d,e,f,g) ---> c" and - caseVfalse: "[| t ---> false; e ---> c |] ==> case(t,d,e,f,g) ---> c" and - caseVpair: "[| t ---> ; f(a,b) ---> c |] ==> case(t,d,e,f,g) ---> c" and - caseVlam: "\b. [| t ---> lam x. b(x); g(b) ---> c |] ==> case(t,d,e,f,g) ---> c" + caseVtrue: "\t ---> true; d ---> c\ \ case(t,d,e,f,g) ---> c" and + caseVfalse: "\t ---> false; e ---> c\ \ case(t,d,e,f,g) ---> c" and + caseVpair: "\t ---> ; f(a,b) ---> c\ \ case(t,d,e,f,g) ---> c" and + caseVlam: "\b. \t ---> lam x. b(x); g(b) ---> c\ \ case(t,d,e,f,g) ---> c" (*** Properties of evaluation: note that "t ---> c" impies that c is canonical ***) axiomatization where - canonical: "[| t ---> c; c==true ==> u--->v; - c==false ==> u--->v; - !!a b. c== ==> u--->v; - !!f. c==lam x. f(x) ==> u--->v |] ==> + canonical: "\t ---> c; c==true \ u--->v; + c==false \ u--->v; + \a b. c== \ u--->v; + \f. c==lam x. f(x) \ u--->v\ \ u--->v" (* Should be derivable - but probably a bitch! *) axiomatization where - substitute: "[| a==a'; t(a)--->c(a) |] ==> t(a')--->c(a')" + substitute: "\a==a'; t(a)--->c(a)\ \ t(a')--->c(a')" (************** LOGIC ***************) @@ -77,26 +77,26 @@ axiomatization where bot_def: "bot == (lam x. x`x)`(lam x. x`x)" and - apply_def: "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))" + apply_def: "f ` t == case(f, bot, bot, \x y. bot, \u. u(t))" -definition "fix" :: "(i=>i)=>i" +definition "fix" :: "(i\i)\i" where "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))" (* The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *) (* as a bisimulation. They can both be expressed as (bi)simulations up to *) (* behavioural equivalence (ie the relations PO and EQ defined below). *) -definition SIM :: "[i,i,i set]=>o" +definition SIM :: "[i,i,i set]\o" where - "SIM(t,t',R) == (t=true & t'=true) | (t=false & t'=false) | - (EX a a' b b'. t= & t'= & : R & : R) | - (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. : R))" + "SIM(t,t',R) == (t=true \ t'=true) | (t=false \ t'=false) | + (\a a' b b'. t= \ t'= \ : R \ : R) | + (\f f'. t=lam x. f(x) \ t'=lam x. f'(x) \ (ALL x. : R))" -definition POgen :: "i set => i set" - where "POgen(R) == {p. EX t t'. p= & (t = bot | SIM(t,t',R))}" +definition POgen :: "i set \ i set" + where "POgen(R) == {p. \t t'. p= \ (t = bot | SIM(t,t',R))}" -definition EQgen :: "i set => i set" - where "EQgen(R) == {p. EX t t'. p= & (t = bot & t' = bot | SIM(t,t',R))}" +definition EQgen :: "i set \ i set" + where "EQgen(R) == {p. \t t'. p= \ (t = bot \ t' = bot | SIM(t,t',R))}" definition PO :: "i set" where "PO == gfp(POgen)" @@ -111,23 +111,23 @@ axiomatization where po_refl: "a [= a" and - po_trans: "[| a [= b; b [= c |] ==> a [= c" and - po_cong: "a [= b ==> f(a) [= f(b)" and + po_trans: "\a [= b; b [= c\ \ a [= c" and + po_cong: "a [= b \ f(a) [= f(b)" and (* Extend definition of [= to program fragments of higher type *) - po_abstractn: "(!!x. f(x) [= g(x)) ==> (%x. f(x)) [= (%x. g(x))" + po_abstractn: "(\x. f(x) [= g(x)) \ (\x. f(x)) [= (\x. g(x))" (** Equality - equivalence axioms inherited from FOL.thy **) (** - congruence of "=" is axiomatised implicitly **) axiomatization where - eq_iff: "t = t' <-> t [= t' & t' [= t" + eq_iff: "t = t' \ t [= t' \ t' [= t" (** Properties of canonical values given by greatest fixed point definitions **) axiomatization where - PO_iff: "t [= t' <-> : PO" and - EQ_iff: "t = t' <-> : EQ" + PO_iff: "t [= t' \ : PO" and + EQ_iff: "t = t' \ : EQ" (** Behaviour of non-canonical terms (ie case) given by the following beta-rules **) @@ -140,19 +140,19 @@ (** The theory is non-trivial **) axiomatization where - distinctness: "~ lam x. b(x) = bot" + distinctness: "\ lam x. b(x) = bot" (*** Definitions of Termination and Divergence ***) -definition Dvg :: "i => o" +definition Dvg :: "i \ o" where "Dvg(t) == t = bot" -definition Trm :: "i => o" - where "Trm(t) == ~ Dvg(t)" +definition Trm :: "i \ o" + where "Trm(t) == \ Dvg(t)" text {* Would be interesting to build a similar theory for a typed programming language: - ie. true :: bool, fix :: ('a=>'a)=>'a etc...... + ie. true :: bool, fix :: ('a\'a)\'a etc...... This is starting to look like LCF. What are the advantages of this approach? @@ -169,14 +169,14 @@ subsection {* Congruence Rules *} (*similar to AP_THM in Gordon's HOL*) -lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)" +lemma fun_cong: "(f::'a\'b) = g \ f(x)=g(x)" by simp (*similar to AP_TERM in Gordon's HOL and FOL's subst_context*) -lemma arg_cong: "x=y ==> f(x)=f(y)" +lemma arg_cong: "x=y \ f(x)=f(y)" by simp -lemma abstractn: "(!!x. f(x) = g(x)) ==> f = g" +lemma abstractn: "(\x. f(x) = g(x)) \ f = g" apply (simp add: eq_iff) apply (blast intro: po_abstractn) done @@ -186,16 +186,16 @@ subsection {* Termination and Divergence *} -lemma Trm_iff: "Trm(t) <-> ~ t = bot" +lemma Trm_iff: "Trm(t) \ \ t = bot" by (simp add: Trm_def Dvg_def) -lemma Dvg_iff: "Dvg(t) <-> t = bot" +lemma Dvg_iff: "Dvg(t) \ t = bot" by (simp add: Trm_def Dvg_def) subsection {* Constructors are injective *} -lemma eq_lemma: "[| x=a; y=b; x=y |] ==> a=b" +lemma eq_lemma: "\x=a; y=b; x=y\ \ a=b" by simp ML {* @@ -215,8 +215,8 @@ *} lemma ccl_injs: - " = <-> (a=a' & b=b')" - "!!b b'. (lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))" + " = \ (a=a' \ b=b')" + "\b b'. (lam x. b(x) = lam x. b'(x)) \ ((ALL z. b(z)=b'(z)))" by (inj_rl caseBs) @@ -226,11 +226,10 @@ subsection {* Constructors are distinct *} -lemma lem: "t=t' ==> case(t,b,c,d,e) = case(t',b,c,d,e)" +lemma lem: "t=t' \ case(t,b,c,d,e) = case(t',b,c,d,e)" by simp ML {* - local fun pairs_of f x [] = [] | pairs_of f x (y::ys) = (f x y) :: (f y x) :: (pairs_of f x ys) @@ -247,7 +246,7 @@ val arity = length (binder_types T) in sy ^ (arg_str arity name "") end - fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b") + fun mk_thm_str thy a b = "\ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b") val lemma = @{thm lem}; val eq_lemma = @{thm eq_lemma}; @@ -259,18 +258,16 @@ fun mk_lemmas rls = maps mk_lemma (mk_combs pair rls) fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs end - *} ML {* - val caseB_lemmas = mk_lemmas @{thms caseBs} val ccl_dstncts = let fun mk_raw_dstnct_thm rls s = Goal.prove_global @{theory} [] [] (Syntax.read_prop_global @{theory} s) - (fn _=> rtac @{thm notI} 1 THEN eresolve_tac rls 1) + (fn _ => rtac @{thm notI} 1 THEN eresolve_tac rls 1) in map (mk_raw_dstnct_thm caseB_lemmas) (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end @@ -307,33 +304,33 @@ subsection {* Facts from gfp Definition of @{text "[="} and @{text "="} *} -lemma XHlemma1: "[| A=B; a:B <-> P |] ==> a:A <-> P" +lemma XHlemma1: "\A=B; a:B \ P\ \ a:A \ P" by simp -lemma XHlemma2: "(P(t,t') <-> Q) ==> ( : {p. EX t t'. p= & P(t,t')} <-> Q)" +lemma XHlemma2: "(P(t,t') \ Q) \ ( : {p. \t t'. p= \ P(t,t')} \ Q)" by blast subsection {* Pre-Order *} -lemma POgen_mono: "mono(%X. POgen(X))" +lemma POgen_mono: "mono(\X. POgen(X))" apply (unfold POgen_def SIM_def) apply (rule monoI) apply blast done lemma POgenXH: - " : POgen(R) <-> t= bot | (t=true & t'=true) | (t=false & t'=false) | - (EX a a' b b'. t= & t'= & : R & : R) | - (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. : R))" + " : POgen(R) \ t= bot | (t=true \ t'=true) | (t=false \ t'=false) | + (EX a a' b b'. t= \ t'= \ : R \ : R) | + (EX f f'. t=lam x. f(x) \ t'=lam x. f'(x) \ (ALL x. : R))" apply (unfold POgen_def SIM_def) apply (rule iff_refl [THEN XHlemma2]) done lemma poXH: - "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | - (EX a a' b b'. t= & t'= & a [= a' & b [= b') | - (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))" + "t [= t' \ t=bot | (t=true \ t'=true) | (t=false \ t'=false) | + (EX a a' b b'. t= \ t'= \ a [= a' \ b [= b') | + (EX f f'. t=lam x. f(x) \ t'=lam x. f'(x) \ (ALL x. f(x) [= f'(x)))" apply (simp add: PO_iff del: ex_simps) apply (rule POgen_mono [THEN PO_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded POgen_def SIM_def]) @@ -345,17 +342,17 @@ apply simp done -lemma bot_poleast: "a [= bot ==> a=bot" +lemma bot_poleast: "a [= bot \ a=bot" apply (drule poXH [THEN iffD1]) apply simp done -lemma po_pair: " [= <-> a [= a' & b [= b'" +lemma po_pair: " [= \ a [= a' \ b [= b'" apply (rule poXH [THEN iff_trans]) apply simp done -lemma po_lam: "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))" +lemma po_lam: "lam x. f(x) [= lam x. f'(x) \ (ALL x. f(x) [= f'(x))" apply (rule poXH [THEN iff_trans]) apply fastforce done @@ -366,41 +363,41 @@ assumes 1: "t [= t'" and 2: "a [= a'" and 3: "b [= b'" - and 4: "!!x y. c(x,y) [= c'(x,y)" - and 5: "!!u. d(u) [= d'(u)" + and 4: "\x y. c(x,y) [= c'(x,y)" + and 5: "\u. d(u) [= d'(u)" shows "case(t,a,b,c,d) [= case(t',a',b',c',d')" apply (rule 1 [THEN po_cong, THEN po_trans]) apply (rule 2 [THEN po_cong, THEN po_trans]) apply (rule 3 [THEN po_cong, THEN po_trans]) apply (rule 4 [THEN po_abstractn, THEN po_abstractn, THEN po_cong, THEN po_trans]) - apply (rule_tac f1 = "%d. case (t',a',b',c',d)" in + apply (rule_tac f1 = "\d. case (t',a',b',c',d)" in 5 [THEN po_abstractn, THEN po_cong, THEN po_trans]) apply (rule po_refl) done -lemma apply_pocong: "[| f [= f'; a [= a' |] ==> f ` a [= f' ` a'" +lemma apply_pocong: "\f [= f'; a [= a'\ \ f ` a [= f' ` a'" unfolding ccl_data_defs apply (rule case_pocong, (rule po_refl | assumption)+) apply (erule po_cong) done -lemma npo_lam_bot: "~ lam x. b(x) [= bot" +lemma npo_lam_bot: "\ lam x. b(x) [= bot" apply (rule notI) apply (drule bot_poleast) apply (erule distinctness [THEN notE]) done -lemma po_lemma: "[| x=a; y=b; x[=y |] ==> a[=b" +lemma po_lemma: "\x=a; y=b; x[=y\ \ a[=b" by simp -lemma npo_pair_lam: "~ [= lam x. f(x)" +lemma npo_pair_lam: "\ [= lam x. f(x)" apply (rule notI) apply (rule npo_lam_bot [THEN notE]) apply (erule case_pocong [THEN caseBlam [THEN caseBpair [THEN po_lemma]]]) apply (rule po_refl npo_lam_bot)+ done -lemma npo_lam_pair: "~ lam x. f(x) [= " +lemma npo_lam_pair: "\ lam x. f(x) [= " apply (rule notI) apply (rule npo_lam_bot [THEN notE]) apply (erule case_pocong [THEN caseBpair [THEN caseBlam [THEN po_lemma]]]) @@ -408,29 +405,25 @@ done lemma npo_rls1: - "~ true [= false" - "~ false [= true" - "~ true [= " - "~ [= true" - "~ true [= lam x. f(x)" - "~ lam x. f(x) [= true" - "~ false [= " - "~ [= false" - "~ false [= lam x. f(x)" - "~ lam x. f(x) [= false" - by (tactic {* - REPEAT (rtac @{thm notI} 1 THEN - dtac @{thm case_pocong} 1 THEN - etac @{thm rev_mp} 5 THEN - ALLGOALS (simp_tac @{context}) THEN - REPEAT (resolve_tac [@{thm po_refl}, @{thm npo_lam_bot}] 1)) *}) + "\ true [= false" + "\ false [= true" + "\ true [= " + "\ [= true" + "\ true [= lam x. f(x)" + "\ lam x. f(x) [= true" + "\ false [= " + "\ [= false" + "\ false [= lam x. f(x)" + "\ lam x. f(x) [= false" + by (rule notI, drule case_pocong, erule_tac [5] rev_mp, simp_all, + (rule po_refl npo_lam_bot)+)+ lemmas npo_rls = npo_pair_lam npo_lam_pair npo_rls1 subsection {* Coinduction for @{text "[="} *} -lemma po_coinduct: "[| : R; R <= POgen(R) |] ==> t [= u" +lemma po_coinduct: "\ : R; R <= POgen(R)\ \ t [= u" apply (rule PO_def [THEN def_coinduct, THEN PO_iff [THEN iffD2]]) apply assumption+ done @@ -438,26 +431,29 @@ subsection {* Equality *} -lemma EQgen_mono: "mono(%X. EQgen(X))" +lemma EQgen_mono: "mono(\X. EQgen(X))" apply (unfold EQgen_def SIM_def) apply (rule monoI) apply blast done lemma EQgenXH: - " : EQgen(R) <-> (t=bot & t'=bot) | (t=true & t'=true) | - (t=false & t'=false) | - (EX a a' b b'. t= & t'= & : R & : R) | - (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. : R))" + " : EQgen(R) \ (t=bot \ t'=bot) | (t=true \ t'=true) | + (t=false \ t'=false) | + (EX a a' b b'. t= \ t'= \ : R \ : R) | + (EX f f'. t=lam x. f(x) \ t'=lam x. f'(x) \ (ALL x. : R))" apply (unfold EQgen_def SIM_def) apply (rule iff_refl [THEN XHlemma2]) done lemma eqXH: - "t=t' <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | - (EX a a' b b'. t= & t'= & a=a' & b=b') | - (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x)=f'(x)))" - apply (subgoal_tac " : EQ <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | (EX a a' b b'. t= & t'= & : EQ & : EQ) | (EX f f'. t=lam x. f (x) & t'=lam x. f' (x) & (ALL x. : EQ))") + "t=t' \ (t=bot \ t'=bot) | (t=true \ t'=true) | (t=false \ t'=false) | + (EX a a' b b'. t= \ t'= \ a=a' \ b=b') | + (EX f f'. t=lam x. f(x) \ t'=lam x. f'(x) \ (ALL x. f(x)=f'(x)))" + apply (subgoal_tac " : EQ \ + (t=bot \ t'=bot) | (t=true \ t'=true) | (t=false \ t'=false) | + (EX a a' b b'. t= \ t'= \ : EQ \ : EQ) | + (EX f f'. t=lam x. f (x) \ t'=lam x. f' (x) \ (ALL x. : EQ))") apply (erule rev_mp) apply (simp add: EQ_iff [THEN iff_sym]) apply (rule EQgen_mono [THEN EQ_def [THEN def_gfp_Tarski], THEN XHlemma1, @@ -465,26 +461,26 @@ apply (rule iff_refl [THEN XHlemma2]) done -lemma eq_coinduct: "[| : R; R <= EQgen(R) |] ==> t = u" +lemma eq_coinduct: "\ : R; R <= EQgen(R)\ \ t = u" apply (rule EQ_def [THEN def_coinduct, THEN EQ_iff [THEN iffD2]]) apply assumption+ done lemma eq_coinduct3: - "[| : R; R <= EQgen(lfp(%x. EQgen(x) Un R Un EQ)) |] ==> t = u" + "\ : R; R <= EQgen(lfp(\x. EQgen(x) Un R Un EQ))\ \ t = u" apply (rule EQ_def [THEN def_coinduct3, THEN EQ_iff [THEN iffD2]]) apply (rule EQgen_mono | assumption)+ done -ML {* - fun eq_coinduct_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct} i - fun eq_coinduct3_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3} i +method_setup eq_coinduct3 = {* + Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => + SIMPLE_METHOD' (res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3})) *} subsection {* Untyped Case Analysis and Other Facts *} -lemma cond_eta: "(EX f. t=lam x. f(x)) ==> t = lam x.(t ` x)" +lemma cond_eta: "(EX f. t=lam x. f(x)) \ t = lam x.(t ` x)" by (auto simp: apply_def) lemma exhaustion: "(t=bot) | (t=true) | (t=false) | (EX a b. t=) | (EX f. t=lam x. f(x))" @@ -493,7 +489,7 @@ done lemma term_case: - "[| P(bot); P(true); P(false); !!x y. P(); !!b. P(lam x. b(x)) |] ==> P(t)" + "\P(bot); P(true); P(false); \x y. P(); \b. P(lam x. b(x))\ \ P(t)" using exhaustion [of t] by blast end diff -r 2f65dcd32a59 -r 51890cb80b30 src/CCL/Fix.thy --- a/src/CCL/Fix.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CCL/Fix.thy Tue Nov 11 21:14:19 2014 +0100 @@ -9,20 +9,20 @@ imports Type begin -definition idgen :: "i => i" - where "idgen(f) == lam t. case(t,true,false,%x y.,%u. lam x. f ` u(x))" +definition idgen :: "i \ i" + where "idgen(f) == lam t. case(t,true,false, \x y., \u. lam x. f ` u(x))" -axiomatization INCL :: "[i=>o]=>o" where - INCL_def: "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))" and - po_INCL: "INCL(%x. a(x) [= b(x))" and - INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))" +axiomatization INCL :: "[i\o]\o" where + INCL_def: "INCL(\x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) \ P(fix(f)))" and + po_INCL: "INCL(\x. a(x) [= b(x))" and + INCL_subst: "INCL(P) \ INCL(\x. P((g::i\i)(x)))" subsection {* Fixed Point Induction *} lemma fix_ind: assumes base: "P(bot)" - and step: "!!x. P(x) ==> P(f(x))" + and step: "\x. P(x) \ P(f(x))" and incl: "INCL(P)" shows "P(fix(f))" apply (rule incl [unfolded INCL_def, rule_format]) @@ -35,22 +35,22 @@ subsection {* Inclusive Predicates *} -lemma inclXH: "INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))" +lemma inclXH: "INCL(P) \ (ALL f. (ALL n:Nat. P(f ^ n ` bot)) \ P(fix(f)))" by (simp add: INCL_def) -lemma inclI: "[| !!f. ALL n:Nat. P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x. P(x))" +lemma inclI: "\\f. ALL n:Nat. P(f^n`bot) \ P(fix(f))\ \ INCL(\x. P(x))" unfolding inclXH by blast -lemma inclD: "[| INCL(P); !!n. n:Nat ==> P(f^n`bot) |] ==> P(fix(f))" +lemma inclD: "\INCL(P); \n. n:Nat \ P(f^n`bot)\ \ P(fix(f))" unfolding inclXH by blast -lemma inclE: "[| INCL(P); (ALL n:Nat. P(f^n`bot))-->P(fix(f)) ==> R |] ==> R" +lemma inclE: "\INCL(P); (ALL n:Nat. P(f^n`bot)) \ P(fix(f)) \ R\ \ R" by (blast dest: inclD) subsection {* Lemmas for Inclusive Predicates *} -lemma npo_INCL: "INCL(%x.~ a(x) [= t)" +lemma npo_INCL: "INCL(\x. \ a(x) [= t)" apply (rule inclI) apply (drule bspec) apply (rule zeroT) @@ -62,16 +62,16 @@ apply (rule po_cong, rule po_bot) done -lemma conj_INCL: "[| INCL(P); INCL(Q) |] ==> INCL(%x. P(x) & Q(x))" +lemma conj_INCL: "\INCL(P); INCL(Q)\ \ INCL(\x. P(x) \ Q(x))" by (blast intro!: inclI dest!: inclD) -lemma all_INCL: "[| !!a. INCL(P(a)) |] ==> INCL(%x. ALL a. P(a,x))" +lemma all_INCL: "(\a. INCL(P(a))) \ INCL(\x. ALL a. P(a,x))" by (blast intro!: inclI dest!: inclD) -lemma ball_INCL: "[| !!a. a:A ==> INCL(P(a)) |] ==> INCL(%x. ALL a:A. P(a,x))" +lemma ball_INCL: "(\a. a:A \ INCL(P(a))) \ INCL(\x. ALL a:A. P(a,x))" by (blast intro!: inclI dest!: inclD) -lemma eq_INCL: "INCL(%x. a(x) = (b(x)::'a::prog))" +lemma eq_INCL: "INCL(\x. a(x) = (b(x)::'a::prog))" apply (simp add: eq_iff) apply (rule conj_INCL po_INCL)+ done @@ -93,7 +93,7 @@ (* All fixed points are lam-expressions *) -schematic_lemma idgenfp_lam: "idgen(d) = d ==> d = lam x. ?f(x)" +schematic_lemma idgenfp_lam: "idgen(d) = d \ d = lam x. ?f(x)" apply (unfold idgen_def) apply (erule ssubst) apply (rule refl) @@ -101,15 +101,15 @@ (* Lemmas for rewriting fixed points of idgen *) -lemma l_lemma: "[| a = b; a ` t = u |] ==> b ` t = u" +lemma l_lemma: "\a = b; a ` t = u\ \ b ` t = u" by (simp add: idgen_def) lemma idgen_lemmas: - "idgen(d) = d ==> d ` bot = bot" - "idgen(d) = d ==> d ` true = true" - "idgen(d) = d ==> d ` false = false" - "idgen(d) = d ==> d ` = " - "idgen(d) = d ==> d ` (lam x. f(x)) = lam x. d ` f(x)" + "idgen(d) = d \ d ` bot = bot" + "idgen(d) = d \ d ` true = true" + "idgen(d) = d \ d ` false = false" + "idgen(d) = d \ d ` = " + "idgen(d) = d \ d ` (lam x. f(x)) = lam x. d ` f(x)" by (erule l_lemma, simp add: idgen_def)+ @@ -117,7 +117,7 @@ of idgen and hence are they same *) lemma po_eta: - "[| ALL x. t ` x [= u ` x; EX f. t=lam x. f(x); EX f. u=lam x. f(x) |] ==> t [= u" + "\ALL x. t ` x [= u ` x; EX f. t=lam x. f(x); EX f. u=lam x. f(x)\ \ t [= u" apply (drule cond_eta)+ apply (erule ssubst) apply (erule ssubst) @@ -125,15 +125,15 @@ apply simp done -schematic_lemma po_eta_lemma: "idgen(d) = d ==> d = lam x. ?f(x)" +schematic_lemma po_eta_lemma: "idgen(d) = d \ d = lam x. ?f(x)" apply (unfold idgen_def) apply (erule sym) done lemma lemma1: - "idgen(d) = d ==> - {p. EX a b. p= & (EX t. a=fix(idgen) ` t & b = d ` t)} <= - POgen({p. EX a b. p= & (EX t. a=fix(idgen) ` t & b = d ` t)})" + "idgen(d) = d \ + {p. EX a b. p= \ (EX t. a=fix(idgen) ` t \ b = d ` t)} <= + POgen({p. EX a b. p= \ (EX t. a=fix(idgen) ` t \ b = d ` t)})" apply clarify apply (rule_tac t = t in term_case) apply (simp_all add: POgenXH idgen_lemmas idgen_lemmas [OF fix_idgenfp]) @@ -141,22 +141,22 @@ apply fast done -lemma fix_least_idgen: "idgen(d) = d ==> fix(idgen) [= d" +lemma fix_least_idgen: "idgen(d) = d \ fix(idgen) [= d" apply (rule allI [THEN po_eta]) apply (rule lemma1 [THEN [2] po_coinduct]) apply (blast intro: po_eta_lemma fix_idgenfp)+ done lemma lemma2: - "idgen(d) = d ==> - {p. EX a b. p= & b = d ` a} <= POgen({p. EX a b. p= & b = d ` a})" + "idgen(d) = d \ + {p. EX a b. p= \ b = d ` a} <= POgen({p. EX a b. p= \ b = d ` a})" apply clarify apply (rule_tac t = a in term_case) apply (simp_all add: POgenXH idgen_lemmas) apply fast done -lemma id_least_idgen: "idgen(d) = d ==> lam x. x [= d" +lemma id_least_idgen: "idgen(d) = d \ lam x. x [= d" apply (rule allI [THEN po_eta]) apply (rule lemma2 [THEN [2] po_coinduct]) apply simp @@ -170,15 +170,15 @@ (********) -lemma id_apply: "f = lam x. x ==> f`t = t" +lemma id_apply: "f = lam x. x \ f`t = t" apply (erule ssubst) apply (rule applyB) done lemma term_ind: assumes 1: "P(bot)" and 2: "P(true)" and 3: "P(false)" - and 4: "!!x y.[| P(x); P(y) |] ==> P()" - and 5: "!!u.(!!x. P(u(x))) ==> P(lam x. u(x))" + and 4: "\x y. \P(x); P(y)\ \ P()" + and 5: "\u.(\x. P(u(x))) \ P(lam x. u(x))" and 6: "INCL(P)" shows "P(t)" apply (rule reachability [THEN id_apply, THEN subst]) diff -r 2f65dcd32a59 -r 51890cb80b30 src/CCL/Gfp.thy --- a/src/CCL/Gfp.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CCL/Gfp.thy Tue Nov 11 21:14:19 2014 +0100 @@ -10,37 +10,35 @@ begin definition - gfp :: "['a set=>'a set] => 'a set" where -- "greatest fixed point" + gfp :: "['a set\'a set] \ 'a set" where -- "greatest fixed point" "gfp(f) == Union({u. u <= f(u)})" (* gfp(f) is the least upper bound of {u. u <= f(u)} *) -lemma gfp_upperbound: "[| A <= f(A) |] ==> A <= gfp(f)" +lemma gfp_upperbound: "A <= f(A) \ A <= gfp(f)" unfolding gfp_def by blast -lemma gfp_least: "[| !!u. u <= f(u) ==> u<=A |] ==> gfp(f) <= A" +lemma gfp_least: "(\u. u <= f(u) \ u <= A) \ gfp(f) <= A" unfolding gfp_def by blast -lemma gfp_lemma2: "mono(f) ==> gfp(f) <= f(gfp(f))" +lemma gfp_lemma2: "mono(f) \ gfp(f) <= f(gfp(f))" by (rule gfp_least, rule subset_trans, assumption, erule monoD, rule gfp_upperbound, assumption) -lemma gfp_lemma3: "mono(f) ==> f(gfp(f)) <= gfp(f)" +lemma gfp_lemma3: "mono(f) \ f(gfp(f)) <= gfp(f)" by (rule gfp_upperbound, frule monoD, rule gfp_lemma2, assumption+) -lemma gfp_Tarski: "mono(f) ==> gfp(f) = f(gfp(f))" +lemma gfp_Tarski: "mono(f) \ gfp(f) = f(gfp(f))" by (rule equalityI gfp_lemma2 gfp_lemma3 | assumption)+ (*** Coinduction rules for greatest fixed points ***) (*weak version*) -lemma coinduct: "[| a: A; A <= f(A) |] ==> a : gfp(f)" +lemma coinduct: "\a: A; A <= f(A)\ \ a : gfp(f)" by (blast dest: gfp_upperbound) -lemma coinduct2_lemma: - "[| A <= f(A) Un gfp(f); mono(f) |] ==> - A Un gfp(f) <= f(A Un gfp(f))" +lemma coinduct2_lemma: "\A <= f(A) Un gfp(f); mono(f)\ \ A Un gfp(f) <= f(A Un gfp(f))" apply (rule subset_trans) prefer 2 apply (erule mono_Un) @@ -50,8 +48,7 @@ done (*strong version, thanks to Martin Coen*) -lemma coinduct2: - "[| a: A; A <= f(A) Un gfp(f); mono(f) |] ==> a : gfp(f)" +lemma coinduct2: "\a: A; A <= f(A) Un gfp(f); mono(f)\ \ a : gfp(f)" apply (rule coinduct) prefer 2 apply (erule coinduct2_lemma, assumption) @@ -62,13 +59,13 @@ - instead of the condition A <= f(A) consider A <= (f(A) Un f(f(A)) ...) Un gfp(A) ***) -lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un A Un B)" +lemma coinduct3_mono_lemma: "mono(f) \ mono(\x. f(x) Un A Un B)" by (rule monoI) (blast dest: monoD) lemma coinduct3_lemma: - assumes prem: "A <= f(lfp(%x. f(x) Un A Un gfp(f)))" + assumes prem: "A <= f(lfp(\x. f(x) Un A Un gfp(f)))" and mono: "mono(f)" - shows "lfp(%x. f(x) Un A Un gfp(f)) <= f(lfp(%x. f(x) Un A Un gfp(f)))" + shows "lfp(\x. f(x) Un A Un gfp(f)) <= f(lfp(\x. f(x) Un A Un gfp(f)))" apply (rule subset_trans) apply (rule mono [THEN coinduct3_mono_lemma, THEN lfp_lemma3]) apply (rule Un_least [THEN Un_least]) @@ -82,7 +79,7 @@ lemma coinduct3: assumes 1: "a:A" - and 2: "A <= f(lfp(%x. f(x) Un A Un gfp(f)))" + and 2: "A <= f(lfp(\x. f(x) Un A Un gfp(f)))" and 3: "mono(f)" shows "a : gfp(f)" apply (rule coinduct) @@ -95,25 +92,25 @@ subsection {* Definition forms of @{text "gfp_Tarski"}, to control unfolding *} -lemma def_gfp_Tarski: "[| h==gfp(f); mono(f) |] ==> h = f(h)" +lemma def_gfp_Tarski: "\h == gfp(f); mono(f)\ \ h = f(h)" apply unfold apply (erule gfp_Tarski) done -lemma def_coinduct: "[| h==gfp(f); a:A; A <= f(A) |] ==> a: h" +lemma def_coinduct: "\h == gfp(f); a:A; A <= f(A)\ \ a: h" apply unfold apply (erule coinduct) apply assumption done -lemma def_coinduct2: "[| h==gfp(f); a:A; A <= f(A) Un h; mono(f) |] ==> a: h" +lemma def_coinduct2: "\h == gfp(f); a:A; A <= f(A) Un h; mono(f)\ \ a: h" apply unfold apply (erule coinduct2) apply assumption apply assumption done -lemma def_coinduct3: "[| h==gfp(f); a:A; A <= f(lfp(%x. f(x) Un A Un h)); mono(f) |] ==> a: h" +lemma def_coinduct3: "\h == gfp(f); a:A; A <= f(lfp(\x. f(x) Un A Un h)); mono(f)\ \ a: h" apply unfold apply (erule coinduct3) apply assumption @@ -121,7 +118,7 @@ done (*Monotonicity of gfp!*) -lemma gfp_mono: "[| mono(f); !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)" +lemma gfp_mono: "\mono(f); \Z. f(Z) <= g(Z)\ \ gfp(f) <= gfp(g)" apply (rule gfp_upperbound) apply (rule subset_trans) apply (rule gfp_lemma2) diff -r 2f65dcd32a59 -r 51890cb80b30 src/CCL/Hered.thy --- a/src/CCL/Hered.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CCL/Hered.thy Tue Nov 11 21:14:19 2014 +0100 @@ -15,10 +15,10 @@ is. Not so useful for functions! *} -definition HTTgen :: "i set => i set" where +definition HTTgen :: "i set \ i set" where "HTTgen(R) == - {t. t=true | t=false | (EX a b. t= & a : R & b : R) | - (EX f. t = lam x. f(x) & (ALL x. f(x) : R))}" + {t. t=true | t=false | (EX a b. t= \ a : R \ b : R) | + (EX f. t = lam x. f(x) \ (ALL x. f(x) : R))}" definition HTT :: "i set" where "HTT == gfp(HTTgen)" @@ -26,22 +26,22 @@ subsection {* Hereditary Termination *} -lemma HTTgen_mono: "mono(%X. HTTgen(X))" +lemma HTTgen_mono: "mono(\X. HTTgen(X))" apply (unfold HTTgen_def) apply (rule monoI) apply blast done lemma HTTgenXH: - "t : HTTgen(A) <-> t=true | t=false | (EX a b. t= & a : A & b : A) | - (EX f. t=lam x. f(x) & (ALL x. f(x) : A))" + "t : HTTgen(A) \ t=true | t=false | (EX a b. t= \ a : A \ b : A) | + (EX f. t=lam x. f(x) \ (ALL x. f(x) : A))" apply (unfold HTTgen_def) apply blast done lemma HTTXH: - "t : HTT <-> t=true | t=false | (EX a b. t= & a : HTT & b : HTT) | - (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))" + "t : HTT \ t=true | t=false | (EX a b. t= \ a : HTT \ b : HTT) | + (EX f. t=lam x. f(x) \ (ALL x. f(x) : HTT))" apply (rule HTTgen_mono [THEN HTT_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded HTTgen_def]) apply blast done @@ -49,7 +49,7 @@ subsection {* Introduction Rules for HTT *} -lemma HTT_bot: "~ bot : HTT" +lemma HTT_bot: "\ bot : HTT" by (blast dest: HTTXH [THEN iffD1]) lemma HTT_true: "true : HTT" @@ -58,12 +58,12 @@ lemma HTT_false: "false : HTT" by (blast intro: HTTXH [THEN iffD2]) -lemma HTT_pair: " : HTT <-> a : HTT & b : HTT" +lemma HTT_pair: " : HTT \ a : HTT \ b : HTT" apply (rule HTTXH [THEN iff_trans]) apply blast done -lemma HTT_lam: "lam x. f(x) : HTT <-> (ALL x. f(x) : HTT)" +lemma HTT_lam: "lam x. f(x) : HTT \ (ALL x. f(x) : HTT)" apply (rule HTTXH [THEN iff_trans]) apply auto done @@ -72,12 +72,12 @@ lemma HTT_rews2: "one : HTT" - "inl(a) : HTT <-> a : HTT" - "inr(b) : HTT <-> b : HTT" + "inl(a) : HTT \ a : HTT" + "inr(b) : HTT \ b : HTT" "zero : HTT" - "succ(n) : HTT <-> n : HTT" + "succ(n) : HTT \ n : HTT" "[] : HTT" - "x$xs : HTT <-> x : HTT & xs : HTT" + "x$xs : HTT \ x : HTT \ xs : HTT" by (simp_all add: data_defs HTT_rews1) lemmas HTT_rews = HTT_rews1 HTT_rews2 @@ -85,13 +85,12 @@ subsection {* Coinduction for HTT *} -lemma HTT_coinduct: "[| t : R; R <= HTTgen(R) |] ==> t : HTT" +lemma HTT_coinduct: "\t : R; R <= HTTgen(R)\ \ t : HTT" apply (erule HTT_def [THEN def_coinduct]) apply assumption done -lemma HTT_coinduct3: - "[| t : R; R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT" +lemma HTT_coinduct3: "\t : R; R <= HTTgen(lfp(\x. HTTgen(x) Un R Un HTT))\ \ t : HTT" apply (erule HTTgen_mono [THEN [3] HTT_def [THEN def_coinduct3]]) apply assumption done @@ -99,16 +98,16 @@ lemma HTTgenIs: "true : HTTgen(R)" "false : HTTgen(R)" - "[| a : R; b : R |] ==> : HTTgen(R)" - "!!b. [| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)" + "\a : R; b : R\ \ : HTTgen(R)" + "\b. (\x. b(x) : R) \ lam x. b(x) : HTTgen(R)" "one : HTTgen(R)" - "a : lfp(%x. HTTgen(x) Un R Un HTT) ==> inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))" - "b : lfp(%x. HTTgen(x) Un R Un HTT) ==> inr(b) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))" - "zero : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))" - "n : lfp(%x. HTTgen(x) Un R Un HTT) ==> succ(n) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))" - "[] : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))" - "[| h : lfp(%x. HTTgen(x) Un R Un HTT); t : lfp(%x. HTTgen(x) Un R Un HTT) |] ==> - h$t : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))" + "a : lfp(\x. HTTgen(x) Un R Un HTT) \ inl(a) : HTTgen(lfp(\x. HTTgen(x) Un R Un HTT))" + "b : lfp(\x. HTTgen(x) Un R Un HTT) \ inr(b) : HTTgen(lfp(\x. HTTgen(x) Un R Un HTT))" + "zero : HTTgen(lfp(\x. HTTgen(x) Un R Un HTT))" + "n : lfp(\x. HTTgen(x) Un R Un HTT) \ succ(n) : HTTgen(lfp(\x. HTTgen(x) Un R Un HTT))" + "[] : HTTgen(lfp(\x. HTTgen(x) Un R Un HTT))" + "\h : lfp(\x. HTTgen(x) Un R Un HTT); t : lfp(\x. HTTgen(x) Un R Un HTT)\ \ + h$t : HTTgen(lfp(\x. HTTgen(x) Un R Un HTT))" unfolding data_defs by (genIs HTTgenXH HTTgen_mono)+ @@ -120,10 +119,10 @@ lemma BoolF: "Bool <= HTT" by (fastforce simp: subsetXH BoolXH iff: HTT_rews) -lemma PlusF: "[| A <= HTT; B <= HTT |] ==> A + B <= HTT" +lemma PlusF: "\A <= HTT; B <= HTT\ \ A + B <= HTT" by (fastforce simp: subsetXH PlusXH iff: HTT_rews) -lemma SigmaF: "[| A <= HTT; !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT" +lemma SigmaF: "\A <= HTT; \x. x:A \ B(x) <= HTT\ \ SUM x:A. B(x) <= HTT" by (fastforce simp: subsetXH SgXH HTT_rews) @@ -144,7 +143,7 @@ apply (fast intro: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] dest: NatXH [THEN iffD1]) done -lemma ListF: "A <= HTT ==> List(A) <= HTT" +lemma ListF: "A <= HTT \ List(A) <= HTT" apply clarify apply (erule HTT_coinduct3) apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] @@ -152,14 +151,14 @@ dest: ListXH [THEN iffD1]) done -lemma ListsF: "A <= HTT ==> Lists(A) <= HTT" +lemma ListsF: "A <= HTT \ Lists(A) <= HTT" apply clarify apply (erule HTT_coinduct3) apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] subsetD [THEN HTTgen_mono [THEN ci3_AI]] dest: ListsXH [THEN iffD1]) done -lemma IListsF: "A <= HTT ==> ILists(A) <= HTT" +lemma IListsF: "A <= HTT \ ILists(A) <= HTT" apply clarify apply (erule HTT_coinduct3) apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI] diff -r 2f65dcd32a59 -r 51890cb80b30 src/CCL/Lfp.thy --- a/src/CCL/Lfp.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CCL/Lfp.thy Tue Nov 11 21:14:19 2014 +0100 @@ -10,24 +10,24 @@ begin definition - lfp :: "['a set=>'a set] => 'a set" where -- "least fixed point" + lfp :: "['a set\'a set] \ 'a set" where -- "least fixed point" "lfp(f) == Inter({u. f(u) <= u})" (* lfp(f) is the greatest lower bound of {u. f(u) <= u} *) -lemma lfp_lowerbound: "[| f(A) <= A |] ==> lfp(f) <= A" +lemma lfp_lowerbound: "f(A) <= A \ lfp(f) <= A" unfolding lfp_def by blast -lemma lfp_greatest: "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)" +lemma lfp_greatest: "(\u. f(u) <= u \ A<=u) \ A <= lfp(f)" unfolding lfp_def by blast -lemma lfp_lemma2: "mono(f) ==> f(lfp(f)) <= lfp(f)" +lemma lfp_lemma2: "mono(f) \ f(lfp(f)) <= lfp(f)" by (rule lfp_greatest, rule subset_trans, drule monoD, rule lfp_lowerbound, assumption+) -lemma lfp_lemma3: "mono(f) ==> lfp(f) <= f(lfp(f))" +lemma lfp_lemma3: "mono(f) \ lfp(f) <= f(lfp(f))" by (rule lfp_lowerbound, frule monoD, drule lfp_lemma2, assumption+) -lemma lfp_Tarski: "mono(f) ==> lfp(f) = f(lfp(f))" +lemma lfp_Tarski: "mono(f) \ lfp(f) = f(lfp(f))" by (rule equalityI lfp_lemma2 lfp_lemma3 | assumption)+ @@ -36,7 +36,7 @@ lemma induct: assumes lfp: "a: lfp(f)" and mono: "mono(f)" - and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)" + and indhyp: "\x. \x: f(lfp(f) Int {x. P(x)})\ \ P(x)" shows "P(a)" apply (rule_tac a = a in Int_lower2 [THEN subsetD, THEN CollectD]) apply (rule lfp [THEN [2] lfp_lowerbound [THEN subsetD]]) @@ -46,16 +46,13 @@ (** Definition forms of lfp_Tarski and induct, to control unfolding **) -lemma def_lfp_Tarski: "[| h==lfp(f); mono(f) |] ==> h = f(h)" +lemma def_lfp_Tarski: "\h == lfp(f); mono(f)\ \ h = f(h)" apply unfold apply (drule lfp_Tarski) apply assumption done -lemma def_induct: - "[| A == lfp(f); a:A; mono(f); - !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x) - |] ==> P(a)" +lemma def_induct: "\A == lfp(f); a:A; mono(f); \x. x: f(A Int {x. P(x)}) \ P(x)\ \ P(a)" apply (rule induct [of concl: P a]) apply simp apply assumption @@ -63,7 +60,7 @@ done (*Monotonicity of lfp!*) -lemma lfp_mono: "[| mono(g); !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)" +lemma lfp_mono: "\mono(g); \Z. f(Z) <= g(Z)\ \ lfp(f) <= lfp(g)" apply (rule lfp_lowerbound) apply (rule subset_trans) apply (erule meta_spec) diff -r 2f65dcd32a59 -r 51890cb80b30 src/CCL/ROOT --- a/src/CCL/ROOT Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CCL/ROOT Tue Nov 11 21:14:19 2014 +0100 @@ -11,15 +11,13 @@ evaluation to weak head-normal form. *} options [document = false] - theories Wfd Fix + theories + Wfd + Fix -session "CCL-ex" in ex = CCL + - description {* - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge + (* Examples for Classical Computational Logic *) + "ex/Nat" + "ex/List" + "ex/Stream" + "ex/Flag" - Examples for Classical Computational Logic. - *} - options [document = false] - theories Nat List Stream Flag - diff -r 2f65dcd32a59 -r 51890cb80b30 src/CCL/Set.thy --- a/src/CCL/Set.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CCL/Set.thy Tue Nov 11 21:14:19 2014 +0100 @@ -10,74 +10,74 @@ instance set :: ("term") "term" .. consts - Collect :: "['a => o] => 'a set" (*comprehension*) - Compl :: "('a set) => 'a set" (*complement*) - Int :: "['a set, 'a set] => 'a set" (infixl "Int" 70) - Un :: "['a set, 'a set] => 'a set" (infixl "Un" 65) - Union :: "(('a set)set) => 'a set" (*...of a set*) - Inter :: "(('a set)set) => 'a set" (*...of a set*) - UNION :: "['a set, 'a => 'b set] => 'b set" (*general*) - INTER :: "['a set, 'a => 'b set] => 'b set" (*general*) - Ball :: "['a set, 'a => o] => o" (*bounded quants*) - Bex :: "['a set, 'a => o] => o" (*bounded quants*) - mono :: "['a set => 'b set] => o" (*monotonicity*) - mem :: "['a, 'a set] => o" (infixl ":" 50) (*membership*) - subset :: "['a set, 'a set] => o" (infixl "<=" 50) - singleton :: "'a => 'a set" ("{_}") + Collect :: "['a \ o] \ 'a set" (*comprehension*) + Compl :: "('a set) \ 'a set" (*complement*) + Int :: "['a set, 'a set] \ 'a set" (infixl "Int" 70) + Un :: "['a set, 'a set] \ 'a set" (infixl "Un" 65) + Union :: "(('a set)set) \ 'a set" (*...of a set*) + Inter :: "(('a set)set) \ 'a set" (*...of a set*) + UNION :: "['a set, 'a \ 'b set] \ 'b set" (*general*) + INTER :: "['a set, 'a \ 'b set] \ 'b set" (*general*) + Ball :: "['a set, 'a \ o] \ o" (*bounded quants*) + Bex :: "['a set, 'a \ o] \ o" (*bounded quants*) + mono :: "['a set \ 'b set] \ o" (*monotonicity*) + mem :: "['a, 'a set] \ o" (infixl ":" 50) (*membership*) + subset :: "['a set, 'a set] \ o" (infixl "<=" 50) + singleton :: "'a \ 'a set" ("{_}") empty :: "'a set" ("{}") syntax - "_Coll" :: "[idt, o] => 'a set" ("(1{_./ _})") (*collection*) + "_Coll" :: "[idt, o] \ 'a set" ("(1{_./ _})") (*collection*) (* Big Intersection / Union *) - "_INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(INT _:_./ _)" [0, 0, 0] 10) - "_UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(UN _:_./ _)" [0, 0, 0] 10) + "_INTER" :: "[idt, 'a set, 'b set] \ 'b set" ("(INT _:_./ _)" [0, 0, 0] 10) + "_UNION" :: "[idt, 'a set, 'b set] \ 'b set" ("(UN _:_./ _)" [0, 0, 0] 10) (* Bounded Quantifiers *) - "_Ball" :: "[idt, 'a set, o] => o" ("(ALL _:_./ _)" [0, 0, 0] 10) - "_Bex" :: "[idt, 'a set, o] => o" ("(EX _:_./ _)" [0, 0, 0] 10) + "_Ball" :: "[idt, 'a set, o] \ o" ("(ALL _:_./ _)" [0, 0, 0] 10) + "_Bex" :: "[idt, 'a set, o] \ o" ("(EX _:_./ _)" [0, 0, 0] 10) translations - "{x. P}" == "CONST Collect(%x. P)" - "INT x:A. B" == "CONST INTER(A, %x. B)" - "UN x:A. B" == "CONST UNION(A, %x. B)" - "ALL x:A. P" == "CONST Ball(A, %x. P)" - "EX x:A. P" == "CONST Bex(A, %x. P)" + "{x. P}" == "CONST Collect(\x. P)" + "INT x:A. B" == "CONST INTER(A, \x. B)" + "UN x:A. B" == "CONST UNION(A, \x. B)" + "ALL x:A. P" == "CONST Ball(A, \x. P)" + "EX x:A. P" == "CONST Bex(A, \x. P)" axiomatization where - mem_Collect_iff: "(a : {x. P(x)}) <-> P(a)" and - set_extension: "A = B <-> (ALL x. x:A <-> x:B)" + mem_Collect_iff: "(a : {x. P(x)}) \ P(a)" and + set_extension: "A = B \ (ALL x. x:A \ x:B)" defs - Ball_def: "Ball(A, P) == ALL x. x:A --> P(x)" - Bex_def: "Bex(A, P) == EX x. x:A & P(x)" - mono_def: "mono(f) == (ALL A B. A <= B --> f(A) <= f(B))" + Ball_def: "Ball(A, P) == ALL x. x:A \ P(x)" + Bex_def: "Bex(A, P) == EX x. x:A \ P(x)" + mono_def: "mono(f) == (ALL A B. A <= B \ f(A) <= f(B))" subset_def: "A <= B == ALL x:A. x:B" singleton_def: "{a} == {x. x=a}" empty_def: "{} == {x. False}" Un_def: "A Un B == {x. x:A | x:B}" - Int_def: "A Int B == {x. x:A & x:B}" - Compl_def: "Compl(A) == {x. ~x:A}" + Int_def: "A Int B == {x. x:A \ x:B}" + Compl_def: "Compl(A) == {x. \x:A}" INTER_def: "INTER(A, B) == {y. ALL x:A. y: B(x)}" UNION_def: "UNION(A, B) == {y. EX x:A. y: B(x)}" Inter_def: "Inter(S) == (INT x:S. x)" Union_def: "Union(S) == (UN x:S. x)" -lemma CollectI: "[| P(a) |] ==> a : {x. P(x)}" +lemma CollectI: "P(a) \ a : {x. P(x)}" apply (rule mem_Collect_iff [THEN iffD2]) apply assumption done -lemma CollectD: "[| a : {x. P(x)} |] ==> P(a)" +lemma CollectD: "a : {x. P(x)} \ P(a)" apply (erule mem_Collect_iff [THEN iffD1]) done lemmas CollectE = CollectD [elim_format] -lemma set_ext: "[| !!x. x:A <-> x:B |] ==> A = B" +lemma set_ext: "(\x. x:A \ x:B) \ A = B" apply (rule set_extension [THEN iffD2]) apply simp done @@ -85,80 +85,79 @@ subsection {* Bounded quantifiers *} -lemma ballI: "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)" +lemma ballI: "(\x. x:A \ P(x)) \ ALL x:A. P(x)" by (simp add: Ball_def) -lemma bspec: "[| ALL x:A. P(x); x:A |] ==> P(x)" +lemma bspec: "\ALL x:A. P(x); x:A\ \ P(x)" by (simp add: Ball_def) -lemma ballE: "[| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q" +lemma ballE: "\ALL x:A. P(x); P(x) \ Q; \ x:A \ Q\ \ Q" unfolding Ball_def by blast -lemma bexI: "[| P(x); x:A |] ==> EX x:A. P(x)" +lemma bexI: "\P(x); x:A\ \ EX x:A. P(x)" unfolding Bex_def by blast -lemma bexCI: "[| EX x:A. ~P(x) ==> P(a); a:A |] ==> EX x:A. P(x)" +lemma bexCI: "\EX x:A. \P(x) \ P(a); a:A\ \ EX x:A. P(x)" unfolding Bex_def by blast -lemma bexE: "[| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q" +lemma bexE: "\EX x:A. P(x); \x. \x:A; P(x)\ \ Q\ \ Q" unfolding Bex_def by blast (*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) -lemma ball_rew: "(ALL x:A. True) <-> True" +lemma ball_rew: "(ALL x:A. True) \ True" by (blast intro: ballI) subsection {* Congruence rules *} lemma ball_cong: - "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> - (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))" + "\A = A'; \x. x:A' \ P(x) \ P'(x)\ \ + (ALL x:A. P(x)) \ (ALL x:A'. P'(x))" by (blast intro: ballI elim: ballE) lemma bex_cong: - "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> - (EX x:A. P(x)) <-> (EX x:A'. P'(x))" + "\A = A'; \x. x:A' \ P(x) \ P'(x)\ \ + (EX x:A. P(x)) \ (EX x:A'. P'(x))" by (blast intro: bexI elim: bexE) subsection {* Rules for subsets *} -lemma subsetI: "(!!x. x:A ==> x:B) ==> A <= B" +lemma subsetI: "(\x. x:A \ x:B) \ A <= B" unfolding subset_def by (blast intro: ballI) (*Rule in Modus Ponens style*) -lemma subsetD: "[| A <= B; c:A |] ==> c:B" +lemma subsetD: "\A <= B; c:A\ \ c:B" unfolding subset_def by (blast elim: ballE) (*Classical elimination rule*) -lemma subsetCE: "[| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P" +lemma subsetCE: "\A <= B; \(c:A) \ P; c:B \ P\ \ P" by (blast dest: subsetD) lemma subset_refl: "A <= A" by (blast intro: subsetI) -lemma subset_trans: "[| A<=B; B<=C |] ==> A<=C" +lemma subset_trans: "\A <= B; B <= C\ \ A <= C" by (blast intro: subsetI dest: subsetD) subsection {* Rules for equality *} (*Anti-symmetry of the subset relation*) -lemma subset_antisym: "[| A <= B; B <= A |] ==> A = B" +lemma subset_antisym: "\A <= B; B <= A\ \ A = B" by (blast intro: set_ext dest: subsetD) lemmas equalityI = subset_antisym (* Equality rules from ZF set theory -- are they appropriate here? *) -lemma equalityD1: "A = B ==> A<=B" - and equalityD2: "A = B ==> B<=A" +lemma equalityD1: "A = B \ A<=B" + and equalityD2: "A = B \ B<=A" by (simp_all add: subset_refl) -lemma equalityE: "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P" +lemma equalityE: "\A = B; \A <= B; B <= A\ \ P\ \ P" by (simp add: subset_refl) -lemma equalityCE: - "[| A = B; [| c:A; c:B |] ==> P; [| ~ c:A; ~ c:B |] ==> P |] ==> P" +lemma equalityCE: "\A = B; \c:A; c:B\ \ P; \\ c:A; \ c:B\ \ P\ \ P" by (blast elim: equalityE subsetCE) lemma trivial_set: "{x. x:A} = A" @@ -167,40 +166,40 @@ subsection {* Rules for binary union *} -lemma UnI1: "c:A ==> c : A Un B" - and UnI2: "c:B ==> c : A Un B" +lemma UnI1: "c:A \ c : A Un B" + and UnI2: "c:B \ c : A Un B" unfolding Un_def by (blast intro: CollectI)+ (*Classical introduction rule: no commitment to A vs B*) -lemma UnCI: "(~c:B ==> c:A) ==> c : A Un B" +lemma UnCI: "(\c:B \ c:A) \ c : A Un B" by (blast intro: UnI1 UnI2) -lemma UnE: "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P" +lemma UnE: "\c : A Un B; c:A \ P; c:B \ P\ \ P" unfolding Un_def by (blast dest: CollectD) subsection {* Rules for small intersection *} -lemma IntI: "[| c:A; c:B |] ==> c : A Int B" +lemma IntI: "\c:A; c:B\ \ c : A Int B" unfolding Int_def by (blast intro: CollectI) -lemma IntD1: "c : A Int B ==> c:A" - and IntD2: "c : A Int B ==> c:B" +lemma IntD1: "c : A Int B \ c:A" + and IntD2: "c : A Int B \ c:B" unfolding Int_def by (blast dest: CollectD)+ -lemma IntE: "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P" +lemma IntE: "\c : A Int B; \c:A; c:B\ \ P\ \ P" by (blast dest: IntD1 IntD2) subsection {* Rules for set complement *} -lemma ComplI: "[| c:A ==> False |] ==> c : Compl(A)" +lemma ComplI: "(c:A \ False) \ c : Compl(A)" unfolding Compl_def by (blast intro: CollectI) (*This form, with negated conclusion, works well with the Classical prover. Negated assumptions behave like formulae on the right side of the notional turnstile...*) -lemma ComplD: "[| c : Compl(A) |] ==> ~c:A" +lemma ComplD: "c : Compl(A) \ \c:A" unfolding Compl_def by (blast dest: CollectD) lemmas ComplE = ComplD [elim_format] @@ -211,13 +210,13 @@ lemma empty_eq: "{x. False} = {}" by (simp add: empty_def) -lemma emptyD: "a : {} ==> P" +lemma emptyD: "a : {} \ P" unfolding empty_def by (blast dest: CollectD) lemmas emptyE = emptyD [elim_format] lemma not_emptyD: - assumes "~ A={}" + assumes "\ A={}" shows "EX x. x:A" proof - have "\ (EX x. x:A) \ A = {}" @@ -231,7 +230,7 @@ lemma singletonI: "a : {a}" unfolding singleton_def by (blast intro: CollectI) -lemma singletonD: "b : {a} ==> b=a" +lemma singletonD: "b : {a} \ b=a" unfolding singleton_def by (blast dest: CollectD) lemmas singletonE = singletonD [elim_format] @@ -240,58 +239,54 @@ subsection {* Unions of families *} (*The order of the premises presupposes that A is rigid; b may be flexible*) -lemma UN_I: "[| a:A; b: B(a) |] ==> b: (UN x:A. B(x))" +lemma UN_I: "\a:A; b: B(a)\ \ b: (UN x:A. B(x))" unfolding UNION_def by (blast intro: bexI CollectI) -lemma UN_E: "[| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R" +lemma UN_E: "\b : (UN x:A. B(x)); \x. \x:A; b: B(x)\ \ R\ \ R" unfolding UNION_def by (blast dest: CollectD elim: bexE) -lemma UN_cong: - "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> - (UN x:A. C(x)) = (UN x:B. D(x))" +lemma UN_cong: "\A = B; \x. x:B \ C(x) = D(x)\ \ (UN x:A. C(x)) = (UN x:B. D(x))" by (simp add: UNION_def cong: bex_cong) subsection {* Intersections of families *} -lemma INT_I: "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))" +lemma INT_I: "(\x. x:A \ b: B(x)) \ b : (INT x:A. B(x))" unfolding INTER_def by (blast intro: CollectI ballI) -lemma INT_D: "[| b : (INT x:A. B(x)); a:A |] ==> b: B(a)" +lemma INT_D: "\b : (INT x:A. B(x)); a:A\ \ b: B(a)" unfolding INTER_def by (blast dest: CollectD bspec) (*"Classical" elimination rule -- does not require proving X:C *) -lemma INT_E: "[| b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R" +lemma INT_E: "\b : (INT x:A. B(x)); b: B(a) \ R; \ a:A \ R\ \ R" unfolding INTER_def by (blast dest: CollectD bspec) -lemma INT_cong: - "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> - (INT x:A. C(x)) = (INT x:B. D(x))" +lemma INT_cong: "\A = B; \x. x:B \ C(x) = D(x)\ \ (INT x:A. C(x)) = (INT x:B. D(x))" by (simp add: INTER_def cong: ball_cong) subsection {* Rules for Unions *} (*The order of the premises presupposes that C is rigid; A may be flexible*) -lemma UnionI: "[| X:C; A:X |] ==> A : Union(C)" +lemma UnionI: "\X:C; A:X\ \ A : Union(C)" unfolding Union_def by (blast intro: UN_I) -lemma UnionE: "[| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R" +lemma UnionE: "\A : Union(C); \X. \ A:X; X:C\ \ R\ \ R" unfolding Union_def by (blast elim: UN_E) subsection {* Rules for Inter *} -lemma InterI: "[| !!X. X:C ==> A:X |] ==> A : Inter(C)" +lemma InterI: "(\X. X:C \ A:X) \ A : Inter(C)" unfolding Inter_def by (blast intro: INT_I) (*A "destruct" rule -- every X in C contains A as an element, but A:X can hold when X:C does not! This rule is analogous to "spec". *) -lemma InterD: "[| A : Inter(C); X:C |] ==> A:X" +lemma InterD: "\A : Inter(C); X:C\ \ A:X" unfolding Inter_def by (blast dest: INT_D) (*"Classical" elimination rule -- does not require proving X:C *) -lemma InterE: "[| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R" +lemma InterE: "\A : Inter(C); A:X \ R; \ X:C \ R\ \ R" unfolding Inter_def by (blast elim: INT_E) @@ -299,19 +294,19 @@ subsection {* Big Union -- least upper bound of a set *} -lemma Union_upper: "B:A ==> B <= Union(A)" +lemma Union_upper: "B:A \ B <= Union(A)" by (blast intro: subsetI UnionI) -lemma Union_least: "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C" +lemma Union_least: "(\X. X:A \ X<=C) \ Union(A) <= C" by (blast intro: subsetI dest: subsetD elim: UnionE) subsection {* Big Intersection -- greatest lower bound of a set *} -lemma Inter_lower: "B:A ==> Inter(A) <= B" +lemma Inter_lower: "B:A \ Inter(A) <= B" by (blast intro: subsetI dest: InterD) -lemma Inter_greatest: "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)" +lemma Inter_greatest: "(\X. X:A \ C<=X) \ C <= Inter(A)" by (blast intro: subsetI InterI dest: subsetD) @@ -323,7 +318,7 @@ lemma Un_upper2: "B <= A Un B" by (blast intro: subsetI UnI2) -lemma Un_least: "[| A<=C; B<=C |] ==> A Un B <= C" +lemma Un_least: "\A<=C; B<=C\ \ A Un B <= C" by (blast intro: subsetI elim: UnE dest: subsetD) @@ -335,22 +330,22 @@ lemma Int_lower2: "A Int B <= B" by (blast intro: subsetI elim: IntE) -lemma Int_greatest: "[| C<=A; C<=B |] ==> C <= A Int B" +lemma Int_greatest: "\C<=A; C<=B\ \ C <= A Int B" by (blast intro: subsetI IntI dest: subsetD) subsection {* Monotonicity *} -lemma monoI: "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)" +lemma monoI: "(\A B. A <= B \ f(A) <= f(B)) \ mono(f)" unfolding mono_def by blast -lemma monoD: "[| mono(f); A <= B |] ==> f(A) <= f(B)" +lemma monoD: "\mono(f); A <= B\ \ f(A) <= f(B)" unfolding mono_def by blast -lemma mono_Un: "mono(f) ==> f(A) Un f(B) <= f(A Un B)" +lemma mono_Un: "mono(f) \ f(A) Un f(B) <= f(A Un B)" by (blast intro: Un_least dest: monoD intro: Un_upper1 Un_upper2) -lemma mono_Int: "mono(f) ==> f(A Int B) <= f(A) Int f(B)" +lemma mono_Int: "mono(f) \ f(A Int B) <= f(A) Int f(B)" by (blast intro: Int_greatest dest: monoD intro: Int_lower1 Int_lower2) @@ -362,12 +357,12 @@ and [elim] = ballE InterD InterE INT_D INT_E subsetD subsetCE lemma mem_rews: - "(a : A Un B) <-> (a:A | a:B)" - "(a : A Int B) <-> (a:A & a:B)" - "(a : Compl(B)) <-> (~a:B)" - "(a : {b}) <-> (a=b)" - "(a : {}) <-> False" - "(a : {x. P(x)}) <-> P(a)" + "(a : A Un B) \ (a:A | a:B)" + "(a : A Int B) \ (a:A \ a:B)" + "(a : Compl(B)) \ (\a:B)" + "(a : {b}) \ (a=b)" + "(a : {}) \ False" + "(a : {x. P(x)}) \ P(a)" by blast+ lemmas [simp] = trivial_set empty_eq mem_rews @@ -390,7 +385,7 @@ lemma Int_Un_distrib: "(A Un B) Int C = (A Int C) Un (B Int C)" by (blast intro: equalityI) -lemma subset_Int_eq: "(A<=B) <-> (A Int B = A)" +lemma subset_Int_eq: "(A<=B) \ (A Int B = A)" by (blast intro: equalityI elim: equalityE) @@ -412,7 +407,7 @@ "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)" by (blast intro: equalityI) -lemma subset_Un_eq: "(A<=B) <-> (A Un B = B)" +lemma subset_Un_eq: "(A<=B) \ (A Un B = B)" by (blast intro: equalityI elim: equalityE) @@ -440,7 +435,7 @@ by (blast intro: equalityI) (*Halmos, Naive Set Theory, page 16.*) -lemma Un_Int_assoc_eq: "((A Int B) Un C = A Int (B Un C)) <-> (C<=A)" +lemma Un_Int_assoc_eq: "((A Int B) Un C = A Int (B Un C)) \ (C<=A)" by (blast intro: equalityI elim: equalityE) @@ -450,7 +445,7 @@ by (blast intro: equalityI) lemma Union_disjoint: - "(Union(C) Int A = {x. False}) <-> (ALL B:C. B Int A = {x. False})" + "(Union(C) Int A = {x. False}) \ (ALL B:C. B Int A = {x. False})" by (blast intro: equalityI elim: equalityE) lemma Inter_Un_distrib: "Inter(A Un B) = Inter(A) Int Inter(B)" @@ -475,29 +470,25 @@ section {* Monotonicity of various operations *} -lemma Union_mono: "A<=B ==> Union(A) <= Union(B)" +lemma Union_mono: "A<=B \ Union(A) <= Union(B)" by blast -lemma Inter_anti_mono: "[| B<=A |] ==> Inter(A) <= Inter(B)" +lemma Inter_anti_mono: "B <= A \ Inter(A) <= Inter(B)" by blast -lemma UN_mono: - "[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> - (UN x:A. f(x)) <= (UN x:B. g(x))" +lemma UN_mono: "\A <= B; \x. x:A \ f(x)<=g(x)\ \ (UN x:A. f(x)) <= (UN x:B. g(x))" by blast -lemma INT_anti_mono: - "[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> - (INT x:A. f(x)) <= (INT x:A. g(x))" +lemma INT_anti_mono: "\B <= A; \x. x:A \ f(x) <= g(x)\ \ (INT x:A. f(x)) <= (INT x:A. g(x))" by blast -lemma Un_mono: "[| A<=C; B<=D |] ==> A Un B <= C Un D" +lemma Un_mono: "\A <= C; B <= D\ \ A Un B <= C Un D" by blast -lemma Int_mono: "[| A<=C; B<=D |] ==> A Int B <= C Int D" +lemma Int_mono: "\A <= C; B <= D\ \ A Int B <= C Int D" by blast -lemma Compl_anti_mono: "[| A<=B |] ==> Compl(B) <= Compl(A)" +lemma Compl_anti_mono: "A <= B \ Compl(B) <= Compl(A)" by blast end diff -r 2f65dcd32a59 -r 51890cb80b30 src/CCL/Term.thy --- a/src/CCL/Term.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CCL/Term.thy Tue Nov 11 21:14:19 2014 +0100 @@ -13,43 +13,43 @@ one :: "i" - "if" :: "[i,i,i]=>i" ("(3if _/ then _/ else _)" [0,0,60] 60) + "if" :: "[i,i,i]\i" ("(3if _/ then _/ else _)" [0,0,60] 60) - inl :: "i=>i" - inr :: "i=>i" - when :: "[i,i=>i,i=>i]=>i" + inl :: "i\i" + inr :: "i\i" + when :: "[i,i\i,i\i]\i" - split :: "[i,[i,i]=>i]=>i" - fst :: "i=>i" - snd :: "i=>i" - thd :: "i=>i" + split :: "[i,[i,i]\i]\i" + fst :: "i\i" + snd :: "i\i" + thd :: "i\i" zero :: "i" - succ :: "i=>i" - ncase :: "[i,i,i=>i]=>i" - nrec :: "[i,i,[i,i]=>i]=>i" + succ :: "i\i" + ncase :: "[i,i,i\i]\i" + nrec :: "[i,i,[i,i]\i]\i" nil :: "i" ("([])") - cons :: "[i,i]=>i" (infixr "$" 80) - lcase :: "[i,i,[i,i]=>i]=>i" - lrec :: "[i,i,[i,i,i]=>i]=>i" + cons :: "[i,i]\i" (infixr "$" 80) + lcase :: "[i,i,[i,i]\i]\i" + lrec :: "[i,i,[i,i,i]\i]\i" - "let" :: "[i,i=>i]=>i" - letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i" - letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i" - letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" + "let" :: "[i,i\i]\i" + letrec :: "[[i,i\i]\i,(i\i)\i]\i" + letrec2 :: "[[i,i,i\i\i]\i,(i\i\i)\i]\i" + letrec3 :: "[[i,i,i,i\i\i\i]\i,(i\i\i\i)\i]\i" syntax - "_let" :: "[id,i,i]=>i" ("(3let _ be _/ in _)" + "_let" :: "[id,i,i]\i" ("(3let _ be _/ in _)" [0,0,60] 60) - "_letrec" :: "[id,id,i,i]=>i" ("(3letrec _ _ be _/ in _)" + "_letrec" :: "[id,id,i,i]\i" ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60) - "_letrec2" :: "[id,id,id,i,i]=>i" ("(3letrec _ _ _ be _/ in _)" + "_letrec2" :: "[id,id,id,i,i]\i" ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60) - "_letrec3" :: "[id,id,id,id,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" + "_letrec3" :: "[id,id,id,id,i,i]\i" ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60) ML {* @@ -91,7 +91,6 @@ val (x',a') = Syntax_Trans.variant_abs(x,T,a3) in Const(@{syntax_const "_letrec3"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b' end; - *} parse_translation {* @@ -109,40 +108,40 @@ *} consts - napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56) + napply :: "[i\i,i,i]\i" ("(_ ^ _ ` _)" [56,56,56] 56) defs one_def: "one == true" - if_def: "if b then t else u == case(b,t,u,% x y. bot,%v. bot)" + if_def: "if b then t else u == case(b, t, u, \ x y. bot, \v. bot)" inl_def: "inl(a) == " inr_def: "inr(b) == " - when_def: "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))" - split_def: "split(t,f) == case(t,bot,bot,f,%u. bot)" - fst_def: "fst(t) == split(t,%x y. x)" - snd_def: "snd(t) == split(t,%x y. y)" - thd_def: "thd(t) == split(t,%x p. split(p,%y z. z))" + when_def: "when(t,f,g) == split(t, \b x. if b then f(x) else g(x))" + split_def: "split(t,f) == case(t, bot, bot, f, \u. bot)" + fst_def: "fst(t) == split(t, \x y. x)" + snd_def: "snd(t) == split(t, \x y. y)" + thd_def: "thd(t) == split(t, \x p. split(p, \y z. z))" zero_def: "zero == inl(one)" succ_def: "succ(n) == inr(n)" - ncase_def: "ncase(n,b,c) == when(n,%x. b,%y. c(y))" - nrec_def: " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)" + ncase_def: "ncase(n,b,c) == when(n, \x. b, \y. c(y))" + nrec_def: " nrec(n,b,c) == letrec g x be ncase(x, b, \y. c(y,g(y))) in g(n)" nil_def: "[] == inl(one)" cons_def: "h$t == inr()" - lcase_def: "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))" - lrec_def: "lrec(l,b,c) == letrec g x be lcase(x,b,%h t. c(h,t,g(t))) in g(l)" + lcase_def: "lcase(l,b,c) == when(l, \x. b, \y. split(y,c))" + lrec_def: "lrec(l,b,c) == letrec g x be lcase(x, b, \h t. c(h,t,g(t))) in g(l)" - let_def: "let x be t in f(x) == case(t,f(true),f(false),%x y. f(),%u. f(lam x. u(x)))" + let_def: "let x be t in f(x) == case(t,f(true),f(false), \x y. f(), \u. f(lam x. u(x)))" letrec_def: - "letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)" + "letrec g x be h(x,g) in b(g) == b(\x. fix(\f. lam x. h(x,\y. f`y))`x)" letrec2_def: "letrec g x y be h(x,y,g) in f(g)== - letrec g' p be split(p,%x y. h(x,y,%u v. g'())) - in f(%x y. g'())" + letrec g' p be split(p,\x y. h(x,y,\u v. g'())) + in f(\x y. g'())" letrec3_def: "letrec g x y z be h(x,y,z,g) in f(g) == - letrec g' p be split(p,%x xs. split(xs,%y z. h(x,y,z,%u v w. g'(>)))) - in f(%x y z. g'(>))" + letrec g' p be split(p,\x xs. split(xs,\y z. h(x,y,z,\u v w. g'(>)))) + in f(\x y z. g'(>))" - napply_def: "f ^n` a == nrec(n,a,%x g. f(g))" + napply_def: "f ^n` a == nrec(n,a,\x g. f(g))" lemmas simp_can_defs = one_def inl_def inr_def @@ -159,7 +158,7 @@ subsection {* Beta Rules, including strictness *} -lemma letB: "~ t=bot ==> let x be t in f(x) = f(t)" +lemma letB: "\ t=bot \ let x be t in f(x) = f(t)" apply (unfold let_def) apply (erule rev_mp) apply (rule_tac t = "t" in term_case) @@ -194,7 +193,7 @@ done lemma letrecB: - "letrec g x be h(x,g) in g(a) = h(a,%y. letrec g x be h(x,g) in g(y))" + "letrec g x be h(x,g) in g(a) = h(a,\y. letrec g x be h(x,g) in g(y))" apply (unfold letrec_def) apply (rule fixB [THEN ssubst], rule applyB [THEN ssubst], rule refl) done @@ -254,12 +253,12 @@ unfolding data_defs by beta_rl+ lemma letrec2B: - "letrec g x y be h(x,y,g) in g(p,q) = h(p,q,%u v. letrec g x y be h(x,y,g) in g(u,v))" + "letrec g x y be h(x,y,g) in g(p,q) = h(p,q,\u v. letrec g x y be h(x,y,g) in g(u,v))" unfolding data_defs letrec2_def by beta_rl+ lemma letrec3B: "letrec g x y z be h(x,y,z,g) in g(p,q,r) = - h(p,q,r,%u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))" + h(p,q,r,\u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))" unfolding data_defs letrec3_def by beta_rl+ lemma napplyBzero: "f^zero`a = a" @@ -276,10 +275,10 @@ subsection {* Constructors are injective *} lemma term_injs: - "(inl(a) = inl(a')) <-> (a=a')" - "(inr(a) = inr(a')) <-> (a=a')" - "(succ(a) = succ(a')) <-> (a=a')" - "(a$b = a'$b') <-> (a=a' & b=b')" + "(inl(a) = inl(a')) \ (a=a')" + "(inr(a) = inr(a')) \ (a=a')" + "(succ(a) = succ(a')) \ (a=a')" + "(a$b = a'$b') \ (a=a' \ b=b')" by (inj_rl applyB splitB whenBinl whenBinr ncaseBsucc lcaseBcons) @@ -295,10 +294,10 @@ subsection {* Rules for pre-order @{text "[="} *} lemma term_porews: - "inl(a) [= inl(a') <-> a [= a'" - "inr(b) [= inr(b') <-> b [= b'" - "succ(n) [= succ(n') <-> n [= n'" - "x$xs [= x'$xs' <-> x [= x' & xs [= xs'" + "inl(a) [= inl(a') \ a [= a'" + "inr(b) [= inr(b') \ b [= b'" + "succ(n) [= succ(n') \ n [= n'" + "x$xs [= x'$xs' \ x [= x' \ xs [= xs'" by (simp_all add: data_defs ccl_porews) diff -r 2f65dcd32a59 -r 51890cb80b30 src/CCL/Trancl.thy --- a/src/CCL/Trancl.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CCL/Trancl.thy Tue Nov 11 21:14:19 2014 +0100 @@ -9,29 +9,28 @@ imports CCL begin -definition trans :: "i set => o" (*transitivity predicate*) - where "trans(r) == (ALL x y z. :r --> :r --> :r)" +definition trans :: "i set \ o" (*transitivity predicate*) + where "trans(r) == (ALL x y z. :r \ :r \ :r)" definition id :: "i set" (*the identity relation*) where "id == {p. EX x. p = }" -definition relcomp :: "[i set,i set] => i set" (infixr "O" 60) (*composition of relations*) - where "r O s == {xz. EX x y z. xz = & :s & :r}" +definition relcomp :: "[i set,i set] \ i set" (infixr "O" 60) (*composition of relations*) + where "r O s == {xz. EX x y z. xz = \ :s \ :r}" -definition rtrancl :: "i set => i set" ("(_^*)" [100] 100) - where "r^* == lfp(%s. id Un (r O s))" +definition rtrancl :: "i set \ i set" ("(_^*)" [100] 100) + where "r^* == lfp(\s. id Un (r O s))" -definition trancl :: "i set => i set" ("(_^+)" [100] 100) +definition trancl :: "i set \ i set" ("(_^+)" [100] 100) where "r^+ == r O rtrancl(r)" subsection {* Natural deduction for @{text "trans(r)"} *} -lemma transI: - "(!! x y z. [| :r; :r |] ==> :r) ==> trans(r)" +lemma transI: "(\x y z. \:r; :r\ \ :r) \ trans(r)" unfolding trans_def by blast -lemma transD: "[| trans(r); :r; :r |] ==> :r" +lemma transD: "\trans(r); :r; :r\ \ :r" unfolding trans_def by blast @@ -44,8 +43,7 @@ apply (rule refl) done -lemma idE: - "[| p: id; !!x.[| p = |] ==> P |] ==> P" +lemma idE: "\p: id; \x. p = \ P\ \ P" apply (unfold id_def) apply (erule CollectE) apply blast @@ -54,20 +52,14 @@ subsection {* Composition of two relations *} -lemma compI: "[| :s; :r |] ==> : r O s" +lemma compI: "\:s; :r\ \ : r O s" unfolding relcomp_def by blast (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*) -lemma compE: - "[| xz : r O s; - !!x y z. [| xz = ; :s; :r |] ==> P - |] ==> P" +lemma compE: "\xz : r O s; \x y z. \xz = ; :s; :r\ \ P\ \ P" unfolding relcomp_def by blast -lemma compEpair: - "[| : r O s; - !!y. [| :s; :r |] ==> P - |] ==> P" +lemma compEpair: "\ : r O s; \y. \:s; :r\ \ P\ \ P" apply (erule compE) apply (simp add: pair_inject) done @@ -76,13 +68,13 @@ and [elim] = compE idE and [elim!] = pair_inject -lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)" +lemma comp_mono: "\r'<=r; s'<=s\ \ (r' O s') <= (r O s)" by blast subsection {* The relation rtrancl *} -lemma rtrancl_fun_mono: "mono(%s. id Un (r O s))" +lemma rtrancl_fun_mono: "mono(\s. id Un (r O s))" apply (rule monoI) apply (rule monoI subset_refl comp_mono Un_mono)+ apply assumption @@ -98,13 +90,13 @@ done (*Closure under composition with r*) -lemma rtrancl_into_rtrancl: "[| : r^*; : r |] ==> : r^*" +lemma rtrancl_into_rtrancl: "\ : r^*; : r\ \ : r^*" apply (subst rtrancl_unfold) apply blast done (*rtrancl of r contains r*) -lemma r_into_rtrancl: "[| : r |] ==> : r^*" +lemma r_into_rtrancl: " : r \ : r^*" apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl]) apply assumption done @@ -113,10 +105,10 @@ subsection {* standard induction rule *} lemma rtrancl_full_induct: - "[| : r^*; - !!x. P(); - !!x y z.[| P(); : r^*; : r |] ==> P() |] - ==> P()" + "\ : r^*; + \x. P(); + \x y z. \P(); : r^*; : r\ \ P()\ + \ P()" apply (erule def_induct [OF rtrancl_def]) apply (rule rtrancl_fun_mono) apply blast @@ -124,12 +116,12 @@ (*nice induction rule*) lemma rtrancl_induct: - "[| : r^*; + "\ : r^*; P(a); - !!y z.[| : r^*; : r; P(y) |] ==> P(z) |] - ==> P(b)" + \y z. \ : r^*; : r; P(y)\ \ P(z) \ + \ P(b)" (*by induction on this formula*) - apply (subgoal_tac "ALL y. = --> P(y)") + apply (subgoal_tac "ALL y. = \ P(y)") (*now solve first subgoal: this formula is sufficient*) apply blast (*now do the induction*) @@ -147,10 +139,8 @@ (*elimination of rtrancl -- by induction on a special formula*) lemma rtranclE: - "[| : r^*; (a = b) ==> P; - !!y.[| : r^*; : r |] ==> P |] - ==> P" - apply (subgoal_tac "a = b | (EX y. : r^* & : r)") + "\ : r^*; a = b \ P; \y. \ : r^*; : r\ \ P\ \ P" + apply (subgoal_tac "a = b | (EX y. : r^* \ : r)") prefer 2 apply (erule rtrancl_induct) apply blast @@ -163,7 +153,7 @@ subsubsection {* Conversions between trancl and rtrancl *} -lemma trancl_into_rtrancl: "[| : r^+ |] ==> : r^*" +lemma trancl_into_rtrancl: " : r^+ \ : r^*" apply (unfold trancl_def) apply (erule compEpair) apply (erule rtrancl_into_rtrancl) @@ -171,15 +161,15 @@ done (*r^+ contains r*) -lemma r_into_trancl: "[| : r |] ==> : r^+" +lemma r_into_trancl: " : r \ : r^+" unfolding trancl_def by (blast intro: rtrancl_refl) (*intro rule by definition: from rtrancl and r*) -lemma rtrancl_into_trancl1: "[| : r^*; : r |] ==> : r^+" +lemma rtrancl_into_trancl1: "\ : r^*; : r\ \ : r^+" unfolding trancl_def by blast (*intro rule from r and rtrancl*) -lemma rtrancl_into_trancl2: "[| : r; : r^* |] ==> : r^+" +lemma rtrancl_into_trancl2: "\ : r; : r^*\ \ : r^+" apply (erule rtranclE) apply (erule subst) apply (erule r_into_trancl) @@ -189,11 +179,10 @@ (*elimination of r^+ -- NOT an induction rule*) lemma tranclE: - "[| : r^+; - : r ==> P; - !!y.[| : r^+; : r |] ==> P - |] ==> P" - apply (subgoal_tac " : r | (EX y. : r^+ & : r)") + "\ : r^+; + : r \ P; + \y. \ : r^+; : r\ \ P\ \ P" + apply (subgoal_tac " : r | (EX y. : r^+ \ : r)") apply blast apply (unfold trancl_def) apply (erule compEpair) @@ -212,7 +201,7 @@ apply assumption+ done -lemma trancl_into_trancl2: "[| : r; : r^+ |] ==> : r^+" +lemma trancl_into_trancl2: "\ : r; : r^+\ \ : r^+" apply (rule r_into_trancl [THEN trans_trancl [THEN transD]]) apply assumption+ done diff -r 2f65dcd32a59 -r 51890cb80b30 src/CCL/Type.thy --- a/src/CCL/Type.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CCL/Type.thy Tue Nov 11 21:14:19 2014 +0100 @@ -11,39 +11,39 @@ consts - Subtype :: "['a set, 'a => o] => 'a set" + Subtype :: "['a set, 'a \ o] \ 'a set" Bool :: "i set" Unit :: "i set" - Plus :: "[i set, i set] => i set" (infixr "+" 55) - Pi :: "[i set, i => i set] => i set" - Sigma :: "[i set, i => i set] => i set" + Plus :: "[i set, i set] \ i set" (infixr "+" 55) + Pi :: "[i set, i \ i set] \ i set" + Sigma :: "[i set, i \ i set] \ i set" Nat :: "i set" - List :: "i set => i set" - Lists :: "i set => i set" - ILists :: "i set => i set" - TAll :: "(i set => i set) => i set" (binder "TALL " 55) - TEx :: "(i set => i set) => i set" (binder "TEX " 55) - Lift :: "i set => i set" ("(3[_])") + List :: "i set \ i set" + Lists :: "i set \ i set" + ILists :: "i set \ i set" + TAll :: "(i set \ i set) \ i set" (binder "TALL " 55) + TEx :: "(i set \ i set) \ i set" (binder "TEX " 55) + Lift :: "i set \ i set" ("(3[_])") - SPLIT :: "[i, [i, i] => i set] => i set" + SPLIT :: "[i, [i, i] \ i set] \ i set" syntax - "_Pi" :: "[idt, i set, i set] => i set" ("(3PROD _:_./ _)" + "_Pi" :: "[idt, i set, i set] \ i set" ("(3PROD _:_./ _)" [0,0,60] 60) - "_Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)" + "_Sigma" :: "[idt, i set, i set] \ i set" ("(3SUM _:_./ _)" [0,0,60] 60) - "_arrow" :: "[i set, i set] => i set" ("(_ ->/ _)" [54, 53] 53) - "_star" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55) - "_Subtype" :: "[idt, 'a set, o] => 'a set" ("(1{_: _ ./ _})") + "_arrow" :: "[i set, i set] \ i set" ("(_ ->/ _)" [54, 53] 53) + "_star" :: "[i set, i set] \ i set" ("(_ */ _)" [56, 55] 55) + "_Subtype" :: "[idt, 'a set, o] \ 'a set" ("(1{_: _ ./ _})") translations - "PROD x:A. B" => "CONST Pi(A, %x. B)" - "A -> B" => "CONST Pi(A, %_. B)" - "SUM x:A. B" => "CONST Sigma(A, %x. B)" - "A * B" => "CONST Sigma(A, %_. B)" - "{x: A. B}" == "CONST Subtype(A, %x. B)" + "PROD x:A. B" => "CONST Pi(A, \x. B)" + "A -> B" => "CONST Pi(A, \_. B)" + "SUM x:A. B" => "CONST Sigma(A, \x. B)" + "A * B" => "CONST Sigma(A, \_. B)" + "{x: A. B}" == "CONST Subtype(A, \x. B)" print_translation {* [(@{const_syntax Pi}, @@ -53,23 +53,23 @@ *} defs - Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}" + Subtype_def: "{x:A. P(x)} == {x. x:A \ P(x)}" Unit_def: "Unit == {x. x=one}" Bool_def: "Bool == {x. x=true | x=false}" Plus_def: "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}" - Pi_def: "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}" + Pi_def: "Pi(A,B) == {x. EX b. x=lam x. b(x) \ (ALL x:A. b(x):B(x))}" Sigma_def: "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=}" - Nat_def: "Nat == lfp(% X. Unit + X)" - List_def: "List(A) == lfp(% X. Unit + A*X)" + Nat_def: "Nat == lfp(\X. Unit + X)" + List_def: "List(A) == lfp(\X. Unit + A*X)" - Lists_def: "Lists(A) == gfp(% X. Unit + A*X)" - ILists_def: "ILists(A) == gfp(% X.{} + A*X)" + Lists_def: "Lists(A) == gfp(\X. Unit + A*X)" + ILists_def: "ILists(A) == gfp(\X.{} + A*X)" Tall_def: "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})" Tex_def: "TEX X. B(X) == Union({X. EX Y. X=B(Y)})" Lift_def: "[A] == A Un {bot}" - SPLIT_def: "SPLIT(p,B) == Union({A. EX x y. p= & A=B(x,y)})" + SPLIT_def: "SPLIT(p,B) == Union({A. EX x y. p= \ A=B(x,y)})" lemmas simp_type_defs = @@ -78,31 +78,29 @@ and simp_data_defs = one_def inl_def inr_def and ind_data_defs = zero_def succ_def nil_def cons_def -lemma subsetXH: "A <= B <-> (ALL x. x:A --> x:B)" +lemma subsetXH: "A <= B \ (ALL x. x:A \ x:B)" by blast subsection {* Exhaustion Rules *} -lemma EmptyXH: "!!a. a : {} <-> False" - and SubtypeXH: "!!a A P. a : {x:A. P(x)} <-> (a:A & P(a))" - and UnitXH: "!!a. a : Unit <-> a=one" - and BoolXH: "!!a. a : Bool <-> a=true | a=false" - and PlusXH: "!!a A B. a : A+B <-> (EX x:A. a=inl(x)) | (EX x:B. a=inr(x))" - and PiXH: "!!a A B. a : PROD x:A. B(x) <-> (EX b. a=lam x. b(x) & (ALL x:A. b(x):B(x)))" - and SgXH: "!!a A B. a : SUM x:A. B(x) <-> (EX x:A. EX y:B(x).a=)" +lemma EmptyXH: "\a. a : {} \ False" + and SubtypeXH: "\a A P. a : {x:A. P(x)} \ (a:A \ P(a))" + and UnitXH: "\a. a : Unit \ a=one" + and BoolXH: "\a. a : Bool \ a=true | a=false" + and PlusXH: "\a A B. a : A+B \ (EX x:A. a=inl(x)) | (EX x:B. a=inr(x))" + and PiXH: "\a A B. a : PROD x:A. B(x) \ (EX b. a=lam x. b(x) \ (ALL x:A. b(x):B(x)))" + and SgXH: "\a A B. a : SUM x:A. B(x) \ (EX x:A. EX y:B(x).a=)" unfolding simp_type_defs by blast+ lemmas XHs = EmptyXH SubtypeXH UnitXH BoolXH PlusXH PiXH SgXH -lemma LiftXH: "a : [A] <-> (a=bot | a:A)" - and TallXH: "a : TALL X. B(X) <-> (ALL X. a:B(X))" - and TexXH: "a : TEX X. B(X) <-> (EX X. a:B(X))" +lemma LiftXH: "a : [A] \ (a=bot | a:A)" + and TallXH: "a : TALL X. B(X) \ (ALL X. a:B(X))" + and TexXH: "a : TEX X. B(X) \ (EX X. a:B(X))" unfolding simp_type_defs by blast+ -ML {* -ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs}); -*} +ML {* ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs}) *} subsection {* Canonical Type Rules *} @@ -110,10 +108,10 @@ lemma oneT: "one : Unit" and trueT: "true : Bool" and falseT: "false : Bool" - and lamT: "!!b B. [| !!x. x:A ==> b(x):B(x) |] ==> lam x. b(x) : Pi(A,B)" - and pairT: "!!b B. [| a:A; b:B(a) |] ==> :Sigma(A,B)" - and inlT: "a:A ==> inl(a) : A+B" - and inrT: "b:B ==> inr(b) : A+B" + and lamT: "\b B. (\x. x:A \ b(x):B(x)) \ lam x. b(x) : Pi(A,B)" + and pairT: "\b B. \a:A; b:B(a)\ \ :Sigma(A,B)" + and inlT: "a:A \ inl(a) : A+B" + and inrT: "b:B \ inr(b) : A+B" by (blast intro: XHs [THEN iffD2])+ lemmas canTs = oneT trueT falseT pairT lamT inlT inrT @@ -121,7 +119,7 @@ subsection {* Non-Canonical Type Rules *} -lemma lem: "[| a:B(u); u=v |] ==> a : B(v)" +lemma lem: "\a:B(u); u = v\ \ a : B(v)" by blast @@ -139,22 +137,19 @@ Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms case_rls} @{thms case_rls}) *} -lemma ifT: - "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==> - if b then t else u : A(b)" +lemma ifT: "\b:Bool; b=true \ t:A(true); b=false \ u:A(false)\ \ if b then t else u : A(b)" by ncanT -lemma applyT: "[| f : Pi(A,B); a:A |] ==> f ` a : B(a)" +lemma applyT: "\f : Pi(A,B); a:A\ \ f ` a : B(a)" by ncanT -lemma splitT: - "[| p:Sigma(A,B); !!x y. [| x:A; y:B(x); p= |] ==> c(x,y):C() |] - ==> split(p,c):C(p)" +lemma splitT: "\p:Sigma(A,B); \x y. \x:A; y:B(x); p=\ \ c(x,y):C()\ \ split(p,c):C(p)" by ncanT lemma whenT: - "[| p:A+B; !!x.[| x:A; p=inl(x) |] ==> a(x):C(inl(x)); !!y.[| y:B; p=inr(y) |] - ==> b(y):C(inr(y)) |] ==> when(p,a,b) : C(p)" + "\p:A+B; + \x. \x:A; p=inl(x)\ \ a(x):C(inl(x)); + \y. \y:B; p=inr(y)\ \ b(y):C(inr(y))\ \ when(p,a,b) : C(p)" by ncanT lemmas ncanTs = ifT applyT splitT whenT @@ -162,30 +157,30 @@ subsection {* Subtypes *} -lemma SubtypeD1: "a : Subtype(A, P) ==> a : A" - and SubtypeD2: "a : Subtype(A, P) ==> P(a)" +lemma SubtypeD1: "a : Subtype(A, P) \ a : A" + and SubtypeD2: "a : Subtype(A, P) \ P(a)" by (simp_all add: SubtypeXH) -lemma SubtypeI: "[| a:A; P(a) |] ==> a : {x:A. P(x)}" +lemma SubtypeI: "\a:A; P(a)\ \ a : {x:A. P(x)}" by (simp add: SubtypeXH) -lemma SubtypeE: "[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> Q |] ==> Q" +lemma SubtypeE: "\a : {x:A. P(x)}; \a:A; P(a)\ \ Q\ \ Q" by (simp add: SubtypeXH) subsection {* Monotonicity *} -lemma idM: "mono (%X. X)" +lemma idM: "mono (\X. X)" apply (rule monoI) apply assumption done -lemma constM: "mono(%X. A)" +lemma constM: "mono(\X. A)" apply (rule monoI) apply (rule subset_refl) done -lemma "mono(%X. A(X)) ==> mono(%X.[A(X)])" +lemma "mono(\X. A(X)) \ mono(\X.[A(X)])" apply (rule subsetI [THEN monoI]) apply (drule LiftXH [THEN iffD1]) apply (erule disjE) @@ -196,18 +191,16 @@ done lemma SgM: - "[| mono(%X. A(X)); !!x X. x:A(X) ==> mono(%X. B(X,x)) |] ==> - mono(%X. Sigma(A(X),B(X)))" + "\mono(\X. A(X)); \x X. x:A(X) \ mono(\X. B(X,x))\ \ + mono(\X. Sigma(A(X),B(X)))" by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls dest!: monoD [THEN subsetD]) -lemma PiM: - "[| !!x. x:A ==> mono(%X. B(X,x)) |] ==> mono(%X. Pi(A,B(X)))" +lemma PiM: "(\x. x:A \ mono(\X. B(X,x))) \ mono(\X. Pi(A,B(X)))" by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls dest!: monoD [THEN subsetD]) -lemma PlusM: - "[| mono(%X. A(X)); mono(%X. B(X)) |] ==> mono(%X. A(X)+B(X))" +lemma PlusM: "\mono(\X. A(X)); mono(\X. B(X))\ \ mono(\X. A(X)+B(X))" by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls dest!: monoD [THEN subsetD]) @@ -216,7 +209,7 @@ subsubsection {* Conversion Rules for Fixed Points via monotonicity and Tarski *} -lemma NatM: "mono(%X. Unit+X)" +lemma NatM: "mono(\X. Unit+X)" apply (rule PlusM constM idM)+ done @@ -225,7 +218,7 @@ apply (rule NatM) done -lemma ListM: "mono(%X.(Unit+Sigma(A,%y. X)))" +lemma ListM: "mono(\X.(Unit+Sigma(A,\y. X)))" apply (rule PlusM SgM constM idM)+ done @@ -239,7 +232,7 @@ apply (rule ListM) done -lemma IListsM: "mono(%X.({} + Sigma(A,%y. X)))" +lemma IListsM: "mono(\X.({} + Sigma(A,\y. X)))" apply (rule PlusM SgM constM idM)+ done @@ -253,10 +246,10 @@ subsection {* Exhaustion Rules *} -lemma NatXH: "a : Nat <-> (a=zero | (EX x:Nat. a=succ(x)))" - and ListXH: "a : List(A) <-> (a=[] | (EX x:A. EX xs:List(A).a=x$xs))" - and ListsXH: "a : Lists(A) <-> (a=[] | (EX x:A. EX xs:Lists(A).a=x$xs))" - and IListsXH: "a : ILists(A) <-> (EX x:A. EX xs:ILists(A).a=x$xs)" +lemma NatXH: "a : Nat \ (a=zero | (EX x:Nat. a=succ(x)))" + and ListXH: "a : List(A) \ (a=[] | (EX x:A. EX xs:List(A).a=x$xs))" + and ListsXH: "a : Lists(A) \ (a=[] | (EX x:A. EX xs:Lists(A).a=x$xs))" + and IListsXH: "a : ILists(A) \ (EX x:A. EX xs:ILists(A).a=x$xs)" unfolding ind_data_defs by (rule ind_type_eqs [THEN XHlemma1], blast intro!: canTs elim!: case_rls)+ @@ -268,9 +261,9 @@ subsection {* Type Rules *} lemma zeroT: "zero : Nat" - and succT: "n:Nat ==> succ(n) : Nat" + and succT: "n:Nat \ succ(n) : Nat" and nilT: "[] : List(A)" - and consT: "[| h:A; t:List(A) |] ==> h$t : List(A)" + and consT: "\h:A; t:List(A)\ \ h$t : List(A)" by (blast intro: iXHs [THEN iffD2])+ lemmas icanTs = zeroT succT nilT consT @@ -280,14 +273,12 @@ Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms icase_rls} @{thms case_rls}) *} -lemma ncaseT: - "[| n:Nat; n=zero ==> b:C(zero); !!x.[| x:Nat; n=succ(x) |] ==> c(x):C(succ(x)) |] - ==> ncase(n,b,c) : C(n)" +lemma ncaseT: "\n:Nat; n=zero \ b:C(zero); \x. \x:Nat; n=succ(x)\ \ c(x):C(succ(x))\ + \ ncase(n,b,c) : C(n)" by incanT -lemma lcaseT: - "[| l:List(A); l=[] ==> b:C([]); !!h t.[| h:A; t:List(A); l=h$t |] ==> - c(h,t):C(h$t) |] ==> lcase(l,b,c) : C(l)" +lemma lcaseT: "\l:List(A); l = [] \ b:C([]); \h t. \h:A; t:List(A); l=h$t\ \ c(h,t):C(h$t)\ + \ lcase(l,b,c) : C(l)" by incanT lemmas incanTs = ncaseT lcaseT @@ -297,14 +288,13 @@ lemmas ind_Ms = NatM ListM -lemma Nat_ind: "[| n:Nat; P(zero); !!x.[| x:Nat; P(x) |] ==> P(succ(x)) |] ==> P(n)" +lemma Nat_ind: "\n:Nat; P(zero); \x. \x:Nat; P(x)\ \ P(succ(x))\ \ P(n)" apply (unfold ind_data_defs) apply (erule def_induct [OF Nat_def _ NatM]) apply (blast intro: canTs elim!: case_rls) done -lemma List_ind: - "[| l:List(A); P([]); !!x xs.[| x:A; xs:List(A); P(xs) |] ==> P(x$xs) |] ==> P(l)" +lemma List_ind: "\l:List(A); P([]); \x xs. \x:A; xs:List(A); P(xs)\ \ P(x$xs)\ \ P(l)" apply (unfold ind_data_defs) apply (erule def_induct [OF List_def _ ListM]) apply (blast intro: canTs elim!: case_rls) @@ -315,16 +305,12 @@ subsection {* Primitive Recursive Rules *} -lemma nrecT: - "[| n:Nat; b:C(zero); - !!x g.[| x:Nat; g:C(x) |] ==> c(x,g):C(succ(x)) |] ==> - nrec(n,b,c) : C(n)" +lemma nrecT: "\n:Nat; b:C(zero); \x g. \x:Nat; g:C(x)\ \ c(x,g):C(succ(x))\ + \ nrec(n,b,c) : C(n)" by (erule Nat_ind) auto -lemma lrecT: - "[| l:List(A); b:C([]); - !!x xs g.[| x:A; xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x$xs) |] ==> - lrec(l,b,c) : C(l)" +lemma lrecT: "\l:List(A); b:C([]); \x xs g. \x:A; xs:List(A); g:C(xs)\ \ c(x,xs,g):C(x$xs) \ + \ lrec(l,b,c) : C(l)" by (erule List_ind) auto lemmas precTs = nrecT lrecT @@ -332,8 +318,7 @@ subsection {* Theorem proving *} -lemma SgE2: - "[| : Sigma(A,B); [| a:A; b:B(a) |] ==> P |] ==> P" +lemma SgE2: "\ : Sigma(A,B); \a:A; b:B(a)\ \ P\ \ P" unfolding SgXH by blast (* General theorem proving ignores non-canonical term-formers, *) @@ -348,7 +333,7 @@ subsection {* Infinite Data Types *} -lemma lfp_subset_gfp: "mono(f) ==> lfp(f) <= gfp(f)" +lemma lfp_subset_gfp: "mono(f) \ lfp(f) <= gfp(f)" apply (rule lfp_lowerbound [THEN subset_trans]) apply (erule gfp_lemma3) apply (rule subset_refl) @@ -356,16 +341,14 @@ lemma gfpI: assumes "a:A" - and "!!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X)" + and "\x X. \x:A; ALL y:A. t(y):X\ \ t(x) : B(X)" shows "t(a) : gfp(B)" apply (rule coinduct) - apply (rule_tac P = "%x. EX y:A. x=t (y)" in CollectI) + apply (rule_tac P = "\x. EX y:A. x=t (y)" in CollectI) apply (blast intro!: assms)+ done -lemma def_gfpI: - "[| C==gfp(B); a:A; !!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> - t(a) : C" +lemma def_gfpI: "\C == gfp(B); a:A; \x X. \x:A; ALL y:A. t(y):X\ \ t(x) : B(X)\ \ t(a) : C" apply unfold apply (erule gfpI) apply blast @@ -383,15 +366,15 @@ subsection {* Lemmas and tactics for using the rule @{text "coinduct3"} on @{text "[="} and @{text "="} *} -lemma lfpI: "[| mono(f); a : f(lfp(f)) |] ==> a : lfp(f)" +lemma lfpI: "\mono(f); a : f(lfp(f))\ \ a : lfp(f)" apply (erule lfp_Tarski [THEN ssubst]) apply assumption done -lemma ssubst_single: "[| a=a'; a' : A |] ==> a : A" +lemma ssubst_single: "\a = a'; a' : A\ \ a : A" by simp -lemma ssubst_pair: "[| a=a'; b=b'; : A |] ==> : A" +lemma ssubst_pair: "\a = a'; b = b'; : A\ \ : A" by simp @@ -402,14 +385,14 @@ method_setup coinduct3 = {* Scan.succeed (SIMPLE_METHOD' o coinduct3_tac) *} -lemma ci3_RI: "[| mono(Agen); a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)" +lemma ci3_RI: "\mono(Agen); a : R\ \ a : lfp(\x. Agen(x) Un R Un A)" by coinduct3 -lemma ci3_AgenI: "[| mono(Agen); a : Agen(lfp(%x. Agen(x) Un R Un A)) |] ==> - a : lfp(%x. Agen(x) Un R Un A)" +lemma ci3_AgenI: "\mono(Agen); a : Agen(lfp(\x. Agen(x) Un R Un A))\ \ + a : lfp(\x. Agen(x) Un R Un A)" by coinduct3 -lemma ci3_AI: "[| mono(Agen); a : A |] ==> a : lfp(%x. Agen(x) Un R Un A)" +lemma ci3_AI: "\mono(Agen); a : A\ \ a : lfp(\x. Agen(x) Un R Un A)" by coinduct3 ML {* @@ -434,19 +417,19 @@ lemma POgenIs: " : POgen(R)" " : POgen(R)" - "[| : R; : R |] ==> <,> : POgen(R)" - "!!b b'. [|!!x. : R |] ==> : POgen(R)" + "\ : R; : R\ \ <,> : POgen(R)" + "\b b'. (\x. : R) \ : POgen(R)" " : POgen(R)" - " : lfp(%x. POgen(x) Un R Un PO) ==> - : POgen(lfp(%x. POgen(x) Un R Un PO))" - " : lfp(%x. POgen(x) Un R Un PO) ==> - : POgen(lfp(%x. POgen(x) Un R Un PO))" - " : POgen(lfp(%x. POgen(x) Un R Un PO))" - " : lfp(%x. POgen(x) Un R Un PO) ==> - : POgen(lfp(%x. POgen(x) Un R Un PO))" - "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))" - "[| : lfp(%x. POgen(x) Un R Un PO); : lfp(%x. POgen(x) Un R Un PO) |] - ==> : POgen(lfp(%x. POgen(x) Un R Un PO))" + " : lfp(\x. POgen(x) Un R Un PO) \ + : POgen(lfp(\x. POgen(x) Un R Un PO))" + " : lfp(\x. POgen(x) Un R Un PO) \ + : POgen(lfp(\x. POgen(x) Un R Un PO))" + " : POgen(lfp(\x. POgen(x) Un R Un PO))" + " : lfp(\x. POgen(x) Un R Un PO) \ + : POgen(lfp(\x. POgen(x) Un R Un PO))" + "<[],[]> : POgen(lfp(\x. POgen(x) Un R Un PO))" + "\ : lfp(\x. POgen(x) Un R Un PO); : lfp(\x. POgen(x) Un R Un PO)\ + \ : POgen(lfp(\x. POgen(x) Un R Un PO))" unfolding data_defs by (genIs POgenXH POgen_mono)+ ML {* @@ -468,19 +451,19 @@ lemma EQgenIs: " : EQgen(R)" " : EQgen(R)" - "[| : R; : R |] ==> <,> : EQgen(R)" - "!!b b'. [|!!x. : R |] ==> : EQgen(R)" + "\ : R; : R\ \ <,> : EQgen(R)" + "\b b'. (\x. : R) \ : EQgen(R)" " : EQgen(R)" - " : lfp(%x. EQgen(x) Un R Un EQ) ==> - : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" - " : lfp(%x. EQgen(x) Un R Un EQ) ==> - : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" - " : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" - " : lfp(%x. EQgen(x) Un R Un EQ) ==> - : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" - "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" - "[| : lfp(%x. EQgen(x) Un R Un EQ); : lfp(%x. EQgen(x) Un R Un EQ) |] - ==> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" + " : lfp(\x. EQgen(x) Un R Un EQ) \ + : EQgen(lfp(\x. EQgen(x) Un R Un EQ))" + " : lfp(\x. EQgen(x) Un R Un EQ) \ + : EQgen(lfp(\x. EQgen(x) Un R Un EQ))" + " : EQgen(lfp(\x. EQgen(x) Un R Un EQ))" + " : lfp(\x. EQgen(x) Un R Un EQ) \ + : EQgen(lfp(\x. EQgen(x) Un R Un EQ))" + "<[],[]> : EQgen(lfp(\x. EQgen(x) Un R Un EQ))" + "\ : lfp(\x. EQgen(x) Un R Un EQ); : lfp(\x. EQgen(x) Un R Un EQ)\ + \ : EQgen(lfp(\x. EQgen(x) Un R Un EQ))" unfolding data_defs by (genIs EQgenXH EQgen_mono)+ ML {* @@ -502,4 +485,8 @@ ALLGOALS EQgen_raw_tac) i *} +method_setup EQgen = {* + Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (EQgen_tac ctxt ths)) +*} + end diff -r 2f65dcd32a59 -r 51890cb80b30 src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CCL/Wfd.thy Tue Nov 11 21:14:19 2014 +0100 @@ -9,56 +9,57 @@ imports Trancl Type Hered begin -definition Wfd :: "[i set] => o" - where "Wfd(R) == ALL P.(ALL x.(ALL y. : R --> y:P) --> x:P) --> (ALL a. a:P)" +definition Wfd :: "[i set] \ o" + where "Wfd(R) == ALL P.(ALL x.(ALL y. : R \ y:P) \ x:P) \ (ALL a. a:P)" -definition wf :: "[i set] => i set" - where "wf(R) == {x. x:R & Wfd(R)}" +definition wf :: "[i set] \ i set" + where "wf(R) == {x. x:R \ Wfd(R)}" -definition wmap :: "[i=>i,i set] => i set" - where "wmap(f,R) == {p. EX x y. p= & : R}" +definition wmap :: "[i\i,i set] \ i set" + where "wmap(f,R) == {p. EX x y. p= \ : R}" definition lex :: "[i set,i set] => i set" (infixl "**" 70) - where "ra**rb == {p. EX a a' b b'. p = <,> & ( : ra | (a=a' & : rb))}" + where "ra**rb == {p. EX a a' b b'. p = <,> \ ( : ra | (a=a' \ : rb))}" definition NatPR :: "i set" where "NatPR == {p. EX x:Nat. p=}" -definition ListPR :: "i set => i set" +definition ListPR :: "i set \ i set" where "ListPR(A) == {p. EX h:A. EX t:List(A). p=}" lemma wfd_induct: assumes 1: "Wfd(R)" - and 2: "!!x.[| ALL y. : R --> P(y) |] ==> P(x)" + and 2: "\x. ALL y. : R \ P(y) \ P(x)" shows "P(a)" apply (rule 1 [unfolded Wfd_def, rule_format, THEN CollectD]) using 2 apply blast done lemma wfd_strengthen_lemma: - assumes 1: "!!x y. : R ==> Q(x)" - and 2: "ALL x. (ALL y. : R --> y : P) --> x : P" - and 3: "!!x. Q(x) ==> x:P" + assumes 1: "\x y. : R \ Q(x)" + and 2: "ALL x. (ALL y. : R \ y : P) \ x : P" + and 3: "\x. Q(x) \ x:P" shows "a:P" apply (rule 2 [rule_format]) using 1 3 apply blast done -ML {* - fun wfd_strengthen_tac ctxt s i = - res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac ctxt (i+1) +method_setup wfd_strengthen = {* + Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => + SIMPLE_METHOD' (fn i => + res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac ctxt (i+1))) *} -lemma wf_anti_sym: "[| Wfd(r); :r; :r |] ==> P" - apply (subgoal_tac "ALL x. :r --> :r --> P") +lemma wf_anti_sym: "\Wfd(r); :r; :r\ \ P" + apply (subgoal_tac "ALL x. :r \ :r \ P") apply blast apply (erule wfd_induct) apply blast done -lemma wf_anti_refl: "[| Wfd(r); : r |] ==> P" +lemma wf_anti_refl: "\Wfd(r); : r\ \ P" apply (rule wf_anti_sym) apply assumption+ done @@ -86,26 +87,26 @@ subsection {* Lexicographic Ordering *} lemma lexXH: - "p : ra**rb <-> (EX a a' b b'. p = <,> & ( : ra | a=a' & : rb))" + "p : ra**rb \ (EX a a' b b'. p = <,> \ ( : ra | a=a' \ : rb))" unfolding lex_def by blast -lemma lexI1: " : ra ==> <,> : ra**rb" +lemma lexI1: " : ra \ <,> : ra**rb" by (blast intro!: lexXH [THEN iffD2]) -lemma lexI2: " : rb ==> <,> : ra**rb" +lemma lexI2: " : rb \ <,> : ra**rb" by (blast intro!: lexXH [THEN iffD2]) lemma lexE: assumes 1: "p : ra**rb" - and 2: "!!a a' b b'.[| : ra; p=<,> |] ==> R" - and 3: "!!a b b'.[| : rb; p = <,> |] ==> R" + and 2: "\a a' b b'. \ : ra; p=<,>\ \ R" + and 3: "\a b b'. \ : rb; p = <,>\ \ R" shows R apply (rule 1 [THEN lexXH [THEN iffD1], THEN exE]) using 2 3 apply blast done -lemma lex_pair: "[| p : r**s; !!a a' b b'. p = <,> ==> P |] ==>P" +lemma lex_pair: "\p : r**s; \a a' b b'. p = <,> \ P\ \P" apply (erule lexE) apply blast+ done @@ -116,7 +117,7 @@ shows "Wfd(R**S)" apply (unfold Wfd_def) apply safe - apply (tactic {* wfd_strengthen_tac @{context} "%x. EX a b. x=" 1 *}) + apply (wfd_strengthen "\x. EX a b. x=") apply (blast elim!: lex_pair) apply (subgoal_tac "ALL a b.:P") apply blast @@ -128,13 +129,13 @@ subsection {* Mapping *} -lemma wmapXH: "p : wmap(f,r) <-> (EX x y. p= & : r)" +lemma wmapXH: "p : wmap(f,r) \ (EX x y. p= \ : r)" unfolding wmap_def by blast -lemma wmapI: " : r ==> : wmap(f,r)" +lemma wmapI: " : r \ : wmap(f,r)" by (blast intro!: wmapXH [THEN iffD2]) -lemma wmapE: "[| p : wmap(f,r); !!a b.[| : r; p= |] ==> R |] ==> R" +lemma wmapE: "\p : wmap(f,r); \a b. \ : r; p=\ \ R\ \ R" by (blast dest!: wmapXH [THEN iffD1]) lemma wmap_wf: @@ -142,7 +143,7 @@ shows "Wfd(wmap(f,r))" apply (unfold Wfd_def) apply clarify - apply (subgoal_tac "ALL b. ALL a. f (a) =b-->a:P") + apply (subgoal_tac "ALL b. ALL a. f (a) = b \ a:P") apply blast apply (rule 1 [THEN wfd_induct, THEN allI]) apply clarify @@ -156,17 +157,17 @@ subsection {* Projections *} -lemma wfstI: " : r ==> <,> : wmap(fst,r)" +lemma wfstI: " : r \ <,> : wmap(fst,r)" apply (rule wmapI) apply simp done -lemma wsndI: " : r ==> <,> : wmap(snd,r)" +lemma wsndI: " : r \ <,> : wmap(snd,r)" apply (rule wmapI) apply simp done -lemma wthdI: " : r ==> <>,>> : wmap(thd,r)" +lemma wthdI: " : r \ <>,>> : wmap(thd,r)" apply (rule wmapI) apply simp done @@ -174,7 +175,7 @@ subsection {* Ground well-founded relations *} -lemma wfI: "[| Wfd(r); a : r |] ==> a : wf(r)" +lemma wfI: "\Wfd(r); a : r\ \ a : wf(r)" unfolding wf_def by blast lemma Empty_wf: "Wfd({})" @@ -187,22 +188,22 @@ apply (rule Empty_wf) done -lemma NatPRXH: "p : NatPR <-> (EX x:Nat. p=)" +lemma NatPRXH: "p : NatPR \ (EX x:Nat. p=)" unfolding NatPR_def by blast -lemma ListPRXH: "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=)" +lemma ListPRXH: "p : ListPR(A) \ (EX h:A. EX t:List(A).p=)" unfolding ListPR_def by blast -lemma NatPRI: "x : Nat ==> : NatPR" +lemma NatPRI: "x : Nat \ : NatPR" by (auto simp: NatPRXH) -lemma ListPRI: "[| t : List(A); h : A |] ==> : ListPR(A)" +lemma ListPRI: "\t : List(A); h : A\ \ : ListPR(A)" by (auto simp: ListPRXH) lemma NatPR_wf: "Wfd(NatPR)" apply (unfold Wfd_def) apply clarify - apply (tactic {* wfd_strengthen_tac @{context} "%x. x:Nat" 1 *}) + apply (wfd_strengthen "\x. x:Nat") apply (fastforce iff: NatPRXH) apply (erule Nat_ind) apply (fastforce iff: NatPRXH)+ @@ -211,7 +212,7 @@ lemma ListPR_wf: "Wfd(ListPR(A))" apply (unfold Wfd_def) apply clarify - apply (tactic {* wfd_strengthen_tac @{context} "%x. x:List (A)" 1 *}) + apply (wfd_strengthen "\x. x:List (A)") apply (fastforce iff: ListPRXH) apply (erule List_ind) apply (fastforce iff: ListPRXH)+ @@ -222,7 +223,7 @@ lemma letrecT: assumes 1: "a : A" - and 2: "!!p g.[| p:A; ALL x:{x: A. :wf(R)}. g(x) : D(x) |] ==> h(p,g) : D(p)" + and 2: "\p g. \p:A; ALL x:{x: A. :wf(R)}. g(x) : D(x)\ \ h(p,g) : D(p)" shows "letrec g x be h(x,g) in g(a) : D(a)" apply (rule 1 [THEN rev_mp]) apply (rule wf_wf [THEN wfd_induct]) @@ -241,8 +242,8 @@ lemma letrec2T: assumes "a : A" and "b : B" - and "!!p q g.[| p:A; q:B; - ALL x:A. ALL y:{y: B. <,>:wf(R)}. g(x,y) : D(x,y) |] ==> + and "\p q g. \p:A; q:B; + ALL x:A. ALL y:{y: B. <,>:wf(R)}. g(x,y) : D(x,y)\ \ h(p,q,g) : D(p,q)" shows "letrec g x y be h(x,y,g) in g(a,b) : D(a,b)" apply (unfold letrec2_def) @@ -255,16 +256,16 @@ erule bspec SubtypeE sym [THEN subst])+ done -lemma lem: "SPLIT(>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)" +lemma lem: "SPLIT(>,\x xs. SPLIT(xs,\y z. B(x,y,z))) = B(a,b,c)" by (simp add: SPLITB) lemma letrec3T: assumes "a : A" and "b : B" and "c : C" - and "!!p q r g.[| p:A; q:B; r:C; - ALL x:A. ALL y:B. ALL z:{z:C. <>,>> : wf(R)}. - g(x,y,z) : D(x,y,z) |] ==> + and "\p q r g. \p:A; q:B; r:C; + ALL x:A. ALL y:B. ALL z:{z:C. <>,>> : wf(R)}. + g(x,y,z) : D(x,y,z) \ \ h(p,q,r,g) : D(p,q,r)" shows "letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)" apply (unfold letrec3_def) @@ -283,22 +284,19 @@ subsection {* Type Checking for Recursive Calls *} lemma rcallT: - "[| ALL x:{x:A.:wf(R)}.g(x):D(x); - g(a) : D(a) ==> g(a) : E; a:A; :wf(R) |] ==> - g(a) : E" + "\ALL x:{x:A.:wf(R)}.g(x):D(x); + g(a) : D(a) \ g(a) : E; a:A; :wf(R)\ \ g(a) : E" by blast lemma rcall2T: - "[| ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y); - g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <,>:wf(R) |] ==> - g(a,b) : E" + "\ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y); + g(a,b) : D(a,b) \ g(a,b) : E; a:A; b:B; <,>:wf(R)\ \ g(a,b) : E" by blast lemma rcall3T: - "[| ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}. g(x,y,z):D(x,y,z); - g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E; - a:A; b:B; c:C; <>,>> : wf(R) |] ==> - g(a,b,c) : E" + "\ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}. g(x,y,z):D(x,y,z); + g(a,b,c) : D(a,b,c) \ g(a,b,c) : E; + a:A; b:B; c:C; <>,>> : wf(R)\ \ g(a,b,c) : E" by blast lemmas rcallTs = rcallT rcall2T rcall3T @@ -309,9 +307,9 @@ lemma hyprcallT: assumes 1: "g(a) = b" and 2: "ALL x:{x:A.:wf(R)}.g(x):D(x)" - and 3: "ALL x:{x:A.:wf(R)}.g(x):D(x) ==> b=g(a) ==> g(a) : D(a) ==> P" - and 4: "ALL x:{x:A.:wf(R)}.g(x):D(x) ==> a:A" - and 5: "ALL x:{x:A.:wf(R)}.g(x):D(x) ==> :wf(R)" + and 3: "ALL x:{x:A.:wf(R)}.g(x):D(x) \ b=g(a) \ g(a) : D(a) \ P" + and 4: "ALL x:{x:A.:wf(R)}.g(x):D(x) \ a:A" + and 5: "ALL x:{x:A.:wf(R)}.g(x):D(x) \ :wf(R)" shows P apply (rule 3 [OF 2, OF 1 [symmetric]]) apply (rule rcallT [OF 2]) @@ -323,7 +321,7 @@ lemma hyprcall2T: assumes 1: "g(a,b) = c" and 2: "ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y)" - and 3: "[| c=g(a,b); g(a,b) : D(a,b) |] ==> P" + and 3: "\c = g(a,b); g(a,b) : D(a,b)\ \ P" and 4: "a:A" and 5: "b:B" and 6: "<,>:wf(R)" @@ -341,7 +339,7 @@ lemma hyprcall3T: assumes 1: "g(a,b,c) = d" and 2: "ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}.g(x,y,z):D(x,y,z)" - and 3: "[| d=g(a,b,c); g(a,b,c) : D(a,b,c) |] ==> P" + and 3: "\d = g(a,b,c); g(a,b,c) : D(a,b,c)\ \ P" and 4: "a:A" and 5: "b:B" and 6: "c:C" @@ -363,14 +361,12 @@ subsection {* Rules to Remove Induction Hypotheses after Type Checking *} -lemma rmIH1: "[| ALL x:{x:A.:wf(R)}.g(x):D(x); P |] ==> P" . +lemma rmIH1: "\ALL x:{x:A.:wf(R)}.g(x):D(x); P\ \ P" . -lemma rmIH2: "[| ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y); P |] ==> P" . +lemma rmIH2: "\ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y); P\ \ P" . lemma rmIH3: - "[| ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}.g(x,y,z):D(x,y,z); - P |] ==> - P" . + "\ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}.g(x,y,z):D(x,y,z); P\ \ P" . lemmas rmIHs = rmIH1 rmIH2 rmIH3 @@ -381,27 +377,27 @@ (* correctly by applying SubtypeI *) lemma Subtype_canTs: - "!!a b A B P. a : {x:A. b:{y:B(a).P()}} ==> : {x:Sigma(A,B).P(x)}" - "!!a A B P. a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}" - "!!b A B P. b : {x:B. P(inr(x))} ==> inr(b) : {x:A+B. P(x)}" - "!!a P. a : {x:Nat. P(succ(x))} ==> succ(a) : {x:Nat. P(x)}" - "!!h t A P. h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}" + "\a b A B P. a : {x:A. b:{y:B(a).P()}} \ : {x:Sigma(A,B).P(x)}" + "\a A B P. a : {x:A. P(inl(x))} \ inl(a) : {x:A+B. P(x)}" + "\b A B P. b : {x:B. P(inr(x))} \ inr(b) : {x:A+B. P(x)}" + "\a P. a : {x:Nat. P(succ(x))} \ succ(a) : {x:Nat. P(x)}" + "\h t A P. h : {x:A. t : {y:List(A).P(x$y)}} \ h$t : {x:List(A).P(x)}" by (assumption | rule SubtypeI canTs icanTs | erule SubtypeE)+ -lemma letT: "[| f(t):B; ~t=bot |] ==> let x be t in f(x) : B" +lemma letT: "\f(t):B; \t=bot\ \ let x be t in f(x) : B" apply (erule letB [THEN ssubst]) apply assumption done -lemma applyT2: "[| a:A; f : Pi(A,B) |] ==> f ` a : B(a)" +lemma applyT2: "\a:A; f : Pi(A,B)\ \ f ` a : B(a)" apply (erule applyT) apply assumption done -lemma rcall_lemma1: "[| a:A; a:A ==> P(a) |] ==> a : {x:A. P(x)}" +lemma rcall_lemma1: "\a:A; a:A \ P(a)\ \ a : {x:A. P(x)}" by blast -lemma rcall_lemma2: "[| a:{x:A. Q(x)}; [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A. P(x)}" +lemma rcall_lemma2: "\a:{x:A. Q(x)}; \a:A; Q(a)\ \ P(a)\ \ a : {x:A. P(x)}" by blast lemmas rcall_lemmas = asm_rl rcall_lemma1 SubtypeD1 rcall_lemma2 @@ -410,7 +406,6 @@ subsection {* Typechecking *} ML {* - local val type_rls = @@ -443,9 +438,11 @@ in try_IHs rnames end) fun is_rigid_prog t = - case (Logic.strip_assums_concl t) of - (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) => null (Term.add_vars a []) - | _ => false + (case (Logic.strip_assums_concl t) of + (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) => + null (Term.add_vars a []) + | _ => false) + in fun rcall_tac ctxt i = @@ -460,11 +457,10 @@ match_tac ctxt [@{thm SubtypeI}] i fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) => - if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac) + if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac) fun typechk_tac ctxt rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls)) i -fun tac ctxt = typechk_tac ctxt [] 1 (*** Clean up Correctness Condictions ***) @@ -481,6 +477,18 @@ end *} +method_setup typechk = {* + Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (typechk_tac ctxt ths)) +*} + +method_setup clean_ccs = {* + Scan.succeed (SIMPLE_METHOD o clean_ccs_tac) +*} + +method_setup gen_ccs = {* + Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (gen_ccs_tac ctxt ths)) +*} + subsection {* Evaluation *} @@ -517,7 +525,7 @@ etac @{thm substitute} 1)) *}) done -lemma fixV: "f(fix(f)) ---> c ==> fix(f) ---> c" +lemma fixV: "f(fix(f)) ---> c \ fix(f) ---> c" apply (unfold fix_def) apply (rule applyV) apply (rule lamV) @@ -525,7 +533,7 @@ done lemma letrecV: - "h(t,%y. letrec g x be h(x,g) in g(y)) ---> c ==> + "h(t,\y. letrec g x be h(x,g) in g(y)) ---> c \ letrec g x be h(x,g) in g(t) ---> c" apply (unfold letrec_def) apply (assumption | rule fixV applyV lamV)+ @@ -536,51 +544,51 @@ lemma V_rls [eval]: "true ---> true" "false ---> false" - "!!b c t u. [| b--->true; t--->c |] ==> if b then t else u ---> c" - "!!b c t u. [| b--->false; u--->c |] ==> if b then t else u ---> c" - "!!a b. ---> " - "!!a b c t h. [| t ---> ; h(a,b) ---> c |] ==> split(t,h) ---> c" + "\b c t u. \b--->true; t--->c\ \ if b then t else u ---> c" + "\b c t u. \b--->false; u--->c\ \ if b then t else u ---> c" + "\a b. ---> " + "\a b c t h. \t ---> ; h(a,b) ---> c\ \ split(t,h) ---> c" "zero ---> zero" - "!!n. succ(n) ---> succ(n)" - "!!c n t u. [| n ---> zero; t ---> c |] ==> ncase(n,t,u) ---> c" - "!!c n t u x. [| n ---> succ(x); u(x) ---> c |] ==> ncase(n,t,u) ---> c" - "!!c n t u. [| n ---> zero; t ---> c |] ==> nrec(n,t,u) ---> c" - "!!c n t u x. [| n--->succ(x); u(x,nrec(x,t,u))--->c |] ==> nrec(n,t,u)--->c" + "\n. succ(n) ---> succ(n)" + "\c n t u. \n ---> zero; t ---> c\ \ ncase(n,t,u) ---> c" + "\c n t u x. \n ---> succ(x); u(x) ---> c\ \ ncase(n,t,u) ---> c" + "\c n t u. \n ---> zero; t ---> c\ \ nrec(n,t,u) ---> c" + "\c n t u x. \n--->succ(x); u(x,nrec(x,t,u))--->c\ \ nrec(n,t,u)--->c" "[] ---> []" - "!!h t. h$t ---> h$t" - "!!c l t u. [| l ---> []; t ---> c |] ==> lcase(l,t,u) ---> c" - "!!c l t u x xs. [| l ---> x$xs; u(x,xs) ---> c |] ==> lcase(l,t,u) ---> c" - "!!c l t u. [| l ---> []; t ---> c |] ==> lrec(l,t,u) ---> c" - "!!c l t u x xs. [| l--->x$xs; u(x,xs,lrec(xs,t,u))--->c |] ==> lrec(l,t,u)--->c" + "\h t. h$t ---> h$t" + "\c l t u. \l ---> []; t ---> c\ \ lcase(l,t,u) ---> c" + "\c l t u x xs. \l ---> x$xs; u(x,xs) ---> c\ \ lcase(l,t,u) ---> c" + "\c l t u. \l ---> []; t ---> c\ \ lrec(l,t,u) ---> c" + "\c l t u x xs. \l--->x$xs; u(x,xs,lrec(xs,t,u))--->c\ \ lrec(l,t,u)--->c" unfolding data_defs by eval+ subsection {* Factorial *} schematic_lemma - "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) + "letrec f n be ncase(n,succ(zero),\x. nrec(n,zero,\y g. nrec(f(x),g,\z h. succ(h)))) in f(succ(succ(zero))) ---> ?a" by eval schematic_lemma - "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) + "letrec f n be ncase(n,succ(zero),\x. nrec(n,zero,\y g. nrec(f(x),g,\z h. succ(h)))) in f(succ(succ(succ(zero)))) ---> ?a" by eval subsection {* Less Than Or Equal *} schematic_lemma - "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f()))) + "letrec f p be split(p,\m n. ncase(m,true,\x. ncase(n,false,\y. f()))) in f() ---> ?a" by eval schematic_lemma - "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f()))) + "letrec f p be split(p,\m n. ncase(m,true,\x. ncase(n,false,\y. f()))) in f() ---> ?a" by eval schematic_lemma - "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f()))) + "letrec f p be split(p,\m n. ncase(m,true,\x. ncase(n,false,\y. f()))) in f() ---> ?a" by eval @@ -588,12 +596,12 @@ subsection {* Reverse *} schematic_lemma - "letrec id l be lcase(l,[],%x xs. x$id(xs)) + "letrec id l be lcase(l,[],\x xs. x$id(xs)) in id(zero$succ(zero)$[]) ---> ?a" by eval schematic_lemma - "letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g)) + "letrec rev l be lcase(l,[],\x xs. lrec(rev(xs),x$[],\y ys g. y$g)) in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a" by eval diff -r 2f65dcd32a59 -r 51890cb80b30 src/CCL/ex/Flag.thy --- a/src/CCL/ex/Flag.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CCL/ex/Flag.thy Tue Nov 11 21:14:19 2014 +0100 @@ -22,32 +22,32 @@ definition blue :: "i" where "blue == inr(inr(one))" -definition ccase :: "[i,i,i,i]=>i" - where "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))" +definition ccase :: "[i,i,i,i]\i" + where "ccase(c,r,w,b) == when(c, \x. r, \wb. when(wb, \x. w, \x. b))" definition flag :: "i" where "flag == lam l. letrec flagx l be lcase(l,<[],<[],[]>>, - %h t. split(flagx(t),%lr p. split(p,%lw lb. + \h t. split(flagx(t), \lr p. split(p, \lw lb. ccase(h, >, >, >)))) in flagx(l)" -axiomatization Perm :: "i => i => o" -definition Flag :: "i => i => o" where +axiomatization Perm :: "i \ i \ o" +definition Flag :: "i \ i \ o" where "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour). - x = > --> - (ALL c:Colour.(c mem lr = true --> c=red) & - (c mem lw = true --> c=white) & - (c mem lb = true --> c=blue)) & + x = > \ + (ALL c:Colour.(c mem lr = true \ c=red) \ + (c mem lw = true \ c=white) \ + (c mem lb = true \ c=blue)) \ Perm(l,lr @ lw @ lb)" lemmas flag_defs = Colour_def red_def white_def blue_def ccase_def -lemma ColourXH: "a : Colour <-> (a=red | a=white | a=blue)" +lemma ColourXH: "a : Colour \ (a=red | a=white | a=blue)" unfolding simp_type_defs flag_defs by blast lemma redT: "red : Colour" @@ -56,23 +56,21 @@ unfolding ColourXH by blast+ lemma ccaseT: - "[| c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |] - ==> ccase(c,r,w,b) : C(c)" + "\c:Colour; c=red \ r : C(red); c=white \ w : C(white); c=blue \ b : C(blue)\ + \ ccase(c,r,w,b) : C(c)" unfolding flag_defs by ncanT lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)" apply (unfold flag_def) - apply (tactic {* typechk_tac @{context} - [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *}) - apply (tactic "clean_ccs_tac @{context}") + apply (typechk redT whiteT blueT ccaseT) + apply clean_ccs apply (erule ListPRI [THEN ListPR_wf [THEN wfI]]) apply assumption done lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).Flag(x,l)}" apply (unfold flag_def) - apply (tactic {* gen_ccs_tac @{context} - [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *}) + apply (gen_ccs redT whiteT blueT ccaseT) oops end diff -r 2f65dcd32a59 -r 51890cb80b30 src/CCL/ex/List.thy --- a/src/CCL/ex/List.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CCL/ex/List.thy Tue Nov 11 21:14:19 2014 +0100 @@ -9,110 +9,109 @@ imports Nat begin -definition map :: "[i=>i,i]=>i" - where "map(f,l) == lrec(l,[],%x xs g. f(x)$g)" +definition map :: "[i\i,i]\i" + where "map(f,l) == lrec(l, [], \x xs g. f(x)$g)" -definition comp :: "[i=>i,i=>i]=>i=>i" (infixr "\" 55) - where "f \ g == (%x. f(g(x)))" +definition comp :: "[i\i,i\i]\i\i" (infixr "\" 55) + where "f \ g == (\x. f(g(x)))" -definition append :: "[i,i]=>i" (infixr "@" 55) - where "l @ m == lrec(l,m,%x xs g. x$g)" +definition append :: "[i,i]\i" (infixr "@" 55) + where "l @ m == lrec(l, m, \x xs g. x$g)" -axiomatization member :: "[i,i]=>i" (infixr "mem" 55) (* FIXME dangling eq *) - where member_ax: "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)" +axiomatization member :: "[i,i]\i" (infixr "mem" 55) (* FIXME dangling eq *) + where member_ax: "a mem l == lrec(l, false, \h t g. if eq(a,h) then true else g)" -definition filter :: "[i,i]=>i" - where "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)" +definition filter :: "[i,i]\i" + where "filter(f,l) == lrec(l, [], \x xs g. if f`x then x$g else g)" -definition flat :: "i=>i" - where "flat(l) == lrec(l,[],%h t g. h @ g)" +definition flat :: "i\i" + where "flat(l) == lrec(l, [], \h t g. h @ g)" -definition partition :: "[i,i]=>i" where - "partition(f,l) == letrec part l a b be lcase(l,,%x xs. +definition partition :: "[i,i]\i" where + "partition(f,l) == letrec part l a b be lcase(l, , \x xs. if f`x then part(xs,x$a,b) else part(xs,a,x$b)) in part(l,[],[])" -definition insert :: "[i,i,i]=>i" - where "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)" +definition insert :: "[i,i,i]\i" + where "insert(f,a,l) == lrec(l, a$[], \h t g. if f`a`h then a$h$t else h$g)" -definition isort :: "i=>i" - where "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))" +definition isort :: "i\i" + where "isort(f) == lam l. lrec(l, [], \h t g. insert(f,h,g))" -definition qsort :: "i=>i" where - "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. +definition qsort :: "i\i" where + "qsort(f) == lam l. letrec qsortx l be lcase(l, [], \h t. let p be partition(f`h,t) - in split(p,%x y. qsortx(x) @ h$qsortx(y))) + in split(p, \x y. qsortx(x) @ h$qsortx(y))) in qsortx(l)" lemmas list_defs = map_def comp_def append_def filter_def flat_def insert_def isort_def partition_def qsort_def lemma listBs [simp]: - "!!f g. (f \ g) = (%a. f(g(a)))" - "!!a f g. (f \ g)(a) = f(g(a))" - "!!f. map(f,[]) = []" - "!!f x xs. map(f,x$xs) = f(x)$map(f,xs)" - "!!m. [] @ m = m" - "!!x xs m. x$xs @ m = x$(xs @ m)" - "!!f. filter(f,[]) = []" - "!!f x xs. filter(f,x$xs) = if f`x then x$filter(f,xs) else filter(f,xs)" + "\f g. (f \ g) = (\a. f(g(a)))" + "\a f g. (f \ g)(a) = f(g(a))" + "\f. map(f,[]) = []" + "\f x xs. map(f,x$xs) = f(x)$map(f,xs)" + "\m. [] @ m = m" + "\x xs m. x$xs @ m = x$(xs @ m)" + "\f. filter(f,[]) = []" + "\f x xs. filter(f,x$xs) = if f`x then x$filter(f,xs) else filter(f,xs)" "flat([]) = []" - "!!x xs. flat(x$xs) = x @ flat(xs)" - "!!a f. insert(f,a,[]) = a$[]" - "!!a f xs. insert(f,a,x$xs) = if f`a`x then a$x$xs else x$insert(f,a,xs)" + "\x xs. flat(x$xs) = x @ flat(xs)" + "\a f. insert(f,a,[]) = a$[]" + "\a f xs. insert(f,a,x$xs) = if f`a`x then a$x$xs else x$insert(f,a,xs)" by (simp_all add: list_defs) -lemma nmapBnil: "n:Nat ==> map(f) ^ n ` [] = []" +lemma nmapBnil: "n:Nat \ map(f) ^ n ` [] = []" apply (erule Nat_ind) apply simp_all done -lemma nmapBcons: "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)" +lemma nmapBcons: "n:Nat \ map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)" apply (erule Nat_ind) apply simp_all done -lemma mapT: "[| !!x. x:A==>f(x):B; l : List(A) |] ==> map(f,l) : List(B)" +lemma mapT: "\\x. x:A \ f(x):B; l : List(A)\ \ map(f,l) : List(B)" apply (unfold map_def) - apply (tactic "typechk_tac @{context} [] 1") + apply typechk apply blast done -lemma appendT: "[| l : List(A); m : List(A) |] ==> l @ m : List(A)" +lemma appendT: "\l : List(A); m : List(A)\ \ l @ m : List(A)" apply (unfold append_def) - apply (tactic "typechk_tac @{context} [] 1") + apply typechk done lemma appendTS: - "[| l : {l:List(A). m : {m:List(A).P(l @ m)}} |] ==> l @ m : {x:List(A). P(x)}" + "\l : {l:List(A). m : {m:List(A).P(l @ m)}}\ \ l @ m : {x:List(A). P(x)}" by (blast intro!: appendT) -lemma filterT: "[| f:A->Bool; l : List(A) |] ==> filter(f,l) : List(A)" +lemma filterT: "\f:A->Bool; l : List(A)\ \ filter(f,l) : List(A)" apply (unfold filter_def) - apply (tactic "typechk_tac @{context} [] 1") + apply typechk done -lemma flatT: "l : List(List(A)) ==> flat(l) : List(A)" +lemma flatT: "l : List(List(A)) \ flat(l) : List(A)" apply (unfold flat_def) - apply (tactic {* typechk_tac @{context} @{thms appendT} 1 *}) + apply (typechk appendT) done -lemma insertT: "[| f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)" +lemma insertT: "\f : A->A->Bool; a:A; l : List(A)\ \ insert(f,a,l) : List(A)" apply (unfold insert_def) - apply (tactic "typechk_tac @{context} [] 1") + apply typechk done lemma insertTS: - "[| f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} |] ==> + "\f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} \ \ insert(f,a,l) : {x:List(A). P(x)}" by (blast intro!: insertT) -lemma partitionT: - "[| f:A->Bool; l : List(A) |] ==> partition(f,l) : List(A)*List(A)" +lemma partitionT: "\f:A->Bool; l : List(A)\ \ partition(f,l) : List(A)*List(A)" apply (unfold partition_def) - apply (tactic "typechk_tac @{context} [] 1") - apply (tactic "clean_ccs_tac @{context}") + apply typechk + apply clean_ccs apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]]) apply assumption+ apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]]) diff -r 2f65dcd32a59 -r 51890cb80b30 src/CCL/ex/Nat.thy --- a/src/CCL/ex/Nat.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CCL/ex/Nat.thy Tue Nov 11 21:14:19 2014 +0100 @@ -6,44 +6,44 @@ section {* Programs defined over the natural numbers *} theory Nat -imports Wfd +imports "../Wfd" begin -definition not :: "i=>i" +definition not :: "i\i" where "not(b) == if b then false else true" -definition add :: "[i,i]=>i" (infixr "#+" 60) - where "a #+ b == nrec(a,b,%x g. succ(g))" +definition add :: "[i,i]\i" (infixr "#+" 60) + where "a #+ b == nrec(a, b, \x g. succ(g))" -definition mult :: "[i,i]=>i" (infixr "#*" 60) - where "a #* b == nrec(a,zero,%x g. b #+ g)" +definition mult :: "[i,i]\i" (infixr "#*" 60) + where "a #* b == nrec(a, zero, \x g. b #+ g)" -definition sub :: "[i,i]=>i" (infixr "#-" 60) +definition sub :: "[i,i]\i" (infixr "#-" 60) where "a #- b == - letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy))) + letrec sub x y be ncase(y, x, \yy. ncase(x, zero, \xx. sub(xx,yy))) in sub(a,b)" -definition le :: "[i,i]=>i" (infixr "#<=" 60) +definition le :: "[i,i]\i" (infixr "#<=" 60) where "a #<= b == - letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy))) + letrec le x y be ncase(x, true, \xx. ncase(y, false, \yy. le(xx,yy))) in le(a,b)" -definition lt :: "[i,i]=>i" (infixr "#<" 60) +definition lt :: "[i,i]\i" (infixr "#<" 60) where "a #< b == not(b #<= a)" -definition div :: "[i,i]=>i" (infixr "##" 60) +definition div :: "[i,i]\i" (infixr "##" 60) where "a ## b == letrec div x y be if x #< y then zero else succ(div(x#-y,y)) in div(a,b)" -definition ackermann :: "[i,i]=>i" +definition ackermann :: "[i,i]\i" where "ackermann(a,b) == - letrec ack n m be ncase(n,succ(m),%x. - ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y)))) + letrec ack n m be ncase(n, succ(m), \x. + ncase(m,ack(x,succ(zero)), \y. ack(x,ack(succ(x),y)))) in ack(a,b)" lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ackermann_def napply_def @@ -60,39 +60,39 @@ by (simp_all add: nat_defs) -lemma napply_f: "n:Nat ==> f^n`f(a) = f^succ(n)`a" +lemma napply_f: "n:Nat \ f^n`f(a) = f^succ(n)`a" apply (erule Nat_ind) apply simp_all done -lemma addT: "[| a:Nat; b:Nat |] ==> a #+ b : Nat" +lemma addT: "\a:Nat; b:Nat\ \ a #+ b : Nat" apply (unfold add_def) - apply (tactic {* typechk_tac @{context} [] 1 *}) + apply typechk done -lemma multT: "[| a:Nat; b:Nat |] ==> a #* b : Nat" +lemma multT: "\a:Nat; b:Nat\ \ a #* b : Nat" apply (unfold add_def mult_def) - apply (tactic {* typechk_tac @{context} [] 1 *}) + apply typechk done (* Defined to return zero if a a #- b : Nat" +lemma subT: "\a:Nat; b:Nat\ \ a #- b : Nat" apply (unfold sub_def) - apply (tactic {* typechk_tac @{context} [] 1 *}) - apply (tactic {* clean_ccs_tac @{context} *}) + apply typechk + apply clean_ccs apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) done -lemma leT: "[| a:Nat; b:Nat |] ==> a #<= b : Bool" +lemma leT: "\a:Nat; b:Nat\ \ a #<= b : Bool" apply (unfold le_def) - apply (tactic {* typechk_tac @{context} [] 1 *}) - apply (tactic {* clean_ccs_tac @{context} *}) + apply typechk + apply clean_ccs apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) done -lemma ltT: "[| a:Nat; b:Nat |] ==> a #< b : Bool" +lemma ltT: "\a:Nat; b:Nat\ \ a #< b : Bool" apply (unfold not_def lt_def) - apply (tactic {* typechk_tac @{context} @{thms leT} 1 *}) + apply (typechk leT) done @@ -100,9 +100,9 @@ lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]] -lemma "[| a:Nat; b:Nat |] ==> ackermann(a,b) : Nat" +lemma "\a:Nat; b:Nat\ \ ackermann(a,b) : Nat" apply (unfold ackermann_def) - apply (tactic {* gen_ccs_tac @{context} [] 1 *}) + apply gen_ccs apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+ done diff -r 2f65dcd32a59 -r 51890cb80b30 src/CCL/ex/Stream.thy --- a/src/CCL/ex/Stream.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CCL/ex/Stream.thy Tue Nov 11 21:14:19 2014 +0100 @@ -9,10 +9,10 @@ imports List begin -definition iter1 :: "[i=>i,i]=>i" +definition iter1 :: "[i\i,i]\i" where "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)" -definition iter2 :: "[i=>i,i]=>i" +definition iter2 :: "[i\i,i]\i" where "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)" (* @@ -27,12 +27,11 @@ lemma map_comp: assumes 1: "l:Lists(A)" shows "map(f \ g,l) = map(f,map(g,l))" - apply (tactic {* eq_coinduct3_tac @{context} - "{p. EX x y. p= & (EX l:Lists (A) .x=map (f \ g,l) & y=map (f,map (g,l)))}" 1 *}) + apply (eq_coinduct3 "{p. EX x y. p= \ (EX l:Lists (A) .x=map (f \ g,l) \ y=map (f,map (g,l)))}") apply (blast intro: 1) apply safe apply (drule ListsXH [THEN iffD1]) - apply (tactic "EQgen_tac @{context} [] 1") + apply EQgen apply fastforce done @@ -40,13 +39,12 @@ lemma map_id: assumes 1: "l:Lists(A)" - shows "map(%x. x,l) = l" - apply (tactic {* eq_coinduct3_tac @{context} - "{p. EX x y. p= & (EX l:Lists (A) .x=map (%x. x,l) & y=l) }" 1 *}) + shows "map(\x. x, l) = l" + apply (eq_coinduct3 "{p. EX x y. p= \ (EX l:Lists (A) .x=map (\x. x,l) \ y=l) }") apply (blast intro: 1) apply safe apply (drule ListsXH [THEN iffD1]) - apply (tactic "EQgen_tac @{context} [] 1") + apply EQgen apply blast done @@ -57,14 +55,14 @@ assumes "l:Lists(A)" and "m:Lists(A)" shows "map(f,l@m) = map(f,l) @ map(f,m)" - apply (tactic {* eq_coinduct3_tac @{context} - "{p. EX x y. p= & (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) & y=map (f,l) @ map (f,m))}" 1 *}) + apply (eq_coinduct3 + "{p. EX x y. p= \ (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) \ y=map (f,l) @ map (f,m))}") apply (blast intro: assms) apply safe apply (drule ListsXH [THEN iffD1]) - apply (tactic "EQgen_tac @{context} [] 1") + apply EQgen apply (drule ListsXH [THEN iffD1]) - apply (tactic "EQgen_tac @{context} [] 1") + apply EQgen apply blast done @@ -76,12 +74,12 @@ and "l:Lists(A)" and "m:Lists(A)" shows "k @ l @ m = (k @ l) @ m" - apply (tactic {* eq_coinduct3_tac @{context} - "{p. EX x y. p= & (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m & y= (k @ l) @ m) }" 1*}) + apply (eq_coinduct3 + "{p. EX x y. p= \ (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m \ y= (k @ l) @ m) }") apply (blast intro: assms) apply safe apply (drule ListsXH [THEN iffD1]) - apply (tactic "EQgen_tac @{context} [] 1") + apply EQgen prefer 2 apply blast apply (tactic {* DEPTH_SOLVE (etac (XH_to_E @{thm ListsXH}) 1 @@ -94,12 +92,11 @@ lemma ilist_append: assumes "l:ILists(A)" shows "l @ m = l" - apply (tactic {* eq_coinduct3_tac @{context} - "{p. EX x y. p= & (EX l:ILists (A) .EX m. x=l@m & y=l)}" 1 *}) + apply (eq_coinduct3 "{p. EX x y. p= \ (EX l:ILists (A) .EX m. x=l@m \ y=l)}") apply (blast intro: assms) apply safe apply (drule IListsXH [THEN iffD1]) - apply (tactic "EQgen_tac @{context} [] 1") + apply EQgen apply blast done @@ -121,17 +118,17 @@ done lemma iter2Blemma: - "n:Nat ==> + "n:Nat \ map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))" - apply (rule_tac P = "%x. ?lhs (x) = ?rhs" in iter2B [THEN ssubst]) + apply (rule_tac P = "\x. ?lhs (x) = ?rhs" in iter2B [THEN ssubst]) apply (simp add: nmapBcons) done lemma iter1_iter2_eq: "iter1(f,a) = iter2(f,a)" - apply (tactic {* eq_coinduct3_tac @{context} - "{p. EX x y. p= & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*}) + apply (eq_coinduct3 + "{p. EX x y. p= \ (EX n:Nat. x=iter1 (f,f^n`a) \ y=map (f) ^n`iter2 (f,a))}") apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong]) - apply (tactic {* EQgen_tac @{context} [@{thm iter1B}, @{thm iter2Blemma}] 1 *}) + apply (EQgen iter1B iter2Blemma) apply (subst napply_f, assumption) apply (rule_tac f1 = f in napplyBsucc [THEN subst]) apply blast diff -r 2f65dcd32a59 -r 51890cb80b30 src/CTT/Arith.thy --- a/src/CTT/Arith.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CTT/Arith.thy Tue Nov 11 21:14:19 2014 +0100 @@ -12,28 +12,28 @@ subsection {* Arithmetic operators and their definitions *} definition - add :: "[i,i]=>i" (infixr "#+" 65) where - "a#+b == rec(a, b, %u v. succ(v))" + add :: "[i,i]\i" (infixr "#+" 65) where + "a#+b == rec(a, b, \u v. succ(v))" definition - diff :: "[i,i]=>i" (infixr "-" 65) where - "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))" + diff :: "[i,i]\i" (infixr "-" 65) where + "a-b == rec(b, a, \u v. rec(v, 0, \x y. x))" definition - absdiff :: "[i,i]=>i" (infixr "|-|" 65) where + absdiff :: "[i,i]\i" (infixr "|-|" 65) where "a|-|b == (a-b) #+ (b-a)" definition - mult :: "[i,i]=>i" (infixr "#*" 70) where - "a#*b == rec(a, 0, %u v. b #+ v)" + mult :: "[i,i]\i" (infixr "#*" 70) where + "a#*b == rec(a, 0, \u v. b #+ v)" definition - mod :: "[i,i]=>i" (infixr "mod" 70) where + mod :: "[i,i]\i" (infixr "mod" 70) where "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))" definition - div :: "[i,i]=>i" (infixr "div" 70) where - "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))" + div :: "[i,i]\i" (infixr "div" 70) where + "a div b == rec(a, 0, \u v. rec(succ(u) mod b, succ(v), \x y. v))" notation (xsymbols) @@ -52,27 +52,27 @@ (*typing of add: short and long versions*) -lemma add_typing: "[| a:N; b:N |] ==> a #+ b : N" +lemma add_typing: "\a:N; b:N\ \ a #+ b : N" apply (unfold arith_defs) -apply (tactic "typechk_tac @{context} []") +apply typechk done -lemma add_typingL: "[| a=c:N; b=d:N |] ==> a #+ b = c #+ d : N" +lemma add_typingL: "\a = c:N; b = d:N\ \ a #+ b = c #+ d : N" apply (unfold arith_defs) -apply (tactic "equal_tac @{context} []") +apply equal done (*computation for add: 0 and successor cases*) -lemma addC0: "b:N ==> 0 #+ b = b : N" +lemma addC0: "b:N \ 0 #+ b = b : N" apply (unfold arith_defs) -apply (tactic "rew_tac @{context} []") +apply rew done -lemma addC_succ: "[| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N" +lemma addC_succ: "\a:N; b:N\ \ succ(a) #+ b = succ(a #+ b) : N" apply (unfold arith_defs) -apply (tactic "rew_tac @{context} []") +apply rew done @@ -80,26 +80,26 @@ (*typing of mult: short and long versions*) -lemma mult_typing: "[| a:N; b:N |] ==> a #* b : N" +lemma mult_typing: "\a:N; b:N\ \ a #* b : N" apply (unfold arith_defs) -apply (tactic {* typechk_tac @{context} [@{thm add_typing}] *}) +apply (typechk add_typing) done -lemma mult_typingL: "[| a=c:N; b=d:N |] ==> a #* b = c #* d : N" +lemma mult_typingL: "\a = c:N; b = d:N\ \ a #* b = c #* d : N" apply (unfold arith_defs) -apply (tactic {* equal_tac @{context} [@{thm add_typingL}] *}) +apply (equal add_typingL) done (*computation for mult: 0 and successor cases*) -lemma multC0: "b:N ==> 0 #* b = 0 : N" +lemma multC0: "b:N \ 0 #* b = 0 : N" apply (unfold arith_defs) -apply (tactic "rew_tac @{context} []") +apply rew done -lemma multC_succ: "[| a:N; b:N |] ==> succ(a) #* b = b #+ (a #* b) : N" +lemma multC_succ: "\a:N; b:N\ \ succ(a) #* b = b #+ (a #* b) : N" apply (unfold arith_defs) -apply (tactic "rew_tac @{context} []") +apply rew done @@ -107,40 +107,40 @@ (*typing of difference*) -lemma diff_typing: "[| a:N; b:N |] ==> a - b : N" +lemma diff_typing: "\a:N; b:N\ \ a - b : N" apply (unfold arith_defs) -apply (tactic "typechk_tac @{context} []") +apply typechk done -lemma diff_typingL: "[| a=c:N; b=d:N |] ==> a - b = c - d : N" +lemma diff_typingL: "\a = c:N; b = d:N\ \ a - b = c - d : N" apply (unfold arith_defs) -apply (tactic "equal_tac @{context} []") +apply equal done (*computation for difference: 0 and successor cases*) -lemma diffC0: "a:N ==> a - 0 = a : N" +lemma diffC0: "a:N \ a - 0 = a : N" apply (unfold arith_defs) -apply (tactic "rew_tac @{context} []") +apply rew done -(*Note: rec(a, 0, %z w.z) is pred(a). *) +(*Note: rec(a, 0, \z w.z) is pred(a). *) -lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N" +lemma diff_0_eq_0: "b:N \ 0 - b = 0 : N" apply (unfold arith_defs) -apply (tactic {* NE_tac @{context} "b" 1 *}) -apply (tactic "hyp_rew_tac @{context} []") +apply (NE b) +apply hyp_rew done (*Essential to simplify FIRST!! (Else we get a critical pair) succ(a) - succ(b) rewrites to pred(succ(a) - b) *) -lemma diff_succ_succ: "[| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N" +lemma diff_succ_succ: "\a:N; b:N\ \ succ(a) - succ(b) = a - b : N" apply (unfold arith_defs) -apply (tactic "hyp_rew_tac @{context} []") -apply (tactic {* NE_tac @{context} "b" 1 *}) -apply (tactic "hyp_rew_tac @{context} []") +apply hyp_rew +apply (NE b) +apply hyp_rew done @@ -174,67 +174,77 @@ local val congr_rls = @{thms congr_rls} in fun arith_rew_tac ctxt prems = make_rew_tac ctxt - (Arith_simp.norm_tac ctxt (congr_rls, prems)) + (Arith_simp.norm_tac ctxt (congr_rls, prems)) fun hyp_arith_rew_tac ctxt prems = make_rew_tac ctxt - (Arith_simp.cond_norm_tac ctxt (prove_cond_tac, congr_rls, prems)) + (Arith_simp.cond_norm_tac ctxt (prove_cond_tac, congr_rls, prems)) end *} +method_setup arith_rew = {* + Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (arith_rew_tac ctxt ths)) +*} + +method_setup hyp_arith_rew = {* + Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_arith_rew_tac ctxt ths)) +*} + subsection {* Addition *} (*Associative law for addition*) -lemma add_assoc: "[| a:N; b:N; c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N" -apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic "hyp_arith_rew_tac @{context} []") +lemma add_assoc: "\a:N; b:N; c:N\ \ (a #+ b) #+ c = a #+ (b #+ c) : N" +apply (NE a) +apply hyp_arith_rew done (*Commutative law for addition. Can be proved using three inductions. Must simplify after first induction! Orientation of rewrites is delicate*) -lemma add_commute: "[| a:N; b:N |] ==> a #+ b = b #+ a : N" -apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic "hyp_arith_rew_tac @{context} []") -apply (tactic {* NE_tac @{context} "b" 2 *}) +lemma add_commute: "\a:N; b:N\ \ a #+ b = b #+ a : N" +apply (NE a) +apply hyp_arith_rew apply (rule sym_elem) -apply (tactic {* NE_tac @{context} "b" 1 *}) -apply (tactic "hyp_arith_rew_tac @{context} []") +prefer 2 +apply (NE b) +prefer 4 +apply (NE b) +apply hyp_arith_rew done subsection {* Multiplication *} (*right annihilation in product*) -lemma mult_0_right: "a:N ==> a #* 0 = 0 : N" -apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic "hyp_arith_rew_tac @{context} []") +lemma mult_0_right: "a:N \ a #* 0 = 0 : N" +apply (NE a) +apply hyp_arith_rew done (*right successor law for multiplication*) -lemma mult_succ_right: "[| a:N; b:N |] ==> a #* succ(b) = a #+ (a #* b) : N" -apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_assoc} RS @{thm sym_elem}] *}) +lemma mult_succ_right: "\a:N; b:N\ \ a #* succ(b) = a #+ (a #* b) : N" +apply (NE a) +apply (hyp_arith_rew add_assoc [THEN sym_elem]) apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+ done (*Commutative law for multiplication*) -lemma mult_commute: "[| a:N; b:N |] ==> a #* b = b #* a : N" -apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic {* hyp_arith_rew_tac @{context} [@{thm mult_0_right}, @{thm mult_succ_right}] *}) +lemma mult_commute: "\a:N; b:N\ \ a #* b = b #* a : N" +apply (NE a) +apply (hyp_arith_rew mult_0_right mult_succ_right) done (*addition distributes over multiplication*) -lemma add_mult_distrib: "[| a:N; b:N; c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N" -apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_assoc} RS @{thm sym_elem}] *}) +lemma add_mult_distrib: "\a:N; b:N; c:N\ \ (a #+ b) #* c = (a #* c) #+ (b #* c) : N" +apply (NE a) +apply (hyp_arith_rew add_assoc [THEN sym_elem]) done (*Associative law for multiplication*) -lemma mult_assoc: "[| a:N; b:N; c:N |] ==> (a #* b) #* c = a #* (b #* c) : N" -apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_mult_distrib}] *}) +lemma mult_assoc: "\a:N; b:N; c:N\ \ (a #* b) #* c = a #* (b #* c) : N" +apply (NE a) +apply (hyp_arith_rew add_mult_distrib) done @@ -244,34 +254,36 @@ Difference on natural numbers, without negative numbers a - b = 0 iff a<=b a - b = succ(c) iff a>b *} -lemma diff_self_eq_0: "a:N ==> a - a = 0 : N" -apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic "hyp_arith_rew_tac @{context} []") +lemma diff_self_eq_0: "a:N \ a - a = 0 : N" +apply (NE a) +apply hyp_arith_rew done -lemma add_0_right: "[| c : N; 0 : N; c : N |] ==> c #+ 0 = c : N" +lemma add_0_right: "\c : N; 0 : N; c : N\ \ c #+ 0 = c : N" by (rule addC0 [THEN [3] add_commute [THEN trans_elem]]) (*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x. An example of induction over a quantified formula (a product). Uses rewriting with a quantified, implicative inductive hypothesis.*) schematic_lemma add_diff_inverse_lemma: - "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)" -apply (tactic {* NE_tac @{context} "b" 1 *}) + "b:N \ ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)" +apply (NE b) (*strip one "universal quantifier" but not the "implication"*) apply (rule_tac [3] intr_rls) (*case analysis on x in (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *) -apply (tactic {* NE_tac @{context} "x" 4 *}, tactic "assume_tac @{context} 4") +prefer 4 +apply (NE x) +apply assumption (*Prepare for simplification of types -- the antecedent succ(u)<=x *) -apply (rule_tac [5] replace_type) -apply (rule_tac [4] replace_type) -apply (tactic "arith_rew_tac @{context} []") +apply (rule_tac [2] replace_type) +apply (rule_tac [1] replace_type) +apply arith_rew (*Solves first 0 goal, simplifies others. Two sugbgoals remain. Both follow by rewriting, (2) using quantified induction hyp*) -apply (tactic "intr_tac @{context} []") (*strips remaining PRODs*) -apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_0_right}] *}) +apply intr (*strips remaining PRODs*) +apply (hyp_arith_rew add_0_right) apply assumption done @@ -280,7 +292,7 @@ Using ProdE does not work -- for ?B(?a) is ambiguous. Instead, add_diff_inverse_lemma states the desired induction scheme the use of RS below instantiates Vars in ProdE automatically. *) -lemma add_diff_inverse: "[| a:N; b:N; b-a = 0 : N |] ==> b #+ (a-b) = a : N" +lemma add_diff_inverse: "\a:N; b:N; b - a = 0 : N\ \ b #+ (a-b) = a : N" apply (rule EqE) apply (rule add_diff_inverse_lemma [THEN ProdE, THEN ProdE]) apply (assumption | rule EqI)+ @@ -291,82 +303,80 @@ (*typing of absolute difference: short and long versions*) -lemma absdiff_typing: "[| a:N; b:N |] ==> a |-| b : N" +lemma absdiff_typing: "\a:N; b:N\ \ a |-| b : N" apply (unfold arith_defs) -apply (tactic "typechk_tac @{context} []") +apply typechk done -lemma absdiff_typingL: "[| a=c:N; b=d:N |] ==> a |-| b = c |-| d : N" +lemma absdiff_typingL: "\a = c:N; b = d:N\ \ a |-| b = c |-| d : N" apply (unfold arith_defs) -apply (tactic "equal_tac @{context} []") +apply equal done -lemma absdiff_self_eq_0: "a:N ==> a |-| a = 0 : N" +lemma absdiff_self_eq_0: "a:N \ a |-| a = 0 : N" apply (unfold absdiff_def) -apply (tactic {* arith_rew_tac @{context} [@{thm diff_self_eq_0}] *}) +apply (arith_rew diff_self_eq_0) done -lemma absdiffC0: "a:N ==> 0 |-| a = a : N" +lemma absdiffC0: "a:N \ 0 |-| a = a : N" apply (unfold absdiff_def) -apply (tactic "hyp_arith_rew_tac @{context} []") +apply hyp_arith_rew done -lemma absdiff_succ_succ: "[| a:N; b:N |] ==> succ(a) |-| succ(b) = a |-| b : N" +lemma absdiff_succ_succ: "\a:N; b:N\ \ succ(a) |-| succ(b) = a |-| b : N" apply (unfold absdiff_def) -apply (tactic "hyp_arith_rew_tac @{context} []") +apply hyp_arith_rew done (*Note how easy using commutative laws can be? ...not always... *) -lemma absdiff_commute: "[| a:N; b:N |] ==> a |-| b = b |-| a : N" +lemma absdiff_commute: "\a:N; b:N\ \ a |-| b = b |-| a : N" apply (unfold absdiff_def) apply (rule add_commute) -apply (tactic {* typechk_tac @{context} [@{thm diff_typing}] *}) +apply (typechk diff_typing) done (*If a+b=0 then a=0. Surprisingly tedious*) -schematic_lemma add_eq0_lemma: "[| a:N; b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)" -apply (tactic {* NE_tac @{context} "a" 1 *}) +schematic_lemma add_eq0_lemma: "\a:N; b:N\ \ ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)" +apply (NE a) apply (rule_tac [3] replace_type) -apply (tactic "arith_rew_tac @{context} []") -apply (tactic "intr_tac @{context} []") (*strips remaining PRODs*) +apply arith_rew +apply intr (*strips remaining PRODs*) apply (rule_tac [2] zero_ne_succ [THEN FE]) apply (erule_tac [3] EqE [THEN sym_elem]) -apply (tactic {* typechk_tac @{context} [@{thm add_typing}] *}) +apply (typechk add_typing) done (*Version of above with the premise a+b=0. Again, resolution instantiates variables in ProdE *) -lemma add_eq0: "[| a:N; b:N; a #+ b = 0 : N |] ==> a = 0 : N" +lemma add_eq0: "\a:N; b:N; a #+ b = 0 : N\ \ a = 0 : N" apply (rule EqE) apply (rule add_eq0_lemma [THEN ProdE]) apply (rule_tac [3] EqI) -apply (tactic "typechk_tac @{context} []") +apply typechk done (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *) schematic_lemma absdiff_eq0_lem: - "[| a:N; b:N; a |-| b = 0 : N |] ==> - ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)" + "\a:N; b:N; a |-| b = 0 : N\ \ ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)" apply (unfold absdiff_def) -apply (tactic "intr_tac @{context} []") -apply (tactic "eqintr_tac @{context}") +apply intr +apply eqintr apply (rule_tac [2] add_eq0) apply (rule add_eq0) apply (rule_tac [6] add_commute [THEN trans_elem]) -apply (tactic {* typechk_tac @{context} [@{thm diff_typing}] *}) +apply (typechk diff_typing) done (*if a |-| b = 0 then a = b proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*) -lemma absdiff_eq0: "[| a |-| b = 0 : N; a:N; b:N |] ==> a = b : N" +lemma absdiff_eq0: "\a |-| b = 0 : N; a:N; b:N\ \ a = b : N" apply (rule EqE) apply (rule absdiff_eq0_lem [THEN SumE]) -apply (tactic "TRYALL (assume_tac @{context})") -apply (tactic "eqintr_tac @{context}") +apply eqintr apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem]) -apply (rule_tac [3] EqE, tactic "assume_tac @{context} 3") -apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_0_right}] *}) +apply (erule_tac [3] EqE) +apply (hyp_arith_rew add_0_right) done @@ -374,41 +384,41 @@ (*typing of remainder: short and long versions*) -lemma mod_typing: "[| a:N; b:N |] ==> a mod b : N" +lemma mod_typing: "\a:N; b:N\ \ a mod b : N" apply (unfold mod_def) -apply (tactic {* typechk_tac @{context} [@{thm absdiff_typing}] *}) +apply (typechk absdiff_typing) done -lemma mod_typingL: "[| a=c:N; b=d:N |] ==> a mod b = c mod d : N" +lemma mod_typingL: "\a = c:N; b = d:N\ \ a mod b = c mod d : N" apply (unfold mod_def) -apply (tactic {* equal_tac @{context} [@{thm absdiff_typingL}] *}) +apply (equal absdiff_typingL) done (*computation for mod : 0 and successor cases*) -lemma modC0: "b:N ==> 0 mod b = 0 : N" +lemma modC0: "b:N \ 0 mod b = 0 : N" apply (unfold mod_def) -apply (tactic {* rew_tac @{context} [@{thm absdiff_typing}] *}) +apply (rew absdiff_typing) done -lemma modC_succ: -"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N" +lemma modC_succ: "\a:N; b:N\ \ + succ(a) mod b = rec(succ(a mod b) |-| b, 0, \x y. succ(a mod b)) : N" apply (unfold mod_def) -apply (tactic {* rew_tac @{context} [@{thm absdiff_typing}] *}) +apply (rew absdiff_typing) done (*typing of quotient: short and long versions*) -lemma div_typing: "[| a:N; b:N |] ==> a div b : N" +lemma div_typing: "\a:N; b:N\ \ a div b : N" apply (unfold div_def) -apply (tactic {* typechk_tac @{context} [@{thm absdiff_typing}, @{thm mod_typing}] *}) +apply (typechk absdiff_typing mod_typing) done -lemma div_typingL: "[| a=c:N; b=d:N |] ==> a div b = c div d : N" +lemma div_typingL: "\a = c:N; b = d:N\ \ a div b = c div d : N" apply (unfold div_def) -apply (tactic {* equal_tac @{context} [@{thm absdiff_typingL}, @{thm mod_typingL}] *}) +apply (equal absdiff_typingL mod_typingL) done lemmas div_typing_rls = mod_typing div_typing absdiff_typing @@ -416,54 +426,51 @@ (*computation for quotient: 0 and successor cases*) -lemma divC0: "b:N ==> 0 div b = 0 : N" +lemma divC0: "b:N \ 0 div b = 0 : N" apply (unfold div_def) -apply (tactic {* rew_tac @{context} [@{thm mod_typing}, @{thm absdiff_typing}] *}) +apply (rew mod_typing absdiff_typing) done -lemma divC_succ: - "[| a:N; b:N |] ==> succ(a) div b = - rec(succ(a) mod b, succ(a div b), %x y. a div b) : N" +lemma divC_succ: "\a:N; b:N\ \ + succ(a) div b = rec(succ(a) mod b, succ(a div b), \x y. a div b) : N" apply (unfold div_def) -apply (tactic {* rew_tac @{context} [@{thm mod_typing}] *}) +apply (rew mod_typing) done (*Version of above with same condition as the mod one*) -lemma divC_succ2: "[| a:N; b:N |] ==> - succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N" +lemma divC_succ2: "\a:N; b:N\ \ + succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), \x y. a div b) : N" apply (rule divC_succ [THEN trans_elem]) -apply (tactic {* rew_tac @{context} (@{thms div_typing_rls} @ [@{thm modC_succ}]) *}) -apply (tactic {* NE_tac @{context} "succ (a mod b) |-|b" 1 *}) -apply (tactic {* rew_tac @{context} [@{thm mod_typing}, @{thm div_typing}, @{thm absdiff_typing}] *}) +apply (rew div_typing_rls modC_succ) +apply (NE "succ (a mod b) |-|b") +apply (rew mod_typing div_typing absdiff_typing) done (*for case analysis on whether a number is 0 or a successor*) -lemma iszero_decidable: "a:N ==> rec(a, inl(eq), %ka kb. inr()) : +lemma iszero_decidable: "a:N \ rec(a, inl(eq), \ka kb. inr()) : Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))" -apply (tactic {* NE_tac @{context} "a" 1 *}) +apply (NE a) apply (rule_tac [3] PlusI_inr) apply (rule_tac [2] PlusI_inl) -apply (tactic "eqintr_tac @{context}") -apply (tactic "equal_tac @{context} []") +apply eqintr +apply equal done (*Main Result. Holds when b is 0 since a mod 0 = a and a div 0 = 0 *) -lemma mod_div_equality: "[| a:N; b:N |] ==> a mod b #+ (a div b) #* b = a : N" -apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic {* arith_rew_tac @{context} (@{thms div_typing_rls} @ - [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *}) +lemma mod_div_equality: "\a:N; b:N\ \ a mod b #+ (a div b) #* b = a : N" +apply (NE a) +apply (arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2) apply (rule EqE) (*case analysis on succ(u mod b)|-|b *) apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE]) apply (erule_tac [3] SumE) -apply (tactic {* hyp_arith_rew_tac @{context} (@{thms div_typing_rls} @ - [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *}) +apply (hyp_arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2) (*Replace one occurrence of b by succ(u mod b). Clumsy!*) apply (rule add_typingL [THEN trans_elem]) apply (erule EqE [THEN absdiff_eq0, THEN sym_elem]) apply (rule_tac [3] refl_elem) -apply (tactic {* hyp_arith_rew_tac @{context} @{thms div_typing_rls} *}) +apply (hyp_arith_rew div_typing_rls) done end diff -r 2f65dcd32a59 -r 51890cb80b30 src/CTT/Bool.thy --- a/src/CTT/Bool.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CTT/Bool.thy Tue Nov 11 21:14:19 2014 +0100 @@ -22,8 +22,8 @@ "false == inr(tt)" definition - cond :: "[i,i,i]=>i" where - "cond(a,b,c) == when(a, %u. b, %u. c)" + cond :: "[i,i,i]\i" where + "cond(a,b,c) == when(a, \u. b, \u. c)" lemmas bool_defs = Bool_def true_def false_def cond_def @@ -33,7 +33,7 @@ (*formation rule*) lemma boolF: "Bool type" apply (unfold bool_defs) -apply (tactic "typechk_tac @{context} []") +apply typechk done @@ -41,26 +41,24 @@ lemma boolI_true: "true : Bool" apply (unfold bool_defs) -apply (tactic "typechk_tac @{context} []") +apply typechk done lemma boolI_false: "false : Bool" apply (unfold bool_defs) -apply (tactic "typechk_tac @{context} []") +apply typechk done (*elimination rule: typing of cond*) -lemma boolE: - "[| p:Bool; a : C(true); b : C(false) |] ==> cond(p,a,b) : C(p)" +lemma boolE: "\p:Bool; a : C(true); b : C(false)\ \ cond(p,a,b) : C(p)" apply (unfold bool_defs) -apply (tactic "typechk_tac @{context} []") +apply typechk apply (erule_tac [!] TE) -apply (tactic "typechk_tac @{context} []") +apply typechk done -lemma boolEL: - "[| p = q : Bool; a = c : C(true); b = d : C(false) |] - ==> cond(p,a,b) = cond(q,c,d) : C(p)" +lemma boolEL: "\p = q : Bool; a = c : C(true); b = d : C(false)\ + \ cond(p,a,b) = cond(q,c,d) : C(p)" apply (unfold bool_defs) apply (rule PlusEL) apply (erule asm_rl refl_elem [THEN TEL])+ @@ -68,22 +66,20 @@ (*computation rules for true, false*) -lemma boolC_true: - "[| a : C(true); b : C(false) |] ==> cond(true,a,b) = a : C(true)" +lemma boolC_true: "\a : C(true); b : C(false)\ \ cond(true,a,b) = a : C(true)" apply (unfold bool_defs) apply (rule comp_rls) -apply (tactic "typechk_tac @{context} []") +apply typechk apply (erule_tac [!] TE) -apply (tactic "typechk_tac @{context} []") +apply typechk done -lemma boolC_false: - "[| a : C(true); b : C(false) |] ==> cond(false,a,b) = b : C(false)" +lemma boolC_false: "\a : C(true); b : C(false)\ \ cond(false,a,b) = b : C(false)" apply (unfold bool_defs) apply (rule comp_rls) -apply (tactic "typechk_tac @{context} []") +apply typechk apply (erule_tac [!] TE) -apply (tactic "typechk_tac @{context} []") +apply typechk done end diff -r 2f65dcd32a59 -r 51890cb80b30 src/CTT/CTT.thy --- a/src/CTT/CTT.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CTT/CTT.thy Tue Nov 11 21:14:19 2014 +0100 @@ -20,56 +20,56 @@ (*Types*) F :: "t" T :: "t" (*F is empty, T contains one element*) - contr :: "i=>i" + contr :: "i\i" tt :: "i" (*Natural numbers*) N :: "t" - succ :: "i=>i" - rec :: "[i, i, [i,i]=>i] => i" + succ :: "i\i" + rec :: "[i, i, [i,i]\i] \ i" (*Unions*) - inl :: "i=>i" - inr :: "i=>i" - when :: "[i, i=>i, i=>i]=>i" + inl :: "i\i" + inr :: "i\i" + when :: "[i, i\i, i\i]\i" (*General Sum and Binary Product*) - Sum :: "[t, i=>t]=>t" - fst :: "i=>i" - snd :: "i=>i" - split :: "[i, [i,i]=>i] =>i" + Sum :: "[t, i\t]\t" + fst :: "i\i" + snd :: "i\i" + split :: "[i, [i,i]\i] \i" (*General Product and Function Space*) - Prod :: "[t, i=>t]=>t" + Prod :: "[t, i\t]\t" (*Types*) - Plus :: "[t,t]=>t" (infixr "+" 40) + Plus :: "[t,t]\t" (infixr "+" 40) (*Equality type*) - Eq :: "[t,i,i]=>t" + Eq :: "[t,i,i]\t" eq :: "i" (*Judgements*) - Type :: "t => prop" ("(_ type)" [10] 5) - Eqtype :: "[t,t]=>prop" ("(_ =/ _)" [10,10] 5) - Elem :: "[i, t]=>prop" ("(_ /: _)" [10,10] 5) - Eqelem :: "[i,i,t]=>prop" ("(_ =/ _ :/ _)" [10,10,10] 5) - Reduce :: "[i,i]=>prop" ("Reduce[_,_]") + Type :: "t \ prop" ("(_ type)" [10] 5) + Eqtype :: "[t,t]\prop" ("(_ =/ _)" [10,10] 5) + Elem :: "[i, t]\prop" ("(_ /: _)" [10,10] 5) + Eqelem :: "[i,i,t]\prop" ("(_ =/ _ :/ _)" [10,10,10] 5) + Reduce :: "[i,i]\prop" ("Reduce[_,_]") (*Types*) (*Functions*) - lambda :: "(i => i) => i" (binder "lam " 10) - app :: "[i,i]=>i" (infixl "`" 60) + lambda :: "(i \ i) \ i" (binder "lam " 10) + app :: "[i,i]\i" (infixl "`" 60) (*Natural numbers*) Zero :: "i" ("0") (*Pairing*) - pair :: "[i,i]=>i" ("(1<_,/_>)") + pair :: "[i,i]\i" ("(1<_,/_>)") syntax - "_PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10) - "_SUM" :: "[idt,t,t]=>t" ("(3SUM _:_./ _)" 10) + "_PROD" :: "[idt,t,t]\t" ("(3PROD _:_./ _)" 10) + "_SUM" :: "[idt,t,t]\t" ("(3SUM _:_./ _)" 10) translations - "PROD x:A. B" == "CONST Prod(A, %x. B)" - "SUM x:A. B" == "CONST Sum(A, %x. B)" + "PROD x:A. B" == "CONST Prod(A, \x. B)" + "SUM x:A. B" == "CONST Sum(A, \x. B)" abbreviation - Arrow :: "[t,t]=>t" (infixr "-->" 30) where + Arrow :: "[t,t]\t" (infixr "-->" 30) where "A --> B == PROD _:A. B" abbreviation - Times :: "[t,t]=>t" (infixr "*" 50) where + Times :: "[t,t]\t" (infixr "*" 50) where "A * B == SUM _:A. B" notation (xsymbols) @@ -86,12 +86,12 @@ Times (infixr "\" 50) syntax (xsymbols) - "_PROD" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) - "_SUM" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) + "_PROD" :: "[idt,t,t] \ t" ("(3\ _\_./ _)" 10) + "_SUM" :: "[idt,t,t] \ t" ("(3\ _\_./ _)" 10) syntax (HTML output) - "_PROD" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) - "_SUM" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) + "_PROD" :: "[idt,t,t] \ t" ("(3\ _\_./ _)" 10) + "_SUM" :: "[idt,t,t] \ t" ("(3\ _\_./ _)" 10) (*Reduction: a weaker notion than equality; a hack for simplification. Reduce[a,b] means either that a=b:A for some A or else that "a" and "b" @@ -101,166 +101,158 @@ No new theorems can be proved about the standard judgements.*) axiomatization where refl_red: "\a. Reduce[a,a]" and - red_if_equal: "\a b A. a = b : A ==> Reduce[a,b]" and - trans_red: "\a b c A. [| a = b : A; Reduce[b,c] |] ==> a = c : A" and + red_if_equal: "\a b A. a = b : A \ Reduce[a,b]" and + trans_red: "\a b c A. \a = b : A; Reduce[b,c]\ \ a = c : A" and (*Reflexivity*) - refl_type: "\A. A type ==> A = A" and - refl_elem: "\a A. a : A ==> a = a : A" and + refl_type: "\A. A type \ A = A" and + refl_elem: "\a A. a : A \ a = a : A" and (*Symmetry*) - sym_type: "\A B. A = B ==> B = A" and - sym_elem: "\a b A. a = b : A ==> b = a : A" and + sym_type: "\A B. A = B \ B = A" and + sym_elem: "\a b A. a = b : A \ b = a : A" and (*Transitivity*) - trans_type: "\A B C. [| A = B; B = C |] ==> A = C" and - trans_elem: "\a b c A. [| a = b : A; b = c : A |] ==> a = c : A" and + trans_type: "\A B C. \A = B; B = C\ \ A = C" and + trans_elem: "\a b c A. \a = b : A; b = c : A\ \ a = c : A" and - equal_types: "\a A B. [| a : A; A = B |] ==> a : B" and - equal_typesL: "\a b A B. [| a = b : A; A = B |] ==> a = b : B" and + equal_types: "\a A B. \a : A; A = B\ \ a : B" and + equal_typesL: "\a b A B. \a = b : A; A = B\ \ a = b : B" and (*Substitution*) - subst_type: "\a A B. [| a : A; !!z. z:A ==> B(z) type |] ==> B(a) type" and - subst_typeL: "\a c A B D. [| a = c : A; !!z. z:A ==> B(z) = D(z) |] ==> B(a) = D(c)" and + subst_type: "\a A B. \a : A; \z. z:A \ B(z) type\ \ B(a) type" and + subst_typeL: "\a c A B D. \a = c : A; \z. z:A \ B(z) = D(z)\ \ B(a) = D(c)" and - subst_elem: "\a b A B. [| a : A; !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)" and + subst_elem: "\a b A B. \a : A; \z. z:A \ b(z):B(z)\ \ b(a):B(a)" and subst_elemL: - "\a b c d A B. [| a=c : A; !!z. z:A ==> b(z)=d(z) : B(z) |] ==> b(a)=d(c) : B(a)" and + "\a b c d A B. \a = c : A; \z. z:A \ b(z)=d(z) : B(z)\ \ b(a)=d(c) : B(a)" and (*The type N -- natural numbers*) NF: "N type" and NI0: "0 : N" and - NI_succ: "\a. a : N ==> succ(a) : N" and - NI_succL: "\a b. a = b : N ==> succ(a) = succ(b) : N" and + NI_succ: "\a. a : N \ succ(a) : N" and + NI_succL: "\a b. a = b : N \ succ(a) = succ(b) : N" and NE: - "\p a b C. [| p: N; a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] - ==> rec(p, a, %u v. b(u,v)) : C(p)" and + "\p a b C. \p: N; a: C(0); \u v. \u: N; v: C(u)\ \ b(u,v): C(succ(u))\ + \ rec(p, a, \u v. b(u,v)) : C(p)" and NEL: - "\p q a b c d C. [| p = q : N; a = c : C(0); - !!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |] - ==> rec(p, a, %u v. b(u,v)) = rec(q,c,d) : C(p)" and + "\p q a b c d C. \p = q : N; a = c : C(0); + \u v. \u: N; v: C(u)\ \ b(u,v) = d(u,v): C(succ(u))\ + \ rec(p, a, \u v. b(u,v)) = rec(q,c,d) : C(p)" and NC0: - "\a b C. [| a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] - ==> rec(0, a, %u v. b(u,v)) = a : C(0)" and + "\a b C. \a: C(0); \u v. \u: N; v: C(u)\ \ b(u,v): C(succ(u))\ + \ rec(0, a, \u v. b(u,v)) = a : C(0)" and NC_succ: - "\p a b C. [| p: N; a: C(0); - !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==> - rec(succ(p), a, %u v. b(u,v)) = b(p, rec(p, a, %u v. b(u,v))) : C(succ(p))" and + "\p a b C. \p: N; a: C(0); \u v. \u: N; v: C(u)\ \ b(u,v): C(succ(u))\ \ + rec(succ(p), a, \u v. b(u,v)) = b(p, rec(p, a, \u v. b(u,v))) : C(succ(p))" and (*The fourth Peano axiom. See page 91 of Martin-Lof's book*) - zero_ne_succ: - "\a. [| a: N; 0 = succ(a) : N |] ==> 0: F" and + zero_ne_succ: "\a. \a: N; 0 = succ(a) : N\ \ 0: F" and (*The Product of a family of types*) - ProdF: "\A B. [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type" and + ProdF: "\A B. \A type; \x. x:A \ B(x) type\ \ PROD x:A. B(x) type" and ProdFL: - "\A B C D. [| A = C; !!x. x:A ==> B(x) = D(x) |] ==> - PROD x:A. B(x) = PROD x:C. D(x)" and + "\A B C D. \A = C; \x. x:A \ B(x) = D(x)\ \ PROD x:A. B(x) = PROD x:C. D(x)" and ProdI: - "\b A B. [| A type; !!x. x:A ==> b(x):B(x)|] ==> lam x. b(x) : PROD x:A. B(x)" and + "\b A B. \A type; \x. x:A \ b(x):B(x)\ \ lam x. b(x) : PROD x:A. B(x)" and - ProdIL: - "\b c A B. [| A type; !!x. x:A ==> b(x) = c(x) : B(x)|] ==> - lam x. b(x) = lam x. c(x) : PROD x:A. B(x)" and + ProdIL: "\b c A B. \A type; \x. x:A \ b(x) = c(x) : B(x)\ \ + lam x. b(x) = lam x. c(x) : PROD x:A. B(x)" and - ProdE: "\p a A B. [| p : PROD x:A. B(x); a : A |] ==> p`a : B(a)" and - ProdEL: "\p q a b A B. [| p=q: PROD x:A. B(x); a=b : A |] ==> p`a = q`b : B(a)" and + ProdE: "\p a A B. \p : PROD x:A. B(x); a : A\ \ p`a : B(a)" and + ProdEL: "\p q a b A B. \p = q: PROD x:A. B(x); a = b : A\ \ p`a = q`b : B(a)" and - ProdC: - "\a b A B. [| a : A; !!x. x:A ==> b(x) : B(x)|] ==> - (lam x. b(x)) ` a = b(a) : B(a)" and + ProdC: "\a b A B. \a : A; \x. x:A \ b(x) : B(x)\ \ (lam x. b(x)) ` a = b(a) : B(a)" and - ProdC2: - "\p A B. p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)" and + ProdC2: "\p A B. p : PROD x:A. B(x) \ (lam x. p`x) = p : PROD x:A. B(x)" and (*The Sum of a family of types*) - SumF: "\A B. [| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type" and - SumFL: - "\A B C D. [| A = C; !!x. x:A ==> B(x) = D(x) |] ==> SUM x:A. B(x) = SUM x:C. D(x)" and + SumF: "\A B. \A type; \x. x:A \ B(x) type\ \ SUM x:A. B(x) type" and + SumFL: "\A B C D. \A = C; \x. x:A \ B(x) = D(x)\ \ SUM x:A. B(x) = SUM x:C. D(x)" and - SumI: "\a b A B. [| a : A; b : B(a) |] ==> : SUM x:A. B(x)" and - SumIL: "\a b c d A B. [| a=c:A; b=d:B(a) |] ==> = : SUM x:A. B(x)" and + SumI: "\a b A B. \a : A; b : B(a)\ \ : SUM x:A. B(x)" and + SumIL: "\a b c d A B. \ a = c : A; b = d : B(a)\ \ = : SUM x:A. B(x)" and - SumE: - "\p c A B C. [| p: SUM x:A. B(x); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C() |] - ==> split(p, %x y. c(x,y)) : C(p)" and + SumE: "\p c A B C. \p: SUM x:A. B(x); \x y. \x:A; y:B(x)\ \ c(x,y): C()\ + \ split(p, \x y. c(x,y)) : C(p)" and - SumEL: - "\p q c d A B C. [| p=q : SUM x:A. B(x); - !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C()|] - ==> split(p, %x y. c(x,y)) = split(q, % x y. d(x,y)) : C(p)" and + SumEL: "\p q c d A B C. \p = q : SUM x:A. B(x); + \x y. \x:A; y:B(x)\ \ c(x,y)=d(x,y): C()\ + \ split(p, \x y. c(x,y)) = split(q, \x y. d(x,y)) : C(p)" and - SumC: - "\a b c A B C. [| a: A; b: B(a); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C() |] - ==> split(, %x y. c(x,y)) = c(a,b) : C()" and + SumC: "\a b c A B C. \a: A; b: B(a); \x y. \x:A; y:B(x)\ \ c(x,y): C()\ + \ split(, \x y. c(x,y)) = c(a,b) : C()" and - fst_def: "\a. fst(a) == split(a, %x y. x)" and - snd_def: "\a. snd(a) == split(a, %x y. y)" and + fst_def: "\a. fst(a) == split(a, \x y. x)" and + snd_def: "\a. snd(a) == split(a, \x y. y)" and (*The sum of two types*) - PlusF: "\A B. [| A type; B type |] ==> A+B type" and - PlusFL: "\A B C D. [| A = C; B = D |] ==> A+B = C+D" and + PlusF: "\A B. \A type; B type\ \ A+B type" and + PlusFL: "\A B C D. \A = C; B = D\ \ A+B = C+D" and - PlusI_inl: "\a A B. [| a : A; B type |] ==> inl(a) : A+B" and - PlusI_inlL: "\a c A B. [| a = c : A; B type |] ==> inl(a) = inl(c) : A+B" and + PlusI_inl: "\a A B. \a : A; B type\ \ inl(a) : A+B" and + PlusI_inlL: "\a c A B. \a = c : A; B type\ \ inl(a) = inl(c) : A+B" and - PlusI_inr: "\b A B. [| A type; b : B |] ==> inr(b) : A+B" and - PlusI_inrL: "\b d A B. [| A type; b = d : B |] ==> inr(b) = inr(d) : A+B" and + PlusI_inr: "\b A B. \A type; b : B\ \ inr(b) : A+B" and + PlusI_inrL: "\b d A B. \A type; b = d : B\ \ inr(b) = inr(d) : A+B" and PlusE: - "\p c d A B C. [| p: A+B; !!x. x:A ==> c(x): C(inl(x)); - !!y. y:B ==> d(y): C(inr(y)) |] - ==> when(p, %x. c(x), %y. d(y)) : C(p)" and + "\p c d A B C. \p: A+B; + \x. x:A \ c(x): C(inl(x)); + \y. y:B \ d(y): C(inr(y)) \ \ when(p, \x. c(x), \y. d(y)) : C(p)" and PlusEL: - "\p q c d e f A B C. [| p = q : A+B; !!x. x: A ==> c(x) = e(x) : C(inl(x)); - !!y. y: B ==> d(y) = f(y) : C(inr(y)) |] - ==> when(p, %x. c(x), %y. d(y)) = when(q, %x. e(x), %y. f(y)) : C(p)" and + "\p q c d e f A B C. \p = q : A+B; + \x. x: A \ c(x) = e(x) : C(inl(x)); + \y. y: B \ d(y) = f(y) : C(inr(y))\ + \ when(p, \x. c(x), \y. d(y)) = when(q, \x. e(x), \y. f(y)) : C(p)" and PlusC_inl: - "\a c d A C. [| a: A; !!x. x:A ==> c(x): C(inl(x)); - !!y. y:B ==> d(y): C(inr(y)) |] - ==> when(inl(a), %x. c(x), %y. d(y)) = c(a) : C(inl(a))" and + "\a c d A C. \a: A; + \x. x:A \ c(x): C(inl(x)); + \y. y:B \ d(y): C(inr(y)) \ + \ when(inl(a), \x. c(x), \y. d(y)) = c(a) : C(inl(a))" and PlusC_inr: - "\b c d A B C. [| b: B; !!x. x:A ==> c(x): C(inl(x)); - !!y. y:B ==> d(y): C(inr(y)) |] - ==> when(inr(b), %x. c(x), %y. d(y)) = d(b) : C(inr(b))" and + "\b c d A B C. \b: B; + \x. x:A \ c(x): C(inl(x)); + \y. y:B \ d(y): C(inr(y))\ + \ when(inr(b), \x. c(x), \y. d(y)) = d(b) : C(inr(b))" and (*The type Eq*) - EqF: "\a b A. [| A type; a : A; b : A |] ==> Eq(A,a,b) type" and - EqFL: "\a b c d A B. [| A=B; a=c: A; b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d)" and - EqI: "\a b A. a = b : A ==> eq : Eq(A,a,b)" and - EqE: "\p a b A. p : Eq(A,a,b) ==> a = b : A" and + EqF: "\a b A. \A type; a : A; b : A\ \ Eq(A,a,b) type" and + EqFL: "\a b c d A B. \A = B; a = c : A; b = d : A\ \ Eq(A,a,b) = Eq(B,c,d)" and + EqI: "\a b A. a = b : A \ eq : Eq(A,a,b)" and + EqE: "\p a b A. p : Eq(A,a,b) \ a = b : A" and (*By equality of types, can prove C(p) from C(eq), an elimination rule*) - EqC: "\p a b A. p : Eq(A,a,b) ==> p = eq : Eq(A,a,b)" and + EqC: "\p a b A. p : Eq(A,a,b) \ p = eq : Eq(A,a,b)" and (*The type F*) FF: "F type" and - FE: "\p C. [| p: F; C type |] ==> contr(p) : C" and - FEL: "\p q C. [| p = q : F; C type |] ==> contr(p) = contr(q) : C" and + FE: "\p C. \p: F; C type\ \ contr(p) : C" and + FEL: "\p q C. \p = q : F; C type\ \ contr(p) = contr(q) : C" and (*The type T Martin-Lof's book (page 68) discusses elimination and computation. @@ -270,9 +262,9 @@ TF: "T type" and TI: "tt : T" and - TE: "\p c C. [| p : T; c : C(tt) |] ==> c : C(p)" and - TEL: "\p q c d C. [| p = q : T; c = d : C(tt) |] ==> c = d : C(p)" and - TC: "\p. p : T ==> p = tt : T" + TE: "\p c C. \p : T; c : C(tt)\ \ c : C(p)" and + TEL: "\p q c d C. \p = q : T; c = d : C(tt)\ \ c = d : C(p)" and + TC: "\p. p : T \ p = tt : T" subsection "Tactics and derived rules for Constructive Type Theory" @@ -302,7 +294,7 @@ lemmas basic_defs = fst_def snd_def (*Compare with standard version: B is applied to UNSIMPLIFIED expression! *) -lemma SumIL2: "[| c=a : A; d=b : B(a) |] ==> = : Sum(A,B)" +lemma SumIL2: "\c = a : A; d = b : B(a)\ \ = : Sum(A,B)" apply (rule sym_elem) apply (rule SumIL) apply (rule_tac [!] sym_elem) @@ -316,7 +308,7 @@ lemma subst_prodE: assumes "p: Prod(A,B)" and "a: A" - and "!!z. z: B(a) ==> c(z): C(z)" + and "\z. z: B(a) \ c(z): C(z)" shows "c(p`a): C(p`a)" apply (rule assms ProdE)+ done @@ -378,14 +370,18 @@ REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac (thms @ equal_rls) 3)) end +*} -*} +method_setup form = {* Scan.succeed (fn ctxt => SIMPLE_METHOD (form_tac ctxt)) *} +method_setup typechk = {* Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (typechk_tac ctxt ths)) *} +method_setup intr = {* Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (intr_tac ctxt ths)) *} +method_setup equal = {* Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (equal_tac ctxt ths)) *} subsection {* Simplification *} (*To simplify the type in a goal*) -lemma replace_type: "[| B = A; a : A |] ==> a : B" +lemma replace_type: "\B = A; a : A\ \ a : B" apply (rule equal_types) apply (rule_tac [2] sym_type) apply assumption+ @@ -394,7 +390,7 @@ (*Simplify the parameter of a unary type operator.*) lemma subst_eqtyparg: assumes 1: "a=c : A" - and 2: "!!z. z:A ==> B(z) type" + and 2: "\z. z:A \ B(z) type" shows "B(a)=B(c)" apply (rule subst_typeL) apply (rule_tac [2] refl_type) @@ -460,12 +456,21 @@ fun pc_tac ctxt thms = DEPTH_SOLVE_1 o (step_tac ctxt thms) *} +method_setup eqintr = {* Scan.succeed (SIMPLE_METHOD o eqintr_tac) *} +method_setup NE = {* + Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s)) +*} +method_setup pc = {* Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths)) *} +method_setup add_mp = {* Scan.succeed (SIMPLE_METHOD' o add_mp_tac) *} + ML_file "rew.ML" +method_setup rew = {* Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (rew_tac ctxt ths)) *} +method_setup hyp_rew = {* Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_rew_tac ctxt ths)) *} subsection {* The elimination rules for fst/snd *} -lemma SumE_fst: "p : Sum(A,B) ==> fst(p) : A" +lemma SumE_fst: "p : Sum(A,B) \ fst(p) : A" apply (unfold basic_defs) apply (erule SumE) apply assumption @@ -475,12 +480,12 @@ lemma SumE_snd: assumes major: "p: Sum(A,B)" and "A type" - and "!!x. x:A ==> B(x) type" + and "\x. x:A \ B(x) type" shows "snd(p) : B(fst(p))" apply (unfold basic_defs) apply (rule major [THEN SumE]) apply (rule SumC [THEN subst_eqtyparg, THEN replace_type]) - apply (tactic {* typechk_tac @{context} @{thms assms} *}) + apply (typechk assms) done end diff -r 2f65dcd32a59 -r 51890cb80b30 src/CTT/ROOT --- a/src/CTT/ROOT Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CTT/ROOT Tue Nov 11 21:14:19 2014 +0100 @@ -17,14 +17,11 @@ 1991) *} options [document = false] - theories Main + theories + Main -session "CTT-ex" in ex = CTT + - description {* - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge - - Examples for Constructive Type Theory. - *} - options [document = false] - theories Typechecking Elimination Equality Synthesis + (* Examples for Constructive Type Theory *) + "ex/Typechecking" + "ex/Elimination" + "ex/Equality" + "ex/Synthesis" diff -r 2f65dcd32a59 -r 51890cb80b30 src/CTT/ex/Elimination.thy --- a/src/CTT/ex/Elimination.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CTT/ex/Elimination.thy Tue Nov 11 21:14:19 2014 +0100 @@ -9,123 +9,123 @@ section "Examples with elimination rules" theory Elimination -imports CTT +imports "../CTT" begin text "This finds the functions fst and snd!" -schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A" -apply (tactic {* pc_tac @{context} [] 1 *}) +schematic_lemma [folded basic_defs]: "A type \ ?a : (A*A) --> A" +apply pc done -schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A" -apply (tactic {* pc_tac @{context} [] 1 *}) +schematic_lemma [folded basic_defs]: "A type \ ?a : (A*A) --> A" +apply pc back done text "Double negation of the Excluded Middle" -schematic_lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F" -apply (tactic "intr_tac @{context} []") +schematic_lemma "A type \ ?a : ((A + (A-->F)) --> F) --> F" +apply intr apply (rule ProdE) apply assumption -apply (tactic "pc_tac @{context} [] 1") +apply pc done -schematic_lemma "[| A type; B type |] ==> ?a : (A*B) --> (B*A)" -apply (tactic "pc_tac @{context} [] 1") +schematic_lemma "\A type; B type\ \ ?a : (A*B) \ (B*A)" +apply pc done (*The sequent version (ITT) could produce an interesting alternative by backtracking. No longer.*) text "Binary sums and products" -schematic_lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)" -apply (tactic "pc_tac @{context} [] 1") +schematic_lemma "\A type; B type; C type\ \ ?a : (A+B --> C) --> (A-->C) * (B-->C)" +apply pc done (*A distributive law*) -schematic_lemma "[| A type; B type; C type |] ==> ?a : A * (B+C) --> (A*B + A*C)" -apply (tactic "pc_tac @{context} [] 1") +schematic_lemma "\A type; B type; C type\ \ ?a : A * (B+C) --> (A*B + A*C)" +apply pc done (*more general version, same proof*) schematic_lemma assumes "A type" - and "!!x. x:A ==> B(x) type" - and "!!x. x:A ==> C(x) type" + and "\x. x:A \ B(x) type" + and "\x. x:A \ C(x) type" shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))" -apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) +apply (pc assms) done text "Construction of the currying functional" -schematic_lemma "[| A type; B type; C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))" -apply (tactic "pc_tac @{context} [] 1") +schematic_lemma "\A type; B type; C type\ \ ?a : (A*B --> C) --> (A--> (B-->C))" +apply pc done (*more general goal with same proof*) schematic_lemma assumes "A type" - and "!!x. x:A ==> B(x) type" - and "!!z. z: (SUM x:A. B(x)) ==> C(z) type" + and "\x. x:A \ B(x) type" + and "\z. z: (SUM x:A. B(x)) \ C(z) type" shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). (PROD x:A . PROD y:B(x) . C())" -apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) +apply (pc assms) done text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)" -schematic_lemma "[| A type; B type; C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)" -apply (tactic "pc_tac @{context} [] 1") +schematic_lemma "\A type; B type; C type\ \ ?a : (A --> (B-->C)) --> (A*B --> C)" +apply pc done (*more general goal with same proof*) schematic_lemma assumes "A type" - and "!!x. x:A ==> B(x) type" - and "!!z. z: (SUM x:A . B(x)) ==> C(z) type" + and "\x. x:A \ B(x) type" + and "\z. z: (SUM x:A . B(x)) \ C(z) type" shows "?a : (PROD x:A . PROD y:B(x) . C()) --> (PROD z : (SUM x:A . B(x)) . C(z))" -apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) +apply (pc assms) done text "Function application" -schematic_lemma "[| A type; B type |] ==> ?a : ((A --> B) * A) --> B" -apply (tactic "pc_tac @{context} [] 1") +schematic_lemma "\A type; B type\ \ ?a : ((A --> B) * A) --> B" +apply pc done text "Basic test of quantifier reasoning" schematic_lemma assumes "A type" and "B type" - and "!!x y.[| x:A; y:B |] ==> C(x,y) type" + and "\x y. \x:A; y:B\ \ C(x,y) type" shows "?a : (SUM y:B . PROD x:A . C(x,y)) --> (PROD x:A . SUM y:B . C(x,y))" -apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) +apply (pc assms) done text "Martin-Lof (1984) pages 36-7: the combinator S" schematic_lemma assumes "A type" - and "!!x. x:A ==> B(x) type" - and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type" + and "\x. x:A \ B(x) type" + and "\x y. \x:A; y:B(x)\ \ C(x,y) type" shows "?a : (PROD x:A. PROD y:B(x). C(x,y)) --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))" -apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) +apply (pc assms) done text "Martin-Lof (1984) page 58: the axiom of disjunction elimination" schematic_lemma assumes "A type" and "B type" - and "!!z. z: A+B ==> C(z) type" + and "\z. z: A+B \ C(z) type" shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y))) --> (PROD z: A+B. C(z))" -apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) +apply (pc assms) done (*towards AXIOM OF CHOICE*) schematic_lemma [folded basic_defs]: - "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)" -apply (tactic "pc_tac @{context} [] 1") + "\A type; B type; C type\ \ ?a : (A --> B*C) --> (A-->B) * (A-->C)" +apply pc done @@ -133,61 +133,64 @@ text "AXIOM OF CHOICE! Delicate use of elimination rules" schematic_lemma assumes "A type" - and "!!x. x:A ==> B(x) type" - and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type" + and "\x. x:A \ B(x) type" + and "\x y. \x:A; y:B(x)\ \ C(x,y) type" shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))" -apply (tactic {* intr_tac @{context} @{thms assms} *}) -apply (tactic "add_mp_tac @{context} 2") -apply (tactic "add_mp_tac @{context} 1") +apply (intr assms) +prefer 2 apply add_mp +prefer 2 apply add_mp apply (erule SumE_fst) apply (rule replace_type) apply (rule subst_eqtyparg) apply (rule comp_rls) apply (rule_tac [4] SumE_snd) -apply (tactic {* typechk_tac @{context} (@{thm SumE_fst} :: @{thms assms}) *}) +apply (typechk SumE_fst assms) done text "Axiom of choice. Proof without fst, snd. Harder still!" schematic_lemma [folded basic_defs]: assumes "A type" - and "!!x. x:A ==> B(x) type" - and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type" + and "\x. x:A \ B(x) type" + and "\x y. \x:A; y:B(x)\ \ C(x,y) type" shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))" -apply (tactic {* intr_tac @{context} @{thms assms} *}) -(*Must not use add_mp_tac as subst_prodE hides the construction.*) -apply (rule ProdE [THEN SumE], assumption) -apply (tactic "TRYALL (assume_tac @{context})") +apply (intr assms) +(*Must not use add_mp as subst_prodE hides the construction.*) +apply (rule ProdE [THEN SumE]) +apply assumption +apply assumption +apply assumption apply (rule replace_type) apply (rule subst_eqtyparg) apply (rule comp_rls) apply (erule_tac [4] ProdE [THEN SumE]) -apply (tactic {* typechk_tac @{context} @{thms assms} *}) +apply (typechk assms) apply (rule replace_type) apply (rule subst_eqtyparg) apply (rule comp_rls) -apply (tactic {* typechk_tac @{context} @{thms assms} *}) +apply (typechk assms) apply assumption done text "Example of sequent_style deduction" (*When splitting z:A*B, the assumption C(z) is affected; ?a becomes - lam u. split(u,%v w.split(v,%x y.lam z. >) ` w) *) + lam u. split(u,\v w.split(v,\x y.lam z. >) ` w) *) schematic_lemma assumes "A type" and "B type" - and "!!z. z:A*B ==> C(z) type" + and "\z. z:A*B \ C(z) type" shows "?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C())" apply (rule intr_rls) apply (tactic {* biresolve_tac safe_brls 2 *}) (*Now must convert assumption C(z) into antecedent C() *) apply (rule_tac [2] a = "y" in ProdE) -apply (tactic {* typechk_tac @{context} @{thms assms} *}) +apply (typechk assms) apply (rule SumE, assumption) -apply (tactic "intr_tac @{context} []") -apply (tactic "TRYALL (assume_tac @{context})") -apply (tactic {* typechk_tac @{context} @{thms assms} *}) +apply intr +defer 1 +apply assumption+ +apply (typechk assms) done end diff -r 2f65dcd32a59 -r 51890cb80b30 src/CTT/ex/Equality.thy --- a/src/CTT/ex/Equality.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CTT/ex/Equality.thy Tue Nov 11 21:14:19 2014 +0100 @@ -6,64 +6,63 @@ section "Equality reasoning by rewriting" theory Equality -imports CTT +imports "../CTT" begin -lemma split_eq: "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)" +lemma split_eq: "p : Sum(A,B) \ split(p,pair) = p : Sum(A,B)" apply (rule EqE) apply (rule elim_rls, assumption) -apply (tactic "rew_tac @{context} []") +apply rew done -lemma when_eq: "[| A type; B type; p : A+B |] ==> when(p,inl,inr) = p : A + B" +lemma when_eq: "\A type; B type; p : A+B\ \ when(p,inl,inr) = p : A + B" apply (rule EqE) apply (rule elim_rls, assumption) -apply (tactic "rew_tac @{context} []") +apply rew done (*in the "rec" formulation of addition, 0+n=n *) -lemma "p:N ==> rec(p,0, %y z. succ(y)) = p : N" +lemma "p:N \ rec(p,0, \y z. succ(y)) = p : N" apply (rule EqE) apply (rule elim_rls, assumption) -apply (tactic "rew_tac @{context} []") +apply rew done (*the harder version, n+0=n: recursive, uses induction hypothesis*) -lemma "p:N ==> rec(p,0, %y z. succ(z)) = p : N" +lemma "p:N \ rec(p,0, \y z. succ(z)) = p : N" apply (rule EqE) apply (rule elim_rls, assumption) -apply (tactic "hyp_rew_tac @{context} []") +apply hyp_rew done (*Associativity of addition*) -lemma "[| a:N; b:N; c:N |] - ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) = - rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N" -apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic "hyp_rew_tac @{context} []") +lemma "\a:N; b:N; c:N\ + \ rec(rec(a, b, \x y. succ(y)), c, \x y. succ(y)) = + rec(a, rec(b, c, \x y. succ(y)), \x y. succ(y)) : N" +apply (NE a) +apply hyp_rew done (*Martin-Lof (1984) page 62: pairing is surjective*) -lemma "p : Sum(A,B) ==> = p : Sum(A,B)" +lemma "p : Sum(A,B) \ x y. x), split(p,\x y. y)> = p : Sum(A,B)" apply (rule EqE) apply (rule elim_rls, assumption) apply (tactic {* DEPTH_SOLVE_1 (rew_tac @{context} []) *}) (*!!!!!!!*) done -lemma "[| a : A; b : B |] ==> - (lam u. split(u, %v w.)) ` = : SUM x:B. A" -apply (tactic "rew_tac @{context} []") +lemma "\a : A; b : B\ \ (lam u. split(u, \v w.)) ` = : SUM x:B. A" +apply rew done (*a contrived, complicated simplication, requires sum-elimination also*) -lemma "(lam f. lam x. f`(f`x)) ` (lam u. split(u, %v w.)) = +lemma "(lam f. lam x. f`(f`x)) ` (lam u. split(u, \v w.)) = lam x. x : PROD x:(SUM y:N. N). (SUM y:N. N)" apply (rule reduction_rls) apply (rule_tac [3] intrL_rls) apply (rule_tac [4] EqE) -apply (rule_tac [4] SumE, tactic "assume_tac @{context} 4") +apply (erule_tac [4] SumE) (*order of unifiers is essential here*) -apply (tactic "rew_tac @{context} []") +apply rew done end diff -r 2f65dcd32a59 -r 51890cb80b30 src/CTT/ex/Synthesis.thy --- a/src/CTT/ex/Synthesis.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CTT/ex/Synthesis.thy Tue Nov 11 21:14:19 2014 +0100 @@ -6,27 +6,27 @@ section "Synthesis examples, using a crude form of narrowing" theory Synthesis -imports Arith +imports "../Arith" begin text "discovery of predecessor function" schematic_lemma "?a : SUM pred:?A . Eq(N, pred`0, 0) * (PROD n:N. Eq(N, pred ` succ(n), n))" -apply (tactic "intr_tac @{context} []") -apply (tactic "eqintr_tac @{context}") +apply intr +apply eqintr apply (rule_tac [3] reduction_rls) apply (rule_tac [5] comp_rls) -apply (tactic "rew_tac @{context} []") +apply rew done text "the function fst as an element of a function type" schematic_lemma [folded basic_defs]: - "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` , i)" -apply (tactic "intr_tac @{context} []") -apply (tactic "eqintr_tac @{context}") + "A type \ ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` , i)" +apply intr +apply eqintr apply (rule_tac [2] reduction_rls) apply (rule_tac [4] comp_rls) -apply (tactic "typechk_tac @{context} []") +apply typechk txt "now put in A everywhere" apply assumption+ done @@ -36,10 +36,10 @@ See following example.*) schematic_lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>) * Eq(?A, ?b(inr(i)), )" -apply (tactic "intr_tac @{context} []") -apply (tactic "eqintr_tac @{context}") +apply intr +apply eqintr apply (rule comp_rls) -apply (tactic "rew_tac @{context} []") +apply rew done (*Here we allow the type to depend on i. @@ -55,13 +55,13 @@ schematic_lemma [folded basic_defs]: "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl()), i) * Eq(?A, ?b(inr()), j)" -apply (tactic "intr_tac @{context} []") -apply (tactic "eqintr_tac @{context}") +apply intr +apply eqintr apply (rule PlusC_inl [THEN trans_elem]) apply (rule_tac [4] comp_rls) apply (rule_tac [7] reduction_rls) apply (rule_tac [10] comp_rls) -apply (tactic "typechk_tac @{context} []") +apply typechk done (*similar but allows the type to depend on i and j*) @@ -79,10 +79,10 @@ schematic_lemma [folded arith_defs]: "?c : PROD n:N. Eq(N, ?f(0,n), n) * (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))" -apply (tactic "intr_tac @{context} []") -apply (tactic "eqintr_tac @{context}") +apply intr +apply eqintr apply (rule comp_rls) -apply (tactic "rew_tac @{context} []") +apply rew done text "The addition function -- using explicit lambdas" @@ -90,15 +90,15 @@ "?c : SUM plus : ?A . PROD x:N. Eq(N, plus`0`x, x) * (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))" -apply (tactic "intr_tac @{context} []") -apply (tactic "eqintr_tac @{context}") +apply intr +apply eqintr apply (tactic "resolve_tac [TSimp.split_eqn] 3") apply (tactic "SELECT_GOAL (rew_tac @{context} []) 4") apply (tactic "resolve_tac [TSimp.split_eqn] 3") apply (tactic "SELECT_GOAL (rew_tac @{context} []) 4") apply (rule_tac [3] p = "y" in NC_succ) (** by (resolve_tac comp_rls 3); caused excessive branching **) -apply (tactic "rew_tac @{context} []") +apply rew done end diff -r 2f65dcd32a59 -r 51890cb80b30 src/CTT/ex/Typechecking.thy --- a/src/CTT/ex/Typechecking.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/CTT/ex/Typechecking.thy Tue Nov 11 21:14:19 2014 +0100 @@ -6,7 +6,7 @@ section "Easy examples: type checking and type deduction" theory Typechecking -imports CTT +imports "../CTT" begin subsection {* Single-step proofs: verifying that a type is well-formed *} @@ -34,54 +34,54 @@ subsection {* Multi-step proofs: Type inference *} lemma "PROD w:N. N + N type" -apply (tactic "form_tac @{context}") +apply form done schematic_lemma "<0, succ(0)> : ?A" -apply (tactic "intr_tac @{context} []") +apply intr done schematic_lemma "PROD w:N . Eq(?A,w,w) type" -apply (tactic "typechk_tac @{context} []") +apply typechk done schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type" -apply (tactic "typechk_tac @{context} []") +apply typechk done text "typechecking an application of fst" -schematic_lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A" -apply (tactic "typechk_tac @{context} []") +schematic_lemma "(lam u. split(u, \v w. v)) ` <0, succ(0)> : ?A" +apply typechk done text "typechecking the predecessor function" -schematic_lemma "lam n. rec(n, 0, %x y. x) : ?A" -apply (tactic "typechk_tac @{context} []") +schematic_lemma "lam n. rec(n, 0, \x y. x) : ?A" +apply typechk done text "typechecking the addition function" -schematic_lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A" -apply (tactic "typechk_tac @{context} []") +schematic_lemma "lam n. lam m. rec(n, m, \x y. succ(y)) : ?A" +apply typechk done (*Proofs involving arbitrary types. For concreteness, every type variable left over is forced to be N*) -ML {* val N_tac = TRYALL (rtac @{thm NF}) *} +method_setup N = {* Scan.succeed (fn _ => SIMPLE_METHOD (TRYALL (resolve_tac @{thms NF}))) *} schematic_lemma "lam w. : ?A" -apply (tactic "typechk_tac @{context} []") -apply (tactic N_tac) +apply typechk +apply N done schematic_lemma "lam x. lam y. x : ?A" -apply (tactic "typechk_tac @{context} []") -apply (tactic N_tac) +apply typechk +apply N done text "typechecking fst (as a function object)" -schematic_lemma "lam i. split(i, %j k. j) : ?A" -apply (tactic "typechk_tac @{context} []") -apply (tactic N_tac) +schematic_lemma "lam i. split(i, \j k. j) : ?A" +apply typechk +apply N done end diff -r 2f65dcd32a59 -r 51890cb80b30 src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Doc/antiquote_setup.ML Tue Nov 11 21:14:19 2014 +0100 @@ -90,7 +90,7 @@ else txt1 ^ " : " ^ txt2; val txt' = if kind = "" then txt else kind ^ " " ^ txt; - val pos = #pos source1; + val (pos, _) = #range source1; val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2)) handle ERROR msg => error (msg ^ Position.here pos); diff -r 2f65dcd32a59 -r 51890cb80b30 src/HOL/ex/Cartouche_Examples.thy --- a/src/HOL/ex/Cartouche_Examples.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/HOL/ex/Cartouche_Examples.thy Tue Nov 11 21:14:19 2014 +0100 @@ -146,7 +146,8 @@ ML_Lex.read Position.none "fn _ => (" @ ML_Lex.read_source false source @ ML_Lex.read Position.none ");"; - val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) toks; + val (pos, _) = #range source; + val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags pos toks; in "" end); *} @@ -213,7 +214,7 @@ fun ml_tactic source ctxt = let val ctxt' = ctxt |> Context.proof_map - (ML_Context.expression (#pos source) + (ML_Context.expression (#range source) "fun tactic (ctxt : Proof.context) : tactic" "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read_source false source)); in Data.get ctxt' ctxt end; diff -r 2f65dcd32a59 -r 51890cb80b30 src/LCF/LCF.thy --- a/src/LCF/LCF.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/LCF/LCF.thy Tue Nov 11 21:14:19 2014 +0100 @@ -31,28 +31,28 @@ UU :: "'a" TT :: "tr" FF :: "tr" - FIX :: "('a => 'a) => 'a" - FST :: "'a*'b => 'a" - SND :: "'a*'b => 'b" - INL :: "'a => 'a+'b" - INR :: "'b => 'a+'b" - WHEN :: "['a=>'c, 'b=>'c, 'a+'b] => 'c" - adm :: "('a => o) => o" + FIX :: "('a \ 'a) \ 'a" + FST :: "'a*'b \ 'a" + SND :: "'a*'b \ 'b" + INL :: "'a \ 'a+'b" + INR :: "'b \ 'a+'b" + WHEN :: "['a\'c, 'b\'c, 'a+'b] \ 'c" + adm :: "('a \ o) \ o" VOID :: "void" ("'(')") - PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100) - COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ |/ _))" [60,60,60] 60) - less :: "['a,'a] => o" (infixl "<<" 50) + PAIR :: "['a,'b] \ 'a*'b" ("(1<_,/_>)" [0,0] 100) + COND :: "[tr,'a,'a] \ 'a" ("(_ \/ (_ |/ _))" [60,60,60] 60) + less :: "['a,'a] \ o" (infixl "<<" 50) axiomatization where (** DOMAIN THEORY **) - eq_def: "x=y == x << y & y << x" and + eq_def: "x=y == x << y \ y << x" and - less_trans: "[| x << y; y << z |] ==> x << z" and + less_trans: "\x << y; y << z\ \ x << z" and - less_ext: "(ALL x. f(x) << g(x)) ==> f << g" and + less_ext: "(\x. f(x) << g(x)) \ f << g" and - mono: "[| f << g; x << y |] ==> f(x) << g(y)" and + mono: "\f << g; x << y\ \ f(x) << g(y)" and minimal: "UU << x" and @@ -61,16 +61,16 @@ axiomatization where (** TR **) - tr_cases: "p=UU | p=TT | p=FF" and + tr_cases: "p=UU \ p=TT \ p=FF" and - not_TT_less_FF: "~ TT << FF" and - not_FF_less_TT: "~ FF << TT" and - not_TT_less_UU: "~ TT << UU" and - not_FF_less_UU: "~ FF << UU" and + not_TT_less_FF: "\ TT << FF" and + not_FF_less_TT: "\ FF << TT" and + not_TT_less_UU: "\ TT << UU" and + not_FF_less_UU: "\ FF << UU" and - COND_UU: "UU => x | y = UU" and - COND_TT: "TT => x | y = x" and - COND_FF: "FF => x | y = y" + COND_UU: "UU \ x | y = UU" and + COND_TT: "TT \ x | y = x" and + COND_FF: "FF \ x | y = y" axiomatization where (** PAIRS **) @@ -83,18 +83,18 @@ axiomatization where (*** STRICT SUM ***) - INL_DEF: "~x=UU ==> ~INL(x)=UU" and - INR_DEF: "~x=UU ==> ~INR(x)=UU" and + INL_DEF: "\x=UU \ \INL(x)=UU" and + INR_DEF: "\x=UU \ \INR(x)=UU" and INL_STRICT: "INL(UU) = UU" and INR_STRICT: "INR(UU) = UU" and WHEN_UU: "WHEN(f,g,UU) = UU" and - WHEN_INL: "~x=UU ==> WHEN(f,g,INL(x)) = f(x)" and - WHEN_INR: "~x=UU ==> WHEN(f,g,INR(x)) = g(x)" and + WHEN_INL: "\x=UU \ WHEN(f,g,INL(x)) = f(x)" and + WHEN_INR: "\x=UU \ WHEN(f,g,INR(x)) = g(x)" and SUM_EXHAUSTION: - "z = UU | (EX x. ~x=UU & z = INL(x)) | (EX y. ~y=UU & z = INR(y))" + "z = UU \ (\x. \x=UU \ z = INL(x)) \ (\y. \y=UU \ z = INR(y))" axiomatization where (** VOID **) @@ -104,7 +104,7 @@ (** INDUCTION **) axiomatization where - induct: "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))" + induct: "\adm(P); P(UU); \x. P(x) \ P(f(x))\ \ P(FIX(f))" axiomatization where (** Admissibility / Chain Completeness **) @@ -112,20 +112,20 @@ Note that "easiness" of types is not taken into account because it cannot be expressed schematically; flatness could be. *) - adm_less: "\t u. adm(%x. t(x) << u(x))" and - adm_not_less: "\t u. adm(%x.~ t(x) << u)" and - adm_not_free: "\A. adm(%x. A)" and - adm_subst: "\P t. adm(P) ==> adm(%x. P(t(x)))" and - adm_conj: "\P Q. [| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))" and - adm_disj: "\P Q. [| adm(P); adm(Q) |] ==> adm(%x. P(x)|Q(x))" and - adm_imp: "\P Q. [| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))" and - adm_all: "\P. (!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))" + adm_less: "\t u. adm(\x. t(x) << u(x))" and + adm_not_less: "\t u. adm(\x.\ t(x) << u)" and + adm_not_free: "\A. adm(\x. A)" and + adm_subst: "\P t. adm(P) \ adm(\x. P(t(x)))" and + adm_conj: "\P Q. \adm(P); adm(Q)\ \ adm(\x. P(x)\Q(x))" and + adm_disj: "\P Q. \adm(P); adm(Q)\ \ adm(\x. P(x)\Q(x))" and + adm_imp: "\P Q. \adm(\x.\P(x)); adm(Q)\ \ adm(\x. P(x)\Q(x))" and + adm_all: "\P. (\y. adm(P(y))) \ adm(\x. \y. P(y,x))" -lemma eq_imp_less1: "x = y ==> x << y" +lemma eq_imp_less1: "x = y \ x << y" by (simp add: eq_def) -lemma eq_imp_less2: "x = y ==> y << x" +lemma eq_imp_less2: "x = y \ y << x" by (simp add: eq_def) lemma less_refl [simp]: "x << x" @@ -133,37 +133,37 @@ apply (rule refl) done -lemma less_anti_sym: "[| x << y; y << x |] ==> x=y" +lemma less_anti_sym: "\x << y; y << x\ \ x=y" by (simp add: eq_def) -lemma ext: "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))" +lemma ext: "(\x::'a::cpo. f(x)=(g(x)::'b::cpo)) \ (\x. f(x))=(\x. g(x))" apply (rule less_anti_sym) apply (rule less_ext) apply simp apply simp done -lemma cong: "[| f=g; x=y |] ==> f(x)=g(y)" +lemma cong: "\f = g; x = y\ \ f(x)=g(y)" by simp -lemma less_ap_term: "x << y ==> f(x) << f(y)" +lemma less_ap_term: "x << y \ f(x) << f(y)" by (rule less_refl [THEN mono]) -lemma less_ap_thm: "f << g ==> f(x) << g(x)" +lemma less_ap_thm: "f << g \ f(x) << g(x)" by (rule less_refl [THEN [2] mono]) -lemma ap_term: "(x::'a::cpo) = y ==> (f(x)::'b::cpo) = f(y)" +lemma ap_term: "(x::'a::cpo) = y \ (f(x)::'b::cpo) = f(y)" apply (rule cong [OF refl]) apply simp done -lemma ap_thm: "f = g ==> f(x) = g(x)" +lemma ap_thm: "f = g \ f(x) = g(x)" apply (erule cong) apply (rule refl) done -lemma UU_abs: "(%x::'a::cpo. UU) = UU" +lemma UU_abs: "(\x::'a::cpo. UU) = UU" apply (rule less_anti_sym) prefer 2 apply (rule minimal) @@ -175,28 +175,28 @@ lemma UU_app: "UU(x) = UU" by (rule UU_abs [symmetric, THEN ap_thm]) -lemma less_UU: "x << UU ==> x=UU" +lemma less_UU: "x << UU \ x=UU" apply (rule less_anti_sym) apply assumption apply (rule minimal) done -lemma tr_induct: "[| P(UU); P(TT); P(FF) |] ==> ALL b. P(b)" +lemma tr_induct: "\P(UU); P(TT); P(FF)\ \ \b. P(b)" apply (rule allI) apply (rule mp) apply (rule_tac [2] p = b in tr_cases) apply blast done -lemma Contrapos: "~ B ==> (A ==> B) ==> ~A" +lemma Contrapos: "\ B \ (A \ B) \ \A" by blast -lemma not_less_imp_not_eq1: "~ x << y \ x \ y" +lemma not_less_imp_not_eq1: "\ x << y \ x \ y" apply (erule Contrapos) apply simp done -lemma not_less_imp_not_eq2: "~ y << x \ x \ y" +lemma not_less_imp_not_eq2: "\ y << x \ x \ y" apply (erule Contrapos) apply simp done @@ -216,7 +216,7 @@ lemma COND_cases_iff [rule_format]: - "ALL b. P(b=>x|y) <-> (b=UU-->P(UU)) & (b=TT-->P(x)) & (b=FF-->P(y))" + "\b. P(b\x|y) \ (b=UU\P(UU)) \ (b=TT\P(x)) \ (b=FF\P(y))" apply (insert not_UU_eq_TT not_UU_eq_FF not_TT_eq_UU not_TT_eq_FF not_FF_eq_UU not_FF_eq_TT) apply (rule tr_induct) @@ -229,7 +229,7 @@ done lemma COND_cases: - "[| x = UU --> P(UU); x = TT --> P(xa); x = FF --> P(y) |] ==> P(x => xa | y)" + "\x = UU \ P(UU); x = TT \ P(xa); x = FF \ P(y)\ \ P(x \ xa | y)" apply (rule COND_cases_iff [THEN iffD2]) apply blast done @@ -247,7 +247,7 @@ subsection {* Ordered pairs and products *} -lemma expand_all_PROD: "(ALL p. P(p)) <-> (ALL x y. P())" +lemma expand_all_PROD: "(\p. P(p)) \ (\x y. P())" apply (rule iffI) apply blast apply (rule allI) @@ -255,7 +255,7 @@ apply blast done -lemma PROD_less: "(p::'a*'b) << q <-> FST(p) << FST(q) & SND(p) << SND(q)" +lemma PROD_less: "(p::'a*'b) << q \ FST(p) << FST(q) \ SND(p) << SND(q)" apply (rule iffI) apply (rule conjI) apply (erule less_ap_term) @@ -266,17 +266,17 @@ apply (rule mono, erule less_ap_term, assumption) done -lemma PROD_eq: "p=q <-> FST(p)=FST(q) & SND(p)=SND(q)" +lemma PROD_eq: "p=q \ FST(p)=FST(q) \ SND(p)=SND(q)" apply (rule iffI) apply simp apply (unfold eq_def) apply (simp add: PROD_less) done -lemma PAIR_less [simp]: " << <-> a< << \ a< b< = <-> a=c & b=d" +lemma PAIR_eq [simp]: " = \ a=c \ b=d" by (simp add: PROD_eq) lemma UU_is_UU_UU [simp]: " = UU" @@ -295,20 +295,20 @@ subsection {* Fixedpoint theory *} -lemma adm_eq: "adm(%x. t(x)=(u(x)::'a::cpo))" +lemma adm_eq: "adm(\x. t(x)=(u(x)::'a::cpo))" apply (unfold eq_def) apply (rule adm_conj adm_less)+ done -lemma adm_not_not: "adm(P) ==> adm(%x.~~P(x))" +lemma adm_not_not: "adm(P) \ adm(\x. \ \ P(x))" by simp -lemma not_eq_TT: "ALL p. ~p=TT <-> (p=FF | p=UU)" - and not_eq_FF: "ALL p. ~p=FF <-> (p=TT | p=UU)" - and not_eq_UU: "ALL p. ~p=UU <-> (p=TT | p=FF)" +lemma not_eq_TT: "\p. \p=TT \ (p=FF \ p=UU)" + and not_eq_FF: "\p. \p=FF \ (p=TT \ p=UU)" + and not_eq_UU: "\p. \p=UU \ (p=TT \ p=FF)" by (rule tr_induct, simp_all)+ -lemma adm_not_eq_tr: "ALL p::tr. adm(%x. ~t(x)=p)" +lemma adm_not_eq_tr: "\p::tr. adm(\x. \t(x)=p)" apply (rule tr_induct) apply (simp_all add: not_eq_TT not_eq_FF not_eq_UU) apply (rule adm_disj adm_eq)+ @@ -318,15 +318,15 @@ adm_not_free adm_eq adm_less adm_not_less adm_not_eq_tr adm_conj adm_disj adm_imp adm_all - -ML {* - fun induct_tac ctxt v i = - res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN - REPEAT (resolve_tac @{thms adm_lemmas} i) +method_setup induct = {* + Scan.lift Args.name_inner_syntax >> (fn v => fn ctxt => + SIMPLE_METHOD' (fn i => + res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN + REPEAT (resolve_tac @{thms adm_lemmas} i))) *} -lemma least_FIX: "f(p) = p ==> FIX(f) << p" - apply (tactic {* induct_tac @{context} "f" 1 *}) +lemma least_FIX: "f(p) = p \ FIX(f) << p" + apply (induct f) apply (rule minimal) apply (intro strip) apply (erule subst) @@ -335,7 +335,7 @@ lemma lfp_is_FIX: assumes 1: "f(p) = p" - and 2: "ALL q. f(q)=q --> p << q" + and 2: "\q. f(q)=q \ p << q" shows "p = FIX(f)" apply (rule less_anti_sym) apply (rule 2 [THEN spec, THEN mp]) @@ -345,7 +345,7 @@ done -lemma FIX_pair: " = FIX(%p.)" +lemma FIX_pair: " = FIX(\p.)" apply (rule lfp_is_FIX) apply (simp add: FIX_eq [of f] FIX_eq [of g]) apply (intro strip) @@ -357,20 +357,20 @@ apply (erule subst, rule SND [symmetric]) done -lemma FIX1: "FIX(f) = FST(FIX(%p. ))" +lemma FIX1: "FIX(f) = FST(FIX(\p. ))" by (rule FIX_pair [unfolded PROD_eq FST SND, THEN conjunct1]) -lemma FIX2: "FIX(g) = SND(FIX(%p. ))" +lemma FIX2: "FIX(g) = SND(FIX(\p. ))" by (rule FIX_pair [unfolded PROD_eq FST SND, THEN conjunct2]) lemma induct2: - assumes 1: "adm(%p. P(FST(p),SND(p)))" + assumes 1: "adm(\p. P(FST(p),SND(p)))" and 2: "P(UU::'a,UU::'b)" - and 3: "ALL x y. P(x,y) --> P(f(x),g(y))" + and 3: "\x y. P(x,y) \ P(f(x),g(y))" shows "P(FIX(f),FIX(g))" apply (rule FIX1 [THEN ssubst, of _ f g]) apply (rule FIX2 [THEN ssubst, of _ f g]) - apply (rule induct [where ?f = "%x. "]) + apply (rule induct [where ?f = "\x. "]) apply (rule 1) apply simp apply (rule 2) diff -r 2f65dcd32a59 -r 51890cb80b30 src/LCF/ROOT --- a/src/LCF/ROOT Tue Nov 11 19:38:45 2014 +0100 +++ b/src/LCF/ROOT Tue Nov 11 21:14:19 2014 +0100 @@ -11,19 +11,12 @@ Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987) *} options [document = false] - theories LCF - -session "LCF-ex" in ex = LCF + - description {* - Author: Tobias Nipkow - Copyright 1991 University of Cambridge + theories + LCF - Some examples from Lawrence Paulson's book Logic and Computation. - *} - options [document = false] - theories - Ex1 - Ex2 - Ex3 - Ex4 + (* Some examples from Lawrence Paulson's book Logic and Computation *) + "ex/Ex1" + "ex/Ex2" + "ex/Ex3" + "ex/Ex4" diff -r 2f65dcd32a59 -r 51890cb80b30 src/LCF/ex/Ex1.thy --- a/src/LCF/ex/Ex1.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/LCF/ex/Ex1.thy Tue Nov 11 21:14:19 2014 +0100 @@ -1,17 +1,17 @@ section {* Section 10.4 *} theory Ex1 -imports LCF +imports "../LCF" begin axiomatization - P :: "'a => tr" and - G :: "'a => 'a" and - H :: "'a => 'a" and - K :: "('a => 'a) => ('a => 'a)" + P :: "'a \ tr" and + G :: "'a \ 'a" and + H :: "'a \ 'a" and + K :: "('a \ 'a) \ ('a \ 'a)" where P_strict: "P(UU) = UU" and - K: "K = (%h x. P(x) => x | h(h(G(x))))" and + K: "K = (\h x. P(x) \ x | h(h(G(x))))" and H: "H = FIX(K)" @@ -27,8 +27,8 @@ apply simp done -lemma H_idemp_lemma: "ALL x. H(FIX(K,x)) = FIX(K,x)" - apply (tactic {* induct_tac @{context} "K" 1 *}) +lemma H_idemp_lemma: "\x. H(FIX(K,x)) = FIX(K,x)" + apply (induct K) apply simp apply (simp split: COND_cases_iff) apply (intro strip) @@ -36,7 +36,7 @@ apply simp done -lemma H_idemp: "ALL x. H(H(x)) = H(x)" +lemma H_idemp: "\x. H(H(x)) = H(x)" apply (rule H_idemp_lemma [folded H]) done diff -r 2f65dcd32a59 -r 51890cb80b30 src/LCF/ex/Ex2.thy --- a/src/LCF/ex/Ex2.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/LCF/ex/Ex2.thy Tue Nov 11 21:14:19 2014 +0100 @@ -1,25 +1,25 @@ section {* Example 3.8 *} theory Ex2 -imports LCF +imports "../LCF" begin axiomatization - P :: "'a => tr" and - F :: "'b => 'b" and - G :: "'a => 'a" and - H :: "'a => 'b => 'b" and - K :: "('a => 'b => 'b) => ('a => 'b => 'b)" + P :: "'a \ tr" and + F :: "'b \ 'b" and + G :: "'a \ 'a" and + H :: "'a \ 'b \ 'b" and + K :: "('a \ 'b \ 'b) \ ('a \ 'b \ 'b)" where F_strict: "F(UU) = UU" and - K: "K = (%h x y. P(x) => y | F(h(G(x),y)))" and + K: "K = (\h x y. P(x) \ y | F(h(G(x),y)))" and H: "H = FIX(K)" declare F_strict [simp] K [simp] -lemma example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))" +lemma example: "\x. F(H(x::'a,y::'b)) = H(x,F(y))" apply (simplesubst H) - apply (tactic {* induct_tac @{context} "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *}) + apply (induct "K:: ('a\'b\'b) \ ('a\'b\'b)") apply simp apply (simp split: COND_cases_iff) done diff -r 2f65dcd32a59 -r 51890cb80b30 src/LCF/ex/Ex3.thy --- a/src/LCF/ex/Ex3.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/LCF/ex/Ex3.thy Tue Nov 11 21:14:19 2014 +0100 @@ -1,12 +1,12 @@ section {* Addition with fixpoint of successor *} theory Ex3 -imports LCF +imports "../LCF" begin axiomatization - s :: "'a => 'a" and - p :: "'a => 'a => 'a" + s :: "'a \ 'a" and + p :: "'a \ 'a \ 'a" where p_strict: "p(UU) = UU" and p_s: "p(s(x),y) = s(p(x,y))" @@ -14,7 +14,7 @@ declare p_strict [simp] p_s [simp] lemma example: "p(FIX(s),y) = FIX(s)" - apply (tactic {* induct_tac @{context} "s" 1 *}) + apply (induct s) apply simp apply simp done diff -r 2f65dcd32a59 -r 51890cb80b30 src/LCF/ex/Ex4.thy --- a/src/LCF/ex/Ex4.thy Tue Nov 11 19:38:45 2014 +0100 +++ b/src/LCF/ex/Ex4.thy Tue Nov 11 21:14:19 2014 +0100 @@ -2,15 +2,15 @@ section {* Prefixpoints *} theory Ex4 -imports LCF +imports "../LCF" begin lemma example: - assumes asms: "f(p) << p" "!!q. f(q) << q ==> p << q" + assumes asms: "f(p) << p" "\q. f(q) << q \ p << q" shows "FIX(f)=p" apply (unfold eq_def) apply (rule conjI) - apply (tactic {* induct_tac @{context} "f" 1 *}) + apply (induct f) apply (rule minimal) apply (intro strip) apply (rule less_trans) diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/General/position.ML Tue Nov 11 21:14:19 2014 +0100 @@ -53,6 +53,8 @@ val set_range: range -> T val reset_range: T -> T val range: T -> T -> range + val range_of_properties: Properties.T -> range + val properties_of_range: range -> Properties.T val thread_data: unit -> T val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b val default: T -> bool * T @@ -134,17 +136,16 @@ (* markup properties *) +fun get props name = + (case Properties.get props name of + NONE => 0 + | SOME s => Markup.parse_int s); + fun of_properties props = - let - fun get name = - (case Properties.get props name of - NONE => 0 - | SOME s => Markup.parse_int s); - in - make {line = get Markup.lineN, offset = get Markup.offsetN, - end_offset = get Markup.end_offsetN, props = props} - end; - + make {line = get props Markup.lineN, + offset = get props Markup.offsetN, + end_offset = get props Markup.end_offsetN, + props = props}; fun value k i = if valid i then [(k, Markup.print_int i)] else []; @@ -221,6 +222,19 @@ fun range pos pos' = (set_range (pos, pos'), pos'); +fun range_of_properties props = + let + val pos = of_properties props; + val pos' = + make {line = get props Markup.end_lineN, + offset = get props Markup.end_offsetN, + end_offset = 0, + props = props}; + in (pos, pos') end; + +fun properties_of_range (pos, pos') = + properties_of pos @ value Markup.end_lineN (the_default 0 (line_of pos')); + (* thread data *) diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/General/symbol_pos.ML Tue Nov 11 21:14:19 2014 +0100 @@ -39,7 +39,7 @@ val implode: T list -> text val implode_range: Position.T -> Position.T -> T list -> text * Position.range val explode: text * Position.T -> T list - type source = {delimited: bool, text: text, pos: Position.T} + type source = {delimited: bool, text: text, range: Position.range} val source_explode: source -> T list val source_content: source -> string * Position.T val scan_ident: T list -> T list * T list @@ -255,11 +255,11 @@ (* full source information *) -type source = {delimited: bool, text: text, pos: Position.T}; +type source = {delimited: bool, text: text, range: Position.range}; -fun source_explode {delimited = _, text, pos} = explode (text, pos); +fun source_explode {delimited = _, text, range = (pos, _)} = explode (text, pos); -fun source_content {delimited = _, text, pos} = +fun source_content {delimited = _, text, range = (pos, _)} = let val syms = explode (text, pos) in (content syms, pos) end; diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/Isar/attrib.ML Tue Nov 11 21:14:19 2014 +0100 @@ -206,13 +206,12 @@ fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd; fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd; -fun attribute_setup name source cmt = - (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @ - ML_Lex.read_source false source @ - ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")) - |> ML_Context.expression (#pos source) - "val (name, scan, comment): binding * attribute context_parser * string" - "Context.map_proof (Attrib.local_setup name scan comment)" +fun attribute_setup name source comment = + ML_Lex.read_source false source + |> ML_Context.expression (#range source) + "val parser: Thm.attribute context_parser" + ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^ + " parser " ^ ML_Syntax.print_string comment ^ ")") |> Context.proof_map; @@ -293,7 +292,7 @@ in (case Token.read_no_commands keywords Parse.attribs syms of [raw_srcs] => check_attribs ctxt raw_srcs - | _ => error ("Malformed attributes" ^ Position.here (#pos source))) + | _ => error ("Malformed attributes" ^ Position.here (#1 (#range source)))) end; diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Tue Nov 11 21:14:19 2014 +0100 @@ -60,12 +60,14 @@ fun global_setup source = ML_Lex.read_source false source - |> ML_Context.expression (#pos source) "val setup: theory -> theory" "Context.map_theory setup" + |> ML_Context.expression (#range source) + "val setup: theory -> theory" "Context.map_theory setup" |> Context.theory_map; fun local_setup source = ML_Lex.read_source false source - |> ML_Context.expression (#pos source) "val setup: local_theory -> local_theory" "Context.map_proof setup" + |> ML_Context.expression (#range source) + "val local_setup: local_theory -> local_theory" "Context.map_proof local_setup" |> Context.proof_map; @@ -73,35 +75,35 @@ fun parse_ast_translation source = ML_Lex.read_source false source - |> ML_Context.expression (#pos source) + |> ML_Context.expression (#range source) "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list" "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)" |> Context.theory_map; fun parse_translation source = ML_Lex.read_source false source - |> ML_Context.expression (#pos source) + |> ML_Context.expression (#range source) "val parse_translation: (string * (Proof.context -> term list -> term)) list" "Context.map_theory (Sign.parse_translation parse_translation)" |> Context.theory_map; fun print_translation source = ML_Lex.read_source false source - |> ML_Context.expression (#pos source) + |> ML_Context.expression (#range source) "val print_translation: (string * (Proof.context -> term list -> term)) list" "Context.map_theory (Sign.print_translation print_translation)" |> Context.theory_map; fun typed_print_translation source = ML_Lex.read_source false source - |> ML_Context.expression (#pos source) + |> ML_Context.expression (#range source) "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list" "Context.map_theory (Sign.typed_print_translation typed_print_translation)" |> Context.theory_map; fun print_ast_translation source = ML_Lex.read_source false source - |> ML_Context.expression (#pos source) + |> ML_Context.expression (#range source) "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list" "Context.map_theory (Sign.print_ast_translation print_ast_translation)" |> Context.theory_map; @@ -139,7 +141,7 @@ \end;\n"); in Context.theory_map - (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#pos source) ants)) + (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#1 (#range source)) ants)) end; @@ -158,7 +160,7 @@ fun declaration {syntax, pervasive} source = ML_Lex.read_source false source - |> ML_Context.expression (#pos source) + |> ML_Context.expression (#range source) "val declaration: Morphism.declaration" ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \ \pervasive = " ^ Bool.toString pervasive ^ "} declaration)") @@ -169,7 +171,7 @@ fun simproc_setup name lhss source identifier = ML_Lex.read_source false source - |> ML_Context.expression (#pos source) + |> ML_Context.expression (#range source) "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option" ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \ \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \ diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/Isar/isar_syn.ML Tue Nov 11 21:14:19 2014 +0100 @@ -232,7 +232,7 @@ (Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy => let val ([{lines, pos, ...}], thy') = files thy; - val source = {delimited = true, text = cat_lines lines, pos = pos}; + val source = {delimited = true, text = cat_lines lines, range = (pos, pos)}; val flags = {SML = true, exchange = false, redirect = true, verbose = true}; in thy' |> Context.theory_map diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/Isar/method.ML Tue Nov 11 21:14:19 2014 +0100 @@ -282,7 +282,7 @@ Scan.lift (Args.text_declaration (fn source => let val context' = context |> - ML_Context.expression (#pos source) + ML_Context.expression (#range source) "fun tactic (morphism: Morphism.morphism) (facts: thm list) : tactic" "Method.set_tactic tactic" (ML_Lex.read_source false source); val tac = the_tactic context'; @@ -377,13 +377,12 @@ fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd; fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd; -fun method_setup name source cmt = - (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @ - ML_Lex.read_source false source @ - ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")) - |> ML_Context.expression (#pos source) - "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string" - "Context.map_proof (Method.local_setup name scan comment)" +fun method_setup name source comment = + ML_Lex.read_source false source + |> ML_Context.expression (#range source) + "val parser: (Proof.context -> Proof.method) context_parser" + ("Context.map_proof (Method.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^ + " parser " ^ ML_Syntax.print_string comment ^ ")") |> Context.proof_map; diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/Isar/token.ML Tue Nov 11 21:14:19 2014 +0100 @@ -268,8 +268,8 @@ val tree = XML.Elem (Markup.token delimited (Position.properties_of pos), [XML.Text source]); in YXML.string_of tree end; -fun source_position_of (Token ((source, (pos, _)), (kind, _), _)) = - {delimited = delimited_kind kind, text = source, pos = pos}; +fun source_position_of (Token ((source, range), (kind, _), _)) = + {delimited = delimited_kind kind, text = source, range = range}; fun content_of (Token (_, (_, x), _)) = x; diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/ML/ml_antiquotations.ML Tue Nov 11 21:14:19 2014 +0100 @@ -34,10 +34,10 @@ val _ = Theory.setup (ML_Antiquotation.value @{binding source} - (Scan.lift Args.text_source_position >> (fn {delimited, text, pos} => + (Scan.lift Args.text_source_position >> (fn {delimited, text, range} => "{delimited = " ^ Bool.toString delimited ^ ", text = " ^ ML_Syntax.print_string text ^ - ", pos = " ^ ML_Syntax.print_position pos ^ "}"))); + ", range = " ^ ML_Syntax.print_range range ^ "}"))); (* formal entities *) diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/ML/ml_context.ML Tue Nov 11 21:14:19 2014 +0100 @@ -25,8 +25,8 @@ val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit val eval_source_in: Proof.context option -> ML_Compiler.flags -> Symbol_Pos.source -> unit - val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list -> - Context.generic -> Context.generic + val expression: Position.range -> string -> string -> + ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic end structure ML_Context: ML_CONTEXT = @@ -173,7 +173,7 @@ in eval flags pos (ML_Lex.read pos (File.read path)) end; fun eval_source flags source = - eval flags (#pos source) (ML_Lex.read_source (#SML flags) source); + eval flags (#1 (#range source)) (ML_Lex.read_source (#SML flags) source); fun eval_in ctxt flags pos ants = Context.setmp_thread_data (Option.map Context.Proof ctxt) @@ -183,11 +183,16 @@ Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval_source flags source) (); -fun expression pos bind body ants = - exec (fn () => - eval ML_Compiler.flags pos - (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @ - ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));"))); +fun expression range bind body ants = + let + val hidden = ML_Lex.read Position.none; + val visible = ML_Lex.read_set_range range; + in + exec (fn () => + eval ML_Compiler.flags (#1 range) + (hidden "Context.set_thread_data (SOME (let" @ visible bind @ hidden "=" @ ants @ + hidden ("in " ^ body ^ " end (ML_Context.the_generic_context ())));"))) + end; end; diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/ML/ml_file.ML --- a/src/Pure/ML/ml_file.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/ML/ml_file.ML Tue Nov 11 21:14:19 2014 +0100 @@ -13,7 +13,7 @@ let val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy); val provide = Resources.provide (src_path, digest); - val source = {delimited = true, text = cat_lines lines, pos = pos}; + val source = {delimited = true, text = cat_lines lines, range = (pos, pos)}; val flags = {SML = false, exchange = false, redirect = true, verbose = true}; in gthy diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/ML/ml_lex.ML Tue Nov 11 21:14:19 2014 +0100 @@ -26,6 +26,7 @@ Source.source) Source.source val tokenize: string -> token list val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list + val read_set_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list val read_source: bool -> Symbol_Pos.source -> token Antiquote.antiquote list end; @@ -325,7 +326,11 @@ val read = gen_read false; -fun read_source SML {delimited, text, pos} = +fun read_set_range range = + read Position.none + #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq); + +fun read_source SML ({delimited, text, range = (pos, _)}: Symbol_Pos.source) = let val language = if SML then Markup.language_SML else Markup.language_ML; val _ = diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/ML/ml_syntax.ML --- a/src/Pure/ML/ml_syntax.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/ML/ml_syntax.ML Tue Nov 11 21:14:19 2014 +0100 @@ -20,6 +20,7 @@ val print_strings: string list -> string val print_properties: Properties.T -> string val print_position: Position.T -> string + val print_range: Position.range -> string val make_binding: string * Position.T -> string val print_indexname: indexname -> string val print_class: class -> string @@ -77,8 +78,15 @@ val print_strings = print_list print_string; val print_properties = print_list (print_pair print_string print_string); -fun print_position pos = "Position.of_properties " ^ print_properties (Position.properties_of pos); -fun make_binding (name, pos) = "Binding.make " ^ print_pair print_string print_position (name, pos); + +fun print_position pos = + "Position.of_properties " ^ print_properties (Position.properties_of pos); + +fun print_range range = + "Position.range_of_properties " ^ print_properties (Position.properties_of_range range); + +fun make_binding (name, pos) = + "Binding.make " ^ print_pair print_string print_position (name, pos); val print_indexname = print_pair print_string print_int; diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/PIDE/markup.ML Tue Nov 11 21:14:19 2014 +0100 @@ -47,6 +47,7 @@ val completionN: string val completion: T val no_completionN: string val no_completion: T val lineN: string + val end_lineN: string val offsetN: string val end_offsetN: string val fileN: string @@ -329,8 +330,11 @@ (* position *) val lineN = "line"; +val end_lineN = "end_line"; + val offsetN = "offset"; val end_offsetN = "end_offset"; + val fileN = "file"; val idN = "id"; diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/PIDE/markup.scala Tue Nov 11 21:14:19 2014 +0100 @@ -100,6 +100,7 @@ /* position */ val LINE = "line" + val END_LINE = "line" val OFFSET = "offset" val END_OFFSET = "end_offset" val FILE = "file" diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/Syntax/syntax.ML Tue Nov 11 21:14:19 2014 +0100 @@ -163,21 +163,21 @@ local -fun token_position (XML.Elem ((name, props), _)) = +fun token_range (XML.Elem ((name, props), _)) = if name = Markup.tokenN - then (Markup.is_delimited props, Position.of_properties props) - else (false, Position.none) - | token_position (XML.Text _) = (false, Position.none); + then (Markup.is_delimited props, Position.range_of_properties props) + else (false, Position.no_range) + | token_range (XML.Text _) = (false, Position.no_range); -fun token_source tree = +fun token_source tree : Symbol_Pos.source = let val text = XML.content_of [tree]; - val (delimited, pos) = token_position tree; - in {delimited = delimited, text = text, pos = pos} end; + val (delimited, range) = token_range tree; + in {delimited = delimited, text = text, range = range} end; in -fun read_token_pos str = #2 (token_position (YXML.parse str handle Fail msg => error msg)); +fun read_token_pos str = #1 (#2 (token_range (YXML.parse str handle Fail msg => error msg))); fun read_token str = token_source (YXML.parse str handle Fail msg => error msg); @@ -187,8 +187,9 @@ let val source = token_source tree; val syms = Symbol_Pos.source_explode source; - val _ = Context_Position.report ctxt (#pos source) (markup (#delimited source)); - in parse (syms, #pos source) end; + val (pos, _) = #range source; + val _ = Context_Position.report ctxt pos (markup (#delimited source)); + in parse (syms, pos) end; in (case YXML.parse_body str handle Fail msg => error msg of body as [tree as XML.Elem ((name, _), _)] => diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Tue Nov 11 21:14:19 2014 +0100 @@ -462,10 +462,11 @@ | decode ps (Ast.Appl asts) = decode_appl ps asts; val source = Syntax.read_token str; + val (pos, _) = #range source; val syms = Symbol_Pos.source_explode source; val ast = - parse_asts ctxt true root (syms, #pos source) - |> uncurry (report_result ctxt (#pos source)) + parse_asts ctxt true root (syms, pos) + |> uncurry (report_result ctxt pos) |> decode []; val _ = Context_Position.reports_text ctxt (! reports); in ast end; diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/Thy/latex.ML Tue Nov 11 21:14:19 2014 +0100 @@ -132,7 +132,7 @@ enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s) else if Token.is_kind Token.Verbatim tok then let - val {text, pos, ...} = Token.source_position_of tok; + val {text, range = (pos, _), ...} = Token.source_position_of tok; val ants = Antiquote.read (Symbol_Pos.explode (text, pos), pos); val out = implode (map output_syms_antiq ants); in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/Thy/thy_output.ML Tue Nov 11 21:14:19 2014 +0100 @@ -195,10 +195,10 @@ val _ = Position.reports (maps words ants); in implode (map expand ants) end; -fun check_text {delimited, text, pos} state = - (Position.report pos (Markup.language_document delimited); +fun check_text {delimited, text, range} state = + (Position.report (fst range) (Markup.language_document delimited); if Toplevel.is_skipped_proof state then () - else ignore (eval_antiquote state (text, pos))); + else ignore (eval_antiquote state (text, fst range))); @@ -372,7 +372,7 @@ Parse.position (Scan.one (Token.is_command andf is_markup mark o Token.content_of)) -- Scan.repeat tag -- Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end) - >> (fn (((tok, pos'), tags), {text, pos, ...}) => + >> (fn (((tok, pos'), tags), {text, range = (pos, _), ...}) => let val name = Token.content_of tok in (SOME (name, pos', tags), (mk (name, (text, pos)), (flag, d))) end)); @@ -385,7 +385,7 @@ val cmt = Scan.peek (fn d => Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source) - >> (fn {text, pos, ...} => (NONE, (MarkupToken ("cmt", (text, pos)), ("", d))))); + >> (fn {text, range = (pos, _), ...} => (NONE, (MarkupToken ("cmt", (text, pos)), ("", d))))); val other = Scan.peek (fn d => Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d))))); @@ -482,7 +482,7 @@ fun pretty_text_report ctxt source = let - val {delimited, pos, ...} = source; + val {delimited, range = (pos, _), ...} = source; val _ = Context_Position.report ctxt pos (Markup.language_text delimited); val (s, _) = Symbol_Pos.source_content source; in pretty_text ctxt s end; @@ -664,7 +664,7 @@ fun ml_text name ml = antiquotation name (Scan.lift Args.text_source_position) (fn {context = ctxt, ...} => fn source => - (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#pos source) (ml source); + (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#1 (#range source)) (ml source); Symbol_Pos.source_content source |> #1 |> verbatim_text ctxt)); diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/Thy/thy_syntax.ML --- a/src/Pure/Thy/thy_syntax.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/Thy/thy_syntax.ML Tue Nov 11 21:14:19 2014 +0100 @@ -26,7 +26,7 @@ fun reports_of_token tok = let - val {text, pos, ...} = Token.source_position_of tok; + val {text, range = (pos, _), ...} = Token.source_position_of tok; val malformed_symbols = Symbol_Pos.explode (text, pos) |> map_filter (fn (sym, pos) => diff -r 2f65dcd32a59 -r 51890cb80b30 src/Pure/Tools/rail.ML --- a/src/Pure/Tools/rail.ML Tue Nov 11 19:38:45 2014 +0100 +++ b/src/Pure/Tools/rail.ML Tue Nov 11 21:14:19 2014 +0100 @@ -283,7 +283,7 @@ fun read ctxt (source: Symbol_Pos.source) = let - val {text, pos, ...} = source; + val {text, range = (pos, _), ...} = source; val _ = Context_Position.report ctxt pos Markup.language_rail; val toks = tokenize (Symbol_Pos.explode (text, pos)); val _ = Context_Position.reports ctxt (maps reports_of_token toks);