--- a/src/CCL/CCL.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CCL/CCL.thy Tue Nov 11 15:55:31 2014 +0100
@@ -27,18 +27,18 @@
consts
(*** Evaluation Judgement ***)
- Eval :: "[i,i]=>prop" (infixl "--->" 20)
+ Eval :: "[i,i]\<Rightarrow>prop" (infixl "--->" 20)
(*** Bisimulations for pre-order and equality ***)
- po :: "['a,'a]=>o" (infixl "[=" 50)
+ po :: "['a,'a]\<Rightarrow>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]\<Rightarrow>i" ("(1<_,/_>)")
+ lambda :: "(i\<Rightarrow>i)\<Rightarrow>i" (binder "lam " 55)
+ "case" :: "[i,i,i,[i,i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+ "apply" :: "[i,i]\<Rightarrow>i" (infixl "`" 56)
bot :: "i"
(******* EVALUATION SEMANTICS *******)
@@ -53,23 +53,23 @@
pairV: "<a,b> ---> <a,b>" and
lamV: "\<And>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 ---> <a,b>; f(a,b) ---> c |] ==> case(t,d,e,f,g) ---> c" and
- caseVlam: "\<And>b. [| t ---> lam x. b(x); g(b) ---> c |] ==> case(t,d,e,f,g) ---> c"
+ caseVtrue: "\<lbrakk>t ---> true; d ---> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) ---> c" and
+ caseVfalse: "\<lbrakk>t ---> false; e ---> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) ---> c" and
+ caseVpair: "\<lbrakk>t ---> <a,b>; f(a,b) ---> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) ---> c" and
+ caseVlam: "\<And>b. \<lbrakk>t ---> lam x. b(x); g(b) ---> c\<rbrakk> \<Longrightarrow> 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==<a,b> ==> u--->v;
- !!f. c==lam x. f(x) ==> u--->v |] ==>
+ canonical: "\<lbrakk>t ---> c; c==true \<Longrightarrow> u--->v;
+ c==false \<Longrightarrow> u--->v;
+ \<And>a b. c==<a,b> \<Longrightarrow> u--->v;
+ \<And>f. c==lam x. f(x) \<Longrightarrow> u--->v\<rbrakk> \<Longrightarrow>
u--->v"
(* Should be derivable - but probably a bitch! *)
axiomatization where
- substitute: "[| a==a'; t(a)--->c(a) |] ==> t(a')--->c(a')"
+ substitute: "\<lbrakk>a==a'; t(a)--->c(a)\<rbrakk> \<Longrightarrow> 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, \<lambda>x y. bot, \<lambda>u. u(t))"
-definition "fix" :: "(i=>i)=>i"
+definition "fix" :: "(i\<Rightarrow>i)\<Rightarrow>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]\<Rightarrow>o"
where
- "SIM(t,t',R) == (t=true & t'=true) | (t=false & t'=false) |
- (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) |
- (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))"
+ "SIM(t,t',R) == (t=true \<and> t'=true) | (t=false \<and> t'=false) |
+ (\<exists>a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : R \<and> <b,b'> : R) |
+ (\<exists>f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x.<f(x),f'(x)> : R))"
-definition POgen :: "i set => i set"
- where "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot | SIM(t,t',R))}"
+definition POgen :: "i set \<Rightarrow> i set"
+ where "POgen(R) == {p. \<exists>t t'. p=<t,t'> \<and> (t = bot | SIM(t,t',R))}"
-definition EQgen :: "i set => i set"
- where "EQgen(R) == {p. EX t t'. p=<t,t'> & (t = bot & t' = bot | SIM(t,t',R))}"
+definition EQgen :: "i set \<Rightarrow> i set"
+ where "EQgen(R) == {p. \<exists>t t'. p=<t,t'> \<and> (t = bot \<and> 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: "\<lbrakk>a [= b; b [= c\<rbrakk> \<Longrightarrow> a [= c" and
+ po_cong: "a [= b \<Longrightarrow> 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: "(\<And>x. f(x) [= g(x)) \<Longrightarrow> (\<lambda>x. f(x)) [= (\<lambda>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' \<longleftrightarrow> t [= t' \<and> t' [= t"
(** Properties of canonical values given by greatest fixed point definitions **)
axiomatization where
- PO_iff: "t [= t' <-> <t,t'> : PO" and
- EQ_iff: "t = t' <-> <t,t'> : EQ"
+ PO_iff: "t [= t' \<longleftrightarrow> <t,t'> : PO" and
+ EQ_iff: "t = t' \<longleftrightarrow> <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: "\<not> lam x. b(x) = bot"
(*** Definitions of Termination and Divergence ***)
-definition Dvg :: "i => o"
+definition Dvg :: "i \<Rightarrow> o"
where "Dvg(t) == t = bot"
-definition Trm :: "i => o"
- where "Trm(t) == ~ Dvg(t)"
+definition Trm :: "i \<Rightarrow> o"
+ where "Trm(t) == \<not> 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\<Rightarrow>'a)\<Rightarrow>'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\<Rightarrow>'b) = g \<Longrightarrow> 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 \<Longrightarrow> f(x)=f(y)"
by simp
-lemma abstractn: "(!!x. f(x) = g(x)) ==> f = g"
+lemma abstractn: "(\<And>x. f(x) = g(x)) \<Longrightarrow> 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) \<longleftrightarrow> \<not> t = bot"
by (simp add: Trm_def Dvg_def)
-lemma Dvg_iff: "Dvg(t) <-> t = bot"
+lemma Dvg_iff: "Dvg(t) \<longleftrightarrow> 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: "\<lbrakk>x=a; y=b; x=y\<rbrakk> \<Longrightarrow> a=b"
by simp
ML {*
@@ -215,8 +215,8 @@
*}
lemma ccl_injs:
- "<a,b> = <a',b'> <-> (a=a' & b=b')"
- "!!b b'. (lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"
+ "<a,b> = <a',b'> \<longleftrightarrow> (a=a' \<and> b=b')"
+ "\<And>b b'. (lam x. b(x) = lam x. b'(x)) \<longleftrightarrow> ((ALL z. b(z)=b'(z)))"
by (inj_rl caseBs)
@@ -226,7 +226,7 @@
subsection {* Constructors are distinct *}
-lemma lem: "t=t' ==> case(t,b,c,d,e) = case(t',b,c,d,e)"
+lemma lem: "t=t' \<Longrightarrow> case(t,b,c,d,e) = case(t',b,c,d,e)"
by simp
ML {*
@@ -246,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 = "\<not> " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b")
val lemma = @{thm lem};
val eq_lemma = @{thm eq_lemma};
@@ -267,7 +267,7 @@
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
@@ -304,33 +304,33 @@
subsection {* Facts from gfp Definition of @{text "[="} and @{text "="} *}
-lemma XHlemma1: "[| A=B; a:B <-> P |] ==> a:A <-> P"
+lemma XHlemma1: "\<lbrakk>A=B; a:B \<longleftrightarrow> P\<rbrakk> \<Longrightarrow> a:A \<longleftrightarrow> P"
by simp
-lemma XHlemma2: "(P(t,t') <-> Q) ==> (<t,t'> : {p. EX t t'. p=<t,t'> & P(t,t')} <-> Q)"
+lemma XHlemma2: "(P(t,t') \<longleftrightarrow> Q) \<Longrightarrow> (<t,t'> : {p. \<exists>t t'. p=<t,t'> \<and> P(t,t')} \<longleftrightarrow> Q)"
by blast
subsection {* Pre-Order *}
-lemma POgen_mono: "mono(%X. POgen(X))"
+lemma POgen_mono: "mono(\<lambda>X. POgen(X))"
apply (unfold POgen_def SIM_def)
apply (rule monoI)
apply blast
done
lemma POgenXH:
- "<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true) | (t=false & t'=false) |
- (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) |
- (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : R))"
+ "<t,t'> : POgen(R) \<longleftrightarrow> t= bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
+ (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : R \<and> <b,b'> : R) |
+ (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. <f(x),f'(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=<a,b> & t'=<a',b'> & 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' \<longleftrightarrow> t=bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
+ (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> a [= a' \<and> b [= b') |
+ (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (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])
@@ -342,17 +342,17 @@
apply simp
done
-lemma bot_poleast: "a [= bot ==> a=bot"
+lemma bot_poleast: "a [= bot \<Longrightarrow> a=bot"
apply (drule poXH [THEN iffD1])
apply simp
done
-lemma po_pair: "<a,b> [= <a',b'> <-> a [= a' & b [= b'"
+lemma po_pair: "<a,b> [= <a',b'> \<longleftrightarrow> a [= a' \<and> 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) \<longleftrightarrow> (ALL x. f(x) [= f'(x))"
apply (rule poXH [THEN iff_trans])
apply fastforce
done
@@ -363,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: "\<And>x y. c(x,y) [= c'(x,y)"
+ and 5: "\<And>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 = "\<lambda>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: "\<lbrakk>f [= f'; a [= a'\<rbrakk> \<Longrightarrow> 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: "\<not> 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: "\<lbrakk>x=a; y=b; x[=y\<rbrakk> \<Longrightarrow> a[=b"
by simp
-lemma npo_pair_lam: "~ <a,b> [= lam x. f(x)"
+lemma npo_pair_lam: "\<not> <a,b> [= 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) [= <a,b>"
+lemma npo_lam_pair: "\<not> lam x. f(x) [= <a,b>"
apply (rule notI)
apply (rule npo_lam_bot [THEN notE])
apply (erule case_pocong [THEN caseBpair [THEN caseBlam [THEN po_lemma]]])
@@ -405,16 +405,16 @@
done
lemma npo_rls1:
- "~ true [= false"
- "~ false [= true"
- "~ true [= <a,b>"
- "~ <a,b> [= true"
- "~ true [= lam x. f(x)"
- "~ lam x. f(x) [= true"
- "~ false [= <a,b>"
- "~ <a,b> [= false"
- "~ false [= lam x. f(x)"
- "~ lam x. f(x) [= false"
+ "\<not> true [= false"
+ "\<not> false [= true"
+ "\<not> true [= <a,b>"
+ "\<not> <a,b> [= true"
+ "\<not> true [= lam x. f(x)"
+ "\<not> lam x. f(x) [= true"
+ "\<not> false [= <a,b>"
+ "\<not> <a,b> [= false"
+ "\<not> false [= lam x. f(x)"
+ "\<not> lam x. f(x) [= false"
by (rule notI, drule case_pocong, erule_tac [5] rev_mp, simp_all,
(rule po_refl npo_lam_bot)+)+
@@ -423,7 +423,7 @@
subsection {* Coinduction for @{text "[="} *}
-lemma po_coinduct: "[| <t,u> : R; R <= POgen(R) |] ==> t [= u"
+lemma po_coinduct: "\<lbrakk><t,u> : R; R <= POgen(R)\<rbrakk> \<Longrightarrow> t [= u"
apply (rule PO_def [THEN def_coinduct, THEN PO_iff [THEN iffD2]])
apply assumption+
done
@@ -431,26 +431,29 @@
subsection {* Equality *}
-lemma EQgen_mono: "mono(%X. EQgen(X))"
+lemma EQgen_mono: "mono(\<lambda>X. EQgen(X))"
apply (unfold EQgen_def SIM_def)
apply (rule monoI)
apply blast
done
lemma EQgenXH:
- "<t,t'> : EQgen(R) <-> (t=bot & t'=bot) | (t=true & t'=true) |
- (t=false & t'=false) |
- (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) |
- (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))"
+ "<t,t'> : EQgen(R) \<longleftrightarrow> (t=bot \<and> t'=bot) | (t=true \<and> t'=true) |
+ (t=false \<and> t'=false) |
+ (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : R \<and> <b,b'> : R) |
+ (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x.<f(x),f'(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=<a,b> & t'=<a',b'> & 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 "<t,t'> : EQ <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : EQ & <b,b'> : EQ) | (EX f f'. t=lam x. f (x) & t'=lam x. f' (x) & (ALL x. <f (x) ,f' (x) > : EQ))")
+ "t=t' \<longleftrightarrow> (t=bot \<and> t'=bot) | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
+ (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> a=a' \<and> b=b') |
+ (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. f(x)=f'(x)))"
+ apply (subgoal_tac "<t,t'> : EQ \<longleftrightarrow>
+ (t=bot \<and> t'=bot) | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
+ (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : EQ \<and> <b,b'> : EQ) |
+ (EX f f'. t=lam x. f (x) \<and> t'=lam x. f' (x) \<and> (ALL x. <f (x) ,f' (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,
@@ -458,13 +461,13 @@
apply (rule iff_refl [THEN XHlemma2])
done
-lemma eq_coinduct: "[| <t,u> : R; R <= EQgen(R) |] ==> t = u"
+lemma eq_coinduct: "\<lbrakk><t,u> : R; R <= EQgen(R)\<rbrakk> \<Longrightarrow> t = u"
apply (rule EQ_def [THEN def_coinduct, THEN EQ_iff [THEN iffD2]])
apply assumption+
done
lemma eq_coinduct3:
- "[| <t,u> : R; R <= EQgen(lfp(%x. EQgen(x) Un R Un EQ)) |] ==> t = u"
+ "\<lbrakk><t,u> : R; R <= EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))\<rbrakk> \<Longrightarrow> t = u"
apply (rule EQ_def [THEN def_coinduct3, THEN EQ_iff [THEN iffD2]])
apply (rule EQgen_mono | assumption)+
done
@@ -477,7 +480,7 @@
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)) \<Longrightarrow> t = lam x.(t ` x)"
by (auto simp: apply_def)
lemma exhaustion: "(t=bot) | (t=true) | (t=false) | (EX a b. t=<a,b>) | (EX f. t=lam x. f(x))"
@@ -486,7 +489,7 @@
done
lemma term_case:
- "[| P(bot); P(true); P(false); !!x y. P(<x,y>); !!b. P(lam x. b(x)) |] ==> P(t)"
+ "\<lbrakk>P(bot); P(true); P(false); \<And>x y. P(<x,y>); \<And>b. P(lam x. b(x))\<rbrakk> \<Longrightarrow> P(t)"
using exhaustion [of t] by blast
end
--- a/src/CCL/Fix.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CCL/Fix.thy Tue Nov 11 15:55:31 2014 +0100
@@ -9,20 +9,20 @@
imports Type
begin
-definition idgen :: "i => i"
- where "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
+definition idgen :: "i \<Rightarrow> i"
+ where "idgen(f) == lam t. case(t,true,false, \<lambda>x y.<f`x, f`y>, \<lambda>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\<Rightarrow>o]\<Rightarrow>o" where
+ INCL_def: "INCL(\<lambda>x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) \<longrightarrow> P(fix(f)))" and
+ po_INCL: "INCL(\<lambda>x. a(x) [= b(x))" and
+ INCL_subst: "INCL(P) \<Longrightarrow> INCL(\<lambda>x. P((g::i\<Rightarrow>i)(x)))"
subsection {* Fixed Point Induction *}
lemma fix_ind:
assumes base: "P(bot)"
- and step: "!!x. P(x) ==> P(f(x))"
+ and step: "\<And>x. P(x) \<Longrightarrow> 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) \<longleftrightarrow> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) \<longrightarrow> 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: "\<lbrakk>\<And>f. ALL n:Nat. P(f^n`bot) \<Longrightarrow> P(fix(f))\<rbrakk> \<Longrightarrow> INCL(\<lambda>x. P(x))"
unfolding inclXH by blast
-lemma inclD: "[| INCL(P); !!n. n:Nat ==> P(f^n`bot) |] ==> P(fix(f))"
+lemma inclD: "\<lbrakk>INCL(P); \<And>n. n:Nat \<Longrightarrow> P(f^n`bot)\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>INCL(P); (ALL n:Nat. P(f^n`bot)) \<longrightarrow> P(fix(f)) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
by (blast dest: inclD)
subsection {* Lemmas for Inclusive Predicates *}
-lemma npo_INCL: "INCL(%x.~ a(x) [= t)"
+lemma npo_INCL: "INCL(\<lambda>x. \<not> 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: "\<lbrakk>INCL(P); INCL(Q)\<rbrakk> \<Longrightarrow> INCL(\<lambda>x. P(x) \<and> 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: "(\<And>a. INCL(P(a))) \<Longrightarrow> INCL(\<lambda>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: "(\<And>a. a:A \<Longrightarrow> INCL(P(a))) \<Longrightarrow> INCL(\<lambda>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(\<lambda>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 \<Longrightarrow> 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: "\<lbrakk>a = b; a ` t = u\<rbrakk> \<Longrightarrow> 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 ` <a,b> = <d ` a,d ` b>"
- "idgen(d) = d ==> d ` (lam x. f(x)) = lam x. d ` f(x)"
+ "idgen(d) = d \<Longrightarrow> d ` bot = bot"
+ "idgen(d) = d \<Longrightarrow> d ` true = true"
+ "idgen(d) = d \<Longrightarrow> d ` false = false"
+ "idgen(d) = d \<Longrightarrow> d ` <a,b> = <d ` a,d ` b>"
+ "idgen(d) = d \<Longrightarrow> 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"
+ "\<lbrakk>ALL x. t ` x [= u ` x; EX f. t=lam x. f(x); EX f. u=lam x. f(x)\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> d = lam x. ?f(x)"
apply (unfold idgen_def)
apply (erule sym)
done
lemma lemma1:
- "idgen(d) = d ==>
- {p. EX a b. p=<a,b> & (EX t. a=fix(idgen) ` t & b = d ` t)} <=
- POgen({p. EX a b. p=<a,b> & (EX t. a=fix(idgen) ` t & b = d ` t)})"
+ "idgen(d) = d \<Longrightarrow>
+ {p. EX a b. p=<a,b> \<and> (EX t. a=fix(idgen) ` t \<and> b = d ` t)} <=
+ POgen({p. EX a b. p=<a,b> \<and> (EX t. a=fix(idgen) ` t \<and> 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 \<Longrightarrow> 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=<a,b> & b = d ` a} <= POgen({p. EX a b. p=<a,b> & b = d ` a})"
+ "idgen(d) = d \<Longrightarrow>
+ {p. EX a b. p=<a,b> \<and> b = d ` a} <= POgen({p. EX a b. p=<a,b> \<and> 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 \<Longrightarrow> 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 \<Longrightarrow> 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(<x,y>)"
- and 5: "!!u.(!!x. P(u(x))) ==> P(lam x. u(x))"
+ and 4: "\<And>x y. \<lbrakk>P(x); P(y)\<rbrakk> \<Longrightarrow> P(<x,y>)"
+ and 5: "\<And>u.(\<And>x. P(u(x))) \<Longrightarrow> P(lam x. u(x))"
and 6: "INCL(P)"
shows "P(t)"
apply (rule reachability [THEN id_apply, THEN subst])
--- a/src/CCL/Gfp.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CCL/Gfp.thy Tue Nov 11 15:55:31 2014 +0100
@@ -10,37 +10,35 @@
begin
definition
- gfp :: "['a set=>'a set] => 'a set" where -- "greatest fixed point"
+ gfp :: "['a set\<Rightarrow>'a set] \<Rightarrow> '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) \<Longrightarrow> A <= gfp(f)"
unfolding gfp_def by blast
-lemma gfp_least: "[| !!u. u <= f(u) ==> u<=A |] ==> gfp(f) <= A"
+lemma gfp_least: "(\<And>u. u <= f(u) \<Longrightarrow> u <= A) \<Longrightarrow> gfp(f) <= A"
unfolding gfp_def by blast
-lemma gfp_lemma2: "mono(f) ==> gfp(f) <= f(gfp(f))"
+lemma gfp_lemma2: "mono(f) \<Longrightarrow> 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) \<Longrightarrow> 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) \<Longrightarrow> 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: "\<lbrakk>a: A; A <= f(A)\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>A <= f(A) Un gfp(f); mono(f)\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>a: A; A <= f(A) Un gfp(f); mono(f)\<rbrakk> \<Longrightarrow> 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) \<Longrightarrow> mono(\<lambda>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(\<lambda>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(\<lambda>x. f(x) Un A Un gfp(f)) <= f(lfp(\<lambda>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(\<lambda>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: "\<lbrakk>h == gfp(f); mono(f)\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>h == gfp(f); a:A; A <= f(A)\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>h == gfp(f); a:A; A <= f(A) Un h; mono(f)\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>h == gfp(f); a:A; A <= f(lfp(\<lambda>x. f(x) Un A Un h)); mono(f)\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>mono(f); \<And>Z. f(Z) <= g(Z)\<rbrakk> \<Longrightarrow> gfp(f) <= gfp(g)"
apply (rule gfp_upperbound)
apply (rule subset_trans)
apply (rule gfp_lemma2)
--- a/src/CCL/Hered.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CCL/Hered.thy Tue Nov 11 15:55:31 2014 +0100
@@ -15,10 +15,10 @@
is. Not so useful for functions!
*}
-definition HTTgen :: "i set => i set" where
+definition HTTgen :: "i set \<Rightarrow> i set" where
"HTTgen(R) ==
- {t. t=true | t=false | (EX a b. t= <a, b> & 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, b> \<and> a : R \<and> b : R) |
+ (EX f. t = lam x. f(x) \<and> (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(\<lambda>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,b> & a : A & b : A) |
- (EX f. t=lam x. f(x) & (ALL x. f(x) : A))"
+ "t : HTTgen(A) \<longleftrightarrow> t=true | t=false | (EX a b. t=<a,b> \<and> a : A \<and> b : A) |
+ (EX f. t=lam x. f(x) \<and> (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,b> & a : HTT & b : HTT) |
- (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))"
+ "t : HTT \<longleftrightarrow> t=true | t=false | (EX a b. t=<a,b> \<and> a : HTT \<and> b : HTT) |
+ (EX f. t=lam x. f(x) \<and> (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: "\<not> 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: "<a,b> : HTT <-> a : HTT & b : HTT"
+lemma HTT_pair: "<a,b> : HTT \<longleftrightarrow> a : HTT \<and> 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 \<longleftrightarrow> (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 \<longleftrightarrow> a : HTT"
+ "inr(b) : HTT \<longleftrightarrow> b : HTT"
"zero : HTT"
- "succ(n) : HTT <-> n : HTT"
+ "succ(n) : HTT \<longleftrightarrow> n : HTT"
"[] : HTT"
- "x$xs : HTT <-> x : HTT & xs : HTT"
+ "x$xs : HTT \<longleftrightarrow> x : HTT \<and> 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: "\<lbrakk>t : R; R <= HTTgen(R)\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>t : R; R <= HTTgen(lfp(\<lambda>x. HTTgen(x) Un R Un HTT))\<rbrakk> \<Longrightarrow> 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 |] ==> <a,b> : HTTgen(R)"
- "!!b. [| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)"
+ "\<lbrakk>a : R; b : R\<rbrakk> \<Longrightarrow> <a,b> : HTTgen(R)"
+ "\<And>b. (\<And>x. b(x) : R) \<Longrightarrow> 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(\<lambda>x. HTTgen(x) Un R Un HTT) \<Longrightarrow> inl(a) : HTTgen(lfp(\<lambda>x. HTTgen(x) Un R Un HTT))"
+ "b : lfp(\<lambda>x. HTTgen(x) Un R Un HTT) \<Longrightarrow> inr(b) : HTTgen(lfp(\<lambda>x. HTTgen(x) Un R Un HTT))"
+ "zero : HTTgen(lfp(\<lambda>x. HTTgen(x) Un R Un HTT))"
+ "n : lfp(\<lambda>x. HTTgen(x) Un R Un HTT) \<Longrightarrow> succ(n) : HTTgen(lfp(\<lambda>x. HTTgen(x) Un R Un HTT))"
+ "[] : HTTgen(lfp(\<lambda>x. HTTgen(x) Un R Un HTT))"
+ "\<lbrakk>h : lfp(\<lambda>x. HTTgen(x) Un R Un HTT); t : lfp(\<lambda>x. HTTgen(x) Un R Un HTT)\<rbrakk> \<Longrightarrow>
+ h$t : HTTgen(lfp(\<lambda>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: "\<lbrakk>A <= HTT; B <= HTT\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>A <= HTT; \<And>x. x:A \<Longrightarrow> B(x) <= HTT\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> ILists(A) <= HTT"
apply clarify
apply (erule HTT_coinduct3)
apply (fast intro!: HTTgenIs elim!: HTTgen_mono [THEN ci3_RI]
--- a/src/CCL/Lfp.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CCL/Lfp.thy Tue Nov 11 15:55:31 2014 +0100
@@ -10,24 +10,24 @@
begin
definition
- lfp :: "['a set=>'a set] => 'a set" where -- "least fixed point"
+ lfp :: "['a set\<Rightarrow>'a set] \<Rightarrow> '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 \<Longrightarrow> lfp(f) <= A"
unfolding lfp_def by blast
-lemma lfp_greatest: "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)"
+lemma lfp_greatest: "(\<And>u. f(u) <= u \<Longrightarrow> A<=u) \<Longrightarrow> A <= lfp(f)"
unfolding lfp_def by blast
-lemma lfp_lemma2: "mono(f) ==> f(lfp(f)) <= lfp(f)"
+lemma lfp_lemma2: "mono(f) \<Longrightarrow> 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) \<Longrightarrow> 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) \<Longrightarrow> 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: "\<And>x. \<lbrakk>x: f(lfp(f) Int {x. P(x)})\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>h == lfp(f); mono(f)\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>A == lfp(f); a:A; mono(f); \<And>x. x: f(A Int {x. P(x)}) \<Longrightarrow> P(x)\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>mono(g); \<And>Z. f(Z) <= g(Z)\<rbrakk> \<Longrightarrow> lfp(f) <= lfp(g)"
apply (rule lfp_lowerbound)
apply (rule subset_trans)
apply (erule meta_spec)
--- a/src/CCL/Set.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CCL/Set.thy Tue Nov 11 15:55:31 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 \<Rightarrow> o] \<Rightarrow> 'a set" (*comprehension*)
+ Compl :: "('a set) \<Rightarrow> 'a set" (*complement*)
+ Int :: "['a set, 'a set] \<Rightarrow> 'a set" (infixl "Int" 70)
+ Un :: "['a set, 'a set] \<Rightarrow> 'a set" (infixl "Un" 65)
+ Union :: "(('a set)set) \<Rightarrow> 'a set" (*...of a set*)
+ Inter :: "(('a set)set) \<Rightarrow> 'a set" (*...of a set*)
+ UNION :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set" (*general*)
+ INTER :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set" (*general*)
+ Ball :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o" (*bounded quants*)
+ Bex :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o" (*bounded quants*)
+ mono :: "['a set \<Rightarrow> 'b set] \<Rightarrow> o" (*monotonicity*)
+ mem :: "['a, 'a set] \<Rightarrow> o" (infixl ":" 50) (*membership*)
+ subset :: "['a set, 'a set] \<Rightarrow> o" (infixl "<=" 50)
+ singleton :: "'a \<Rightarrow> 'a set" ("{_}")
empty :: "'a set" ("{}")
syntax
- "_Coll" :: "[idt, o] => 'a set" ("(1{_./ _})") (*collection*)
+ "_Coll" :: "[idt, o] \<Rightarrow> '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] \<Rightarrow> 'b set" ("(INT _:_./ _)" [0, 0, 0] 10)
+ "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> '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] \<Rightarrow> o" ("(ALL _:_./ _)" [0, 0, 0] 10)
+ "_Bex" :: "[idt, 'a set, o] \<Rightarrow> 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(\<lambda>x. P)"
+ "INT x:A. B" == "CONST INTER(A, \<lambda>x. B)"
+ "UN x:A. B" == "CONST UNION(A, \<lambda>x. B)"
+ "ALL x:A. P" == "CONST Ball(A, \<lambda>x. P)"
+ "EX x:A. P" == "CONST Bex(A, \<lambda>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)}) \<longleftrightarrow> P(a)" and
+ set_extension: "A = B \<longleftrightarrow> (ALL x. x:A \<longleftrightarrow> 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 \<longrightarrow> P(x)"
+ Bex_def: "Bex(A, P) == EX x. x:A \<and> P(x)"
+ mono_def: "mono(f) == (ALL A B. A <= B \<longrightarrow> 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 \<and> x:B}"
+ Compl_def: "Compl(A) == {x. \<not>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) \<Longrightarrow> 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)} \<Longrightarrow> 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: "(\<And>x. x:A \<longleftrightarrow> x:B) \<Longrightarrow> 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: "(\<And>x. x:A \<Longrightarrow> P(x)) \<Longrightarrow> ALL x:A. P(x)"
by (simp add: Ball_def)
-lemma bspec: "[| ALL x:A. P(x); x:A |] ==> P(x)"
+lemma bspec: "\<lbrakk>ALL x:A. P(x); x:A\<rbrakk> \<Longrightarrow> P(x)"
by (simp add: Ball_def)
-lemma ballE: "[| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q"
+lemma ballE: "\<lbrakk>ALL x:A. P(x); P(x) \<Longrightarrow> Q; \<not> x:A \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
unfolding Ball_def by blast
-lemma bexI: "[| P(x); x:A |] ==> EX x:A. P(x)"
+lemma bexI: "\<lbrakk>P(x); x:A\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>EX x:A. \<not>P(x) \<Longrightarrow> P(a); a:A\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>EX x:A. P(x); \<And>x. \<lbrakk>x:A; P(x)\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> 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) \<longleftrightarrow> 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))"
+ "\<lbrakk>A = A'; \<And>x. x:A' \<Longrightarrow> P(x) \<longleftrightarrow> P'(x)\<rbrakk> \<Longrightarrow>
+ (ALL x:A. P(x)) \<longleftrightarrow> (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))"
+ "\<lbrakk>A = A'; \<And>x. x:A' \<Longrightarrow> P(x) \<longleftrightarrow> P'(x)\<rbrakk> \<Longrightarrow>
+ (EX x:A. P(x)) \<longleftrightarrow> (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: "(\<And>x. x:A \<Longrightarrow> x:B) \<Longrightarrow> A <= B"
unfolding subset_def by (blast intro: ballI)
(*Rule in Modus Ponens style*)
-lemma subsetD: "[| A <= B; c:A |] ==> c:B"
+lemma subsetD: "\<lbrakk>A <= B; c:A\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>A <= B; \<not>(c:A) \<Longrightarrow> P; c:B \<Longrightarrow> P\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>A <= B; B <= C\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>A <= B; B <= A\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> A<=B"
+ and equalityD2: "A = B \<Longrightarrow> B<=A"
by (simp_all add: subset_refl)
-lemma equalityE: "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P"
+lemma equalityE: "\<lbrakk>A = B; \<lbrakk>A <= B; B <= A\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (simp add: subset_refl)
-lemma equalityCE:
- "[| A = B; [| c:A; c:B |] ==> P; [| ~ c:A; ~ c:B |] ==> P |] ==> P"
+lemma equalityCE: "\<lbrakk>A = B; \<lbrakk>c:A; c:B\<rbrakk> \<Longrightarrow> P; \<lbrakk>\<not> c:A; \<not> c:B\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> c : A Un B"
+ and UnI2: "c:B \<Longrightarrow> 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: "(\<not>c:B \<Longrightarrow> c:A) \<Longrightarrow> c : A Un B"
by (blast intro: UnI1 UnI2)
-lemma UnE: "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"
+lemma UnE: "\<lbrakk>c : A Un B; c:A \<Longrightarrow> P; c:B \<Longrightarrow> P\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>c:A; c:B\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> c:A"
+ and IntD2: "c : A Int B \<Longrightarrow> c:B"
unfolding Int_def by (blast dest: CollectD)+
-lemma IntE: "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P"
+lemma IntE: "\<lbrakk>c : A Int B; \<lbrakk>c:A; c:B\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (blast dest: IntD1 IntD2)
subsection {* Rules for set complement *}
-lemma ComplI: "[| c:A ==> False |] ==> c : Compl(A)"
+lemma ComplI: "(c:A \<Longrightarrow> False) \<Longrightarrow> 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) \<Longrightarrow> \<not>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 : {} \<Longrightarrow> P"
unfolding empty_def by (blast dest: CollectD)
lemmas emptyE = emptyD [elim_format]
lemma not_emptyD:
- assumes "~ A={}"
+ assumes "\<not> A={}"
shows "EX x. x:A"
proof -
have "\<not> (EX x. x:A) \<Longrightarrow> 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} \<Longrightarrow> 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: "\<lbrakk>a:A; b: B(a)\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>b : (UN x:A. B(x)); \<And>x. \<lbrakk>x:A; b: B(x)\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>A = B; \<And>x. x:B \<Longrightarrow> C(x) = D(x)\<rbrakk> \<Longrightarrow> (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: "(\<And>x. x:A \<Longrightarrow> b: B(x)) \<Longrightarrow> 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: "\<lbrakk>b : (INT x:A. B(x)); a:A\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>b : (INT x:A. B(x)); b: B(a) \<Longrightarrow> R; \<not> a:A \<Longrightarrow> R\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>A = B; \<And>x. x:B \<Longrightarrow> C(x) = D(x)\<rbrakk> \<Longrightarrow> (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: "\<lbrakk>X:C; A:X\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>A : Union(C); \<And>X. \<lbrakk> A:X; X:C\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> 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: "(\<And>X. X:C \<Longrightarrow> A:X) \<Longrightarrow> 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: "\<lbrakk>A : Inter(C); X:C\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>A : Inter(C); A:X \<Longrightarrow> R; \<not> X:C \<Longrightarrow> R\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> B <= Union(A)"
by (blast intro: subsetI UnionI)
-lemma Union_least: "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C"
+lemma Union_least: "(\<And>X. X:A \<Longrightarrow> X<=C) \<Longrightarrow> 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 \<Longrightarrow> Inter(A) <= B"
by (blast intro: subsetI dest: InterD)
-lemma Inter_greatest: "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)"
+lemma Inter_greatest: "(\<And>X. X:A \<Longrightarrow> C<=X) \<Longrightarrow> 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: "\<lbrakk>A<=C; B<=C\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>C<=A; C<=B\<rbrakk> \<Longrightarrow> 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: "(\<And>A B. A <= B \<Longrightarrow> f(A) <= f(B)) \<Longrightarrow> mono(f)"
unfolding mono_def by blast
-lemma monoD: "[| mono(f); A <= B |] ==> f(A) <= f(B)"
+lemma monoD: "\<lbrakk>mono(f); A <= B\<rbrakk> \<Longrightarrow> 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) \<Longrightarrow> 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) \<Longrightarrow> 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) \<longleftrightarrow> (a:A | a:B)"
+ "(a : A Int B) \<longleftrightarrow> (a:A \<and> a:B)"
+ "(a : Compl(B)) \<longleftrightarrow> (\<not>a:B)"
+ "(a : {b}) \<longleftrightarrow> (a=b)"
+ "(a : {}) \<longleftrightarrow> False"
+ "(a : {x. P(x)}) \<longleftrightarrow> 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) \<longleftrightarrow> (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) \<longleftrightarrow> (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)) \<longleftrightarrow> (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}) \<longleftrightarrow> (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 \<Longrightarrow> Union(A) <= Union(B)"
by blast
-lemma Inter_anti_mono: "[| B<=A |] ==> Inter(A) <= Inter(B)"
+lemma Inter_anti_mono: "B <= A \<Longrightarrow> 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: "\<lbrakk>A <= B; \<And>x. x:A \<Longrightarrow> f(x)<=g(x)\<rbrakk> \<Longrightarrow> (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: "\<lbrakk>B <= A; \<And>x. x:A \<Longrightarrow> f(x) <= g(x)\<rbrakk> \<Longrightarrow> (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: "\<lbrakk>A <= C; B <= D\<rbrakk> \<Longrightarrow> A Un B <= C Un D"
by blast
-lemma Int_mono: "[| A<=C; B<=D |] ==> A Int B <= C Int D"
+lemma Int_mono: "\<lbrakk>A <= C; B <= D\<rbrakk> \<Longrightarrow> A Int B <= C Int D"
by blast
-lemma Compl_anti_mono: "[| A<=B |] ==> Compl(B) <= Compl(A)"
+lemma Compl_anti_mono: "A <= B \<Longrightarrow> Compl(B) <= Compl(A)"
by blast
end
--- a/src/CCL/Term.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CCL/Term.thy Tue Nov 11 15:55:31 2014 +0100
@@ -13,43 +13,43 @@
one :: "i"
- "if" :: "[i,i,i]=>i" ("(3if _/ then _/ else _)" [0,0,60] 60)
+ "if" :: "[i,i,i]\<Rightarrow>i" ("(3if _/ then _/ else _)" [0,0,60] 60)
- inl :: "i=>i"
- inr :: "i=>i"
- when :: "[i,i=>i,i=>i]=>i"
+ inl :: "i\<Rightarrow>i"
+ inr :: "i\<Rightarrow>i"
+ when :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
- split :: "[i,[i,i]=>i]=>i"
- fst :: "i=>i"
- snd :: "i=>i"
- thd :: "i=>i"
+ split :: "[i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+ fst :: "i\<Rightarrow>i"
+ snd :: "i\<Rightarrow>i"
+ thd :: "i\<Rightarrow>i"
zero :: "i"
- succ :: "i=>i"
- ncase :: "[i,i,i=>i]=>i"
- nrec :: "[i,i,[i,i]=>i]=>i"
+ succ :: "i\<Rightarrow>i"
+ ncase :: "[i,i,i\<Rightarrow>i]\<Rightarrow>i"
+ nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>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]\<Rightarrow>i" (infixr "$" 80)
+ lcase :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
+ lrec :: "[i,i,[i,i,i]\<Rightarrow>i]\<Rightarrow>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\<Rightarrow>i]\<Rightarrow>i"
+ letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+ letrec2 :: "[[i,i,i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
+ letrec3 :: "[[i,i,i,i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
syntax
- "_let" :: "[id,i,i]=>i" ("(3let _ be _/ in _)"
+ "_let" :: "[id,i,i]\<Rightarrow>i" ("(3let _ be _/ in _)"
[0,0,60] 60)
- "_letrec" :: "[id,id,i,i]=>i" ("(3letrec _ _ be _/ in _)"
+ "_letrec" :: "[id,id,i,i]\<Rightarrow>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]\<Rightarrow>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]\<Rightarrow>i" ("(3letrec _ _ _ _ be _/ in _)"
[0,0,0,0,0,60] 60)
ML {*
@@ -108,40 +108,40 @@
*}
consts
- napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56)
+ napply :: "[i\<Rightarrow>i,i,i]\<Rightarrow>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, \<lambda> x y. bot, \<lambda>v. bot)"
inl_def: "inl(a) == <true,a>"
inr_def: "inr(b) == <false,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, \<lambda>b x. if b then f(x) else g(x))"
+ split_def: "split(t,f) == case(t, bot, bot, f, \<lambda>u. bot)"
+ fst_def: "fst(t) == split(t, \<lambda>x y. x)"
+ snd_def: "snd(t) == split(t, \<lambda>x y. y)"
+ thd_def: "thd(t) == split(t, \<lambda>x p. split(p, \<lambda>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, \<lambda>x. b, \<lambda>y. c(y))"
+ nrec_def: " nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
nil_def: "[] == inl(one)"
cons_def: "h$t == inr(<h,t>)"
- 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, \<lambda>x. b, \<lambda>y. split(y,c))"
+ lrec_def: "lrec(l,b,c) == letrec g x be lcase(x, b, \<lambda>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(<x,y>),%u. f(lam x. u(x)))"
+ let_def: "let x be t in f(x) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>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(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>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'(<u,v>)))
- in f(%x y. g'(<x,y>))"
+ letrec g' p be split(p,\<lambda>x y. h(x,y,\<lambda>u v. g'(<u,v>)))
+ in f(\<lambda>x y. g'(<x,y>))"
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'(<u,<v,w>>))))
- in f(%x y z. g'(<x,<y,z>>))"
+ letrec g' p be split(p,\<lambda>x xs. split(xs,\<lambda>y z. h(x,y,z,\<lambda>u v w. g'(<u,<v,w>>))))
+ in f(\<lambda>x y z. g'(<x,<y,z>>))"
- napply_def: "f ^n` a == nrec(n,a,%x g. f(g))"
+ napply_def: "f ^n` a == nrec(n,a,\<lambda>x g. f(g))"
lemmas simp_can_defs = one_def inl_def inr_def
@@ -158,7 +158,7 @@
subsection {* Beta Rules, including strictness *}
-lemma letB: "~ t=bot ==> let x be t in f(x) = f(t)"
+lemma letB: "\<not> t=bot \<Longrightarrow> 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)
@@ -193,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,\<lambda>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
@@ -253,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,\<lambda>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,\<lambda>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"
@@ -275,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')) \<longleftrightarrow> (a=a')"
+ "(inr(a) = inr(a')) \<longleftrightarrow> (a=a')"
+ "(succ(a) = succ(a')) \<longleftrightarrow> (a=a')"
+ "(a$b = a'$b') \<longleftrightarrow> (a=a' \<and> b=b')"
by (inj_rl applyB splitB whenBinl whenBinr ncaseBsucc lcaseBcons)
@@ -294,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') \<longleftrightarrow> a [= a'"
+ "inr(b) [= inr(b') \<longleftrightarrow> b [= b'"
+ "succ(n) [= succ(n') \<longleftrightarrow> n [= n'"
+ "x$xs [= x'$xs' \<longleftrightarrow> x [= x' \<and> xs [= xs'"
by (simp_all add: data_defs ccl_porews)
--- a/src/CCL/Trancl.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CCL/Trancl.thy Tue Nov 11 15:55:31 2014 +0100
@@ -9,29 +9,28 @@
imports CCL
begin
-definition trans :: "i set => o" (*transitivity predicate*)
- where "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
+definition trans :: "i set \<Rightarrow> o" (*transitivity predicate*)
+ where "trans(r) == (ALL x y z. <x,y>:r \<longrightarrow> <y,z>:r \<longrightarrow> <x,z>:r)"
definition id :: "i set" (*the identity relation*)
where "id == {p. EX x. p = <x,x>}"
-definition relcomp :: "[i set,i set] => i set" (infixr "O" 60) (*composition of relations*)
- where "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
+definition relcomp :: "[i set,i set] \<Rightarrow> i set" (infixr "O" 60) (*composition of relations*)
+ where "r O s == {xz. EX x y z. xz = <x,z> \<and> <x,y>:s \<and> <y,z>:r}"
-definition rtrancl :: "i set => i set" ("(_^*)" [100] 100)
- where "r^* == lfp(%s. id Un (r O s))"
+definition rtrancl :: "i set \<Rightarrow> i set" ("(_^*)" [100] 100)
+ where "r^* == lfp(\<lambda>s. id Un (r O s))"
-definition trancl :: "i set => i set" ("(_^+)" [100] 100)
+definition trancl :: "i set \<Rightarrow> i set" ("(_^+)" [100] 100)
where "r^+ == r O rtrancl(r)"
subsection {* Natural deduction for @{text "trans(r)"} *}
-lemma transI:
- "(!! x y z. [| <x,y>:r; <y,z>:r |] ==> <x,z>:r) ==> trans(r)"
+lemma transI: "(\<And>x y z. \<lbrakk><x,y>:r; <y,z>:r\<rbrakk> \<Longrightarrow> <x,z>:r) \<Longrightarrow> trans(r)"
unfolding trans_def by blast
-lemma transD: "[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r"
+lemma transD: "\<lbrakk>trans(r); <a,b>:r; <b,c>:r\<rbrakk> \<Longrightarrow> <a,c>:r"
unfolding trans_def by blast
@@ -44,8 +43,7 @@
apply (rule refl)
done
-lemma idE:
- "[| p: id; !!x.[| p = <x,x> |] ==> P |] ==> P"
+lemma idE: "\<lbrakk>p: id; \<And>x. p = <x,x> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
apply (unfold id_def)
apply (erule CollectE)
apply blast
@@ -54,20 +52,14 @@
subsection {* Composition of two relations *}
-lemma compI: "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s"
+lemma compI: "\<lbrakk><a,b>:s; <b,c>:r\<rbrakk> \<Longrightarrow> <a,c> : 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 = <x,z>; <x,y>:s; <y,z>:r |] ==> P
- |] ==> P"
+lemma compE: "\<lbrakk>xz : r O s; \<And>x y z. \<lbrakk>xz = <x,z>; <x,y>:s; <y,z>:r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
unfolding relcomp_def by blast
-lemma compEpair:
- "[| <a,c> : r O s;
- !!y. [| <a,y>:s; <y,c>:r |] ==> P
- |] ==> P"
+lemma compEpair: "\<lbrakk><a,c> : r O s; \<And>y. \<lbrakk><a,y>:s; <y,c>:r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>r'<=r; s'<=s\<rbrakk> \<Longrightarrow> (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(\<lambda>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: "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^*"
+lemma rtrancl_into_rtrancl: "\<lbrakk><a,b> : r^*; <b,c> : r\<rbrakk> \<Longrightarrow> <a,c> : r^*"
apply (subst rtrancl_unfold)
apply blast
done
(*rtrancl of r contains r*)
-lemma r_into_rtrancl: "[| <a,b> : r |] ==> <a,b> : r^*"
+lemma r_into_rtrancl: "<a,b> : r \<Longrightarrow> <a,b> : r^*"
apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])
apply assumption
done
@@ -113,10 +105,10 @@
subsection {* standard induction rule *}
lemma rtrancl_full_induct:
- "[| <a,b> : r^*;
- !!x. P(<x,x>);
- !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |]
- ==> P(<a,b>)"
+ "\<lbrakk><a,b> : r^*;
+ \<And>x. P(<x,x>);
+ \<And>x y z. \<lbrakk>P(<x,y>); <x,y>: r^*; <y,z>: r\<rbrakk> \<Longrightarrow> P(<x,z>)\<rbrakk>
+ \<Longrightarrow> P(<a,b>)"
apply (erule def_induct [OF rtrancl_def])
apply (rule rtrancl_fun_mono)
apply blast
@@ -124,12 +116,12 @@
(*nice induction rule*)
lemma rtrancl_induct:
- "[| <a,b> : r^*;
+ "\<lbrakk><a,b> : r^*;
P(a);
- !!y z.[| <a,y> : r^*; <y,z> : r; P(y) |] ==> P(z) |]
- ==> P(b)"
+ \<And>y z. \<lbrakk><a,y> : r^*; <y,z> : r; P(y)\<rbrakk> \<Longrightarrow> P(z) \<rbrakk>
+ \<Longrightarrow> P(b)"
(*by induction on this formula*)
- apply (subgoal_tac "ALL y. <a,b> = <a,y> --> P(y)")
+ apply (subgoal_tac "ALL y. <a,b> = <a,y> \<longrightarrow> 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:
- "[| <a,b> : r^*; (a = b) ==> P;
- !!y.[| <a,y> : r^*; <y,b> : r |] ==> P |]
- ==> P"
- apply (subgoal_tac "a = b | (EX y. <a,y> : r^* & <y,b> : r)")
+ "\<lbrakk><a,b> : r^*; a = b \<Longrightarrow> P; \<And>y. \<lbrakk><a,y> : r^*; <y,b> : r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+ apply (subgoal_tac "a = b | (EX y. <a,y> : r^* \<and> <y,b> : r)")
prefer 2
apply (erule rtrancl_induct)
apply blast
@@ -163,7 +153,7 @@
subsubsection {* Conversions between trancl and rtrancl *}
-lemma trancl_into_rtrancl: "[| <a,b> : r^+ |] ==> <a,b> : r^*"
+lemma trancl_into_rtrancl: "<a,b> : r^+ \<Longrightarrow> <a,b> : 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: "[| <a,b> : r |] ==> <a,b> : r^+"
+lemma r_into_trancl: "<a,b> : r \<Longrightarrow> <a,b> : r^+"
unfolding trancl_def by (blast intro: rtrancl_refl)
(*intro rule by definition: from rtrancl and r*)
-lemma rtrancl_into_trancl1: "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^+"
+lemma rtrancl_into_trancl1: "\<lbrakk><a,b> : r^*; <b,c> : r\<rbrakk> \<Longrightarrow> <a,c> : r^+"
unfolding trancl_def by blast
(*intro rule from r and rtrancl*)
-lemma rtrancl_into_trancl2: "[| <a,b> : r; <b,c> : r^* |] ==> <a,c> : r^+"
+lemma rtrancl_into_trancl2: "\<lbrakk><a,b> : r; <b,c> : r^*\<rbrakk> \<Longrightarrow> <a,c> : 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:
- "[| <a,b> : r^+;
- <a,b> : r ==> P;
- !!y.[| <a,y> : r^+; <y,b> : r |] ==> P
- |] ==> P"
- apply (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ & <y,b> : r)")
+ "\<lbrakk><a,b> : r^+;
+ <a,b> : r \<Longrightarrow> P;
+ \<And>y. \<lbrakk><a,y> : r^+; <y,b> : r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+ apply (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ \<and> <y,b> : r)")
apply blast
apply (unfold trancl_def)
apply (erule compEpair)
@@ -212,7 +201,7 @@
apply assumption+
done
-lemma trancl_into_trancl2: "[| <a,b> : r; <b,c> : r^+ |] ==> <a,c> : r^+"
+lemma trancl_into_trancl2: "\<lbrakk><a,b> : r; <b,c> : r^+\<rbrakk> \<Longrightarrow> <a,c> : r^+"
apply (rule r_into_trancl [THEN trans_trancl [THEN transD]])
apply assumption+
done
--- a/src/CCL/Type.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CCL/Type.thy Tue Nov 11 15:55:31 2014 +0100
@@ -11,39 +11,39 @@
consts
- Subtype :: "['a set, 'a => o] => 'a set"
+ Subtype :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> '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] \<Rightarrow> i set" (infixr "+" 55)
+ Pi :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set"
+ Sigma :: "[i set, i \<Rightarrow> i set] \<Rightarrow> 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 \<Rightarrow> i set"
+ Lists :: "i set \<Rightarrow> i set"
+ ILists :: "i set \<Rightarrow> i set"
+ TAll :: "(i set \<Rightarrow> i set) \<Rightarrow> i set" (binder "TALL " 55)
+ TEx :: "(i set \<Rightarrow> i set) \<Rightarrow> i set" (binder "TEX " 55)
+ Lift :: "i set \<Rightarrow> i set" ("(3[_])")
- SPLIT :: "[i, [i, i] => i set] => i set"
+ SPLIT :: "[i, [i, i] \<Rightarrow> i set] \<Rightarrow> i set"
syntax
- "_Pi" :: "[idt, i set, i set] => i set" ("(3PROD _:_./ _)"
+ "_Pi" :: "[idt, i set, i set] \<Rightarrow> i set" ("(3PROD _:_./ _)"
[0,0,60] 60)
- "_Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)"
+ "_Sigma" :: "[idt, i set, i set] \<Rightarrow> 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] \<Rightarrow> i set" ("(_ ->/ _)" [54, 53] 53)
+ "_star" :: "[i set, i set] \<Rightarrow> i set" ("(_ */ _)" [56, 55] 55)
+ "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> '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, \<lambda>x. B)"
+ "A -> B" => "CONST Pi(A, \<lambda>_. B)"
+ "SUM x:A. B" => "CONST Sigma(A, \<lambda>x. B)"
+ "A * B" => "CONST Sigma(A, \<lambda>_. B)"
+ "{x: A. B}" == "CONST Subtype(A, \<lambda>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 \<and> 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) \<and> (ALL x:A. b(x):B(x))}"
Sigma_def: "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
- Nat_def: "Nat == lfp(% X. Unit + X)"
- List_def: "List(A) == lfp(% X. Unit + A*X)"
+ Nat_def: "Nat == lfp(\<lambda>X. Unit + X)"
+ List_def: "List(A) == lfp(\<lambda>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(\<lambda>X. Unit + A*X)"
+ ILists_def: "ILists(A) == gfp(\<lambda>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=<x,y> & A=B(x,y)})"
+ SPLIT_def: "SPLIT(p,B) == Union({A. EX x y. p=<x,y> \<and> A=B(x,y)})"
lemmas simp_type_defs =
@@ -78,26 +78,26 @@
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 \<longleftrightarrow> (ALL x. x:A \<longrightarrow> 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=<x,y>)"
+lemma EmptyXH: "\<And>a. a : {} \<longleftrightarrow> False"
+ and SubtypeXH: "\<And>a A P. a : {x:A. P(x)} \<longleftrightarrow> (a:A \<and> P(a))"
+ and UnitXH: "\<And>a. a : Unit \<longleftrightarrow> a=one"
+ and BoolXH: "\<And>a. a : Bool \<longleftrightarrow> a=true | a=false"
+ and PlusXH: "\<And>a A B. a : A+B \<longleftrightarrow> (EX x:A. a=inl(x)) | (EX x:B. a=inr(x))"
+ and PiXH: "\<And>a A B. a : PROD x:A. B(x) \<longleftrightarrow> (EX b. a=lam x. b(x) \<and> (ALL x:A. b(x):B(x)))"
+ and SgXH: "\<And>a A B. a : SUM x:A. B(x) \<longleftrightarrow> (EX x:A. EX y:B(x).a=<x,y>)"
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] \<longleftrightarrow> (a=bot | a:A)"
+ and TallXH: "a : TALL X. B(X) \<longleftrightarrow> (ALL X. a:B(X))"
+ and TexXH: "a : TEX X. B(X) \<longleftrightarrow> (EX X. a:B(X))"
unfolding simp_type_defs by blast+
ML {* ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs}) *}
@@ -108,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) |] ==> <a,b>:Sigma(A,B)"
- and inlT: "a:A ==> inl(a) : A+B"
- and inrT: "b:B ==> inr(b) : A+B"
+ and lamT: "\<And>b B. (\<And>x. x:A \<Longrightarrow> b(x):B(x)) \<Longrightarrow> lam x. b(x) : Pi(A,B)"
+ and pairT: "\<And>b B. \<lbrakk>a:A; b:B(a)\<rbrakk> \<Longrightarrow> <a,b>:Sigma(A,B)"
+ and inlT: "a:A \<Longrightarrow> inl(a) : A+B"
+ and inrT: "b:B \<Longrightarrow> inr(b) : A+B"
by (blast intro: XHs [THEN iffD2])+
lemmas canTs = oneT trueT falseT pairT lamT inlT inrT
@@ -119,7 +119,7 @@
subsection {* Non-Canonical Type Rules *}
-lemma lem: "[| a:B(u); u=v |] ==> a : B(v)"
+lemma lem: "\<lbrakk>a:B(u); u = v\<rbrakk> \<Longrightarrow> a : B(v)"
by blast
@@ -137,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: "\<lbrakk>b:Bool; b=true \<Longrightarrow> t:A(true); b=false \<Longrightarrow> u:A(false)\<rbrakk> \<Longrightarrow> if b then t else u : A(b)"
by ncanT
-lemma applyT: "[| f : Pi(A,B); a:A |] ==> f ` a : B(a)"
+lemma applyT: "\<lbrakk>f : Pi(A,B); a:A\<rbrakk> \<Longrightarrow> f ` a : B(a)"
by ncanT
-lemma splitT:
- "[| p:Sigma(A,B); !!x y. [| x:A; y:B(x); p=<x,y> |] ==> c(x,y):C(<x,y>) |]
- ==> split(p,c):C(p)"
+lemma splitT: "\<lbrakk>p:Sigma(A,B); \<And>x y. \<lbrakk>x:A; y:B(x); p=<x,y>\<rbrakk> \<Longrightarrow> c(x,y):C(<x,y>)\<rbrakk> \<Longrightarrow> 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)"
+ "\<lbrakk>p:A+B;
+ \<And>x. \<lbrakk>x:A; p=inl(x)\<rbrakk> \<Longrightarrow> a(x):C(inl(x));
+ \<And>y. \<lbrakk>y:B; p=inr(y)\<rbrakk> \<Longrightarrow> b(y):C(inr(y))\<rbrakk> \<Longrightarrow> when(p,a,b) : C(p)"
by ncanT
lemmas ncanTs = ifT applyT splitT whenT
@@ -160,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) \<Longrightarrow> a : A"
+ and SubtypeD2: "a : Subtype(A, P) \<Longrightarrow> P(a)"
by (simp_all add: SubtypeXH)
-lemma SubtypeI: "[| a:A; P(a) |] ==> a : {x:A. P(x)}"
+lemma SubtypeI: "\<lbrakk>a:A; P(a)\<rbrakk> \<Longrightarrow> a : {x:A. P(x)}"
by (simp add: SubtypeXH)
-lemma SubtypeE: "[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> Q |] ==> Q"
+lemma SubtypeE: "\<lbrakk>a : {x:A. P(x)}; \<lbrakk>a:A; P(a)\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
by (simp add: SubtypeXH)
subsection {* Monotonicity *}
-lemma idM: "mono (%X. X)"
+lemma idM: "mono (\<lambda>X. X)"
apply (rule monoI)
apply assumption
done
-lemma constM: "mono(%X. A)"
+lemma constM: "mono(\<lambda>X. A)"
apply (rule monoI)
apply (rule subset_refl)
done
-lemma "mono(%X. A(X)) ==> mono(%X.[A(X)])"
+lemma "mono(\<lambda>X. A(X)) \<Longrightarrow> mono(\<lambda>X.[A(X)])"
apply (rule subsetI [THEN monoI])
apply (drule LiftXH [THEN iffD1])
apply (erule disjE)
@@ -194,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)))"
+ "\<lbrakk>mono(\<lambda>X. A(X)); \<And>x X. x:A(X) \<Longrightarrow> mono(\<lambda>X. B(X,x))\<rbrakk> \<Longrightarrow>
+ mono(\<lambda>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: "(\<And>x. x:A \<Longrightarrow> mono(\<lambda>X. B(X,x))) \<Longrightarrow> mono(\<lambda>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: "\<lbrakk>mono(\<lambda>X. A(X)); mono(\<lambda>X. B(X))\<rbrakk> \<Longrightarrow> mono(\<lambda>X. A(X)+B(X))"
by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls
dest!: monoD [THEN subsetD])
@@ -214,7 +209,7 @@
subsubsection {* Conversion Rules for Fixed Points via monotonicity and Tarski *}
-lemma NatM: "mono(%X. Unit+X)"
+lemma NatM: "mono(\<lambda>X. Unit+X)"
apply (rule PlusM constM idM)+
done
@@ -223,7 +218,7 @@
apply (rule NatM)
done
-lemma ListM: "mono(%X.(Unit+Sigma(A,%y. X)))"
+lemma ListM: "mono(\<lambda>X.(Unit+Sigma(A,\<lambda>y. X)))"
apply (rule PlusM SgM constM idM)+
done
@@ -237,7 +232,7 @@
apply (rule ListM)
done
-lemma IListsM: "mono(%X.({} + Sigma(A,%y. X)))"
+lemma IListsM: "mono(\<lambda>X.({} + Sigma(A,\<lambda>y. X)))"
apply (rule PlusM SgM constM idM)+
done
@@ -251,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 \<longleftrightarrow> (a=zero | (EX x:Nat. a=succ(x)))"
+ and ListXH: "a : List(A) \<longleftrightarrow> (a=[] | (EX x:A. EX xs:List(A).a=x$xs))"
+ and ListsXH: "a : Lists(A) \<longleftrightarrow> (a=[] | (EX x:A. EX xs:Lists(A).a=x$xs))"
+ and IListsXH: "a : ILists(A) \<longleftrightarrow> (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)+
@@ -266,9 +261,9 @@
subsection {* Type Rules *}
lemma zeroT: "zero : Nat"
- and succT: "n:Nat ==> succ(n) : Nat"
+ and succT: "n:Nat \<Longrightarrow> succ(n) : Nat"
and nilT: "[] : List(A)"
- and consT: "[| h:A; t:List(A) |] ==> h$t : List(A)"
+ and consT: "\<lbrakk>h:A; t:List(A)\<rbrakk> \<Longrightarrow> h$t : List(A)"
by (blast intro: iXHs [THEN iffD2])+
lemmas icanTs = zeroT succT nilT consT
@@ -278,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: "\<lbrakk>n:Nat; n=zero \<Longrightarrow> b:C(zero); \<And>x. \<lbrakk>x:Nat; n=succ(x)\<rbrakk> \<Longrightarrow> c(x):C(succ(x))\<rbrakk>
+ \<Longrightarrow> 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: "\<lbrakk>l:List(A); l = [] \<Longrightarrow> b:C([]); \<And>h t. \<lbrakk>h:A; t:List(A); l=h$t\<rbrakk> \<Longrightarrow> c(h,t):C(h$t)\<rbrakk>
+ \<Longrightarrow> lcase(l,b,c) : C(l)"
by incanT
lemmas incanTs = ncaseT lcaseT
@@ -295,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: "\<lbrakk>n:Nat; P(zero); \<And>x. \<lbrakk>x:Nat; P(x)\<rbrakk> \<Longrightarrow> P(succ(x))\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>l:List(A); P([]); \<And>x xs. \<lbrakk>x:A; xs:List(A); P(xs)\<rbrakk> \<Longrightarrow> P(x$xs)\<rbrakk> \<Longrightarrow> P(l)"
apply (unfold ind_data_defs)
apply (erule def_induct [OF List_def _ ListM])
apply (blast intro: canTs elim!: case_rls)
@@ -313,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: "\<lbrakk>n:Nat; b:C(zero); \<And>x g. \<lbrakk>x:Nat; g:C(x)\<rbrakk> \<Longrightarrow> c(x,g):C(succ(x))\<rbrakk>
+ \<Longrightarrow> 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: "\<lbrakk>l:List(A); b:C([]); \<And>x xs g. \<lbrakk>x:A; xs:List(A); g:C(xs)\<rbrakk> \<Longrightarrow> c(x,xs,g):C(x$xs) \<rbrakk>
+ \<Longrightarrow> lrec(l,b,c) : C(l)"
by (erule List_ind) auto
lemmas precTs = nrecT lrecT
@@ -330,8 +318,7 @@
subsection {* Theorem proving *}
-lemma SgE2:
- "[| <a,b> : Sigma(A,B); [| a:A; b:B(a) |] ==> P |] ==> P"
+lemma SgE2: "\<lbrakk><a,b> : Sigma(A,B); \<lbrakk>a:A; b:B(a)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
unfolding SgXH by blast
(* General theorem proving ignores non-canonical term-formers, *)
@@ -346,7 +333,7 @@
subsection {* Infinite Data Types *}
-lemma lfp_subset_gfp: "mono(f) ==> lfp(f) <= gfp(f)"
+lemma lfp_subset_gfp: "mono(f) \<Longrightarrow> lfp(f) <= gfp(f)"
apply (rule lfp_lowerbound [THEN subset_trans])
apply (erule gfp_lemma3)
apply (rule subset_refl)
@@ -354,16 +341,14 @@
lemma gfpI:
assumes "a:A"
- and "!!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X)"
+ and "\<And>x X. \<lbrakk>x:A; ALL y:A. t(y):X\<rbrakk> \<Longrightarrow> 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 = "\<lambda>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: "\<lbrakk>C == gfp(B); a:A; \<And>x X. \<lbrakk>x:A; ALL y:A. t(y):X\<rbrakk> \<Longrightarrow> t(x) : B(X)\<rbrakk> \<Longrightarrow> t(a) : C"
apply unfold
apply (erule gfpI)
apply blast
@@ -381,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: "\<lbrakk>mono(f); a : f(lfp(f))\<rbrakk> \<Longrightarrow> a : lfp(f)"
apply (erule lfp_Tarski [THEN ssubst])
apply assumption
done
-lemma ssubst_single: "[| a=a'; a' : A |] ==> a : A"
+lemma ssubst_single: "\<lbrakk>a = a'; a' : A\<rbrakk> \<Longrightarrow> a : A"
by simp
-lemma ssubst_pair: "[| a=a'; b=b'; <a',b'> : A |] ==> <a,b> : A"
+lemma ssubst_pair: "\<lbrakk>a = a'; b = b'; <a',b'> : A\<rbrakk> \<Longrightarrow> <a,b> : A"
by simp
@@ -400,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: "\<lbrakk>mono(Agen); a : R\<rbrakk> \<Longrightarrow> a : lfp(\<lambda>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: "\<lbrakk>mono(Agen); a : Agen(lfp(\<lambda>x. Agen(x) Un R Un A))\<rbrakk> \<Longrightarrow>
+ a : lfp(\<lambda>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: "\<lbrakk>mono(Agen); a : A\<rbrakk> \<Longrightarrow> a : lfp(\<lambda>x. Agen(x) Un R Un A)"
by coinduct3
ML {*
@@ -432,19 +417,19 @@
lemma POgenIs:
"<true,true> : POgen(R)"
"<false,false> : POgen(R)"
- "[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)"
- "!!b b'. [|!!x. <b(x),b'(x)> : R |] ==><lam x. b(x),lam x. b'(x)> : POgen(R)"
+ "\<lbrakk><a,a'> : R; <b,b'> : R\<rbrakk> \<Longrightarrow> <<a,b>,<a',b'>> : POgen(R)"
+ "\<And>b b'. (\<And>x. <b(x),b'(x)> : R) \<Longrightarrow> <lam x. b(x),lam x. b'(x)> : POgen(R)"
"<one,one> : POgen(R)"
- "<a,a'> : lfp(%x. POgen(x) Un R Un PO) ==>
- <inl(a),inl(a')> : POgen(lfp(%x. POgen(x) Un R Un PO))"
- "<b,b'> : lfp(%x. POgen(x) Un R Un PO) ==>
- <inr(b),inr(b')> : POgen(lfp(%x. POgen(x) Un R Un PO))"
- "<zero,zero> : POgen(lfp(%x. POgen(x) Un R Un PO))"
- "<n,n'> : lfp(%x. POgen(x) Un R Un PO) ==>
- <succ(n),succ(n')> : POgen(lfp(%x. POgen(x) Un R Un PO))"
- "<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))"
- "[| <h,h'> : lfp(%x. POgen(x) Un R Un PO); <t,t'> : lfp(%x. POgen(x) Un R Un PO) |]
- ==> <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"
+ "<a,a'> : lfp(\<lambda>x. POgen(x) Un R Un PO) \<Longrightarrow>
+ <inl(a),inl(a')> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))"
+ "<b,b'> : lfp(\<lambda>x. POgen(x) Un R Un PO) \<Longrightarrow>
+ <inr(b),inr(b')> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))"
+ "<zero,zero> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))"
+ "<n,n'> : lfp(\<lambda>x. POgen(x) Un R Un PO) \<Longrightarrow>
+ <succ(n),succ(n')> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))"
+ "<[],[]> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))"
+ "\<lbrakk><h,h'> : lfp(\<lambda>x. POgen(x) Un R Un PO); <t,t'> : lfp(\<lambda>x. POgen(x) Un R Un PO)\<rbrakk>
+ \<Longrightarrow> <h$t,h'$t'> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))"
unfolding data_defs by (genIs POgenXH POgen_mono)+
ML {*
@@ -466,19 +451,19 @@
lemma EQgenIs:
"<true,true> : EQgen(R)"
"<false,false> : EQgen(R)"
- "[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)"
- "!!b b'. [|!!x. <b(x),b'(x)> : R |] ==> <lam x. b(x),lam x. b'(x)> : EQgen(R)"
+ "\<lbrakk><a,a'> : R; <b,b'> : R\<rbrakk> \<Longrightarrow> <<a,b>,<a',b'>> : EQgen(R)"
+ "\<And>b b'. (\<And>x. <b(x),b'(x)> : R) \<Longrightarrow> <lam x. b(x),lam x. b'(x)> : EQgen(R)"
"<one,one> : EQgen(R)"
- "<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==>
- <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
- "<b,b'> : lfp(%x. EQgen(x) Un R Un EQ) ==>
- <inr(b),inr(b')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
- "<zero,zero> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
- "<n,n'> : lfp(%x. EQgen(x) Un R Un EQ) ==>
- <succ(n),succ(n')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
- "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
- "[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) |]
- ==> <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"
+ "<a,a'> : lfp(\<lambda>x. EQgen(x) Un R Un EQ) \<Longrightarrow>
+ <inl(a),inl(a')> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))"
+ "<b,b'> : lfp(\<lambda>x. EQgen(x) Un R Un EQ) \<Longrightarrow>
+ <inr(b),inr(b')> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))"
+ "<zero,zero> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))"
+ "<n,n'> : lfp(\<lambda>x. EQgen(x) Un R Un EQ) \<Longrightarrow>
+ <succ(n),succ(n')> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))"
+ "<[],[]> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))"
+ "\<lbrakk><h,h'> : lfp(\<lambda>x. EQgen(x) Un R Un EQ); <t,t'> : lfp(\<lambda>x. EQgen(x) Un R Un EQ)\<rbrakk>
+ \<Longrightarrow> <h$t,h'$t'> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))"
unfolding data_defs by (genIs EQgenXH EQgen_mono)+
ML {*
--- a/src/CCL/Wfd.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CCL/Wfd.thy Tue Nov 11 15:55:31 2014 +0100
@@ -9,37 +9,37 @@
imports Trancl Type Hered
begin
-definition Wfd :: "[i set] => o"
- where "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a. a:P)"
+definition Wfd :: "[i set] \<Rightarrow> o"
+ where "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R \<longrightarrow> y:P) \<longrightarrow> x:P) \<longrightarrow> (ALL a. a:P)"
-definition wf :: "[i set] => i set"
- where "wf(R) == {x. x:R & Wfd(R)}"
+definition wf :: "[i set] \<Rightarrow> i set"
+ where "wf(R) == {x. x:R \<and> Wfd(R)}"
-definition wmap :: "[i=>i,i set] => i set"
- where "wmap(f,R) == {p. EX x y. p=<x,y> & <f(x),f(y)> : R}"
+definition wmap :: "[i\<Rightarrow>i,i set] \<Rightarrow> i set"
+ where "wmap(f,R) == {p. EX x y. p=<x,y> \<and> <f(x),f(y)> : R}"
definition lex :: "[i set,i set] => i set" (infixl "**" 70)
- where "ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
+ where "ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> \<and> (<a,a'> : ra | (a=a' \<and> <b,b'> : rb))}"
definition NatPR :: "i set"
where "NatPR == {p. EX x:Nat. p=<x,succ(x)>}"
-definition ListPR :: "i set => i set"
+definition ListPR :: "i set \<Rightarrow> i set"
where "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}"
lemma wfd_induct:
assumes 1: "Wfd(R)"
- and 2: "!!x.[| ALL y. <y,x>: R --> P(y) |] ==> P(x)"
+ and 2: "\<And>x. ALL y. <y,x>: R \<longrightarrow> P(y) \<Longrightarrow> 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.<x,y> : R ==> Q(x)"
- and 2: "ALL x. (ALL y. <y,x> : R --> y : P) --> x : P"
- and 3: "!!x. Q(x) ==> x:P"
+ assumes 1: "\<And>x y.<x,y> : R \<Longrightarrow> Q(x)"
+ and 2: "ALL x. (ALL y. <y,x> : R \<longrightarrow> y : P) \<longrightarrow> x : P"
+ and 3: "\<And>x. Q(x) \<Longrightarrow> x:P"
shows "a:P"
apply (rule 2 [rule_format])
using 1 3
@@ -52,14 +52,14 @@
res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac ctxt (i+1)))
*}
-lemma wf_anti_sym: "[| Wfd(r); <a,x>:r; <x,a>:r |] ==> P"
- apply (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P")
+lemma wf_anti_sym: "\<lbrakk>Wfd(r); <a,x>:r; <x,a>:r\<rbrakk> \<Longrightarrow> P"
+ apply (subgoal_tac "ALL x. <a,x>:r \<longrightarrow> <x,a>:r \<longrightarrow> P")
apply blast
apply (erule wfd_induct)
apply blast
done
-lemma wf_anti_refl: "[| Wfd(r); <a,a>: r |] ==> P"
+lemma wf_anti_refl: "\<lbrakk>Wfd(r); <a,a>: r\<rbrakk> \<Longrightarrow> P"
apply (rule wf_anti_sym)
apply assumption+
done
@@ -87,26 +87,26 @@
subsection {* Lexicographic Ordering *}
lemma lexXH:
- "p : ra**rb <-> (EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))"
+ "p : ra**rb \<longleftrightarrow> (EX a a' b b'. p = <<a,b>,<a',b'>> \<and> (<a,a'> : ra | a=a' \<and> <b,b'> : rb))"
unfolding lex_def by blast
-lemma lexI1: "<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb"
+lemma lexI1: "<a,a'> : ra \<Longrightarrow> <<a,b>,<a',b'>> : ra**rb"
by (blast intro!: lexXH [THEN iffD2])
-lemma lexI2: "<b,b'> : rb ==> <<a,b>,<a,b'>> : ra**rb"
+lemma lexI2: "<b,b'> : rb \<Longrightarrow> <<a,b>,<a,b'>> : ra**rb"
by (blast intro!: lexXH [THEN iffD2])
lemma lexE:
assumes 1: "p : ra**rb"
- and 2: "!!a a' b b'.[| <a,a'> : ra; p=<<a,b>,<a',b'>> |] ==> R"
- and 3: "!!a b b'.[| <b,b'> : rb; p = <<a,b>,<a,b'>> |] ==> R"
+ and 2: "\<And>a a' b b'. \<lbrakk><a,a'> : ra; p=<<a,b>,<a',b'>>\<rbrakk> \<Longrightarrow> R"
+ and 3: "\<And>a b b'. \<lbrakk><b,b'> : rb; p = <<a,b>,<a,b'>>\<rbrakk> \<Longrightarrow> 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 = <<a,b>,<a',b'>> ==> P |] ==>P"
+lemma lex_pair: "\<lbrakk>p : r**s; \<And>a a' b b'. p = <<a,b>,<a',b'>> \<Longrightarrow> P\<rbrakk> \<Longrightarrow>P"
apply (erule lexE)
apply blast+
done
@@ -117,7 +117,7 @@
shows "Wfd(R**S)"
apply (unfold Wfd_def)
apply safe
- apply (wfd_strengthen "%x. EX a b. x=<a,b>")
+ apply (wfd_strengthen "\<lambda>x. EX a b. x=<a,b>")
apply (blast elim!: lex_pair)
apply (subgoal_tac "ALL a b.<a,b>:P")
apply blast
@@ -129,13 +129,13 @@
subsection {* Mapping *}
-lemma wmapXH: "p : wmap(f,r) <-> (EX x y. p=<x,y> & <f(x),f(y)> : r)"
+lemma wmapXH: "p : wmap(f,r) \<longleftrightarrow> (EX x y. p=<x,y> \<and> <f(x),f(y)> : r)"
unfolding wmap_def by blast
-lemma wmapI: "<f(a),f(b)> : r ==> <a,b> : wmap(f,r)"
+lemma wmapI: "<f(a),f(b)> : r \<Longrightarrow> <a,b> : wmap(f,r)"
by (blast intro!: wmapXH [THEN iffD2])
-lemma wmapE: "[| p : wmap(f,r); !!a b.[| <f(a),f(b)> : r; p=<a,b> |] ==> R |] ==> R"
+lemma wmapE: "\<lbrakk>p : wmap(f,r); \<And>a b. \<lbrakk><f(a),f(b)> : r; p=<a,b>\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
by (blast dest!: wmapXH [THEN iffD1])
lemma wmap_wf:
@@ -143,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 \<longrightarrow> a:P")
apply blast
apply (rule 1 [THEN wfd_induct, THEN allI])
apply clarify
@@ -157,17 +157,17 @@
subsection {* Projections *}
-lemma wfstI: "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)"
+lemma wfstI: "<xa,ya> : r \<Longrightarrow> <<xa,xb>,<ya,yb>> : wmap(fst,r)"
apply (rule wmapI)
apply simp
done
-lemma wsndI: "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)"
+lemma wsndI: "<xb,yb> : r \<Longrightarrow> <<xa,xb>,<ya,yb>> : wmap(snd,r)"
apply (rule wmapI)
apply simp
done
-lemma wthdI: "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)"
+lemma wthdI: "<xc,yc> : r \<Longrightarrow> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)"
apply (rule wmapI)
apply simp
done
@@ -175,7 +175,7 @@
subsection {* Ground well-founded relations *}
-lemma wfI: "[| Wfd(r); a : r |] ==> a : wf(r)"
+lemma wfI: "\<lbrakk>Wfd(r); a : r\<rbrakk> \<Longrightarrow> a : wf(r)"
unfolding wf_def by blast
lemma Empty_wf: "Wfd({})"
@@ -188,22 +188,22 @@
apply (rule Empty_wf)
done
-lemma NatPRXH: "p : NatPR <-> (EX x:Nat. p=<x,succ(x)>)"
+lemma NatPRXH: "p : NatPR \<longleftrightarrow> (EX x:Nat. p=<x,succ(x)>)"
unfolding NatPR_def by blast
-lemma ListPRXH: "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=<t,h$t>)"
+lemma ListPRXH: "p : ListPR(A) \<longleftrightarrow> (EX h:A. EX t:List(A).p=<t,h$t>)"
unfolding ListPR_def by blast
-lemma NatPRI: "x : Nat ==> <x,succ(x)> : NatPR"
+lemma NatPRI: "x : Nat \<Longrightarrow> <x,succ(x)> : NatPR"
by (auto simp: NatPRXH)
-lemma ListPRI: "[| t : List(A); h : A |] ==> <t,h $ t> : ListPR(A)"
+lemma ListPRI: "\<lbrakk>t : List(A); h : A\<rbrakk> \<Longrightarrow> <t,h $ t> : ListPR(A)"
by (auto simp: ListPRXH)
lemma NatPR_wf: "Wfd(NatPR)"
apply (unfold Wfd_def)
apply clarify
- apply (wfd_strengthen "%x. x:Nat")
+ apply (wfd_strengthen "\<lambda>x. x:Nat")
apply (fastforce iff: NatPRXH)
apply (erule Nat_ind)
apply (fastforce iff: NatPRXH)+
@@ -212,7 +212,7 @@
lemma ListPR_wf: "Wfd(ListPR(A))"
apply (unfold Wfd_def)
apply clarify
- apply (wfd_strengthen "%x. x:List (A)")
+ apply (wfd_strengthen "\<lambda>x. x:List (A)")
apply (fastforce iff: ListPRXH)
apply (erule List_ind)
apply (fastforce iff: ListPRXH)+
@@ -223,7 +223,7 @@
lemma letrecT:
assumes 1: "a : A"
- and 2: "!!p g.[| p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x) |] ==> h(p,g) : D(p)"
+ and 2: "\<And>p g. \<lbrakk>p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x)\<rbrakk> \<Longrightarrow> 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])
@@ -242,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. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>
+ and "\<And>p q g. \<lbrakk>p:A; q:B;
+ ALL x:A. ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y)\<rbrakk> \<Longrightarrow>
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)
@@ -256,16 +256,16 @@
erule bspec SubtypeE sym [THEN subst])+
done
-lemma lem: "SPLIT(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)"
+lemma lem: "SPLIT(<a,<b,c>>,\<lambda>x xs. SPLIT(xs,\<lambda>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. <<x,<y,z>>,<p,<q,r>>> : wf(R)}.
- g(x,y,z) : D(x,y,z) |] ==>
+ and "\<And>p q r g. \<lbrakk>p:A; q:B; r:C;
+ ALL x:A. ALL y:B. ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}.
+ g(x,y,z) : D(x,y,z) \<rbrakk> \<Longrightarrow>
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)
@@ -284,22 +284,19 @@
subsection {* Type Checking for Recursive Calls *}
lemma rcallT:
- "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);
- g(a) : D(a) ==> g(a) : E; a:A; <a,p>:wf(R) |] ==>
- g(a) : E"
+ "\<lbrakk>ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);
+ g(a) : D(a) \<Longrightarrow> g(a) : E; a:A; <a,p>:wf(R)\<rbrakk> \<Longrightarrow> g(a) : E"
by blast
lemma rcall2T:
- "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y);
- g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <<a,b>,<p,q>>:wf(R) |] ==>
- g(a,b) : E"
+ "\<lbrakk>ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y);
+ g(a,b) : D(a,b) \<Longrightarrow> g(a,b) : E; a:A; b:B; <<a,b>,<p,q>>:wf(R)\<rbrakk> \<Longrightarrow> g(a,b) : E"
by blast
lemma rcall3T:
- "[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>: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; <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==>
- g(a,b,c) : E"
+ "\<lbrakk>ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z);
+ g(a,b,c) : D(a,b,c) \<Longrightarrow> g(a,b,c) : E;
+ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R)\<rbrakk> \<Longrightarrow> g(a,b,c) : E"
by blast
lemmas rcallTs = rcallT rcall2T rcall3T
@@ -310,9 +307,9 @@
lemma hyprcallT:
assumes 1: "g(a) = b"
and 2: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x)"
- and 3: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> b=g(a) ==> g(a) : D(a) ==> P"
- and 4: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> a:A"
- and 5: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> <a,p>:wf(R)"
+ and 3: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) \<Longrightarrow> b=g(a) \<Longrightarrow> g(a) : D(a) \<Longrightarrow> P"
+ and 4: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) \<Longrightarrow> a:A"
+ and 5: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) \<Longrightarrow> <a,p>:wf(R)"
shows P
apply (rule 3 [OF 2, OF 1 [symmetric]])
apply (rule rcallT [OF 2])
@@ -324,7 +321,7 @@
lemma hyprcall2T:
assumes 1: "g(a,b) = c"
and 2: "ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y)"
- and 3: "[| c=g(a,b); g(a,b) : D(a,b) |] ==> P"
+ and 3: "\<lbrakk>c = g(a,b); g(a,b) : D(a,b)\<rbrakk> \<Longrightarrow> P"
and 4: "a:A"
and 5: "b:B"
and 6: "<<a,b>,<p,q>>:wf(R)"
@@ -342,7 +339,7 @@
lemma hyprcall3T:
assumes 1: "g(a,b,c) = d"
and 2: "ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>: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: "\<lbrakk>d = g(a,b,c); g(a,b,c) : D(a,b,c)\<rbrakk> \<Longrightarrow> P"
and 4: "a:A"
and 5: "b:B"
and 6: "c:C"
@@ -364,14 +361,12 @@
subsection {* Rules to Remove Induction Hypotheses after Type Checking *}
-lemma rmIH1: "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P |] ==> P" .
+lemma rmIH1: "\<lbrakk>ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P\<rbrakk> \<Longrightarrow> P" .
-lemma rmIH2: "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> P" .
+lemma rmIH2: "\<lbrakk>ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P\<rbrakk> \<Longrightarrow> P" .
lemma rmIH3:
- "[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z);
- P |] ==>
- P" .
+ "\<lbrakk>ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); P\<rbrakk> \<Longrightarrow> P" .
lemmas rmIHs = rmIH1 rmIH2 rmIH3
@@ -382,27 +377,27 @@
(* correctly by applying SubtypeI *)
lemma Subtype_canTs:
- "!!a b A B P. a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {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)}"
+ "\<And>a b A B P. a : {x:A. b:{y:B(a).P(<x,y>)}} \<Longrightarrow> <a,b> : {x:Sigma(A,B).P(x)}"
+ "\<And>a A B P. a : {x:A. P(inl(x))} \<Longrightarrow> inl(a) : {x:A+B. P(x)}"
+ "\<And>b A B P. b : {x:B. P(inr(x))} \<Longrightarrow> inr(b) : {x:A+B. P(x)}"
+ "\<And>a P. a : {x:Nat. P(succ(x))} \<Longrightarrow> succ(a) : {x:Nat. P(x)}"
+ "\<And>h t A P. h : {x:A. t : {y:List(A).P(x$y)}} \<Longrightarrow> 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: "\<lbrakk>f(t):B; \<not>t=bot\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>a:A; f : Pi(A,B)\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>a:A; a:A \<Longrightarrow> P(a)\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>a:{x:A. Q(x)}; \<lbrakk>a:A; Q(a)\<rbrakk> \<Longrightarrow> P(a)\<rbrakk> \<Longrightarrow> a : {x:A. P(x)}"
by blast
lemmas rcall_lemmas = asm_rl rcall_lemma1 SubtypeD1 rcall_lemma2
@@ -530,7 +525,7 @@
etac @{thm substitute} 1)) *})
done
-lemma fixV: "f(fix(f)) ---> c ==> fix(f) ---> c"
+lemma fixV: "f(fix(f)) ---> c \<Longrightarrow> fix(f) ---> c"
apply (unfold fix_def)
apply (rule applyV)
apply (rule lamV)
@@ -538,7 +533,7 @@
done
lemma letrecV:
- "h(t,%y. letrec g x be h(x,g) in g(y)) ---> c ==>
+ "h(t,\<lambda>y. letrec g x be h(x,g) in g(y)) ---> c \<Longrightarrow>
letrec g x be h(x,g) in g(t) ---> c"
apply (unfold letrec_def)
apply (assumption | rule fixV applyV lamV)+
@@ -549,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> ---> <a,b>"
- "!!a b c t h. [| t ---> <a,b>; h(a,b) ---> c |] ==> split(t,h) ---> c"
+ "\<And>b c t u. \<lbrakk>b--->true; t--->c\<rbrakk> \<Longrightarrow> if b then t else u ---> c"
+ "\<And>b c t u. \<lbrakk>b--->false; u--->c\<rbrakk> \<Longrightarrow> if b then t else u ---> c"
+ "\<And>a b. <a,b> ---> <a,b>"
+ "\<And>a b c t h. \<lbrakk>t ---> <a,b>; h(a,b) ---> c\<rbrakk> \<Longrightarrow> 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"
+ "\<And>n. succ(n) ---> succ(n)"
+ "\<And>c n t u. \<lbrakk>n ---> zero; t ---> c\<rbrakk> \<Longrightarrow> ncase(n,t,u) ---> c"
+ "\<And>c n t u x. \<lbrakk>n ---> succ(x); u(x) ---> c\<rbrakk> \<Longrightarrow> ncase(n,t,u) ---> c"
+ "\<And>c n t u. \<lbrakk>n ---> zero; t ---> c\<rbrakk> \<Longrightarrow> nrec(n,t,u) ---> c"
+ "\<And>c n t u x. \<lbrakk>n--->succ(x); u(x,nrec(x,t,u))--->c\<rbrakk> \<Longrightarrow> 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"
+ "\<And>h t. h$t ---> h$t"
+ "\<And>c l t u. \<lbrakk>l ---> []; t ---> c\<rbrakk> \<Longrightarrow> lcase(l,t,u) ---> c"
+ "\<And>c l t u x xs. \<lbrakk>l ---> x$xs; u(x,xs) ---> c\<rbrakk> \<Longrightarrow> lcase(l,t,u) ---> c"
+ "\<And>c l t u. \<lbrakk>l ---> []; t ---> c\<rbrakk> \<Longrightarrow> lrec(l,t,u) ---> c"
+ "\<And>c l t u x xs. \<lbrakk>l--->x$xs; u(x,xs,lrec(xs,t,u))--->c\<rbrakk> \<Longrightarrow> 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),\<lambda>x. nrec(n,zero,\<lambda>y g. nrec(f(x),g,\<lambda>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),\<lambda>x. nrec(n,zero,\<lambda>y g. nrec(f(x),g,\<lambda>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(<x,y>))))
+ "letrec f p be split(p,\<lambda>m n. ncase(m,true,\<lambda>x. ncase(n,false,\<lambda>y. f(<x,y>))))
in f(<succ(zero), succ(zero)>) ---> ?a"
by eval
schematic_lemma
- "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
+ "letrec f p be split(p,\<lambda>m n. ncase(m,true,\<lambda>x. ncase(n,false,\<lambda>y. f(<x,y>))))
in f(<succ(zero), succ(succ(succ(succ(zero))))>) ---> ?a"
by eval
schematic_lemma
- "letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>))))
+ "letrec f p be split(p,\<lambda>m n. ncase(m,true,\<lambda>x. ncase(n,false,\<lambda>y. f(<x,y>))))
in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) ---> ?a"
by eval
@@ -601,12 +596,12 @@
subsection {* Reverse *}
schematic_lemma
- "letrec id l be lcase(l,[],%x xs. x$id(xs))
+ "letrec id l be lcase(l,[],\<lambda>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,[],\<lambda>x xs. lrec(rev(xs),x$[],\<lambda>y ys g. y$g))
in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a"
by eval
--- a/src/CCL/ex/Flag.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CCL/ex/Flag.thy Tue Nov 11 15:55:31 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]\<Rightarrow>i"
+ where "ccase(c,r,w,b) == when(c, \<lambda>x. r, \<lambda>wb. when(wb, \<lambda>x. w, \<lambda>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.
+ \<lambda>h t. split(flagx(t), \<lambda>lr p. split(p, \<lambda>lw lb.
ccase(h, <red$lr,<lw,lb>>,
<lr,<white$lw,lb>>,
<lr,<lw,blue$lb>>))))
in flagx(l)"
-axiomatization Perm :: "i => i => o"
-definition Flag :: "i => i => o" where
+axiomatization Perm :: "i \<Rightarrow> i \<Rightarrow> o"
+definition Flag :: "i \<Rightarrow> i \<Rightarrow> o" where
"Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour).
- x = <lr,<lw,lb>> -->
- (ALL c:Colour.(c mem lr = true --> c=red) &
- (c mem lw = true --> c=white) &
- (c mem lb = true --> c=blue)) &
+ x = <lr,<lw,lb>> \<longrightarrow>
+ (ALL c:Colour.(c mem lr = true \<longrightarrow> c=red) \<and>
+ (c mem lw = true \<longrightarrow> c=white) \<and>
+ (c mem lb = true \<longrightarrow> c=blue)) \<and>
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 \<longleftrightarrow> (a=red | a=white | a=blue)"
unfolding simp_type_defs flag_defs by blast
lemma redT: "red : Colour"
@@ -56,8 +56,8 @@
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)"
+ "\<lbrakk>c:Colour; c=red \<Longrightarrow> r : C(red); c=white \<Longrightarrow> w : C(white); c=blue \<Longrightarrow> b : C(blue)\<rbrakk>
+ \<Longrightarrow> ccase(c,r,w,b) : C(c)"
unfolding flag_defs by ncanT
lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)"
--- a/src/CCL/ex/List.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CCL/ex/List.thy Tue Nov 11 15:55:31 2014 +0100
@@ -9,107 +9,106 @@
imports Nat
begin
-definition map :: "[i=>i,i]=>i"
- where "map(f,l) == lrec(l,[],%x xs g. f(x)$g)"
+definition map :: "[i\<Rightarrow>i,i]\<Rightarrow>i"
+ where "map(f,l) == lrec(l, [], \<lambda>x xs g. f(x)$g)"
-definition comp :: "[i=>i,i=>i]=>i=>i" (infixr "\<circ>" 55)
- where "f \<circ> g == (%x. f(g(x)))"
+definition comp :: "[i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i\<Rightarrow>i" (infixr "\<circ>" 55)
+ where "f \<circ> g == (\<lambda>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]\<Rightarrow>i" (infixr "@" 55)
+ where "l @ m == lrec(l, m, \<lambda>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]\<Rightarrow>i" (infixr "mem" 55) (* FIXME dangling eq *)
+ where member_ax: "a mem l == lrec(l, false, \<lambda>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]\<Rightarrow>i"
+ where "filter(f,l) == lrec(l, [], \<lambda>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\<Rightarrow>i"
+ where "flat(l) == lrec(l, [], \<lambda>h t g. h @ g)"
-definition partition :: "[i,i]=>i" where
- "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.
+definition partition :: "[i,i]\<Rightarrow>i" where
+ "partition(f,l) == letrec part l a b be lcase(l, <a,b>, \<lambda>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]\<Rightarrow>i"
+ where "insert(f,a,l) == lrec(l, a$[], \<lambda>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\<Rightarrow>i"
+ where "isort(f) == lam l. lrec(l, [], \<lambda>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\<Rightarrow>i" where
+ "qsort(f) == lam l. letrec qsortx l be lcase(l, [], \<lambda>h t.
let p be partition(f`h,t)
- in split(p,%x y. qsortx(x) @ h$qsortx(y)))
+ in split(p, \<lambda>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 \<circ> g) = (%a. f(g(a)))"
- "!!a f g. (f \<circ> 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)"
+ "\<And>f g. (f \<circ> g) = (\<lambda>a. f(g(a)))"
+ "\<And>a f g. (f \<circ> g)(a) = f(g(a))"
+ "\<And>f. map(f,[]) = []"
+ "\<And>f x xs. map(f,x$xs) = f(x)$map(f,xs)"
+ "\<And>m. [] @ m = m"
+ "\<And>x xs m. x$xs @ m = x$(xs @ m)"
+ "\<And>f. filter(f,[]) = []"
+ "\<And>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)"
+ "\<And>x xs. flat(x$xs) = x @ flat(xs)"
+ "\<And>a f. insert(f,a,[]) = a$[]"
+ "\<And>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 \<Longrightarrow> 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 \<Longrightarrow> 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: "\<lbrakk>\<And>x. x:A \<Longrightarrow> f(x):B; l : List(A)\<rbrakk> \<Longrightarrow> map(f,l) : List(B)"
apply (unfold map_def)
apply typechk
apply blast
done
-lemma appendT: "[| l : List(A); m : List(A) |] ==> l @ m : List(A)"
+lemma appendT: "\<lbrakk>l : List(A); m : List(A)\<rbrakk> \<Longrightarrow> l @ m : List(A)"
apply (unfold append_def)
apply typechk
done
lemma appendTS:
- "[| l : {l:List(A). m : {m:List(A).P(l @ m)}} |] ==> l @ m : {x:List(A). P(x)}"
+ "\<lbrakk>l : {l:List(A). m : {m:List(A).P(l @ m)}}\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>f:A->Bool; l : List(A)\<rbrakk> \<Longrightarrow> filter(f,l) : List(A)"
apply (unfold filter_def)
apply typechk
done
-lemma flatT: "l : List(List(A)) ==> flat(l) : List(A)"
+lemma flatT: "l : List(List(A)) \<Longrightarrow> flat(l) : List(A)"
apply (unfold flat_def)
apply (typechk appendT)
done
-lemma insertT: "[| f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)"
+lemma insertT: "\<lbrakk>f : A->A->Bool; a:A; l : List(A)\<rbrakk> \<Longrightarrow> insert(f,a,l) : List(A)"
apply (unfold insert_def)
apply typechk
done
lemma insertTS:
- "[| f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} |] ==>
+ "\<lbrakk>f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} \<rbrakk> \<Longrightarrow>
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: "\<lbrakk>f:A->Bool; l : List(A)\<rbrakk> \<Longrightarrow> partition(f,l) : List(A)*List(A)"
apply (unfold partition_def)
apply typechk
apply clean_ccs
--- a/src/CCL/ex/Nat.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CCL/ex/Nat.thy Tue Nov 11 15:55:31 2014 +0100
@@ -9,41 +9,41 @@
imports "../Wfd"
begin
-definition not :: "i=>i"
+definition not :: "i\<Rightarrow>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]\<Rightarrow>i" (infixr "#+" 60)
+ where "a #+ b == nrec(a, b, \<lambda>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]\<Rightarrow>i" (infixr "#*" 60)
+ where "a #* b == nrec(a, zero, \<lambda>x g. b #+ g)"
-definition sub :: "[i,i]=>i" (infixr "#-" 60)
+definition sub :: "[i,i]\<Rightarrow>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, \<lambda>yy. ncase(x, zero, \<lambda>xx. sub(xx,yy)))
in sub(a,b)"
-definition le :: "[i,i]=>i" (infixr "#<=" 60)
+definition le :: "[i,i]\<Rightarrow>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, \<lambda>xx. ncase(y, false, \<lambda>yy. le(xx,yy)))
in le(a,b)"
-definition lt :: "[i,i]=>i" (infixr "#<" 60)
+definition lt :: "[i,i]\<Rightarrow>i" (infixr "#<" 60)
where "a #< b == not(b #<= a)"
-definition div :: "[i,i]=>i" (infixr "##" 60)
+definition div :: "[i,i]\<Rightarrow>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]\<Rightarrow>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), \<lambda>x.
+ ncase(m,ack(x,succ(zero)), \<lambda>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,37 +60,37 @@
by (simp_all add: nat_defs)
-lemma napply_f: "n:Nat ==> f^n`f(a) = f^succ(n)`a"
+lemma napply_f: "n:Nat \<Longrightarrow> 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: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #+ b : Nat"
apply (unfold add_def)
apply typechk
done
-lemma multT: "[| a:Nat; b:Nat |] ==> a #* b : Nat"
+lemma multT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #* b : Nat"
apply (unfold add_def mult_def)
apply typechk
done
(* Defined to return zero if a<b *)
-lemma subT: "[| a:Nat; b:Nat |] ==> a #- b : Nat"
+lemma subT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #- b : Nat"
apply (unfold sub_def)
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: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #<= b : Bool"
apply (unfold le_def)
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: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #< b : Bool"
apply (unfold not_def lt_def)
apply (typechk leT)
done
@@ -100,7 +100,7 @@
lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]]
-lemma "[| a:Nat; b:Nat |] ==> ackermann(a,b) : Nat"
+lemma "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> ackermann(a,b) : Nat"
apply (unfold ackermann_def)
apply gen_ccs
apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+
--- a/src/CCL/ex/Stream.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CCL/ex/Stream.thy Tue Nov 11 15:55:31 2014 +0100
@@ -9,10 +9,10 @@
imports List
begin
-definition iter1 :: "[i=>i,i]=>i"
+definition iter1 :: "[i\<Rightarrow>i,i]\<Rightarrow>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\<Rightarrow>i,i]\<Rightarrow>i"
where "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)"
(*
@@ -27,7 +27,7 @@
lemma map_comp:
assumes 1: "l:Lists(A)"
shows "map(f \<circ> g,l) = map(f,map(g,l))"
- apply (eq_coinduct3 "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f \<circ> g,l) & y=map (f,map (g,l)))}")
+ apply (eq_coinduct3 "{p. EX x y. p=<x,y> \<and> (EX l:Lists (A) .x=map (f \<circ> g,l) \<and> y=map (f,map (g,l)))}")
apply (blast intro: 1)
apply safe
apply (drule ListsXH [THEN iffD1])
@@ -39,8 +39,8 @@
lemma map_id:
assumes 1: "l:Lists(A)"
- shows "map(%x. x,l) = l"
- apply (eq_coinduct3 "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (%x. x,l) & y=l) }")
+ shows "map(\<lambda>x. x, l) = l"
+ apply (eq_coinduct3 "{p. EX x y. p=<x,y> \<and> (EX l:Lists (A) .x=map (\<lambda>x. x,l) \<and> y=l) }")
apply (blast intro: 1)
apply safe
apply (drule ListsXH [THEN iffD1])
@@ -56,7 +56,7 @@
and "m:Lists(A)"
shows "map(f,l@m) = map(f,l) @ map(f,m)"
apply (eq_coinduct3
- "{p. EX x y. p=<x,y> & (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) & y=map (f,l) @ map (f,m))}")
+ "{p. EX x y. p=<x,y> \<and> (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) \<and> y=map (f,l) @ map (f,m))}")
apply (blast intro: assms)
apply safe
apply (drule ListsXH [THEN iffD1])
@@ -75,7 +75,7 @@
and "m:Lists(A)"
shows "k @ l @ m = (k @ l) @ m"
apply (eq_coinduct3
- "{p. EX x y. p=<x,y> & (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m & y= (k @ l) @ m) }")
+ "{p. EX x y. p=<x,y> \<and> (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m \<and> y= (k @ l) @ m) }")
apply (blast intro: assms)
apply safe
apply (drule ListsXH [THEN iffD1])
@@ -92,7 +92,7 @@
lemma ilist_append:
assumes "l:ILists(A)"
shows "l @ m = l"
- apply (eq_coinduct3 "{p. EX x y. p=<x,y> & (EX l:ILists (A) .EX m. x=l@m & y=l)}")
+ apply (eq_coinduct3 "{p. EX x y. p=<x,y> \<and> (EX l:ILists (A) .EX m. x=l@m \<and> y=l)}")
apply (blast intro: assms)
apply safe
apply (drule IListsXH [THEN iffD1])
@@ -118,15 +118,15 @@
done
lemma iter2Blemma:
- "n:Nat ==>
+ "n:Nat \<Longrightarrow>
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 = "\<lambda>x. ?lhs (x) = ?rhs" in iter2B [THEN ssubst])
apply (simp add: nmapBcons)
done
lemma iter1_iter2_eq: "iter1(f,a) = iter2(f,a)"
apply (eq_coinduct3
- "{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}")
+ "{p. EX x y. p=<x,y> \<and> (EX n:Nat. x=iter1 (f,f^n`a) \<and> y=map (f) ^n`iter2 (f,a))}")
apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong])
apply (EQgen iter1B iter2Blemma)
apply (subst napply_f, assumption)
--- a/src/CTT/Arith.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CTT/Arith.thy Tue Nov 11 15:55:31 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]\<Rightarrow>i" (infixr "#+" 65) where
+ "a#+b == rec(a, b, \<lambda>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]\<Rightarrow>i" (infixr "-" 65) where
+ "a-b == rec(b, a, \<lambda>u v. rec(v, 0, \<lambda>x y. x))"
definition
- absdiff :: "[i,i]=>i" (infixr "|-|" 65) where
+ absdiff :: "[i,i]\<Rightarrow>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]\<Rightarrow>i" (infixr "#*" 70) where
+ "a#*b == rec(a, 0, \<lambda>u v. b #+ v)"
definition
- mod :: "[i,i]=>i" (infixr "mod" 70) where
+ mod :: "[i,i]\<Rightarrow>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]\<Rightarrow>i" (infixr "div" 70) where
+ "a div b == rec(a, 0, \<lambda>u v. rec(succ(u) mod b, succ(v), \<lambda>x y. v))"
notation (xsymbols)
@@ -52,12 +52,12 @@
(*typing of add: short and long versions*)
-lemma add_typing: "[| a:N; b:N |] ==> a #+ b : N"
+lemma add_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #+ b : N"
apply (unfold arith_defs)
apply typechk
done
-lemma add_typingL: "[| a=c:N; b=d:N |] ==> a #+ b = c #+ d : N"
+lemma add_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #+ b = c #+ d : N"
apply (unfold arith_defs)
apply equal
done
@@ -65,12 +65,12 @@
(*computation for add: 0 and successor cases*)
-lemma addC0: "b:N ==> 0 #+ b = b : N"
+lemma addC0: "b:N \<Longrightarrow> 0 #+ b = b : N"
apply (unfold arith_defs)
apply rew
done
-lemma addC_succ: "[| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"
+lemma addC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #+ b = succ(a #+ b) : N"
apply (unfold arith_defs)
apply rew
done
@@ -80,24 +80,24 @@
(*typing of mult: short and long versions*)
-lemma mult_typing: "[| a:N; b:N |] ==> a #* b : N"
+lemma mult_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* b : N"
apply (unfold arith_defs)
apply (typechk add_typing)
done
-lemma mult_typingL: "[| a=c:N; b=d:N |] ==> a #* b = c #* d : N"
+lemma mult_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #* b = c #* d : N"
apply (unfold arith_defs)
apply (equal add_typingL)
done
(*computation for mult: 0 and successor cases*)
-lemma multC0: "b:N ==> 0 #* b = 0 : N"
+lemma multC0: "b:N \<Longrightarrow> 0 #* b = 0 : N"
apply (unfold arith_defs)
apply rew
done
-lemma multC_succ: "[| a:N; b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"
+lemma multC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #* b = b #+ (a #* b) : N"
apply (unfold arith_defs)
apply rew
done
@@ -107,12 +107,12 @@
(*typing of difference*)
-lemma diff_typing: "[| a:N; b:N |] ==> a - b : N"
+lemma diff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a - b : N"
apply (unfold arith_defs)
apply typechk
done
-lemma diff_typingL: "[| a=c:N; b=d:N |] ==> a - b = c - d : N"
+lemma diff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a - b = c - d : N"
apply (unfold arith_defs)
apply equal
done
@@ -120,14 +120,14 @@
(*computation for difference: 0 and successor cases*)
-lemma diffC0: "a:N ==> a - 0 = a : N"
+lemma diffC0: "a:N \<Longrightarrow> a - 0 = a : N"
apply (unfold arith_defs)
apply rew
done
-(*Note: rec(a, 0, %z w.z) is pred(a). *)
+(*Note: rec(a, 0, \<lambda>z w.z) is pred(a). *)
-lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N"
+lemma diff_0_eq_0: "b:N \<Longrightarrow> 0 - b = 0 : N"
apply (unfold arith_defs)
apply (NE b)
apply hyp_rew
@@ -136,7 +136,7 @@
(*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: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) - succ(b) = a - b : N"
apply (unfold arith_defs)
apply hyp_rew
apply (NE b)
@@ -194,7 +194,7 @@
subsection {* Addition *}
(*Associative law for addition*)
-lemma add_assoc: "[| a:N; b:N; c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"
+lemma add_assoc: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #+ b) #+ c = a #+ (b #+ c) : N"
apply (NE a)
apply hyp_arith_rew
done
@@ -202,7 +202,7 @@
(*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"
+lemma add_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #+ b = b #+ a : N"
apply (NE a)
apply hyp_arith_rew
apply (rule sym_elem)
@@ -217,32 +217,32 @@
subsection {* Multiplication *}
(*right annihilation in product*)
-lemma mult_0_right: "a:N ==> a #* 0 = 0 : N"
+lemma mult_0_right: "a:N \<Longrightarrow> 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"
+lemma mult_succ_right: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> 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"
+lemma mult_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> 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"
+lemma add_mult_distrib: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (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"
+lemma mult_assoc: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #* b) #* c = a #* (b #* c) : N"
apply (NE a)
apply (hyp_arith_rew add_mult_distrib)
done
@@ -254,20 +254,20 @@
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"
+lemma diff_self_eq_0: "a:N \<Longrightarrow> 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: "\<lbrakk>c : N; 0 : N; c : N\<rbrakk> \<Longrightarrow> 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)"
+ "b:N \<Longrightarrow> ?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)
@@ -292,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: "\<lbrakk>a:N; b:N; b - a = 0 : N\<rbrakk> \<Longrightarrow> b #+ (a-b) = a : N"
apply (rule EqE)
apply (rule add_diff_inverse_lemma [THEN ProdE, THEN ProdE])
apply (assumption | rule EqI)+
@@ -303,41 +303,41 @@
(*typing of absolute difference: short and long versions*)
-lemma absdiff_typing: "[| a:N; b:N |] ==> a |-| b : N"
+lemma absdiff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a |-| b : N"
apply (unfold arith_defs)
apply typechk
done
-lemma absdiff_typingL: "[| a=c:N; b=d:N |] ==> a |-| b = c |-| d : N"
+lemma absdiff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a |-| b = c |-| d : N"
apply (unfold arith_defs)
apply equal
done
-lemma absdiff_self_eq_0: "a:N ==> a |-| a = 0 : N"
+lemma absdiff_self_eq_0: "a:N \<Longrightarrow> a |-| a = 0 : N"
apply (unfold absdiff_def)
apply (arith_rew diff_self_eq_0)
done
-lemma absdiffC0: "a:N ==> 0 |-| a = a : N"
+lemma absdiffC0: "a:N \<Longrightarrow> 0 |-| a = a : N"
apply (unfold absdiff_def)
apply hyp_arith_rew
done
-lemma absdiff_succ_succ: "[| a:N; b:N |] ==> succ(a) |-| succ(b) = a |-| b : N"
+lemma absdiff_succ_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) |-| succ(b) = a |-| b : N"
apply (unfold absdiff_def)
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: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a |-| b = b |-| a : N"
apply (unfold absdiff_def)
apply (rule add_commute)
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)"
+schematic_lemma add_eq0_lemma: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)"
apply (NE a)
apply (rule_tac [3] replace_type)
apply arith_rew
@@ -349,7 +349,7 @@
(*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: "\<lbrakk>a:N; b:N; a #+ b = 0 : N\<rbrakk> \<Longrightarrow> a = 0 : N"
apply (rule EqE)
apply (rule add_eq0_lemma [THEN ProdE])
apply (rule_tac [3] EqI)
@@ -358,8 +358,7 @@
(*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)"
+ "\<lbrakk>a:N; b:N; a |-| b = 0 : N\<rbrakk> \<Longrightarrow> ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
apply (unfold absdiff_def)
apply intr
apply eqintr
@@ -371,7 +370,7 @@
(*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: "\<lbrakk>a |-| b = 0 : N; a:N; b:N\<rbrakk> \<Longrightarrow> a = b : N"
apply (rule EqE)
apply (rule absdiff_eq0_lem [THEN SumE])
apply eqintr
@@ -385,12 +384,12 @@
(*typing of remainder: short and long versions*)
-lemma mod_typing: "[| a:N; b:N |] ==> a mod b : N"
+lemma mod_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a mod b : N"
apply (unfold mod_def)
apply (typechk absdiff_typing)
done
-lemma mod_typingL: "[| a=c:N; b=d:N |] ==> a mod b = c mod d : N"
+lemma mod_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a mod b = c mod d : N"
apply (unfold mod_def)
apply (equal absdiff_typingL)
done
@@ -398,13 +397,13 @@
(*computation for mod : 0 and successor cases*)
-lemma modC0: "b:N ==> 0 mod b = 0 : N"
+lemma modC0: "b:N \<Longrightarrow> 0 mod b = 0 : N"
apply (unfold mod_def)
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: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow>
+ succ(a) mod b = rec(succ(a mod b) |-| b, 0, \<lambda>x y. succ(a mod b)) : N"
apply (unfold mod_def)
apply (rew absdiff_typing)
done
@@ -412,12 +411,12 @@
(*typing of quotient: short and long versions*)
-lemma div_typing: "[| a:N; b:N |] ==> a div b : N"
+lemma div_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a div b : N"
apply (unfold div_def)
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: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a div b = c div d : N"
apply (unfold div_def)
apply (equal absdiff_typingL mod_typingL)
done
@@ -427,22 +426,21 @@
(*computation for quotient: 0 and successor cases*)
-lemma divC0: "b:N ==> 0 div b = 0 : N"
+lemma divC0: "b:N \<Longrightarrow> 0 div b = 0 : N"
apply (unfold div_def)
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: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow>
+ succ(a) div b = rec(succ(a) mod b, succ(a div b), \<lambda>x y. a div b) : N"
apply (unfold div_def)
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: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow>
+ succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), \<lambda>x y. a div b) : N"
apply (rule divC_succ [THEN trans_elem])
apply (rew div_typing_rls modC_succ)
apply (NE "succ (a mod b) |-|b")
@@ -450,7 +448,7 @@
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(<ka, eq>)) :
+lemma iszero_decidable: "a:N \<Longrightarrow> rec(a, inl(eq), \<lambda>ka kb. inr(<ka, eq>)) :
Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
apply (NE a)
apply (rule_tac [3] PlusI_inr)
@@ -460,7 +458,7 @@
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"
+lemma mod_div_equality: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> 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)
--- a/src/CTT/Bool.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CTT/Bool.thy Tue Nov 11 15:55:31 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]\<Rightarrow>i" where
+ "cond(a,b,c) == when(a, \<lambda>u. b, \<lambda>u. c)"
lemmas bool_defs = Bool_def true_def false_def cond_def
@@ -50,17 +50,15 @@
done
(*elimination rule: typing of cond*)
-lemma boolE:
- "[| p:Bool; a : C(true); b : C(false) |] ==> cond(p,a,b) : C(p)"
+lemma boolE: "\<lbrakk>p:Bool; a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(p,a,b) : C(p)"
apply (unfold bool_defs)
apply typechk
apply (erule_tac [!] TE)
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: "\<lbrakk>p = q : Bool; a = c : C(true); b = d : C(false)\<rbrakk>
+ \<Longrightarrow> 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,8 +66,7 @@
(*computation rules for true, false*)
-lemma boolC_true:
- "[| a : C(true); b : C(false) |] ==> cond(true,a,b) = a : C(true)"
+lemma boolC_true: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(true,a,b) = a : C(true)"
apply (unfold bool_defs)
apply (rule comp_rls)
apply typechk
@@ -77,8 +74,7 @@
apply typechk
done
-lemma boolC_false:
- "[| a : C(true); b : C(false) |] ==> cond(false,a,b) = b : C(false)"
+lemma boolC_false: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(false,a,b) = b : C(false)"
apply (unfold bool_defs)
apply (rule comp_rls)
apply typechk
--- a/src/CTT/CTT.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CTT/CTT.thy Tue Nov 11 15:55:31 2014 +0100
@@ -20,56 +20,56 @@
(*Types*)
F :: "t"
T :: "t" (*F is empty, T contains one element*)
- contr :: "i=>i"
+ contr :: "i\<Rightarrow>i"
tt :: "i"
(*Natural numbers*)
N :: "t"
- succ :: "i=>i"
- rec :: "[i, i, [i,i]=>i] => i"
+ succ :: "i\<Rightarrow>i"
+ rec :: "[i, i, [i,i]\<Rightarrow>i] \<Rightarrow> i"
(*Unions*)
- inl :: "i=>i"
- inr :: "i=>i"
- when :: "[i, i=>i, i=>i]=>i"
+ inl :: "i\<Rightarrow>i"
+ inr :: "i\<Rightarrow>i"
+ when :: "[i, i\<Rightarrow>i, i\<Rightarrow>i]\<Rightarrow>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\<Rightarrow>t]\<Rightarrow>t"
+ fst :: "i\<Rightarrow>i"
+ snd :: "i\<Rightarrow>i"
+ split :: "[i, [i,i]\<Rightarrow>i] \<Rightarrow>i"
(*General Product and Function Space*)
- Prod :: "[t, i=>t]=>t"
+ Prod :: "[t, i\<Rightarrow>t]\<Rightarrow>t"
(*Types*)
- Plus :: "[t,t]=>t" (infixr "+" 40)
+ Plus :: "[t,t]\<Rightarrow>t" (infixr "+" 40)
(*Equality type*)
- Eq :: "[t,i,i]=>t"
+ Eq :: "[t,i,i]\<Rightarrow>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 \<Rightarrow> prop" ("(_ type)" [10] 5)
+ Eqtype :: "[t,t]\<Rightarrow>prop" ("(_ =/ _)" [10,10] 5)
+ Elem :: "[i, t]\<Rightarrow>prop" ("(_ /: _)" [10,10] 5)
+ Eqelem :: "[i,i,t]\<Rightarrow>prop" ("(_ =/ _ :/ _)" [10,10,10] 5)
+ Reduce :: "[i,i]\<Rightarrow>prop" ("Reduce[_,_]")
(*Types*)
(*Functions*)
- lambda :: "(i => i) => i" (binder "lam " 10)
- app :: "[i,i]=>i" (infixl "`" 60)
+ lambda :: "(i \<Rightarrow> i) \<Rightarrow> i" (binder "lam " 10)
+ app :: "[i,i]\<Rightarrow>i" (infixl "`" 60)
(*Natural numbers*)
Zero :: "i" ("0")
(*Pairing*)
- pair :: "[i,i]=>i" ("(1<_,/_>)")
+ pair :: "[i,i]\<Rightarrow>i" ("(1<_,/_>)")
syntax
- "_PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10)
- "_SUM" :: "[idt,t,t]=>t" ("(3SUM _:_./ _)" 10)
+ "_PROD" :: "[idt,t,t]\<Rightarrow>t" ("(3PROD _:_./ _)" 10)
+ "_SUM" :: "[idt,t,t]\<Rightarrow>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, \<lambda>x. B)"
+ "SUM x:A. B" == "CONST Sum(A, \<lambda>x. B)"
abbreviation
- Arrow :: "[t,t]=>t" (infixr "-->" 30) where
+ Arrow :: "[t,t]\<Rightarrow>t" (infixr "-->" 30) where
"A --> B == PROD _:A. B"
abbreviation
- Times :: "[t,t]=>t" (infixr "*" 50) where
+ Times :: "[t,t]\<Rightarrow>t" (infixr "*" 50) where
"A * B == SUM _:A. B"
notation (xsymbols)
@@ -86,12 +86,12 @@
Times (infixr "\<times>" 50)
syntax (xsymbols)
- "_PROD" :: "[idt,t,t] => t" ("(3\<Pi> _\<in>_./ _)" 10)
- "_SUM" :: "[idt,t,t] => t" ("(3\<Sigma> _\<in>_./ _)" 10)
+ "_PROD" :: "[idt,t,t] \<Rightarrow> t" ("(3\<Pi> _\<in>_./ _)" 10)
+ "_SUM" :: "[idt,t,t] \<Rightarrow> t" ("(3\<Sigma> _\<in>_./ _)" 10)
syntax (HTML output)
- "_PROD" :: "[idt,t,t] => t" ("(3\<Pi> _\<in>_./ _)" 10)
- "_SUM" :: "[idt,t,t] => t" ("(3\<Sigma> _\<in>_./ _)" 10)
+ "_PROD" :: "[idt,t,t] \<Rightarrow> t" ("(3\<Pi> _\<in>_./ _)" 10)
+ "_SUM" :: "[idt,t,t] \<Rightarrow> t" ("(3\<Sigma> _\<in>_./ _)" 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: "\<And>a. Reduce[a,a]" and
- red_if_equal: "\<And>a b A. a = b : A ==> Reduce[a,b]" and
- trans_red: "\<And>a b c A. [| a = b : A; Reduce[b,c] |] ==> a = c : A" and
+ red_if_equal: "\<And>a b A. a = b : A \<Longrightarrow> Reduce[a,b]" and
+ trans_red: "\<And>a b c A. \<lbrakk>a = b : A; Reduce[b,c]\<rbrakk> \<Longrightarrow> a = c : A" and
(*Reflexivity*)
- refl_type: "\<And>A. A type ==> A = A" and
- refl_elem: "\<And>a A. a : A ==> a = a : A" and
+ refl_type: "\<And>A. A type \<Longrightarrow> A = A" and
+ refl_elem: "\<And>a A. a : A \<Longrightarrow> a = a : A" and
(*Symmetry*)
- sym_type: "\<And>A B. A = B ==> B = A" and
- sym_elem: "\<And>a b A. a = b : A ==> b = a : A" and
+ sym_type: "\<And>A B. A = B \<Longrightarrow> B = A" and
+ sym_elem: "\<And>a b A. a = b : A \<Longrightarrow> b = a : A" and
(*Transitivity*)
- trans_type: "\<And>A B C. [| A = B; B = C |] ==> A = C" and
- trans_elem: "\<And>a b c A. [| a = b : A; b = c : A |] ==> a = c : A" and
+ trans_type: "\<And>A B C. \<lbrakk>A = B; B = C\<rbrakk> \<Longrightarrow> A = C" and
+ trans_elem: "\<And>a b c A. \<lbrakk>a = b : A; b = c : A\<rbrakk> \<Longrightarrow> a = c : A" and
- equal_types: "\<And>a A B. [| a : A; A = B |] ==> a : B" and
- equal_typesL: "\<And>a b A B. [| a = b : A; A = B |] ==> a = b : B" and
+ equal_types: "\<And>a A B. \<lbrakk>a : A; A = B\<rbrakk> \<Longrightarrow> a : B" and
+ equal_typesL: "\<And>a b A B. \<lbrakk>a = b : A; A = B\<rbrakk> \<Longrightarrow> a = b : B" and
(*Substitution*)
- subst_type: "\<And>a A B. [| a : A; !!z. z:A ==> B(z) type |] ==> B(a) type" and
- subst_typeL: "\<And>a c A B D. [| a = c : A; !!z. z:A ==> B(z) = D(z) |] ==> B(a) = D(c)" and
+ subst_type: "\<And>a A B. \<lbrakk>a : A; \<And>z. z:A \<Longrightarrow> B(z) type\<rbrakk> \<Longrightarrow> B(a) type" and
+ subst_typeL: "\<And>a c A B D. \<lbrakk>a = c : A; \<And>z. z:A \<Longrightarrow> B(z) = D(z)\<rbrakk> \<Longrightarrow> B(a) = D(c)" and
- subst_elem: "\<And>a b A B. [| a : A; !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)" and
+ subst_elem: "\<And>a b A B. \<lbrakk>a : A; \<And>z. z:A \<Longrightarrow> b(z):B(z)\<rbrakk> \<Longrightarrow> b(a):B(a)" and
subst_elemL:
- "\<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
+ "\<And>a b c d A B. \<lbrakk>a = c : A; \<And>z. z:A \<Longrightarrow> b(z)=d(z) : B(z)\<rbrakk> \<Longrightarrow> b(a)=d(c) : B(a)" and
(*The type N -- natural numbers*)
NF: "N type" and
NI0: "0 : N" and
- NI_succ: "\<And>a. a : N ==> succ(a) : N" and
- NI_succL: "\<And>a b. a = b : N ==> succ(a) = succ(b) : N" and
+ NI_succ: "\<And>a. a : N \<Longrightarrow> succ(a) : N" and
+ NI_succL: "\<And>a b. a = b : N \<Longrightarrow> succ(a) = succ(b) : N" and
NE:
- "\<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
+ "\<And>p a b C. \<lbrakk>p: N; a: C(0); \<And>u v. \<lbrakk>u: N; v: C(u)\<rbrakk> \<Longrightarrow> b(u,v): C(succ(u))\<rbrakk>
+ \<Longrightarrow> rec(p, a, \<lambda>u v. b(u,v)) : C(p)" and
NEL:
- "\<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
+ "\<And>p q a b c d C. \<lbrakk>p = q : N; a = c : C(0);
+ \<And>u v. \<lbrakk>u: N; v: C(u)\<rbrakk> \<Longrightarrow> b(u,v) = d(u,v): C(succ(u))\<rbrakk>
+ \<Longrightarrow> rec(p, a, \<lambda>u v. b(u,v)) = rec(q,c,d) : C(p)" and
NC0:
- "\<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
+ "\<And>a b C. \<lbrakk>a: C(0); \<And>u v. \<lbrakk>u: N; v: C(u)\<rbrakk> \<Longrightarrow> b(u,v): C(succ(u))\<rbrakk>
+ \<Longrightarrow> rec(0, a, \<lambda>u v. b(u,v)) = a : C(0)" and
NC_succ:
- "\<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
+ "\<And>p a b C. \<lbrakk>p: N; a: C(0); \<And>u v. \<lbrakk>u: N; v: C(u)\<rbrakk> \<Longrightarrow> b(u,v): C(succ(u))\<rbrakk> \<Longrightarrow>
+ rec(succ(p), a, \<lambda>u v. b(u,v)) = b(p, rec(p, a, \<lambda>u v. b(u,v))) : C(succ(p))" and
(*The fourth Peano axiom. See page 91 of Martin-Lof's book*)
- zero_ne_succ:
- "\<And>a. [| a: N; 0 = succ(a) : N |] ==> 0: F" and
+ zero_ne_succ: "\<And>a. \<lbrakk>a: N; 0 = succ(a) : N\<rbrakk> \<Longrightarrow> 0: F" and
(*The Product of a family of types*)
- ProdF: "\<And>A B. [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type" and
+ ProdF: "\<And>A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> B(x) type\<rbrakk> \<Longrightarrow> PROD x:A. B(x) type" and
ProdFL:
- "\<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
+ "\<And>A B C D. \<lbrakk>A = C; \<And>x. x:A \<Longrightarrow> B(x) = D(x)\<rbrakk> \<Longrightarrow> PROD x:A. B(x) = PROD x:C. D(x)" and
ProdI:
- "\<And>b A B. [| A type; !!x. x:A ==> b(x):B(x)|] ==> lam x. b(x) : PROD x:A. B(x)" and
+ "\<And>b A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> b(x):B(x)\<rbrakk> \<Longrightarrow> lam x. b(x) : PROD x:A. B(x)" and
- ProdIL:
- "\<And>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: "\<And>b c A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> b(x) = c(x) : B(x)\<rbrakk> \<Longrightarrow>
+ lam x. b(x) = lam x. c(x) : PROD x:A. B(x)" and
- ProdE: "\<And>p a A B. [| p : PROD x:A. B(x); a : A |] ==> p`a : B(a)" and
- ProdEL: "\<And>p q a b A B. [| p=q: PROD x:A. B(x); a=b : A |] ==> p`a = q`b : B(a)" and
+ ProdE: "\<And>p a A B. \<lbrakk>p : PROD x:A. B(x); a : A\<rbrakk> \<Longrightarrow> p`a : B(a)" and
+ ProdEL: "\<And>p q a b A B. \<lbrakk>p = q: PROD x:A. B(x); a = b : A\<rbrakk> \<Longrightarrow> p`a = q`b : B(a)" and
- ProdC:
- "\<And>a b A B. [| a : A; !!x. x:A ==> b(x) : B(x)|] ==>
- (lam x. b(x)) ` a = b(a) : B(a)" and
+ ProdC: "\<And>a b A B. \<lbrakk>a : A; \<And>x. x:A \<Longrightarrow> b(x) : B(x)\<rbrakk> \<Longrightarrow> (lam x. b(x)) ` a = b(a) : B(a)" and
- ProdC2:
- "\<And>p A B. p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)" and
+ ProdC2: "\<And>p A B. p : PROD x:A. B(x) \<Longrightarrow> (lam x. p`x) = p : PROD x:A. B(x)" and
(*The Sum of a family of types*)
- SumF: "\<And>A B. [| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type" and
- SumFL:
- "\<And>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: "\<And>A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> B(x) type\<rbrakk> \<Longrightarrow> SUM x:A. B(x) type" and
+ SumFL: "\<And>A B C D. \<lbrakk>A = C; \<And>x. x:A \<Longrightarrow> B(x) = D(x)\<rbrakk> \<Longrightarrow> SUM x:A. B(x) = SUM x:C. D(x)" and
- SumI: "\<And>a b A B. [| a : A; b : B(a) |] ==> <a,b> : SUM x:A. B(x)" and
- SumIL: "\<And>a b c d A B. [| a=c:A; b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x)" and
+ SumI: "\<And>a b A B. \<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> <a,b> : SUM x:A. B(x)" and
+ SumIL: "\<And>a b c d A B. \<lbrakk> a = c : A; b = d : B(a)\<rbrakk> \<Longrightarrow> <a,b> = <c,d> : SUM x:A. B(x)" and
- SumE:
- "\<And>p c A B C. [| p: SUM x:A. B(x); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |]
- ==> split(p, %x y. c(x,y)) : C(p)" and
+ SumE: "\<And>p c A B C. \<lbrakk>p: SUM x:A. B(x); \<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> c(x,y): C(<x,y>)\<rbrakk>
+ \<Longrightarrow> split(p, \<lambda>x y. c(x,y)) : C(p)" and
- SumEL:
- "\<And>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(<x,y>)|]
- ==> split(p, %x y. c(x,y)) = split(q, % x y. d(x,y)) : C(p)" and
+ SumEL: "\<And>p q c d A B C. \<lbrakk>p = q : SUM x:A. B(x);
+ \<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> c(x,y)=d(x,y): C(<x,y>)\<rbrakk>
+ \<Longrightarrow> split(p, \<lambda>x y. c(x,y)) = split(q, \<lambda>x y. d(x,y)) : C(p)" and
- SumC:
- "\<And>a b c A B C. [| a: A; b: B(a); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |]
- ==> split(<a,b>, %x y. c(x,y)) = c(a,b) : C(<a,b>)" and
+ SumC: "\<And>a b c A B C. \<lbrakk>a: A; b: B(a); \<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> c(x,y): C(<x,y>)\<rbrakk>
+ \<Longrightarrow> split(<a,b>, \<lambda>x y. c(x,y)) = c(a,b) : C(<a,b>)" and
- fst_def: "\<And>a. fst(a) == split(a, %x y. x)" and
- snd_def: "\<And>a. snd(a) == split(a, %x y. y)" and
+ fst_def: "\<And>a. fst(a) == split(a, \<lambda>x y. x)" and
+ snd_def: "\<And>a. snd(a) == split(a, \<lambda>x y. y)" and
(*The sum of two types*)
- PlusF: "\<And>A B. [| A type; B type |] ==> A+B type" and
- PlusFL: "\<And>A B C D. [| A = C; B = D |] ==> A+B = C+D" and
+ PlusF: "\<And>A B. \<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> A+B type" and
+ PlusFL: "\<And>A B C D. \<lbrakk>A = C; B = D\<rbrakk> \<Longrightarrow> A+B = C+D" and
- PlusI_inl: "\<And>a A B. [| a : A; B type |] ==> inl(a) : A+B" and
- PlusI_inlL: "\<And>a c A B. [| a = c : A; B type |] ==> inl(a) = inl(c) : A+B" and
+ PlusI_inl: "\<And>a A B. \<lbrakk>a : A; B type\<rbrakk> \<Longrightarrow> inl(a) : A+B" and
+ PlusI_inlL: "\<And>a c A B. \<lbrakk>a = c : A; B type\<rbrakk> \<Longrightarrow> inl(a) = inl(c) : A+B" and
- PlusI_inr: "\<And>b A B. [| A type; b : B |] ==> inr(b) : A+B" and
- PlusI_inrL: "\<And>b d A B. [| A type; b = d : B |] ==> inr(b) = inr(d) : A+B" and
+ PlusI_inr: "\<And>b A B. \<lbrakk>A type; b : B\<rbrakk> \<Longrightarrow> inr(b) : A+B" and
+ PlusI_inrL: "\<And>b d A B. \<lbrakk>A type; b = d : B\<rbrakk> \<Longrightarrow> inr(b) = inr(d) : A+B" and
PlusE:
- "\<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
+ "\<And>p c d A B C. \<lbrakk>p: A+B;
+ \<And>x. x:A \<Longrightarrow> c(x): C(inl(x));
+ \<And>y. y:B \<Longrightarrow> d(y): C(inr(y)) \<rbrakk> \<Longrightarrow> when(p, \<lambda>x. c(x), \<lambda>y. d(y)) : C(p)" and
PlusEL:
- "\<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
+ "\<And>p q c d e f A B C. \<lbrakk>p = q : A+B;
+ \<And>x. x: A \<Longrightarrow> c(x) = e(x) : C(inl(x));
+ \<And>y. y: B \<Longrightarrow> d(y) = f(y) : C(inr(y))\<rbrakk>
+ \<Longrightarrow> when(p, \<lambda>x. c(x), \<lambda>y. d(y)) = when(q, \<lambda>x. e(x), \<lambda>y. f(y)) : C(p)" and
PlusC_inl:
- "\<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
+ "\<And>a c d A C. \<lbrakk>a: A;
+ \<And>x. x:A \<Longrightarrow> c(x): C(inl(x));
+ \<And>y. y:B \<Longrightarrow> d(y): C(inr(y)) \<rbrakk>
+ \<Longrightarrow> when(inl(a), \<lambda>x. c(x), \<lambda>y. d(y)) = c(a) : C(inl(a))" and
PlusC_inr:
- "\<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
+ "\<And>b c d A B C. \<lbrakk>b: B;
+ \<And>x. x:A \<Longrightarrow> c(x): C(inl(x));
+ \<And>y. y:B \<Longrightarrow> d(y): C(inr(y))\<rbrakk>
+ \<Longrightarrow> when(inr(b), \<lambda>x. c(x), \<lambda>y. d(y)) = d(b) : C(inr(b))" and
(*The type Eq*)
- EqF: "\<And>a b A. [| A type; a : A; b : A |] ==> Eq(A,a,b) type" and
- EqFL: "\<And>a b c d A B. [| A=B; a=c: A; b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d)" and
- EqI: "\<And>a b A. a = b : A ==> eq : Eq(A,a,b)" and
- EqE: "\<And>p a b A. p : Eq(A,a,b) ==> a = b : A" and
+ EqF: "\<And>a b A. \<lbrakk>A type; a : A; b : A\<rbrakk> \<Longrightarrow> Eq(A,a,b) type" and
+ EqFL: "\<And>a b c d A B. \<lbrakk>A = B; a = c : A; b = d : A\<rbrakk> \<Longrightarrow> Eq(A,a,b) = Eq(B,c,d)" and
+ EqI: "\<And>a b A. a = b : A \<Longrightarrow> eq : Eq(A,a,b)" and
+ EqE: "\<And>p a b A. p : Eq(A,a,b) \<Longrightarrow> a = b : A" and
(*By equality of types, can prove C(p) from C(eq), an elimination rule*)
- EqC: "\<And>p a b A. p : Eq(A,a,b) ==> p = eq : Eq(A,a,b)" and
+ EqC: "\<And>p a b A. p : Eq(A,a,b) \<Longrightarrow> p = eq : Eq(A,a,b)" and
(*The type F*)
FF: "F type" and
- FE: "\<And>p C. [| p: F; C type |] ==> contr(p) : C" and
- FEL: "\<And>p q C. [| p = q : F; C type |] ==> contr(p) = contr(q) : C" and
+ FE: "\<And>p C. \<lbrakk>p: F; C type\<rbrakk> \<Longrightarrow> contr(p) : C" and
+ FEL: "\<And>p q C. \<lbrakk>p = q : F; C type\<rbrakk> \<Longrightarrow> 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: "\<And>p c C. [| p : T; c : C(tt) |] ==> c : C(p)" and
- TEL: "\<And>p q c d C. [| p = q : T; c = d : C(tt) |] ==> c = d : C(p)" and
- TC: "\<And>p. p : T ==> p = tt : T"
+ TE: "\<And>p c C. \<lbrakk>p : T; c : C(tt)\<rbrakk> \<Longrightarrow> c : C(p)" and
+ TEL: "\<And>p q c d C. \<lbrakk>p = q : T; c = d : C(tt)\<rbrakk> \<Longrightarrow> c = d : C(p)" and
+ TC: "\<And>p. p : T \<Longrightarrow> 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) |] ==> <c,d> = <a,b> : Sum(A,B)"
+lemma SumIL2: "\<lbrakk>c = a : A; d = b : B(a)\<rbrakk> \<Longrightarrow> <c,d> = <a,b> : 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 "\<And>z. z: B(a) \<Longrightarrow> c(z): C(z)"
shows "c(p`a): C(p`a)"
apply (rule assms ProdE)+
done
@@ -389,7 +381,7 @@
subsection {* Simplification *}
(*To simplify the type in a goal*)
-lemma replace_type: "[| B = A; a : A |] ==> a : B"
+lemma replace_type: "\<lbrakk>B = A; a : A\<rbrakk> \<Longrightarrow> a : B"
apply (rule equal_types)
apply (rule_tac [2] sym_type)
apply assumption+
@@ -398,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: "\<And>z. z:A \<Longrightarrow> B(z) type"
shows "B(a)=B(c)"
apply (rule subst_typeL)
apply (rule_tac [2] refl_type)
@@ -478,7 +470,7 @@
subsection {* The elimination rules for fst/snd *}
-lemma SumE_fst: "p : Sum(A,B) ==> fst(p) : A"
+lemma SumE_fst: "p : Sum(A,B) \<Longrightarrow> fst(p) : A"
apply (unfold basic_defs)
apply (erule SumE)
apply assumption
@@ -488,7 +480,7 @@
lemma SumE_snd:
assumes major: "p: Sum(A,B)"
and "A type"
- and "!!x. x:A ==> B(x) type"
+ and "\<And>x. x:A \<Longrightarrow> B(x) type"
shows "snd(p) : B(fst(p))"
apply (unfold basic_defs)
apply (rule major [THEN SumE])
--- a/src/CTT/ex/Elimination.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CTT/ex/Elimination.thy Tue Nov 11 15:55:31 2014 +0100
@@ -14,80 +14,80 @@
text "This finds the functions fst and snd!"
-schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
+schematic_lemma [folded basic_defs]: "A type \<Longrightarrow> ?a : (A*A) --> A"
apply pc
done
-schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
+schematic_lemma [folded basic_defs]: "A type \<Longrightarrow> ?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"
+schematic_lemma "A type \<Longrightarrow> ?a : ((A + (A-->F)) --> F) --> F"
apply intr
apply (rule ProdE)
apply assumption
apply pc
done
-schematic_lemma "[| A type; B type |] ==> ?a : (A*B) --> (B*A)"
+schematic_lemma "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A*B) \<longrightarrow> (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)"
+schematic_lemma "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?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)"
+schematic_lemma "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?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 "\<And>x. x:A \<Longrightarrow> B(x) type"
+ and "\<And>x. x:A \<Longrightarrow> C(x) type"
shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))"
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))"
+schematic_lemma "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?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 "\<And>x. x:A \<Longrightarrow> B(x) type"
+ and "\<And>z. z: (SUM x:A. B(x)) \<Longrightarrow> C(z) type"
shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).
(PROD x:A . PROD y:B(x) . C(<x,y>))"
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)"
+schematic_lemma "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?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 "\<And>x. x:A \<Longrightarrow> B(x) type"
+ and "\<And>z. z: (SUM x:A . B(x)) \<Longrightarrow> C(z) type"
shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>))
--> (PROD z : (SUM x:A . B(x)) . C(z))"
apply (pc assms)
done
text "Function application"
-schematic_lemma "[| A type; B type |] ==> ?a : ((A --> B) * A) --> B"
+schematic_lemma "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A --> B) * A) --> B"
apply pc
done
@@ -95,7 +95,7 @@
schematic_lemma
assumes "A type"
and "B type"
- and "!!x y.[| x:A; y:B |] ==> C(x,y) type"
+ and "\<And>x y. \<lbrakk>x:A; y:B\<rbrakk> \<Longrightarrow> C(x,y) type"
shows
"?a : (SUM y:B . PROD x:A . C(x,y))
--> (PROD x:A . SUM y:B . C(x,y))"
@@ -105,8 +105,8 @@
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 "\<And>x. x:A \<Longrightarrow> B(x) type"
+ and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> 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 (pc assms)
@@ -116,7 +116,7 @@
schematic_lemma
assumes "A type"
and "B type"
- and "!!z. z: A+B ==> C(z) type"
+ and "\<And>z. z: A+B \<Longrightarrow> C(z) type"
shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))
--> (PROD z: A+B. C(z))"
apply (pc assms)
@@ -124,7 +124,7 @@
(*towards AXIOM OF CHOICE*)
schematic_lemma [folded basic_defs]:
- "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)"
+ "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A --> B*C) --> (A-->B) * (A-->C)"
apply pc
done
@@ -133,8 +133,8 @@
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 "\<And>x. x:A \<Longrightarrow> B(x) type"
+ and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> 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 (intr assms)
@@ -151,8 +151,8 @@
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 "\<And>x. x:A \<Longrightarrow> B(x) type"
+ and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> 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 (intr assms)
@@ -175,11 +175,11 @@
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. <x,<y,z>>) ` w) *)
+ lam u. split(u,\<lambda>v w.split(v,\<lambda>x y.lam z. <x,<y,z>>) ` w) *)
schematic_lemma
assumes "A type"
and "B type"
- and "!!z. z:A*B ==> C(z) type"
+ and "\<And>z. z:A*B \<Longrightarrow> C(z) type"
shows "?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))"
apply (rule intr_rls)
apply (tactic {* biresolve_tac safe_brls 2 *})
--- a/src/CTT/ex/Equality.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CTT/ex/Equality.thy Tue Nov 11 15:55:31 2014 +0100
@@ -9,54 +9,53 @@
imports "../CTT"
begin
-lemma split_eq: "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)"
+lemma split_eq: "p : Sum(A,B) \<Longrightarrow> split(p,pair) = p : Sum(A,B)"
apply (rule EqE)
apply (rule elim_rls, assumption)
apply rew
done
-lemma when_eq: "[| A type; B type; p : A+B |] ==> when(p,inl,inr) = p : A + B"
+lemma when_eq: "\<lbrakk>A type; B type; p : A+B\<rbrakk> \<Longrightarrow> when(p,inl,inr) = p : A + B"
apply (rule EqE)
apply (rule elim_rls, assumption)
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 \<Longrightarrow> rec(p,0, \<lambda>y z. succ(y)) = p : N"
apply (rule EqE)
apply (rule elim_rls, assumption)
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 \<Longrightarrow> rec(p,0, \<lambda>y z. succ(z)) = p : N"
apply (rule EqE)
apply (rule elim_rls, assumption)
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"
+lemma "\<lbrakk>a:N; b:N; c:N\<rbrakk>
+ \<Longrightarrow> rec(rec(a, b, \<lambda>x y. succ(y)), c, \<lambda>x y. succ(y)) =
+ rec(a, rec(b, c, \<lambda>x y. succ(y)), \<lambda>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) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)"
+lemma "p : Sum(A,B) \<Longrightarrow> <split(p,\<lambda>x y. x), split(p,\<lambda>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.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A"
+lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (lam u. split(u, \<lambda>v w.<w,v>)) ` <a,b> = <b,a> : 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.<w,v>)) =
+lemma "(lam f. lam x. f`(f`x)) ` (lam u. split(u, \<lambda>v w.<w,v>)) =
lam x. x : PROD x:(SUM y:N. N). (SUM y:N. N)"
apply (rule reduction_rls)
apply (rule_tac [3] intrL_rls)
--- a/src/CTT/ex/Synthesis.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CTT/ex/Synthesis.thy Tue Nov 11 15:55:31 2014 +0100
@@ -21,7 +21,7 @@
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,j>, i)"
+ "A type \<Longrightarrow> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)"
apply intr
apply eqintr
apply (rule_tac [2] reduction_rls)
--- a/src/CTT/ex/Typechecking.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/CTT/ex/Typechecking.thy Tue Nov 11 15:55:31 2014 +0100
@@ -50,17 +50,17 @@
done
text "typechecking an application of fst"
-schematic_lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
+schematic_lemma "(lam u. split(u, \<lambda>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"
+schematic_lemma "lam n. rec(n, 0, \<lambda>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"
+schematic_lemma "lam n. lam m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
apply typechk
done
@@ -79,7 +79,7 @@
done
text "typechecking fst (as a function object)"
-schematic_lemma "lam i. split(i, %j k. j) : ?A"
+schematic_lemma "lam i. split(i, \<lambda>j k. j) : ?A"
apply typechk
apply N
done
--- a/src/LCF/LCF.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/LCF/LCF.thy Tue Nov 11 15:55:31 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 \<Rightarrow> 'a) \<Rightarrow> 'a"
+ FST :: "'a*'b \<Rightarrow> 'a"
+ SND :: "'a*'b \<Rightarrow> 'b"
+ INL :: "'a \<Rightarrow> 'a+'b"
+ INR :: "'b \<Rightarrow> 'a+'b"
+ WHEN :: "['a\<Rightarrow>'c, 'b\<Rightarrow>'c, 'a+'b] \<Rightarrow> 'c"
+ adm :: "('a \<Rightarrow> o) \<Rightarrow> 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] \<Rightarrow> 'a*'b" ("(1<_,/_>)" [0,0] 100)
+ COND :: "[tr,'a,'a] \<Rightarrow> 'a" ("(_ \<Rightarrow>/ (_ |/ _))" [60,60,60] 60)
+ less :: "['a,'a] \<Rightarrow> o" (infixl "<<" 50)
axiomatization where
(** DOMAIN THEORY **)
- eq_def: "x=y == x << y & y << x" and
+ eq_def: "x=y == x << y \<and> y << x" and
- less_trans: "[| x << y; y << z |] ==> x << z" and
+ less_trans: "\<lbrakk>x << y; y << z\<rbrakk> \<Longrightarrow> x << z" and
- less_ext: "(ALL x. f(x) << g(x)) ==> f << g" and
+ less_ext: "(\<forall>x. f(x) << g(x)) \<Longrightarrow> f << g" and
- mono: "[| f << g; x << y |] ==> f(x) << g(y)" and
+ mono: "\<lbrakk>f << g; x << y\<rbrakk> \<Longrightarrow> 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 \<or> p=TT \<or> 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: "\<not> TT << FF" and
+ not_FF_less_TT: "\<not> FF << TT" and
+ not_TT_less_UU: "\<not> TT << UU" and
+ not_FF_less_UU: "\<not> 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 \<Rightarrow> x | y = UU" and
+ COND_TT: "TT \<Rightarrow> x | y = x" and
+ COND_FF: "FF \<Rightarrow> 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: "\<not>x=UU \<Longrightarrow> \<not>INL(x)=UU" and
+ INR_DEF: "\<not>x=UU \<Longrightarrow> \<not>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: "\<not>x=UU \<Longrightarrow> WHEN(f,g,INL(x)) = f(x)" and
+ WHEN_INR: "\<not>x=UU \<Longrightarrow> 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 \<or> (\<exists>x. \<not>x=UU \<and> z = INL(x)) \<or> (\<exists>y. \<not>y=UU \<and> 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: "\<lbrakk>adm(P); P(UU); \<forall>x. P(x) \<longrightarrow> P(f(x))\<rbrakk> \<Longrightarrow> 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: "\<And>t u. adm(%x. t(x) << u(x))" and
- adm_not_less: "\<And>t u. adm(%x.~ t(x) << u)" and
- adm_not_free: "\<And>A. adm(%x. A)" and
- adm_subst: "\<And>P t. adm(P) ==> adm(%x. P(t(x)))" and
- adm_conj: "\<And>P Q. [| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))" and
- adm_disj: "\<And>P Q. [| adm(P); adm(Q) |] ==> adm(%x. P(x)|Q(x))" and
- adm_imp: "\<And>P Q. [| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))" and
- adm_all: "\<And>P. (!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))"
+ adm_less: "\<And>t u. adm(\<lambda>x. t(x) << u(x))" and
+ adm_not_less: "\<And>t u. adm(\<lambda>x.\<not> t(x) << u)" and
+ adm_not_free: "\<And>A. adm(\<lambda>x. A)" and
+ adm_subst: "\<And>P t. adm(P) \<Longrightarrow> adm(\<lambda>x. P(t(x)))" and
+ adm_conj: "\<And>P Q. \<lbrakk>adm(P); adm(Q)\<rbrakk> \<Longrightarrow> adm(\<lambda>x. P(x)\<and>Q(x))" and
+ adm_disj: "\<And>P Q. \<lbrakk>adm(P); adm(Q)\<rbrakk> \<Longrightarrow> adm(\<lambda>x. P(x)\<or>Q(x))" and
+ adm_imp: "\<And>P Q. \<lbrakk>adm(\<lambda>x.\<not>P(x)); adm(Q)\<rbrakk> \<Longrightarrow> adm(\<lambda>x. P(x)\<longrightarrow>Q(x))" and
+ adm_all: "\<And>P. (\<And>y. adm(P(y))) \<Longrightarrow> adm(\<lambda>x. \<forall>y. P(y,x))"
-lemma eq_imp_less1: "x = y ==> x << y"
+lemma eq_imp_less1: "x = y \<Longrightarrow> x << y"
by (simp add: eq_def)
-lemma eq_imp_less2: "x = y ==> y << x"
+lemma eq_imp_less2: "x = y \<Longrightarrow> 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: "\<lbrakk>x << y; y << x\<rbrakk> \<Longrightarrow> 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: "(\<And>x::'a::cpo. f(x)=(g(x)::'b::cpo)) \<Longrightarrow> (\<lambda>x. f(x))=(\<lambda>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: "\<lbrakk>f = g; x = y\<rbrakk> \<Longrightarrow> f(x)=g(y)"
by simp
-lemma less_ap_term: "x << y ==> f(x) << f(y)"
+lemma less_ap_term: "x << y \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> (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 \<Longrightarrow> f(x) = g(x)"
apply (erule cong)
apply (rule refl)
done
-lemma UU_abs: "(%x::'a::cpo. UU) = UU"
+lemma UU_abs: "(\<lambda>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 \<Longrightarrow> 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: "\<lbrakk>P(UU); P(TT); P(FF)\<rbrakk> \<Longrightarrow> \<forall>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: "\<not> B \<Longrightarrow> (A \<Longrightarrow> B) \<Longrightarrow> \<not>A"
by blast
-lemma not_less_imp_not_eq1: "~ x << y \<Longrightarrow> x \<noteq> y"
+lemma not_less_imp_not_eq1: "\<not> x << y \<Longrightarrow> x \<noteq> y"
apply (erule Contrapos)
apply simp
done
-lemma not_less_imp_not_eq2: "~ y << x \<Longrightarrow> x \<noteq> y"
+lemma not_less_imp_not_eq2: "\<not> y << x \<Longrightarrow> x \<noteq> 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))"
+ "\<forall>b. P(b\<Rightarrow>x|y) \<longleftrightarrow> (b=UU\<longrightarrow>P(UU)) \<and> (b=TT\<longrightarrow>P(x)) \<and> (b=FF\<longrightarrow>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)"
+ "\<lbrakk>x = UU \<longrightarrow> P(UU); x = TT \<longrightarrow> P(xa); x = FF \<longrightarrow> P(y)\<rbrakk> \<Longrightarrow> P(x \<Rightarrow> 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(<x,y>))"
+lemma expand_all_PROD: "(\<forall>p. P(p)) \<longleftrightarrow> (\<forall>x y. P(<x,y>))"
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 \<longleftrightarrow> FST(p) << FST(q) \<and> 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 \<longleftrightarrow> FST(p)=FST(q) \<and> SND(p)=SND(q)"
apply (rule iffI)
apply simp
apply (unfold eq_def)
apply (simp add: PROD_less)
done
-lemma PAIR_less [simp]: "<a,b> << <c,d> <-> a<<c & b<<d"
+lemma PAIR_less [simp]: "<a,b> << <c,d> \<longleftrightarrow> a<<c \<and> b<<d"
by (simp add: PROD_less)
-lemma PAIR_eq [simp]: "<a,b> = <c,d> <-> a=c & b=d"
+lemma PAIR_eq [simp]: "<a,b> = <c,d> \<longleftrightarrow> a=c \<and> b=d"
by (simp add: PROD_eq)
lemma UU_is_UU_UU [simp]: "<UU,UU> = UU"
@@ -295,20 +295,20 @@
subsection {* Fixedpoint theory *}
-lemma adm_eq: "adm(%x. t(x)=(u(x)::'a::cpo))"
+lemma adm_eq: "adm(\<lambda>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) \<Longrightarrow> adm(\<lambda>x. \<not> \<not> 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: "\<forall>p. \<not>p=TT \<longleftrightarrow> (p=FF \<or> p=UU)"
+ and not_eq_FF: "\<forall>p. \<not>p=FF \<longleftrightarrow> (p=TT \<or> p=UU)"
+ and not_eq_UU: "\<forall>p. \<not>p=UU \<longleftrightarrow> (p=TT \<or> 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: "\<forall>p::tr. adm(\<lambda>x. \<not>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)+
@@ -325,7 +325,7 @@
REPEAT (resolve_tac @{thms adm_lemmas} i)))
*}
-lemma least_FIX: "f(p) = p ==> FIX(f) << p"
+lemma least_FIX: "f(p) = p \<Longrightarrow> FIX(f) << p"
apply (induct f)
apply (rule minimal)
apply (intro strip)
@@ -335,7 +335,7 @@
lemma lfp_is_FIX:
assumes 1: "f(p) = p"
- and 2: "ALL q. f(q)=q --> p << q"
+ and 2: "\<forall>q. f(q)=q \<longrightarrow> 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(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)"
+lemma FIX_pair: "<FIX(f),FIX(g)> = FIX(\<lambda>p.<f(FST(p)),g(SND(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. <f(FST(p)),g(SND(p))>))"
+lemma FIX1: "FIX(f) = FST(FIX(\<lambda>p. <f(FST(p)),g(SND(p))>))"
by (rule FIX_pair [unfolded PROD_eq FST SND, THEN conjunct1])
-lemma FIX2: "FIX(g) = SND(FIX(%p. <f(FST(p)),g(SND(p))>))"
+lemma FIX2: "FIX(g) = SND(FIX(\<lambda>p. <f(FST(p)),g(SND(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(\<lambda>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: "\<forall>x y. P(x,y) \<longrightarrow> 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. <f(FST(x)),g(SND(x))>"])
+ apply (rule induct [where ?f = "\<lambda>x. <f(FST(x)),g(SND(x))>"])
apply (rule 1)
apply simp
apply (rule 2)
--- a/src/LCF/ex/Ex1.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/LCF/ex/Ex1.thy Tue Nov 11 15:55:31 2014 +0100
@@ -5,13 +5,13 @@
begin
axiomatization
- P :: "'a => tr" and
- G :: "'a => 'a" and
- H :: "'a => 'a" and
- K :: "('a => 'a) => ('a => 'a)"
+ P :: "'a \<Rightarrow> tr" and
+ G :: "'a \<Rightarrow> 'a" and
+ H :: "'a \<Rightarrow> 'a" and
+ K :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
where
P_strict: "P(UU) = UU" and
- K: "K = (%h x. P(x) => x | h(h(G(x))))" and
+ K: "K = (\<lambda>h x. P(x) \<Rightarrow> x | h(h(G(x))))" and
H: "H = FIX(K)"
@@ -27,7 +27,7 @@
apply simp
done
-lemma H_idemp_lemma: "ALL x. H(FIX(K,x)) = FIX(K,x)"
+lemma H_idemp_lemma: "\<forall>x. H(FIX(K,x)) = FIX(K,x)"
apply (induct K)
apply simp
apply (simp split: COND_cases_iff)
@@ -36,7 +36,7 @@
apply simp
done
-lemma H_idemp: "ALL x. H(H(x)) = H(x)"
+lemma H_idemp: "\<forall>x. H(H(x)) = H(x)"
apply (rule H_idemp_lemma [folded H])
done
--- a/src/LCF/ex/Ex2.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/LCF/ex/Ex2.thy Tue Nov 11 15:55:31 2014 +0100
@@ -5,21 +5,21 @@
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 \<Rightarrow> tr" and
+ F :: "'b \<Rightarrow> 'b" and
+ G :: "'a \<Rightarrow> 'a" and
+ H :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and
+ K :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b)"
where
F_strict: "F(UU) = UU" and
- K: "K = (%h x y. P(x) => y | F(h(G(x),y)))" and
+ K: "K = (\<lambda>h x y. P(x) \<Rightarrow> 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: "\<forall>x. F(H(x::'a,y::'b)) = H(x,F(y))"
apply (simplesubst H)
- apply (induct "K:: ('a=>'b=>'b) => ('a=>'b=>'b)")
+ apply (induct "K:: ('a\<Rightarrow>'b\<Rightarrow>'b) \<Rightarrow> ('a\<Rightarrow>'b\<Rightarrow>'b)")
apply simp
apply (simp split: COND_cases_iff)
done
--- a/src/LCF/ex/Ex3.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/LCF/ex/Ex3.thy Tue Nov 11 15:55:31 2014 +0100
@@ -5,8 +5,8 @@
begin
axiomatization
- s :: "'a => 'a" and
- p :: "'a => 'a => 'a"
+ s :: "'a \<Rightarrow> 'a" and
+ p :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
where
p_strict: "p(UU) = UU" and
p_s: "p(s(x),y) = s(p(x,y))"
--- a/src/LCF/ex/Ex4.thy Tue Nov 11 13:50:56 2014 +0100
+++ b/src/LCF/ex/Ex4.thy Tue Nov 11 15:55:31 2014 +0100
@@ -6,7 +6,7 @@
begin
lemma example:
- assumes asms: "f(p) << p" "!!q. f(q) << q ==> p << q"
+ assumes asms: "f(p) << p" "\<And>q. f(q) << q \<Longrightarrow> p << q"
shows "FIX(f)=p"
apply (unfold eq_def)
apply (rule conjI)