# HG changeset patch # User huffman # Date 1268540125 28800 # Node ID b7738ab762b165fd89c5c3bbfa1ef380e55bba76 # Parent 98fd7910f70aa5a21624293fcf04963692907956 renamed some lemmas generated by the domain package diff -r 98fd7910f70a -r b7738ab762b1 src/HOLCF/FOCUS/Fstream.thy --- 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]) diff -r 98fd7910f70a -r b7738ab762b1 src/HOLCF/FOCUS/Fstreams.thy --- 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 ( 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 = ooo t)" -apply (rule stream.casedist [of s],auto) +apply (cases s, auto) by ((*drule sym,*) auto simp add: fsingleton_def2) lemma surjective_fstreams: "( ooo y = x) = (ft$x = Def d & rt$x = y)" diff -r 98fd7910f70a -r b7738ab762b1 src/HOLCF/IOA/meta_theory/Seq.thy --- 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 diff -r 98fd7910f70a -r b7738ab762b1 src/HOLCF/IOA/meta_theory/Sequence.thy --- 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 diff -r 98fd7910f70a -r b7738ab762b1 src/HOLCF/Tools/Domain/domain_constructors.ML --- 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, diff -r 98fd7910f70a -r b7738ab762b1 src/HOLCF/Tools/Domain/domain_theorems.ML --- 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 diff -r 98fd7910f70a -r b7738ab762b1 src/HOLCF/ex/Dnat.thy --- 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< 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) diff -r 98fd7910f70a -r b7738ab762b1 src/HOLCF/ex/Domain_ex.thy --- 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 "\P \; P Tip; \x y. \x \ \; y \ \; P x; P y\ \ P (Branch\x\y)\ \ 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 *} diff -r 98fd7910f70a -r b7738ab762b1 src/HOLCF/ex/Powerdomain_ex.thy --- 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\\x,a\\\y,b\ = (r2\\x,a\\\y,b\ :: tr convex_pd)" apply (simp add: r1_def r2_def) apply (simp add: is_le_def is_less_def) -apply (cases "compare\x\y" rule: ordering.casedist) +apply (cases "compare\x\y") apply simp_all done @@ -70,8 +70,7 @@ pick_strict [simp]: "pick\\" lemma pick_mirror: "pick\(mirror\t) = pick\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\(Node\(Leaf\(Def 1))\(Leaf\(Def 2))) diff -r 98fd7910f70a -r b7738ab762b1 src/HOLCF/ex/Stream.thy --- 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 = \)" -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 = \)" -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 ~= \ & 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 ~= \ & #y = n)" -by (rule stream.casedist [of x], auto) +by (cases x, auto) lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \" by (simp add: slen_def) lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y | a = \ | #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"