Skip to content

Commit 4e93daa

Browse files
yutakangyutakang
committed
update to Isabelle2025
1 parent ee10ab9 commit 4e93daa

9 files changed

Lines changed: 17 additions & 25 deletions

‎UR/TIP/TIP15/TIP15/TIP_sort_StoogeSort2Count.thy‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ function stooge2sort2 :: "int list => int list"
4747
and stoogesort2 :: "int list => int list"
4848
and stooge2sort1 :: "int list => int list" where
4949
"stooge2sort2 y =
50-
(case splitAt ((op div) ((2 * (length y)) + 1) 3) y of
50+
(case splitAt (divide ((2 * (length y)) + 1) 3) y of
5151
pair2 ys2 zs1 => x (stoogesort2 ys2) zs1)"
5252
| "stoogesort2 (nil2) = nil2"
5353
| "stoogesort2 (cons2 z (nil2)) = cons2 z (nil2)"
@@ -56,7 +56,7 @@ function stooge2sort2 :: "int list => int list"
5656
stooge2sort2
5757
(stooge2sort1 (stooge2sort2 (cons2 z (cons2 y2 (cons2 x3 x4)))))"
5858
| "stooge2sort1 y =
59-
(case splitAt ((op div) (length y) 3) y of
59+
(case splitAt (divide (length y) 3) y of
6060
pair2 ys2 zs1 => x ys2 (stoogesort2 zs1))"
6161
by pat_completeness auto
6262

‎UR/TIP/TIP15/TIP15/TIP_sort_StoogeSort2IsSort.thy‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,7 @@ function stooge2sort2 :: "int list => int list"
5757
and stoogesort2 :: "int list => int list"
5858
and stooge2sort1 :: "int list => int list" where
5959
"stooge2sort2 y =
60-
(case splitAt ((op div) ((2 * (length y)) + 1) 3) y of
60+
(case splitAt (divide ((2 * (length y)) + 1) 3) y of
6161
pair2 ys2 zs1 => x (stoogesort2 ys2) zs1)"
6262
| "stoogesort2 (nil2) = nil2"
6363
| "stoogesort2 (cons2 z (nil2)) = cons2 z (nil2)"
@@ -66,7 +66,7 @@ function stooge2sort2 :: "int list => int list"
6666
stooge2sort2
6767
(stooge2sort1 (stooge2sort2 (cons2 z (cons2 y2 (cons2 x3 x4)))))"
6868
| "stooge2sort1 y =
69-
(case splitAt ((op div) (length y) 3) y of
69+
(case splitAt (divide (length y) 3) y of
7070
pair2 ys2 zs1 => x ys2 (stoogesort2 zs1))"
7171
by pat_completeness auto
7272

‎UR/TIP/TIP15/TIP15/TIP_sort_StoogeSort2Permutes.thy‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ function stooge2sort2 :: "int list => int list"
5151
and stoogesort2 :: "int list => int list"
5252
and stooge2sort1 :: "int list => int list" where
5353
"stooge2sort2 y =
54-
(case splitAt ((op div) ((2 * (length y)) + 1) 3) y of
54+
(case splitAt (divide ((2 * (length y)) + 1) 3) y of
5555
pair2 ys2 zs1 => x (stoogesort2 ys2) zs1)"
5656
| "stoogesort2 (nil2) = nil2"
5757
| "stoogesort2 (cons2 z (nil2)) = cons2 z (nil2)"
@@ -60,7 +60,7 @@ function stooge2sort2 :: "int list => int list"
6060
stooge2sort2
6161
(stooge2sort1 (stooge2sort2 (cons2 z (cons2 y2 (cons2 x3 x4)))))"
6262
| "stooge2sort1 y =
63-
(case splitAt ((op div) (length y) 3) y of
63+
(case splitAt (divide (length y) 3) y of
6464
pair2 ys2 zs1 => x ys2 (stoogesort2 zs1))"
6565
by pat_completeness auto
6666

‎UR/TIP/TIP15/TIP15/TIP_sort_StoogeSort2Sorts.thy‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ function stooge2sort2 :: "int list => int list"
5353
and stoogesort2 :: "int list => int list"
5454
and stooge2sort1 :: "int list => int list" where
5555
"stooge2sort2 y =
56-
(case splitAt ((op div) ((2 * (length y)) + 1) 3) y of
56+
(case splitAt (divide ((2 * (length y)) + 1) 3) y of
5757
pair2 ys2 zs1 => x (stoogesort2 ys2) zs1)"
5858
| "stoogesort2 (nil2) = nil2"
5959
| "stoogesort2 (cons2 z (nil2)) = cons2 z (nil2)"
@@ -62,7 +62,7 @@ function stooge2sort2 :: "int list => int list"
6262
stooge2sort2
6363
(stooge2sort1 (stooge2sort2 (cons2 z (cons2 y2 (cons2 x3 x4)))))"
6464
| "stooge2sort1 y =
65-
(case splitAt ((op div) (length y) 3) y of
65+
(case splitAt (divide (length y) 3) y of
6666
pair2 ys2 zs1 => x ys2 (stoogesort2 zs1))"
6767
by pat_completeness auto
6868

‎UR/TIP/TIP15/TIP15/TIP_sort_StoogeSortCount.thy‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ function stooge1sort2 :: "int list => int list"
5151
and stoogesort :: "int list => int list"
5252
and stooge1sort1 :: "int list => int list" where
5353
"stooge1sort2 y =
54-
(case splitAt ((op div) (length y) 3) (reverse y) of
54+
(case splitAt (divide (length y) 3) (reverse y) of
5555
pair2 ys2 zs2 => x (stoogesort zs2) (reverse ys2))"
5656
| "stoogesort (nil2) = nil2"
5757
| "stoogesort (cons2 z (nil2)) = cons2 z (nil2)"
@@ -60,7 +60,7 @@ function stooge1sort2 :: "int list => int list"
6060
stooge1sort2
6161
(stooge1sort1 (stooge1sort2 (cons2 z (cons2 y2 (cons2 x3 x4)))))"
6262
| "stooge1sort1 y =
63-
(case splitAt ((op div) (length y) 3) y of
63+
(case splitAt (divide (length y) 3) y of
6464
pair2 ys2 zs1 => x ys2 (stoogesort zs1))"
6565
by pat_completeness auto
6666

‎UR/TIP/TIP15/TIP15/TIP_sort_StoogeSortIsSort.thy‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ function stooge1sort2 :: "int list => int list"
6161
and stoogesort :: "int list => int list"
6262
and stooge1sort1 :: "int list => int list" where
6363
"stooge1sort2 y =
64-
(case splitAt ((op div) (length y) 3) (reverse y) of
64+
(case splitAt (divide (length y) 3) (reverse y) of
6565
pair2 ys2 zs2 => x (stoogesort zs2) (reverse ys2))"
6666
| "stoogesort (nil2) = nil2"
6767
| "stoogesort (cons2 z (nil2)) = cons2 z (nil2)"
@@ -70,7 +70,7 @@ function stooge1sort2 :: "int list => int list"
7070
stooge1sort2
7171
(stooge1sort1 (stooge1sort2 (cons2 z (cons2 y2 (cons2 x3 x4)))))"
7272
| "stooge1sort1 y =
73-
(case splitAt ((op div) (length y) 3) y of
73+
(case splitAt (divide (length y) 3) y of
7474
pair2 ys2 zs1 => x ys2 (stoogesort zs1))"
7575
by pat_completeness auto
7676

‎UR/TIP/TIP15/TIP15/TIP_sort_StoogeSortPermutes.thy‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ function stooge1sort2 :: "int list => int list"
5555
and stoogesort :: "int list => int list"
5656
and stooge1sort1 :: "int list => int list" where
5757
"stooge1sort2 y =
58-
(case splitAt ((op div) (length y) 3) (reverse y) of
58+
(case splitAt (divide (length y) 3) (reverse y) of
5959
pair2 ys2 zs2 => x (stoogesort zs2) (reverse ys2))"
6060
| "stoogesort (nil2) = nil2"
6161
| "stoogesort (cons2 z (nil2)) = cons2 z (nil2)"
@@ -64,7 +64,7 @@ function stooge1sort2 :: "int list => int list"
6464
stooge1sort2
6565
(stooge1sort1 (stooge1sort2 (cons2 z (cons2 y2 (cons2 x3 x4)))))"
6666
| "stooge1sort1 y =
67-
(case splitAt ((op div) (length y) 3) y of
67+
(case splitAt (divide (length y) 3) y of
6868
pair2 ys2 zs1 => x ys2 (stoogesort zs1))"
6969
by pat_completeness auto
7070

‎UR/TIP/TIP15/TIP15/TIP_sort_StoogeSortSorts.thy‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,7 @@ function stooge1sort2 :: "int list => int list"
5757
and stoogesort :: "int list => int list"
5858
and stooge1sort1 :: "int list => int list" where
5959
"stooge1sort2 y =
60-
(case splitAt ((op div) (length y) 3) (reverse y) of
60+
(case splitAt (divide (length y) 3) (reverse y) of
6161
pair2 ys2 zs2 => x (stoogesort zs2) (reverse ys2))"
6262
| "stoogesort (nil2) = nil2"
6363
| "stoogesort (cons2 z (nil2)) = cons2 z (nil2)"
@@ -66,7 +66,7 @@ function stooge1sort2 :: "int list => int list"
6666
stooge1sort2
6767
(stooge1sort1 (stooge1sort2 (cons2 z (cons2 y2 (cons2 x3 x4)))))"
6868
| "stooge1sort1 y =
69-
(case splitAt ((op div) (length y) 3) y of
69+
(case splitAt (divide (length y) 3) y of
7070
pair2 ys2 zs1 => x ys2 (stoogesort zs1))"
7171
by pat_completeness auto
7272

‎UR/TIP/Test_Base.thy‎

Lines changed: 1 addition & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,5 @@
11
theory Test_Base
2-
imports Main "../../PSL"
2+
imports Main "Smart_Isabelle.Smart_Isabelle"
33
begin
44

5-
strategy DIndTac = Thens [Dynamic (InductTac), Auto, IsSolved]
6-
strategy DInd = Thens [Dynamic (Induct), Auto, IsSolved]
7-
strategy DIndHams = Thens [Dynamic (Induct), RepeatN (Hammer), IsSolved]
8-
strategy Test = Thens [RepeatN (Hammer), IsSolved]
9-
10-
lemma meta_allI: "\<forall> x. P x \<Longrightarrow> (\<And>x. P x)"
11-
apply auto done
12-
135
end

0 commit comments

Comments
 (0)