--- a/src/HOLCF/FOCUS/Fstream.thy Sat Mar 13 19:06:18 2010 -0800
+++ b/src/HOLCF/FOCUS/Fstream.thy Sat Mar 13 20:15:25 2010 -0800
@@ -58,7 +58,7 @@
lemma fstream_exhaust: "x = UU | (? a y. x = a~> y)"
apply (simp add: fscons_def2)
-apply (cut_tac stream.exhaust)
+apply (cut_tac stream.nchotomy)
apply (fast dest: not_Undef_is_Def [THEN iffD1])
done
@@ -179,7 +179,7 @@
lemma fstream_ind:
"[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x"
-apply (erule stream.ind)
+apply (erule stream.induct)
apply (assumption)
apply (unfold fscons_def2)
apply (fast dest: not_Undef_is_Def [THEN iffD1])
--- a/src/HOLCF/FOCUS/Fstreams.thy Sat Mar 13 19:06:18 2010 -0800
+++ b/src/HOLCF/FOCUS/Fstreams.thy Sat Mar 13 20:15:25 2010 -0800
@@ -135,7 +135,7 @@
lemma fstreams_ind:
"[| adm P; P <>; !!a s. P s ==> P (<a> ooo s) |] ==> P x"
apply (simp add: fsingleton_def2)
-apply (rule stream.ind, auto)
+apply (rule stream.induct, auto)
by (drule not_Undef_is_Def [THEN iffD1], auto)
lemma fstreams_ind2:
@@ -189,7 +189,7 @@
by (simp add: fsingleton_def2)
lemma ft_eq[simp]: "(ft$s = Def a) = (EX t. s = <a> ooo t)"
-apply (rule stream.casedist [of s],auto)
+apply (cases s, auto)
by ((*drule sym,*) auto simp add: fsingleton_def2)
lemma surjective_fstreams: "(<d> ooo y = x) = (ft$x = Def d & rt$x = y)"
--- a/src/HOLCF/IOA/meta_theory/Seq.thy Sat Mar 13 19:06:18 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy Sat Mar 13 20:15:25 2010 -0800
@@ -205,7 +205,7 @@
lemma sfiltersconc: "sfilter$P$(x @@ y) = (sfilter$P$x @@ sfilter$P$y)"
-apply (rule_tac x="x" in seq.ind)
+apply (induct x)
(* adm *)
apply simp
(* base cases *)
@@ -220,7 +220,7 @@
lemma sforallPstakewhileP: "sforall P (stakewhile$P$x)"
apply (simp add: sforall_def)
-apply (rule_tac x="x" in seq.ind)
+apply (induct x)
(* adm *)
apply simp
(* base cases *)
@@ -235,7 +235,7 @@
lemma forallPsfilterP: "sforall P (sfilter$P$x)"
apply (simp add: sforall_def)
-apply (rule_tac x="x" in seq.ind)
+apply (induct x)
(* adm *)
apply simp
(* base cases *)
@@ -318,7 +318,7 @@
!! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)
|] ==> seq_finite(s) --> P(s)"
apply (rule seq_finite_ind_lemma)
-apply (erule seq.finite_ind)
+apply (erule seq.finite_induct)
apply assumption
apply simp
done
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Sat Mar 13 19:06:18 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Sat Mar 13 20:15:25 2010 -0800
@@ -258,7 +258,7 @@
lemma Seq_exhaust: "x = UU | x = nil | (? a s. x = a >> s)"
apply (simp add: Consq_def2)
-apply (cut_tac seq.exhaust)
+apply (cut_tac seq.nchotomy)
apply (fast dest: not_Undef_is_Def [THEN iffD1])
done
@@ -332,7 +332,7 @@
lemma Seq_induct:
"!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x"
-apply (erule (2) seq.ind)
+apply (erule (2) seq.induct)
apply defined
apply (simp add: Consq_def)
done
@@ -459,7 +459,7 @@
done
lemma nilConc [simp]: "s@@ nil = s"
-apply (rule_tac x="s" in seq.ind)
+apply (induct s)
apply simp
apply simp
apply simp
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Mar 13 19:06:18 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Mar 13 20:15:25 2010 -0800
@@ -14,9 +14,9 @@
-> theory
-> { con_consts : term list,
con_betas : thm list,
+ nchotomy : thm,
exhaust : thm,
- casedist : thm,
- con_compacts : thm list,
+ compacts : thm list,
con_rews : thm list,
inverts : thm list,
injects : thm list,
@@ -206,15 +206,15 @@
rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
rtac thm3 1];
in
- val exhaust = prove thy con_betas goal (K tacs);
- val casedist =
- (exhaust RS @{thm exh_casedist0})
+ val nchotomy = prove thy con_betas goal (K tacs);
+ val exhaust =
+ (nchotomy RS @{thm exh_casedist0})
|> rewrite_rule @{thms exh_casedists}
|> Drule.export_without_context;
end;
(* prove compactness rules for constructors *)
- val con_compacts =
+ val compacts =
let
val rules = @{thms compact_sinl compact_sinr compact_spair
compact_up compact_ONE};
@@ -347,9 +347,9 @@
{
con_consts = con_consts,
con_betas = con_betas,
+ nchotomy = nchotomy,
exhaust = exhaust,
- casedist = casedist,
- con_compacts = con_compacts,
+ compacts = compacts,
con_rews = con_rews,
inverts = inverts,
injects = injects,
@@ -369,7 +369,7 @@
(lhsT : typ)
(dbind : binding)
(con_betas : thm list)
- (casedist : thm)
+ (exhaust : thm)
(iso_locale : thm)
(rep_const : term)
(thy : theory)
@@ -674,7 +674,7 @@
(bindings : binding list)
(spec : (term * (bool * typ) list) list)
(lhsT : typ)
- (casedist : thm)
+ (exhaust : thm)
(case_const : typ -> term)
(case_rews : thm list)
(thy : theory) =
@@ -745,7 +745,7 @@
val tacs =
[rtac @{thm iffI} 1,
asm_simp_tac (HOL_basic_ss addsimps dis_stricts) 2,
- rtac casedist 1, atac 1,
+ rtac exhaust 1, atac 1,
DETERM_UNTIL_SOLVED (CHANGED
(asm_full_simp_tac (simple_ss addsimps simps) 1))];
val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x));
@@ -766,7 +766,7 @@
(bindings : binding list)
(spec : (term * (bool * typ) list) list)
(lhsT : typ)
- (casedist : thm)
+ (exhaust : thm)
(case_const : typ -> term)
(case_rews : thm list)
(thy : theory) =
@@ -858,7 +858,7 @@
(bindings : binding list)
(spec : (term * (bool * typ) list) list)
(lhsT : typ)
- (casedist : thm)
+ (exhaust : thm)
(case_const : typ -> term)
(case_rews : thm list)
(thy : theory) =
@@ -1041,7 +1041,7 @@
in
add_constructors con_spec abs_const iso_locale thy
end;
- val {con_consts, con_betas, casedist, ...} = con_result;
+ val {con_consts, con_betas, exhaust, ...} = con_result;
(* define case combinator *)
val ((case_const : typ -> term, cases : thm list), thy) =
@@ -1051,7 +1051,7 @@
val case_spec = map2 prep_con con_consts spec;
in
add_case_combinator case_spec lhsT dbind
- con_betas casedist iso_locale rep_const thy
+ con_betas exhaust iso_locale rep_const thy
end;
(* define and prove theorems for selector functions *)
@@ -1073,7 +1073,7 @@
val dis_spec = map2 prep_con con_consts spec;
in
add_discriminators bindings dis_spec lhsT
- casedist case_const cases thy
+ exhaust case_const cases thy
end
(* define and prove theorems for match combinators *)
@@ -1085,7 +1085,7 @@
val mat_spec = map2 prep_con con_consts spec;
in
add_match_combinators bindings mat_spec lhsT
- casedist case_const cases thy
+ exhaust case_const cases thy
end
(* define and prove theorems for pattern combinators *)
@@ -1097,7 +1097,7 @@
val pat_spec = map2 prep_con con_consts spec;
in
add_pattern_combinators bindings pat_spec lhsT
- casedist case_const cases thy
+ exhaust case_const cases thy
end
(* restore original signature path *)
@@ -1106,9 +1106,9 @@
val result =
{ con_consts = con_consts,
con_betas = con_betas,
- exhaust = #exhaust con_result,
- casedist = casedist,
- con_compacts = #con_compacts con_result,
+ nchotomy = #nchotomy con_result,
+ exhaust = exhaust,
+ compacts = #compacts con_result,
con_rews = #con_rews con_result,
inverts = #inverts con_result,
injects = #injects con_result,
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Mar 13 19:06:18 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Mar 13 20:15:25 2010 -0800
@@ -118,8 +118,8 @@
Domain_Constructors.add_domain_constructors dbind spec iso_info thy;
val con_appls = #con_betas result;
-val {exhaust, casedist, ...} = result;
-val {con_compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result;
+val {nchotomy, exhaust, ...} = result;
+val {compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result;
val {sel_rews, ...} = result;
val when_rews = #cases result;
val when_strict = hd when_rews;
@@ -185,11 +185,11 @@
thy
|> PureThy.add_thmss [
((qualified "iso_rews" , iso_rews ), [simp]),
- ((qualified "exhaust" , [exhaust] ), []),
- ((qualified "casedist" , [casedist] ),
+ ((qualified "nchotomy" , [nchotomy] ), []),
+ ((qualified "exhaust" , [exhaust] ),
[Rule_Cases.case_names case_ns, Induct.cases_type dname]),
((qualified "when_rews" , when_rews ), [simp]),
- ((qualified "compacts" , con_compacts), [simp]),
+ ((qualified "compacts" , compacts ), [simp]),
((qualified "con_rews" , con_rews ), [simp, fixrec_simp]),
((qualified "sel_rews" , sel_rews ), [simp]),
((qualified "dis_rews" , dis_rews ), [simp]),
@@ -229,7 +229,7 @@
in
val axs_rep_iso = map (ga "rep_iso") dnames;
val axs_abs_iso = map (ga "abs_iso") dnames;
- val cases = map (ga "casedist" ) dnames;
+ val exhausts = map (ga "exhaust" ) dnames;
val con_rews = maps (gts "con_rews" ) dnames;
end;
@@ -317,12 +317,12 @@
[resolve_tac prems 1] @
map (K (atac 1)) (nonlazy args) @
map (K (etac spec 1)) (filter is_rec args);
- fun cases_tacs (cons, cases) =
- res_inst_tac context [(("y", 0), "x")] cases 1 ::
+ fun cases_tacs (cons, exhaust) =
+ res_inst_tac context [(("y", 0), "x")] exhaust 1 ::
asm_simp_tac (take_ss addsimps prems) 1 ::
maps con_tacs cons;
in
- tacs1 @ maps cases_tacs (conss ~~ cases)
+ tacs1 @ maps cases_tacs (conss ~~ exhausts)
end;
in pg'' thy [] goal tacf end;
@@ -407,8 +407,8 @@
in
thy
|> snd o PureThy.add_thmss [
- ((Binding.qualified true "finite_ind" comp_dbind, [finite_ind]), []),
- ((Binding.qualified true "ind" comp_dbind, [ind] ), [])]
+ ((Binding.qualified true "finite_induct" comp_dbind, [finite_ind]), []),
+ ((Binding.qualified true "induct" comp_dbind, [ind] ), [])]
|> (snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
end; (* prove_induction *)
@@ -554,7 +554,7 @@
end; (* local *)
in thy |> snd o PureThy.add_thmss
- [((Binding.qualified true "coind" comp_dbind, [coind]), [])]
+ [((Binding.qualified true "coinduct" comp_dbind, [coind]), [])]
end; (* let *)
fun comp_theorems
--- a/src/HOLCF/ex/Dnat.thy Sat Mar 13 19:06:18 2010 -0800
+++ b/src/HOLCF/ex/Dnat.thy Sat Mar 13 20:15:25 2010 -0800
@@ -52,7 +52,7 @@
lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y"
apply (rule allI)
- apply (induct_tac x rule: dnat.ind)
+ apply (induct_tac x)
apply fast
apply (rule allI)
apply (case_tac y)
--- a/src/HOLCF/ex/Domain_ex.thy Sat Mar 13 19:06:18 2010 -0800
+++ b/src/HOLCF/ex/Domain_ex.thy Sat Mar 13 20:15:25 2010 -0800
@@ -95,7 +95,7 @@
domain 'a flattree = Tip | Branch "'a flattree" "'a flattree"
lemma "\<lbrakk>P \<bottom>; P Tip; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; P x; P y\<rbrakk> \<Longrightarrow> P (Branch\<cdot>x\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
-by (rule flattree.ind) -- "no admissibility requirement"
+by (rule flattree.induct) -- "no admissibility requirement"
text {* Trivial datatypes will produce a warning message. *}
@@ -123,8 +123,8 @@
term Leaf
term Node
thm Leaf_def Node_def
+thm tree.nchotomy
thm tree.exhaust
-thm tree.casedist
thm tree.compacts
thm tree.con_rews
thm tree.dist_les
@@ -166,10 +166,11 @@
thm tree.chain_take
thm tree.take_take
thm tree.deflation_take
+thm tree.take_below
thm tree.take_lemma
thm tree.lub_take
thm tree.reach
-thm tree.finite_ind
+thm tree.finite_induct
text {* Rules about finiteness predicate *}
term tree_finite
@@ -179,10 +180,10 @@
text {* Rules about bisimulation predicate *}
term tree_bisim
thm tree.bisim_def
-thm tree.coind
+thm tree.coinduct
text {* Induction rule *}
-thm tree.ind
+thm tree.induct
subsection {* Known bugs *}
--- a/src/HOLCF/ex/Powerdomain_ex.thy Sat Mar 13 19:06:18 2010 -0800
+++ b/src/HOLCF/ex/Powerdomain_ex.thy Sat Mar 13 20:15:25 2010 -0800
@@ -40,7 +40,7 @@
lemma r1_r2: "r1\<cdot>\<langle>x,a\<rangle>\<cdot>\<langle>y,b\<rangle> = (r2\<cdot>\<langle>x,a\<rangle>\<cdot>\<langle>y,b\<rangle> :: tr convex_pd)"
apply (simp add: r1_def r2_def)
apply (simp add: is_le_def is_less_def)
-apply (cases "compare\<cdot>x\<cdot>y" rule: ordering.casedist)
+apply (cases "compare\<cdot>x\<cdot>y")
apply simp_all
done
@@ -70,8 +70,7 @@
pick_strict [simp]: "pick\<cdot>\<bottom>"
lemma pick_mirror: "pick\<cdot>(mirror\<cdot>t) = pick\<cdot>t"
-by (induct t rule: tree.ind)
- (simp_all add: convex_plus_ac)
+by (induct t) (simp_all add: convex_plus_ac)
fixrec tree1 :: "int lift tree"
where "tree1 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>(Leaf\<cdot>(Def 2)))
--- a/src/HOLCF/ex/Stream.thy Sat Mar 13 19:06:18 2010 -0800
+++ b/src/HOLCF/ex/Stream.thy Sat Mar 13 20:15:25 2010 -0800
@@ -67,24 +67,19 @@
by simp
lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU & x = a && y)"
-by (auto,insert stream.exhaust [of x],auto)
+by (cases x, auto)
lemma stream_neq_UU: "x~=UU ==> EX a a_s. x=a&&a_s & a~=UU"
by (simp add: stream_exhaust_eq,auto)
-lemma stream_inject_eq [simp]:
- "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b & s = t)"
-by (insert stream.injects [of a s b t], auto)
-
lemma stream_prefix:
"[| a && s << t; a ~= UU |] ==> EX b tt. t = b && tt & b ~= UU & s << tt"
-by (insert stream.exhaust [of t], auto)
+by (cases t, auto)
lemma stream_prefix':
"b ~= UU ==> x << b && z =
(x = UU | (EX a y. x = a && y & a ~= UU & a << b & y << z))"
-apply (case_tac "x=UU",auto)
-by (drule stream_exhaust_eq [THEN iffD1],auto)
+by (cases x, auto)
(*
@@ -108,7 +103,7 @@
lemma stream_when_strictf: "stream_when$UU$s=UU"
-by (rule stream.casedist [of s], auto)
+by (cases s, auto)
@@ -121,13 +116,13 @@
lemma ft_defin: "s~=UU ==> ft$s~=UU"
-by (drule stream_exhaust_eq [THEN iffD1],auto)
+by simp
lemma rt_strict_rev: "rt$s~=UU ==> s~=UU"
by auto
lemma surjectiv_scons: "(ft$s)&&(rt$s)=s"
-by (rule stream.casedist [of s], auto)
+by (cases s, auto)
lemma monofun_rt_mult: "x << s ==> iterate i$rt$x << iterate i$rt$s"
by (rule monofun_cfun_arg)
@@ -146,7 +141,7 @@
by (rule stream.reach)
lemma chain_stream_take: "chain (%i. stream_take i$s)"
-by (simp add: stream.chain_take)
+by simp
lemma stream_take_prefix [simp]: "stream_take n$s << s"
apply (insert stream_reach2 [of s])
@@ -235,7 +230,7 @@
"[| stream_finite x; P UU; !!a s. [| a ~= UU; P s |] ==> P (a && s) |] ==> P x"
apply (simp add: stream.finite_def,auto)
apply (erule subst)
-by (drule stream.finite_ind [of P _ x], auto)
+by (drule stream.finite_induct [of P _ x], auto)
lemma stream_finite_ind2:
"[| P UU; !! x. x ~= UU ==> P (x && UU); !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )|] ==>
@@ -299,7 +294,7 @@
by (erule stream_take_lemma3,simp)
lemma stream_finite_rt_eq: "stream_finite (rt$s) = stream_finite s"
-apply (rule stream.casedist [of s], auto)
+apply (cases s, auto)
apply (rule stream_finite_lemma1, simp)
by (rule stream_finite_lemma2,simp)
@@ -344,10 +339,10 @@
by (drule stream_finite_lemma1,auto)
lemma slen_less_1_eq: "(#x < Fin (Suc 0)) = (x = \<bottom>)"
-by (rule stream.casedist [of x], auto simp add: Fin_0 iSuc_Fin[THEN sym])
+by (cases x, auto simp add: Fin_0 iSuc_Fin[THEN sym])
lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)"
-by (rule stream.casedist [of x], auto)
+by (cases x, auto)
lemma slen_scons_eq: "(Fin (Suc n) < #x) = (? a y. x = a && y & a ~= \<bottom> & Fin n < #y)"
apply (auto, case_tac "x=UU",auto)
@@ -357,13 +352,13 @@
done
lemma slen_iSuc: "#x = iSuc n --> (? a y. x = a&&y & a ~= \<bottom> & #y = n)"
-by (rule stream.casedist [of x], auto)
+by (cases x, auto)
lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \<infinity>"
by (simp add: slen_def)
lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y | a = \<bottom> | #y < Fin (Suc n))"
- apply (rule stream.casedist [of x], auto)
+ apply (cases x, auto)
apply (simp add: zero_inat_def)
apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
@@ -415,8 +410,8 @@
by (rule slen_take_eq_rev [THEN iffD1], auto)
lemma slen_rt_mono: "#s2 <= #s1 ==> #(rt$s2) <= #(rt$s1)"
-apply (rule stream.casedist [of s1])
- by (rule stream.casedist [of s2],simp+)+
+apply (cases s1)
+ by (cases s2, simp+)+
lemma slen_take_lemma5: "#(stream_take n$s) <= Fin n"
apply (case_tac "stream_take n$s = s")
@@ -480,7 +475,7 @@
apply auto
apply (subgoal_tac "stream_take n$s ~=s")
apply (insert slen_take_lemma4 [of n s],auto)
-apply (rule stream.casedist [of s],simp)
+apply (cases s, simp)
by (simp add: slen_take_lemma4 iSuc_Fin)
(* ----------------------------------------------------------------------- *)
@@ -581,7 +576,7 @@
lemma stream_finite_i_rt [simp]: "stream_finite (i_rt n s) = stream_finite s"
apply (induct_tac n, auto)
- apply (rule stream.casedist [of "s"], auto simp del: i_rt_Suc)
+ apply (cases s, auto simp del: i_rt_Suc)
by (simp add: i_rt_Suc_back stream_finite_rt_eq)+
lemma take_i_rt_len_lemma: "ALL sl x j t. Fin sl = #x & n <= sl &
@@ -618,8 +613,8 @@
"[| i_th n s1 << i_th n s2; i_rt (Suc n) s1 << i_rt (Suc n) s2 |] ==>
i_rt n s1 << i_rt n s2"
apply (simp add: i_th_def i_rt_Suc_back)
-apply (rule stream.casedist [of "i_rt n s1"],simp)
-apply (rule stream.casedist [of "i_rt n s2"],auto)
+apply (cases "i_rt n s1", simp)
+apply (cases "i_rt n s2", auto)
done
lemma i_th_stream_take_Suc [rule_format]:
@@ -758,7 +753,7 @@
by (simp add: sconc_def)
lemma ft_sconc: "x ~= UU ==> ft$(x ooo y) = ft$x"
-by (rule stream.casedist [of x],auto)
+by (cases x, auto)
lemma sconc_assoc: "(x ooo y) ooo z = x ooo y ooo z"
apply (case_tac "#x")
@@ -799,7 +794,7 @@
(* ----------------------------------------------------------------------- *)
lemma rt_sconc [rule_format, simp]: "s~=UU --> rt$(s ooo x) = rt$s ooo x"
-by (rule stream.casedist,auto)
+by (cases s, auto)
lemma i_th_sconc_lemma [rule_format]:
"ALL x y. Fin n < #x --> i_th n (x ooo y) = i_th n x"