Skip to content

Commit 0de3952

Browse files
simondfostersimondfoster
committed
Clean-up in preparation for submission to AFP
1 parent 30c06e3 commit 0de3952

14 files changed

Lines changed: 11 additions & 67 deletions

‎Bounded_List.thy‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ text \<open> This proof is performed by transfer \<close>
5252
lemma bappend_bmake [code]:
5353
"bmake TYPE('a::finite) xs @\<^sub>s bmake TYPE('b::finite) ys
5454
= bmake TYPE('a + 'b) (take CARD('a) xs @ take CARD('b) ys)"
55-
by (transfer, simp add: min.absorb2)
55+
by (transfer, simp)
5656

5757
instantiation blist :: (type, finite) equal
5858
begin

‎Countable_Set_Extra.thy‎

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,3 @@
1-
(******************************************************************************)
2-
(* Project: Isabelle/UTP Toolkit *)
3-
(* File: Countable_Set_Extra.thy *)
4-
(* Authors: Simon Foster and Frank Zeyda *)
5-
(* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk *)
6-
(******************************************************************************)
7-
81
section \<open> Countable Sets: Extra functions and properties \<close>
92

103
theory Countable_Set_Extra

‎Enum_Type.ML‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,6 @@ fun enum_type tname cs thy =
6161
val (thm1, ctx3) = define_overloaded ("enum_" ^ tname, mk_def (HOLogic.listT ty) (@{const_name "enum_class.enum"}) (HOLogic.mk_list dummyT cs')) ctx2
6262
val (thm2, ctx4) = define_overloaded ("enum_all_" ^ tname, mk_def dummyT (@{const_name "enum_class.enum_all"}) (Abs ("P", dummyT, foldl1 HOLogic.mk_conj (map (fn c => Bound 0 $ c) cs')))) ctx3
6363
val (thm3, ctx5) = define_overloaded ("enum_ex_" ^ tname, mk_def dummyT (@{const_name "enum_class.enum_ex"}) (Abs ("P", dummyT, foldl1 HOLogic.mk_disj (map (fn c => Bound 0 $ c) cs')))) ctx4
64-
val exhaust = Proof_Context.get_thm ctx5 (tname ^ ".exhaust");
6564
fun mk_def ty x v = Const ("Pure.eq", ty --> ty --> Term.propT) $ Free (x, ty) $ v;
6665
(* FIXME: The following proof relies on the splitting variable being called "x"; if it breaks this is probably why *)
6766
val thy1 = Class.prove_instantiation_exit

‎Finite_Fun.thy‎

Lines changed: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,7 @@
1-
(******************************************************************************)
2-
(* Project: Isabelle/UTP Toolkit *)
3-
(* File: Finite_Fun.thy *)
4-
(* Authors: Simon Foster and Frank Zeyda *)
5-
(* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk *)
6-
(******************************************************************************)
7-
81
section \<open> Finite Functions \<close>
92

103
theory Finite_Fun
11-
imports Map_Extra Partial_Fun
4+
imports Map_Extra Partial_Fun
125
begin
136

147
subsection \<open> Finite function type and operations \<close>

‎Infinite_Sequence.thy‎

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,3 @@
1-
(******************************************************************************)
2-
(* Project: Isabelle/UTP Toolkit *)
3-
(* File: Sequence.thy *)
4-
(* Authors: Simon Foster and Frank Zeyda *)
5-
(* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk *)
6-
(******************************************************************************)
7-
81
section \<open> Infinite Sequences \<close>
92

103
theory Infinite_Sequence

‎Infinity.thy‎

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,3 @@
1-
(******************************************************************************)
2-
(* Project: Isabelle/UTP Toolkit *)
3-
(* File: Infinity.thy *)
4-
(* Authors: Frank Zeyda and Simon Foster (University of York, UK) *)
5-
(* Emails: frank.zeyda@york.ac.uk and simon.foster@york.ac.uk *)
6-
(******************************************************************************)
7-
81
section \<open> Infinity Supplement \<close>
92

103
theory Infinity

‎List_Extra.thy‎

Lines changed: 0 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,3 @@
1-
(*****************************************************************************************)
2-
(* Project: Isabelle/UTP Toolkit *)
3-
(* File: List_Extra.thy *)
4-
(* Authors: Simon Foster, Pedro Ribeiro, and Frank Zeyda *)
5-
(* Emails: simon.foster@york.ac.uk, pedro.ribeiro@york.ac.uk, and frank.zeyda@york.ac.uk *)
6-
(*****************************************************************************************)
7-
81
section \<open> Lists: extra functions and properties \<close>
92

103
theory List_Extra
@@ -173,8 +166,6 @@ next
173166
qed
174167
qed
175168

176-
term sorted
177-
178169
lemma is_sorted_list_of_set_alt_def:
179170
"is_sorted_list_of_set A xs \<longleftrightarrow> sorted (xs) \<and> distinct (xs) \<and> set(xs) = A"
180171
apply (auto intro: sorted_is_sorted_list_of_set)

‎Map_Extra.thy‎

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,3 @@
1-
(******************************************************************************)
2-
(* Project: Isabelle/UTP Toolkit *)
3-
(* File: Map_Extra.thy *)
4-
(* Authors: Simon Foster and Frank Zeyda *)
5-
(* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk *)
6-
(******************************************************************************)
7-
81
section \<open> Map Type: extra functions and properties \<close>
92

103
theory Map_Extra

‎Partial_Fun.thy‎

Lines changed: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,3 @@
1-
(******************************************************************************)
2-
(* Project: Isabelle/UTP Toolkit *)
3-
(* File: Partial_Fun.thy *)
4-
(* Authors: Simon Foster and Frank Zeyda *)
5-
(* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk *)
6-
(******************************************************************************)
7-
81
section \<open> Partial Functions \<close>
92

103
theory Partial_Fun
@@ -1078,7 +1071,7 @@ lemma range_list_pfun:
10781071
apply (rename_tac f i)
10791072
apply (rule_tac x="map (the \<circ> f \<circ> nat) [1..i]" in exI)
10801073
apply (auto simp add: fun_eq_iff restrict_map_def)
1081-
apply (metis Suc_le_mono Suc_pred atLeastAtMost_iff domIff le0 nat_int of_nat_Suc option.exhaust_sel)
1074+
apply (metis Suc_le_mono Suc_pred atLeastAtMost_iff domIff le0 option.exhaust_sel)
10821075
apply (metis One_nat_def atLeastAtMost_iff domIff le_zero_eq zero_neq_one)
10831076
done
10841077

‎Positive.thy‎

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,3 @@
1-
(******************************************************************************)
2-
(* Project: Isabelle/UTP Toolkit *)
3-
(* File: Positive.thy *)
4-
(* Authors: Simon Foster and Frank Zeyda *)
5-
(* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk *)
6-
(******************************************************************************)
7-
81
section \<open> Positive Subtypes \<close>
92

103
theory Positive

0 commit comments

Comments
 (0)