--- a/NEWS Wed Oct 06 17:44:07 2010 +0200
+++ b/NEWS Wed Oct 06 17:44:21 2010 +0200
@@ -74,6 +74,10 @@
*** HOL ***
+* Predicates `distinct` and `sorted` now defined inductively, with nice
+induction rules. INCOMPATIBILITY: former distinct.simps and sorted.simps
+now named distinct_simps and sorted_simps.
+
* Constant `contents` renamed to `the_elem`, to free the generic name
contents for other uses. INCOMPATIBILITY.
--- a/src/HOL/Library/AssocList.thy Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Library/AssocList.thy Wed Oct 06 17:44:21 2010 +0200
@@ -96,7 +96,7 @@
proof -
have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) =
More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
- by (rule fold_apply) (auto simp add: fun_eq_iff update_conv')
+ by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_fold split_def)
qed
@@ -113,7 +113,7 @@
by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) =
More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
- by (rule fold_apply) (simp add: update_keys split_def prod_case_beta comp_def)
+ by (rule fold_commute) (simp add: update_keys split_def prod_case_beta comp_def)
ultimately show ?thesis by (simp add: updates_def fun_eq_iff)
qed
@@ -341,7 +341,7 @@
proof -
have "clearjunk \<circ> More_List.fold (prod_case update) (zip ks vs) =
More_List.fold (prod_case update) (zip ks vs) \<circ> clearjunk"
- by (rule fold_apply) (simp add: clearjunk_update prod_case_beta o_def)
+ by (rule fold_commute) (simp add: clearjunk_update prod_case_beta o_def)
then show ?thesis by (simp add: updates_def fun_eq_iff)
qed
@@ -446,7 +446,7 @@
proof -
have "map_of \<circ> More_List.fold (prod_case update) (rev ys) =
More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
- by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
+ by (rule fold_commute) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
then show ?thesis
by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev fun_eq_iff)
qed
--- a/src/HOL/Library/Dlist.thy Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Wed Oct 06 17:44:21 2010 +0200
@@ -140,7 +140,7 @@
case (Abs_dlist xs)
then have "distinct xs" and dxs: "dxs = Dlist xs" by (simp_all add: Dlist_def distinct_remdups_id)
from `distinct xs` have "P (Dlist xs)"
- proof (induct xs rule: distinct_induct)
+ proof (induct xs)
case Nil from empty show ?case by (simp add: empty_def)
next
case (insert x xs)
--- a/src/HOL/Library/Fset.thy Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Library/Fset.thy Wed Oct 06 17:44:21 2010 +0200
@@ -1,7 +1,7 @@
(* Author: Florian Haftmann, TU Muenchen *)
-header {* Executable finite sets *}
+header {* A set type which is executable on its finite part *}
theory Fset
imports More_Set More_List
@@ -257,7 +257,7 @@
by (simp add: fun_eq_iff)
have "member \<circ> fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs =
fold More_Set.remove xs \<circ> member"
- by (rule fold_apply) (simp add: fun_eq_iff)
+ by (rule fold_commute) (simp add: fun_eq_iff)
then have "fold More_Set.remove xs (member A) =
member (fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs A)"
by (simp add: fun_eq_iff)
@@ -282,7 +282,7 @@
by (simp add: fun_eq_iff)
have "member \<circ> fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs =
fold Set.insert xs \<circ> member"
- by (rule fold_apply) (simp add: fun_eq_iff)
+ by (rule fold_commute) (simp add: fun_eq_iff)
then have "fold Set.insert xs (member A) =
member (fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs A)"
by (simp add: fun_eq_iff)
--- a/src/HOL/Library/More_List.thy Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Library/More_List.thy Wed Oct 06 17:44:21 2010 +0200
@@ -45,11 +45,19 @@
shows "fold f xs = id"
using assms by (induct xs) simp_all
-lemma fold_apply:
+lemma fold_commute:
assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
shows "h \<circ> fold g xs = fold f xs \<circ> h"
using assms by (induct xs) (simp_all add: fun_eq_iff)
+lemma fold_commute_apply:
+ assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
+ shows "h (fold g xs s) = fold f xs (h s)"
+proof -
+ from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute)
+ then show ?thesis by (simp add: fun_eq_iff)
+qed
+
lemma fold_invariant:
assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
@@ -73,7 +81,7 @@
lemma fold_rev:
assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
shows "fold f (rev xs) = fold f xs"
- using assms by (induct xs) (simp_all del: o_apply add: fold_apply)
+ using assms by (induct xs) (simp_all del: o_apply add: fold_commute)
lemma foldr_fold:
assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
--- a/src/HOL/Library/Permutation.thy Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Library/Permutation.thy Wed Oct 06 17:44:21 2010 +0200
@@ -168,7 +168,7 @@
apply simp
apply (subgoal_tac "a#list <~~> a#ysa@zs")
apply (metis Cons_eq_appendI perm_append_Cons trans)
- apply (metis Cons Cons_eq_appendI distinct.simps(2)
+ apply (metis Cons Cons_eq_appendI distinct_simps(2)
distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
apply (fastsimp simp add: insert_ident)
--- a/src/HOL/Library/positivstellensatz.ML Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Wed Oct 06 17:44:21 2010 +0200
@@ -270,7 +270,7 @@
by (atomize (full)) (cases "x <= y", auto simp add: min_def)};
- (* Miscalineous *)
+ (* Miscellaneous *)
fun literals_conv bops uops cv =
let fun h t =
case (term_of t) of
--- a/src/HOL/List.thy Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/List.thy Wed Oct 06 17:44:21 2010 +0200
@@ -157,16 +157,6 @@
upt_0: "[i..<0] = []"
| upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
-primrec
- distinct :: "'a list \<Rightarrow> bool" where
- "distinct [] \<longleftrightarrow> True"
- | "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
-
-primrec
- remdups :: "'a list \<Rightarrow> 'a list" where
- "remdups [] = []"
- | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
-
definition
insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"insert x xs = (if x \<in> set xs then xs else x # xs)"
@@ -184,6 +174,21 @@
"removeAll x [] = []"
| "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"
+inductive
+ distinct :: "'a list \<Rightarrow> bool" where
+ Nil: "distinct []"
+ | insert: "x \<notin> set xs \<Longrightarrow> distinct xs \<Longrightarrow> distinct (x # xs)"
+
+lemma distinct_simps [simp, code]:
+ "distinct [] \<longleftrightarrow> True"
+ "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
+ by (auto intro: distinct.intros elim: distinct.cases)
+
+primrec
+ remdups :: "'a list \<Rightarrow> 'a list" where
+ "remdups [] = []"
+ | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
+
primrec
replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
replicate_0: "replicate 0 x = []"
@@ -275,10 +280,26 @@
context linorder
begin
-fun sorted :: "'a list \<Rightarrow> bool" where
-"sorted [] \<longleftrightarrow> True" |
-"sorted [x] \<longleftrightarrow> True" |
-"sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
+inductive sorted :: "'a list \<Rightarrow> bool" where
+ Nil [iff]: "sorted []"
+| Cons: "\<forall>y\<in>set xs. x \<le> y \<Longrightarrow> sorted xs \<Longrightarrow> sorted (x # xs)"
+
+lemma sorted_single [iff]:
+ "sorted [x]"
+ by (rule sorted.Cons) auto
+
+lemma sorted_many:
+ "x \<le> y \<Longrightarrow> sorted (y # zs) \<Longrightarrow> sorted (x # y # zs)"
+ by (rule sorted.Cons) (cases "y # zs" rule: sorted.cases, auto)
+
+lemma sorted_many_eq [simp, code]:
+ "sorted (x # y # zs) \<longleftrightarrow> x \<le> y \<and> sorted (y # zs)"
+ by (auto intro: sorted_many elim: sorted.cases)
+
+lemma [code]:
+ "sorted [] \<longleftrightarrow> True"
+ "sorted [x] \<longleftrightarrow> True"
+ by simp_all
primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
"insort_key f x [] = [x]" |
@@ -2118,36 +2139,6 @@
"length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
by (auto simp add: zip_map_fst_snd)
-lemma distinct_zipI1:
- "distinct xs \<Longrightarrow> distinct (zip xs ys)"
-proof (induct xs arbitrary: ys)
- case (Cons x xs)
- show ?case
- proof (cases ys)
- case (Cons y ys')
- have "(x, y) \<notin> set (zip xs ys')"
- using Cons.prems by (auto simp: set_zip)
- thus ?thesis
- unfolding Cons zip_Cons_Cons distinct.simps
- using Cons.hyps Cons.prems by simp
- qed simp
-qed simp
-
-lemma distinct_zipI2:
- "distinct xs \<Longrightarrow> distinct (zip xs ys)"
-proof (induct xs arbitrary: ys)
- case (Cons x xs)
- show ?case
- proof (cases ys)
- case (Cons y ys')
- have "(x, y) \<notin> set (zip xs ys')"
- using Cons.prems by (auto simp: set_zip)
- thus ?thesis
- unfolding Cons zip_Cons_Cons distinct.simps
- using Cons.hyps Cons.prems by simp
- qed simp
-qed simp
-
subsubsection {* @{text list_all2} *}
@@ -2868,6 +2859,30 @@
"remdups (map f (remdups xs)) = remdups (map f xs)"
by (induct xs) simp_all
+lemma distinct_zipI1:
+ assumes "distinct xs"
+ shows "distinct (zip xs ys)"
+proof (rule zip_obtain_same_length)
+ fix xs' :: "'a list" and ys' :: "'b list" and n
+ assume "length xs' = length ys'"
+ assume "xs' = take n xs"
+ with assms have "distinct xs'" by simp
+ with `length xs' = length ys'` show "distinct (zip xs' ys')"
+ by (induct xs' ys' rule: list_induct2) (auto elim: in_set_zipE)
+qed
+
+lemma distinct_zipI2:
+ assumes "distinct ys"
+ shows "distinct (zip xs ys)"
+proof (rule zip_obtain_same_length)
+ fix xs' :: "'b list" and ys' :: "'a list" and n
+ assume "length xs' = length ys'"
+ assume "ys' = take n ys"
+ with assms have "distinct ys'" by simp
+ with `length xs' = length ys'` show "distinct (zip xs' ys')"
+ by (induct xs' ys' rule: list_induct2) (auto elim: in_set_zipE)
+qed
+
subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
@@ -3023,21 +3038,6 @@
"List.insert x (remdups xs) = remdups (List.insert x xs)"
by (simp add: List.insert_def)
-lemma distinct_induct [consumes 1, case_names Nil insert]:
- assumes "distinct xs"
- assumes "P []"
- assumes insert: "\<And>x xs. distinct xs \<Longrightarrow> x \<notin> set xs
- \<Longrightarrow> P xs \<Longrightarrow> P (List.insert x xs)"
- shows "P xs"
-using `distinct xs` proof (induct xs)
- case Nil from `P []` show ?case .
-next
- case (Cons x xs)
- then have "distinct xs" and "x \<notin> set xs" and "P xs" by simp_all
- with insert have "P (List.insert x xs)" .
- with `x \<notin> set xs` show ?case by simp
-qed
-
subsubsection {* @{text remove1} *}
@@ -3822,39 +3822,21 @@
apply (auto simp: sorted_distinct_set_unique)
done
-lemma sorted_take:
- "sorted xs \<Longrightarrow> sorted (take n xs)"
-proof (induct xs arbitrary: n rule: sorted.induct)
- case 1 show ?case by simp
-next
- case 2 show ?case by (cases n) simp_all
-next
- case (3 x y xs)
- then have "x \<le> y" by simp
- show ?case proof (cases n)
- case 0 then show ?thesis by simp
- next
- case (Suc m)
- with 3 have "sorted (take m (y # xs))" by simp
- with Suc `x \<le> y` show ?thesis by (cases m) simp_all
- qed
-qed
-
-lemma sorted_drop:
- "sorted xs \<Longrightarrow> sorted (drop n xs)"
-proof (induct xs arbitrary: n rule: sorted.induct)
- case 1 show ?case by simp
-next
- case 2 show ?case by (cases n) simp_all
-next
- case 3 then show ?case by (cases n) simp_all
+lemma
+ assumes "sorted xs"
+ shows sorted_take: "sorted (take n xs)"
+ and sorted_drop: "sorted (drop n xs)"
+proof -
+ from assms have "sorted (take n xs @ drop n xs)" by simp
+ then show "sorted (take n xs)" and "sorted (drop n xs)"
+ unfolding sorted_append by simp_all
qed
lemma sorted_dropWhile: "sorted xs \<Longrightarrow> sorted (dropWhile P xs)"
- unfolding dropWhile_eq_drop by (rule sorted_drop)
+ by (auto dest: sorted_drop simp add: dropWhile_eq_drop)
lemma sorted_takeWhile: "sorted xs \<Longrightarrow> sorted (takeWhile P xs)"
- apply (subst takeWhile_eq_take) by (rule sorted_take)
+ by (subst takeWhile_eq_take) (auto dest: sorted_take)
lemma sorted_filter:
"sorted (map f xs) \<Longrightarrow> sorted (map f (filter P xs))"
@@ -4153,7 +4135,6 @@
by (rule sorted_distinct_set_unique) simp_all
-
subsubsection {* @{text lists}: the list-forming operator over sets *}
inductive_set
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy Wed Oct 06 17:44:21 2010 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/Comp/AuxLemmas.thy
- ID: $Id$
Author: Martin Strecker
*)
@@ -78,30 +77,24 @@
"y \<notin> set xs \<Longrightarrow> map (the \<circ> f(y\<mapsto>v)) xs = map (the \<circ> f) xs"
by (simp add: the_map_upd)
-lemma map_map_upds [rule_format (no_asm), simp]:
-"\<forall> f vs. (\<forall>y\<in>set ys. y \<notin> set xs) \<longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) xs = map (the \<circ> f) xs"
-apply (induct xs)
+lemma map_map_upds [simp]:
+ "(\<forall>y\<in>set ys. y \<notin> set xs) \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) xs = map (the \<circ> f) xs"
+apply (induct xs arbitrary: f vs)
apply simp
apply fastsimp
done
-lemma map_upds_distinct [rule_format (no_asm), simp]:
- "\<forall> f vs. length ys = length vs \<longrightarrow> distinct ys \<longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) ys = vs"
-apply (induct ys)
+lemma map_upds_distinct [simp]:
+ "distinct ys \<Longrightarrow> length ys = length vs \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) ys = vs"
+apply (induct ys arbitrary: f vs rule: distinct.induct)
apply simp
-apply (intro strip)
apply (case_tac vs)
-apply simp
-apply (simp only: map_upds_Cons distinct.simps hd.simps tl.simps map.simps)
-apply clarify
-apply (simp del: o_apply)
-apply simp
+apply simp_all
done
-
-lemma map_of_map_as_map_upd [rule_format (no_asm)]: "distinct (map f zs) \<longrightarrow>
-map_of (map (\<lambda> p. (f p, g p)) zs) = empty (map f zs [\<mapsto>] map g zs)"
-by (induct zs, auto)
+lemma map_of_map_as_map_upd:
+ "distinct (map f zs) \<Longrightarrow> map_of (map (\<lambda> p. (f p, g p)) zs) = empty (map f zs [\<mapsto>] map g zs)"
+ by (induct zs) auto
(* In analogy to Map.map_of_SomeD *)
lemma map_upds_SomeD [rule_format (no_asm)]:
--- a/src/HOL/MicroJava/MicroJava.thy Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/MicroJava/MicroJava.thy Wed Oct 06 17:44:21 2010 +0200
@@ -12,4 +12,4 @@
"Comp/CorrCompTp"
begin
-end
\ No newline at end of file
+end
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Wed Oct 06 17:44:21 2010 +0200
@@ -4,7 +4,7 @@
section {* Specialisation Examples *}
-fun nth_el'
+primrec nth_el'
where
"nth_el' [] i = None"
| "nth_el' (x # xs) i = (case i of 0 => Some x | Suc j => nth_el' xs j)"
@@ -48,7 +48,27 @@
subsection {* Sorts *}
-code_pred [inductify] sorted .
+declare sorted.Nil [code_pred_intro]
+ sorted_single [code_pred_intro]
+ sorted_many [code_pred_intro]
+
+code_pred sorted proof -
+ assume "sorted xa"
+ assume 1: "xa = [] \<Longrightarrow> thesis"
+ assume 2: "\<And>x. xa = [x] \<Longrightarrow> thesis"
+ assume 3: "\<And>x y zs. xa = x # y # zs \<Longrightarrow> x \<le> y \<Longrightarrow> sorted (y # zs) \<Longrightarrow> thesis"
+ show thesis proof (cases xa)
+ case Nil with 1 show ?thesis .
+ next
+ case (Cons x xs) show ?thesis proof (cases xs)
+ case Nil with Cons 2 show ?thesis by simp
+ next
+ case (Cons y zs) with `xa = x # xs` have "xa = x # y # zs" by simp
+ moreover with `sorted xa` have "x \<le> y" and "sorted (y # zs)" by simp_all
+ ultimately show ?thesis by (rule 3)
+ qed
+ qed
+qed
thm sorted.equation
section {* Specialisation in POPLmark theory *}
@@ -212,10 +232,10 @@
where
T_Var: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma>\<langle>i\<rangle> = \<lfloor>VarB U\<rfloor> \<Longrightarrow> T = \<up>\<^isub>\<tau> (Suc i) 0 U \<Longrightarrow> \<Gamma> \<turnstile> Var i : T"
| T_Abs: "VarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>:T\<^isub>1. t\<^isub>2) : T\<^isub>1 \<rightarrow> \<down>\<^isub>\<tau> 1 0 T\<^isub>2"
-| T_App: "\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>1\<^isub>1 \<rightarrow> T\<^isub>1\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<bullet> t\<^isub>2 : T\<^isub>1\<^isub>2"
+| T_App: "\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>11 \<rightarrow> T\<^isub>12 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>11 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<bullet> t\<^isub>2 : T\<^isub>12"
| T_TAbs: "TVarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda><:T\<^isub>1. t\<^isub>2) : (\<forall><:T\<^isub>1. T\<^isub>2)"
-| T_TApp: "\<Gamma> \<turnstile> t\<^isub>1 : (\<forall><:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2) \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1 \<Longrightarrow>
- \<Gamma> \<turnstile> t\<^isub>1 \<bullet>\<^isub>\<tau> T\<^isub>2 : T\<^isub>1\<^isub>2[0 \<mapsto>\<^isub>\<tau> T\<^isub>2]\<^isub>\<tau>"
+| T_TApp: "\<Gamma> \<turnstile> t\<^isub>1 : (\<forall><:T\<^isub>11. T\<^isub>12) \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>11 \<Longrightarrow>
+ \<Gamma> \<turnstile> t\<^isub>1 \<bullet>\<^isub>\<tau> T\<^isub>2 : T\<^isub>12[0 \<mapsto>\<^isub>\<tau> T\<^isub>2]\<^isub>\<tau>"
| T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T"
code_pred [inductify, skip_proof, specialise] typing .
--- a/src/HOL/Tools/Function/lexicographic_order.ML Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Wed Oct 06 17:44:21 2010 +0200
@@ -1,7 +1,8 @@
(* Title: HOL/Tools/Function/lexicographic_order.ML
Author: Lukas Bulwahn, TU Muenchen
+ Author: Alexander Krauss, TU Muenchen
-Method for termination proofs with lexicographic orderings.
+Termination proofs with lexicographic orders.
*)
signature LEXICOGRAPHIC_ORDER =
@@ -41,23 +42,15 @@
(** Matrix cell datatype **)
datatype cell =
- Less of thm| LessEq of (thm * thm) | None of (thm * thm) | False of thm;
-
-fun is_Less (Less _) = true
- | is_Less _ = false
+ Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
-fun is_LessEq (LessEq _) = true
- | is_LessEq _ = false
-
-fun pr_cell (Less _ ) = " < "
- | pr_cell (LessEq _) = " <="
- | pr_cell (None _) = " ? "
- | pr_cell (False _) = " F "
+fun is_Less lcell = case Lazy.force lcell of Less _ => true | _ => false;
+fun is_LessEq lcell = case Lazy.force lcell of LessEq _ => true | _ => false;
(** Proof attempts to build the matrix **)
-fun dest_term (t : term) =
+fun dest_term t =
let
val (vars, prop) = Function_Lib.dest_all_all t
val (prems, concl) = Logic.strip_horn prop
@@ -76,7 +69,7 @@
fold_rev Logic.all vars (Logic.list_implies (prems, concl))
end
-fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun =
+fun mk_cell thy solve_tac (vars, prems, lhs, rhs) mfun = Lazy.lazy (fn _ =>
let
val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
in
@@ -90,46 +83,42 @@
else None (thm2, thm)
| _ => raise Match) (* FIXME *)
| _ => raise Match
- end
+ end);
(** Search algorithms **)
-fun check_col ls = forall (fn c => is_Less c orelse is_LessEq c) ls andalso not (forall (is_LessEq) ls)
+fun check_col ls = forall (fn c => is_Less c orelse is_LessEq c) ls andalso not (forall is_LessEq ls)
fun transform_table table col = table |> filter_out (fn x => is_Less (nth x col)) |> map (del_index col)
fun transform_order col order = map (fn x => if x >= col then x + 1 else x) order
(* simple depth-first search algorithm for the table *)
-fun search_table table =
- case table of
- [] => SOME []
- | _ =>
- let
- val col = find_index (check_col) (transpose table)
- in case col of
- ~1 => NONE
- | _ =>
- let
- val order_opt = (table, col) |-> transform_table |> search_table
- in case order_opt of
- NONE => NONE
- | SOME order =>SOME (col :: transform_order col order)
- end
- end
+fun search_table [] = SOME []
+ | search_table table =
+ case find_index check_col (transpose table) of
+ ~1 => NONE
+ | col =>
+ (case (table, col) |-> transform_table |> search_table of
+ NONE => NONE
+ | SOME order => SOME (col :: transform_order col order))
+
(** Proof Reconstruction **)
(* prove row :: cell list -> tactic *)
-fun prove_row (Less less_thm :: _) =
- (rtac @{thm "mlex_less"} 1)
- THEN PRIMITIVE (Thm.elim_implies less_thm)
- | prove_row (LessEq (lesseq_thm, _) :: tail) =
- (rtac @{thm "mlex_leq"} 1)
- THEN PRIMITIVE (Thm.elim_implies lesseq_thm)
- THEN prove_row tail
- | prove_row _ = sys_error "lexicographic_order"
+fun prove_row (c :: cs) =
+ (case Lazy.force c of
+ Less thm =>
+ rtac @{thm "mlex_less"} 1
+ THEN PRIMITIVE (Thm.elim_implies thm)
+ | LessEq (thm, _) =>
+ rtac @{thm "mlex_leq"} 1
+ THEN PRIMITIVE (Thm.elim_implies thm)
+ THEN prove_row cs
+ | _ => sys_error "lexicographic_order")
+ | prove_row [] = no_tac;
(** Error reporting **)
@@ -158,8 +147,14 @@
|> flat
|> map (pr_unprovable_cell ctxt)
-fun no_order_msg ctxt table tl measure_funs =
+fun pr_cell (Less _ ) = " < "
+ | pr_cell (LessEq _) = " <="
+ | pr_cell (None _) = " ? "
+ | pr_cell (False _) = " F "
+
+fun no_order_msg ctxt ltable tl measure_funs =
let
+ val table = map (map Lazy.force) ltable
val prterm = Syntax.string_of_term ctxt
fun pr_fun t i = string_of_int i ^ ") " ^ prterm t
@@ -195,7 +190,7 @@
MeasureFunctions.get_measure_functions ctxt domT
val table = (* 2: create table *)
- Par_List.map (fn t => Par_List.map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
+ map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
in
case search_table table of
NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Wed Oct 06 17:44:21 2010 +0200
@@ -298,52 +298,7 @@
end
-
-local open Termination in
-fun print_cell (SOME (Less _)) = "<"
- | print_cell (SOME (LessEq _)) = "\<le>"
- | print_cell (SOME (None _)) = "-"
- | print_cell (SOME (False _)) = "-"
- | print_cell (NONE) = "?"
-
-fun print_error ctxt D = CALLS (fn (cs, _) =>
- let
- val np = get_num_points D
- val ms = map_range (get_measures D) np
- fun index xs = (1 upto length xs) ~~ xs
- fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
- val ims = index (map index ms)
- val _ = tracing (implode (outp "fn #" ":\n" (implode o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
- fun print_call (k, c) =
- let
- val (_, p, _, q, _, _) = dest_call D c
- val _ = tracing ("call table for call #" ^ Int.toString k ^ ": fn " ^
- Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1))
- val caller_ms = nth ms p
- val callee_ms = nth ms q
- val entries = map (fn x => map (pair x) (callee_ms)) (caller_ms)
- fun print_ln (i : int, l) = implode (Int.toString i :: " " :: map (enclose " " " " o print_cell o (uncurry (get_descent D c))) l)
- val _ = tracing (implode (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^
- " " :: map (enclose " " " " o Int.toString) (1 upto length callee_ms)) ^ "\n"
- ^ cat_lines (map print_ln ((1 upto (length entries)) ~~ entries)))
- in
- true
- end
- fun list_call (k, c) =
- let
- val (_, p, _, q, _, _) = dest_call D c
- val _ = tracing ("call #" ^ (Int.toString k) ^ ": fn " ^
- Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1) ^ "\n" ^
- (Syntax.string_of_term ctxt c))
- in true end
- val _ = forall list_call ((1 upto length cs) ~~ cs)
- val _ = forall print_call ((1 upto length cs) ~~ cs)
- in
- all_tac
- end)
-end
-
-fun single_scnp_tac use_tags orders ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
+fun single_scnp_tac use_tags orders ctxt D = Termination.CALLS (fn (cs, i) =>
let
val ms_configured = is_some (Multiset_Setup.get (ProofContext.theory_of ctxt))
val orders' = if ms_configured then orders
@@ -352,56 +307,40 @@
val certificate = generate_certificate use_tags orders' gp
in
case certificate
- of NONE => err_cont D i
+ of NONE => no_tac
| SOME cert =>
SELECT_GOAL (reconstruct_tac ctxt D cs gp cert) i
- THEN (rtac @{thm wf_empty} i ORELSE cont D i)
+ THEN TRY (rtac @{thm wf_empty} i)
end)
-fun gen_decomp_scnp_tac orders autom_tac ctxt err_cont =
- let
- open Termination
- val derive_diag = Termination.derive_diag ctxt autom_tac
- val derive_all = Termination.derive_all ctxt autom_tac
- val decompose = Termination.decompose_tac ctxt autom_tac
- val scnp_no_tags = single_scnp_tac false orders ctxt
- val scnp_full = single_scnp_tac true orders ctxt
-
- fun first_round c e =
- derive_diag (REPEAT scnp_no_tags c e)
-
- val second_round =
- REPEAT (fn c => fn e => decompose (scnp_no_tags c c) e)
+local open Termination in
- val third_round =
- derive_all oo
- REPEAT (fn c => fn e =>
- scnp_full (decompose c c) e)
-
- fun Then s1 s2 c e = s1 (s2 c c) (s2 c e)
+fun gen_decomp_scnp_tac orders autom_tac ctxt =
+TERMINATION ctxt autom_tac (fn D =>
+ let
+ val decompose = decompose_tac D
+ val scnp_full = single_scnp_tac true orders ctxt D
+ in
+ REPEAT_ALL_NEW (scnp_full ORELSE' decompose)
+ end)
+end
- val strategy = Then (Then first_round second_round) third_round
-
- in
- TERMINATION ctxt (strategy err_cont err_cont)
- end
-
-fun gen_sizechange_tac orders autom_tac ctxt err_cont =
+fun gen_sizechange_tac orders autom_tac ctxt =
TRY (Function_Common.apply_termination_rule ctxt 1)
THEN TRY (Termination.wf_union_tac ctxt)
THEN
(rtac @{thm wf_empty} 1
- ORELSE gen_decomp_scnp_tac orders autom_tac ctxt err_cont 1)
+ ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)
fun sizechange_tac ctxt autom_tac =
- gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt (K (K all_tac))
+ gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt
fun decomp_scnp_tac orders ctxt =
let
val extra_simps = Function_Common.Termination_Simps.get ctxt
val autom_tac = auto_tac (clasimpset_of ctxt addsimps2 extra_simps)
in
- gen_sizechange_tac orders autom_tac ctxt (print_error ctxt)
+ gen_sizechange_tac orders autom_tac ctxt
end
--- a/src/HOL/Tools/Function/termination.ML Wed Oct 06 17:44:07 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML Wed Oct 06 17:44:21 2010 +0200
@@ -9,7 +9,7 @@
sig
type data
- datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm
+ datatype cell = Less of thm | LessEq of thm * thm | None of thm * thm | False of thm
val mk_sumcases : data -> typ -> term list -> term
@@ -17,7 +17,6 @@
val get_types : data -> int -> typ
val get_measures : data -> int -> term list
- (* read from cache *)
val get_chain : data -> term -> term -> thm option option
val get_descent : data -> term -> term -> term -> cell option
@@ -25,23 +24,14 @@
val CALLS : (term list * int -> tactic) -> int -> tactic
- (* Termination tactics. Sequential composition via continuations. (2nd argument is the error continuation) *)
- type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
+ (* Termination tactics *)
+ type ttac = data -> int -> tactic
- val TERMINATION : Proof.context -> (data -> int -> tactic) -> int -> tactic
-
- val REPEAT : ttac -> ttac
+ val TERMINATION : Proof.context -> tactic -> ttac -> int -> tactic
val wf_union_tac : Proof.context -> tactic
- val decompose_tac : Proof.context -> tactic -> ttac
-
- val derive_diag : Proof.context -> tactic ->
- (data -> int -> tactic) -> data -> int -> tactic
-
- val derive_all : Proof.context -> tactic ->
- (data -> int -> tactic) -> data -> int -> tactic
-
+ val decompose_tac : ttac
end
@@ -119,22 +109,16 @@
(** Matrix cell datatype **)
-datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
+datatype cell = Less of thm | LessEq of thm * thm | None of thm * thm | False of thm;
type data =
skel (* structure of the sum type encoding "program points" *)
* (int -> typ) (* types of program points *)
* (term list Inttab.table) (* measures for program points *)
- * (thm option Term2tab.table) (* which calls form chains? *)
- * (cell Term3tab.table) (* local descents *)
-
+ * (term * term -> thm option) (* which calls form chains? (cached) *)
+ * (term * (term * term) -> cell)(* local descents (cached) *)
-fun map_chains f (p, T, M, C, D) = (p, T, M, f C, D)
-fun map_descent f (p, T, M, C, D) = (p, T, M, C, f D)
-
-fun note_chain c1 c2 res = map_chains (Term2tab.update ((c1, c2), res))
-fun note_descent c m1 m2 res = map_descent (Term3tab.update ((c,(m1, m2)), res))
(* Build case expression *)
fun mk_sumcases (sk, _, _, _, _) T fs =
@@ -155,33 +139,21 @@
mk_skel (fold collect_pats cs [])
end
-fun create ctxt T rel =
+fun prove_chain thy chain_tac (c1, c2) =
let
- val sk = mk_sum_skel rel
- val Ts = node_types sk T
- val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts)
+ val goal =
+ HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
+ Const (@{const_abbrev Set.empty}, fastype_of c1))
+ |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
in
- (sk, nth Ts, M, Term2tab.empty, Term3tab.empty)
+ case Function_Lib.try_proof (cterm_of thy goal) chain_tac of
+ Function_Lib.Solved thm => SOME thm
+ | _ => NONE
end
-fun get_num_points (sk, _, _, _, _) =
+
+fun dest_call' sk (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
- fun num (SLeaf i) = i + 1
- | num (SBranch (s, t)) = num t
- in num sk end
-
-fun get_types (_, T, _, _, _) = T
-fun get_measures (_, _, M, _, _) = Inttab.lookup_list M
-
-fun get_chain (_, _, _, C, _) c1 c2 =
- Term2tab.lookup C (c1, c2)
-
-fun get_descent (_, _, _, _, D) c m1 m2 =
- Term3tab.lookup D (c, (m1, m2))
-
-fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
- let
- val (sk, _, _, _, _) = D
val vs = Term.strip_qnt_vars @{const_name Ex} c
(* FIXME: throw error "dest_call" for malformed terms *)
@@ -192,8 +164,9 @@
in
(vs, p, l', q, r', Gam)
end
- | dest_call D t = error "dest_call"
+ | dest_call' _ _ = error "dest_call"
+fun dest_call (sk, _, _, _, _) = dest_call' sk
fun mk_desc thy tac vs Gam l r m1 m2 =
let
@@ -216,15 +189,41 @@
| _ => raise Match
end
-fun derive_descent thy tac c m1 m2 D =
- case get_descent D c m1 m2 of
- SOME _ => D
- | NONE =>
- let
- val (vs, _, l, _, r, Gam) = dest_call D c
- in
- note_descent c m1 m2 (mk_desc thy tac vs Gam l r m1 m2) D
- end
+fun prove_descent thy tac sk (c, (m1, m2)) =
+ let
+ val (vs, _, l, _, r, Gam) = dest_call' sk c
+ in
+ mk_desc thy tac vs Gam l r m1 m2
+ end
+
+fun create ctxt chain_tac descent_tac T rel =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val sk = mk_sum_skel rel
+ val Ts = node_types sk T
+ val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts)
+ val chain_cache = Cache.create Term2tab.empty Term2tab.lookup Term2tab.update
+ (prove_chain thy chain_tac)
+ val descent_cache = Cache.create Term3tab.empty Term3tab.lookup Term3tab.update
+ (prove_descent thy descent_tac sk)
+ in
+ (sk, nth Ts, M, chain_cache, descent_cache)
+ end
+
+fun get_num_points (sk, _, _, _, _) =
+ let
+ fun num (SLeaf i) = i + 1
+ | num (SBranch (s, t)) = num t
+ in num sk end
+
+fun get_types (_, T, _, _, _) = T
+fun get_measures (_, _, M, _, _) = Inttab.lookup_list M
+
+fun get_chain (_, _, _, C, _) c1 c2 =
+ SOME (C (c1, c2))
+
+fun get_descent (_, _, _, _, D) c m1 m2 =
+ SOME (D (c, (m1, m2)))
fun CALLS tac i st =
if Thm.no_prems st then all_tac st
@@ -232,14 +231,14 @@
(_ $ (_ $ rel)) => tac (Function_Lib.dest_binop_list @{const_name Lattices.sup} rel, i) st
|_ => no_tac st
-type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
+type ttac = data -> int -> tactic
-fun TERMINATION ctxt tac =
+fun TERMINATION ctxt atac tac =
SUBGOAL (fn (_ $ (Const (@{const_name wf}, wfT) $ rel), i) =>
let
val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT))
in
- tac (create ctxt T rel) i
+ tac (create ctxt atac atac T rel) i
end)
@@ -309,36 +308,9 @@
end
-(* continuation passing repeat combinator *)
-fun REPEAT ttac cont err_cont =
- ttac (fn D => fn i => (REPEAT ttac cont cont D i)) err_cont
(*** DEPENDENCY GRAPHS ***)
-fun prove_chain thy chain_tac c1 c2 =
- let
- val goal =
- HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
- Const (@{const_abbrev Set.empty}, fastype_of c1))
- |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
- in
- case Function_Lib.try_proof (cterm_of thy goal) chain_tac of
- Function_Lib.Solved thm => SOME thm
- | _ => NONE
- end
-
-fun derive_chains ctxt chain_tac cont D = CALLS (fn (cs, i) =>
- let
- val thy = ProofContext.theory_of ctxt
-
- fun derive_chain c1 c2 D =
- if is_some (get_chain D c1 c2) then D else
- note_chain c1 c2 (prove_chain thy chain_tac c1 c2) D
- in
- cont (fold_product derive_chain cs cs D) i
- end)
-
-
fun mk_dgraph D cs =
Term_Graph.empty
|> fold (fn c => Term_Graph.new_node (c, ())) cs
@@ -368,50 +340,23 @@
| _ => no_tac)
| _ => no_tac)
-fun decompose_tac' cont err_cont D = CALLS (fn (cs, i) =>
+fun decompose_tac D = CALLS (fn (cs, i) =>
let
val G = mk_dgraph D cs
val sccs = Term_Graph.strong_conn G
- fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i)
+ fun split [SCC] i = TRY (solve_trivial_tac D i)
| split (SCC::rest) i =
regroup_calls_tac SCC i
THEN rtac @{thm wf_union_compatible} i
THEN rtac @{thm less_by_empty} (i + 2)
THEN ucomp_empty_tac (the o the oo get_chain D) (i + 2)
THEN split rest (i + 1)
- THEN (solve_trivial_tac D i ORELSE cont D i)
+ THEN TRY (solve_trivial_tac D i)
in
if length sccs > 1 then split sccs i
- else solve_trivial_tac D i ORELSE err_cont D i
+ else solve_trivial_tac D i
end)
-fun decompose_tac ctxt chain_tac cont err_cont =
- derive_chains ctxt chain_tac (decompose_tac' cont err_cont)
-
-
-(*** Local Descent Proofs ***)
-
-fun gen_descent diag ctxt tac cont D = CALLS (fn (cs, i) =>
- let
- val thy = ProofContext.theory_of ctxt
- val measures_of = get_measures D
-
- fun derive c D =
- let
- val (_, p, _, q, _, _) = dest_call D c
- in
- if diag andalso p = q
- then fold (fn m => derive_descent thy tac c m m) (measures_of p) D
- else fold_product (derive_descent thy tac c)
- (measures_of p) (measures_of q) D
- end
- in
- cont (Function_Common.PROFILE "deriving descents" (fold derive cs) D) i
- end)
-
-fun derive_diag ctxt = gen_descent true ctxt
-fun derive_all ctxt = gen_descent false ctxt
-
end