--- a/src/HOL/Library/Fin_Fun.thy Sun Jun 14 23:25:49 2009 +0200
+++ b/src/HOL/Library/Fin_Fun.thy Mon Jun 15 10:58:05 2009 +0200
@@ -76,10 +76,13 @@
subsection {* The finfun type *}
typedef ('a,'b) finfun = "{f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
-apply(auto)
-apply(rule_tac x="\<lambda>x. arbitrary" in exI)
-apply(auto)
-done
+proof -
+ have "\<exists>f. finite {x. f x \<noteq> undefined}"
+ proof
+ show "finite {x. (\<lambda>y. undefined) x \<noteq> undefined}" by auto
+ qed
+ then show ?thesis by auto
+qed
syntax
"finfun" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ \<Rightarrow>\<^isub>f /_)" [22, 21] 21)
@@ -318,32 +321,27 @@
instantiation finfun :: (random, random) random
begin
-primrec random_finfun' :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
- "random_finfun' 0 j = Quickcheck.collapse (Random.select_default 0
- (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))
- (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
- | "random_finfun' (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_default i
- (random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun' i j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f)))))
- (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
-
+primrec random_finfun_aux :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
+ "random_finfun_aux 0 j = Quickcheck.collapse (Random.select_weight
+ [(1, random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
+ | "random_finfun_aux (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_weight
+ [(Suc_code_numeral i, random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun_aux i j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f))))),
+ (1, random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
+
definition
- "random i = random_finfun' i i"
+ "random i = random_finfun_aux i i"
instance ..
end
-lemma select_default_zero:
- "Random.select_default 0 y y = Random.select_default 0 x y"
- by (simp add: select_default_def)
-
-lemma random_finfun'_code [code]:
- "random_finfun' i j = Quickcheck.collapse (Random.select_default (i - 1)
- (random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun' (i - 1) j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f)))))
- (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
+lemma random_finfun_aux_code [code]:
+ "random_finfun_aux i j = Quickcheck.collapse (Random.select_weight
+ [(i, random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun_aux (i - 1) j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f))))),
+ (1, random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))])"
apply (cases i rule: code_numeral.exhaust)
- apply (simp_all only: random_finfun'.simps code_numeral_zero_minus_one Suc_code_numeral_minus_one)
- apply (subst select_default_zero) apply (simp only:)
+ apply (simp_all only: random_finfun_aux.simps code_numeral_zero_minus_one Suc_code_numeral_minus_one)
+ apply (subst select_weight_cons_zero) apply (simp only:)
done
no_notation fcomp (infixl "o>" 60)
--- a/src/HOL/Random.thy Sun Jun 14 23:25:49 2009 +0200
+++ b/src/HOL/Random.thy Mon Jun 15 10:58:05 2009 +0200
@@ -143,28 +143,6 @@
expand_fun_eq pick_same [symmetric])
qed
-definition select_default :: "code_numeral \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
- [code del]: "select_default k x y = range k
- o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
-
-lemma select_default_zero:
- "fst (select_default 0 x y s) = y"
- by (simp add: scomp_apply split_beta select_default_def)
-
-lemma select_default_code [code]:
- "select_default k x y = (if k = 0
- then range 1 o\<rightarrow> (\<lambda>_. Pair y)
- else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))"
-proof
- fix s
- have "snd (range (Code_Numeral.of_nat 0) s) = snd (range (Code_Numeral.of_nat 1) s)"
- by (simp add: range_def scomp_Pair scomp_apply split_beta)
- then show "select_default k x y s = (if k = 0
- then range 1 o\<rightarrow> (\<lambda>_. Pair y)
- else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))) s"
- by (cases "k = 0") (simp_all add: select_default_def scomp_apply split_beta)
-qed
-
subsection {* @{text ML} interface *}
@@ -198,7 +176,7 @@
hide (open) type seed
hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
- iterate range select pick select_weight select_default
+ iterate range select pick select_weight
no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/Provers/Arith/fast_lin_arith.ML Sun Jun 14 23:25:49 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Mon Jun 15 10:58:05 2009 +0200
@@ -122,7 +122,7 @@
val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
lessD = [], neqE = [], simpset = Simplifier.empty_ss,
- number_of = (serial (), no_number_of) };
+ number_of = (serial (), no_number_of) } : T;
val extend = I;
fun merge _
({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
--- a/src/Pure/Isar/class_target.ML Sun Jun 14 23:25:49 2009 +0200
+++ b/src/Pure/Isar/class_target.ML Mon Jun 15 10:58:05 2009 +0200
@@ -10,8 +10,6 @@
val register: class -> class list -> ((string * typ) * (string * typ)) list
-> sort -> morphism -> thm option -> thm option -> thm
-> theory -> theory
- val register_subclass: class * class -> morphism option -> Element.witness option
- -> morphism -> theory -> theory
val is_class: theory -> class -> bool
val base_sort: theory -> class -> sort
@@ -46,8 +44,16 @@
val instantiation_param: local_theory -> binding -> string option
val confirm_declaration: binding -> local_theory -> local_theory
val pretty_instantiation: local_theory -> Pretty.T
+ val instance_arity_cmd: xstring * xstring list * xstring -> theory -> Proof.state
val type_name: string -> string
+ (*subclasses*)
+ val register_subclass: class * class -> morphism option -> Element.witness option
+ -> morphism -> theory -> theory
+ val classrel: class * class -> theory -> Proof.state
+ val classrel_cmd: xstring * xstring -> theory -> Proof.state
+
+ (*tactics*)
val intro_classes_tac: thm list -> tactic
val default_intro_tac: Proof.context -> thm list -> tactic
@@ -55,58 +61,11 @@
val axclass_cmd: binding * xstring list
-> (Attrib.binding * string list) list
-> theory -> class * theory
- val classrel_cmd: xstring * xstring -> theory -> Proof.state
- val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
- val instance_arity_cmd: xstring * xstring list * xstring -> theory -> Proof.state
end;
structure Class_Target : CLASS_TARGET =
struct
-(** primitive axclass and instance commands **)
-
-fun axclass_cmd (class, raw_superclasses) raw_specs thy =
- let
- val ctxt = ProofContext.init thy;
- val superclasses = map (Sign.read_class thy) raw_superclasses;
- val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst)
- raw_specs;
- val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd)
- raw_specs)
- |> snd
- |> (map o map) fst;
- in
- AxClass.define_class (class, superclasses) []
- (name_atts ~~ axiomss) thy
- end;
-
-local
-
-fun gen_instance mk_prop add_thm after_qed insts thy =
- let
- fun after_qed' results =
- ProofContext.theory ((fold o fold) add_thm results #> after_qed);
- in
- thy
- |> ProofContext.init
- |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])])
- o mk_prop thy) insts)
- end;
-
-in
-
-val instance_arity =
- gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
-val instance_arity_cmd =
- gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity I;
-val classrel =
- gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) AxClass.add_classrel I;
-val classrel_cmd =
- gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I;
-
-end; (*local*)
-
-
(** class data **)
datatype class_data = ClassData of {
@@ -276,7 +235,7 @@
[Option.map (Drule.standard' o Element.conclude_witness) some_wit,
(fst o rules thy) sub];
val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
- val classrel = Goal.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
+ val classrel = SkipProof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
(K tac);
val diff_sort = Sign.complete_sort thy [sup]
|> subtract (op =) (Sign.complete_sort thy [sub])
@@ -403,6 +362,30 @@
end;
+(* simple subclasses *)
+
+local
+
+fun gen_classrel mk_prop classrel thy =
+ let
+ fun after_qed results =
+ ProofContext.theory ((fold o fold) AxClass.add_classrel results);
+ in
+ thy
+ |> ProofContext.init
+ |> Proof.theorem_i NONE after_qed [[(mk_prop thy classrel, [])]]
+ end;
+
+in
+
+val classrel =
+ gen_classrel (Logic.mk_classrel oo AxClass.cert_classrel);
+val classrel_cmd =
+ gen_classrel (Logic.mk_classrel oo AxClass.read_classrel);
+
+end; (*local*)
+
+
(** instantiation target **)
(* bookkeeping *)
@@ -593,6 +576,20 @@
end;
+(* simplified instantiation interface with no class parameter *)
+
+fun instance_arity_cmd arities thy =
+ let
+ fun after_qed results = ProofContext.theory
+ ((fold o fold) AxClass.add_arity results);
+ in
+ thy
+ |> ProofContext.init
+ |> Proof.theorem_i NONE after_qed ((map (fn t => [(t, [])])
+ o Logic.mk_arities o Sign.read_arity thy) arities)
+ end;
+
+
(** tactics and methods **)
fun intro_classes_tac facts st =
@@ -620,5 +617,24 @@
Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
"apply some intro/elim rule"));
+
+(** old axclass command **)
+
+fun axclass_cmd (class, raw_superclasses) raw_specs thy =
+ let
+ val _ = Output.legacy_feature "command \"axclass\" deprecated; use \"class\" instead.";
+ val ctxt = ProofContext.init thy;
+ val superclasses = map (Sign.read_class thy) raw_superclasses;
+ val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst)
+ raw_specs;
+ val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd)
+ raw_specs)
+ |> snd
+ |> (map o map) fst;
+ in
+ AxClass.define_class (class, superclasses) []
+ (name_atts ~~ axiomss) thy
+ end;
+
end;