--- a/src/HOL/BNF_Cardinal_Arithmetic.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy Thu Feb 20 21:45:08 2014 +0100
@@ -400,7 +400,8 @@
proof (cases "Field p2 = {}")
case True
with n have "Field r2 = {}" .
- hence "cone \<le>o r1 ^c r2" unfolding cone_def cexp_def Func_def by (auto intro: card_of_ordLeqI)
+ hence "cone \<le>o r1 ^c r2" unfolding cone_def cexp_def Func_def
+ by (auto intro: card_of_ordLeqI[where f="\<lambda>_ _. undefined"])
thus ?thesis using `p1 ^c p2 \<le>o cone` ordLeq_transitive by auto
next
case False with True have "|Field (p1 ^c p2)| =o czero"
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Thu Feb 20 21:45:08 2014 +0100
@@ -414,7 +414,7 @@
let ?h = "\<lambda> b'::'b. if b' = b then a else undefined"
have "inj_on ?h {b} \<and> ?h ` {b} \<le> A"
using * unfolding inj_on_def by auto
- thus ?thesis using card_of_ordLeq by fast
+ thus ?thesis unfolding card_of_ordLeq[symmetric] by (intro exI)
qed
corollary Card_order_singl_ordLeq:
--- a/src/HOL/BNF_Constructions_on_Wellorders.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/BNF_Constructions_on_Wellorders.thy Thu Feb 20 21:45:08 2014 +0100
@@ -1652,8 +1652,7 @@
qed(insert h, unfold Func_def Func_map_def, auto)
qed
moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h])
- using inv_into_into j2A2 B1 A2 inv_into_into
- unfolding j1_def image_def by fast+
+ using j2A2 B1 A2 unfolding j1_def image_def by (fast intro: inv_into_into)+
ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1"
unfolding Func_map_def[abs_def] unfolding image_def by auto
qed(insert B1 Func_map[OF _ _ A2(2)], auto)
--- a/src/HOL/IMP/Abs_Int1_const.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy Thu Feb 20 21:45:08 2014 +0100
@@ -53,7 +53,7 @@
end
-interpretation Val_semilattice
+permanent_interpretation Val_semilattice
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
proof
case goal1 thus ?case
@@ -67,9 +67,9 @@
by(auto simp: plus_const_cases split: const.split)
qed
-interpretation Abs_Int
+permanent_interpretation Abs_Int
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
-defines AI_const is AI and step_const is step' and aval'_const is aval'
+defining AI_const = AI and step_const = step' and aval'_const = aval'
..
@@ -121,7 +121,7 @@
text{* Monotonicity: *}
-interpretation Abs_Int_mono
+permanent_interpretation Abs_Int_mono
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
proof
case goal1 thus ?case
@@ -133,7 +133,7 @@
definition m_const :: "const \<Rightarrow> nat" where
"m_const x = (if x = Any then 0 else 1)"
-interpretation Abs_Int_measure
+permanent_interpretation Abs_Int_measure
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
and m = m_const and h = "1"
proof
--- a/src/HOL/IMP/Abs_Int1_parity.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Thu Feb 20 21:45:08 2014 +0100
@@ -102,7 +102,7 @@
text{* First we instantiate the abstract value interface and prove that the
functions on type @{typ parity} have all the necessary properties: *}
-interpretation Val_semilattice
+permanent_interpretation Val_semilattice
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
proof txt{* of the locale axioms *}
fix a b :: parity
@@ -123,9 +123,9 @@
proofs (they happened in the instatiation above) but delivers the
instantiated abstract interpreter which we call @{text AI_parity}: *}
-interpretation Abs_Int
+permanent_interpretation Abs_Int
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
-defines aval_parity is aval' and step_parity is step' and AI_parity is AI
+defining aval_parity = aval' and step_parity = step' and AI_parity = AI
..
@@ -154,7 +154,7 @@
subsubsection "Termination"
-interpretation Abs_Int_mono
+permanent_interpretation Abs_Int_mono
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
proof
case goal1 thus ?case
@@ -165,7 +165,7 @@
definition m_parity :: "parity \<Rightarrow> nat" where
"m_parity x = (if x = Either then 0 else 1)"
-interpretation Abs_Int_measure
+permanent_interpretation Abs_Int_measure
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
and m = m_parity and h = "1"
proof
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Thu Feb 20 21:45:08 2014 +0100
@@ -302,7 +302,7 @@
"\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2"
by(drule (1) add_mono) simp
-interpretation Val_semilattice
+permanent_interpretation Val_semilattice
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
proof
case goal1 thus ?case by transfer (simp add: le_iff_subset)
@@ -318,16 +318,16 @@
qed
-interpretation Val_lattice_gamma
+permanent_interpretation Val_lattice_gamma
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
-defines aval_ivl is aval'
+defining aval_ivl = aval'
proof
case goal1 show ?case by(simp add: \<gamma>_inf)
next
case goal2 show ?case unfolding bot_ivl_def by transfer simp
qed
-interpretation Val_inv
+permanent_interpretation Val_inv
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -350,15 +350,15 @@
done
qed
-interpretation Abs_Int_inv
+permanent_interpretation Abs_Int_inv
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
-defines inv_aval_ivl is inv_aval'
-and inv_bval_ivl is inv_bval'
-and step_ivl is step'
-and AI_ivl is AI
-and aval_ivl' is aval''
+defining inv_aval_ivl = inv_aval'
+and inv_bval_ivl = inv_bval'
+and step_ivl = step'
+and AI_ivl = AI
+and aval_ivl' = aval''
..
@@ -384,7 +384,7 @@
apply(auto simp: below_rep_def le_iff_subset split: if_splits prod.split)
by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
-interpretation Abs_Int_inv_mono
+permanent_interpretation Abs_Int_inv_mono
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
--- a/src/HOL/IMP/Abs_Int3.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy Thu Feb 20 21:45:08 2014 +0100
@@ -260,11 +260,11 @@
end
-interpretation Abs_Int_wn
+permanent_interpretation Abs_Int_wn
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
-defines AI_wn_ivl is AI_wn
+defining AI_wn_ivl = AI_wn
..
@@ -545,7 +545,7 @@
split: prod.splits if_splits extended.split)
-interpretation Abs_Int_wn_measure
+permanent_interpretation Abs_Int_wn_measure
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Thu Feb 20 21:45:08 2014 +0100
@@ -47,13 +47,13 @@
end
-interpretation Rep rep_cval
+permanent_interpretation Rep rep_cval
proof
case goal1 thus ?case
by(cases a, cases b, simp, simp, cases b, simp, simp)
qed
-interpretation Val_abs rep_cval Const plus_cval
+permanent_interpretation Val_abs rep_cval Const plus_cval
proof
case goal1 show ?case by simp
next
@@ -61,9 +61,9 @@
by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
qed
-interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
-defines AI_const is AI
-and aval'_const is aval'
+permanent_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
+defining AI_const = AI
+and aval'_const = aval'
proof qed (auto simp: iter'_pfp_above)
text{* Straight line code: *}
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Thu Feb 20 21:45:08 2014 +0100
@@ -3,7 +3,7 @@
header "Denotational Abstract Interpretation"
theory Abs_Int_den0_fun
-imports "~~/src/HOL/ex/Interpretation_with_Defs" "../Big_Step"
+imports "~~/src/Tools/Permanent_Interpretation" "../Big_Step"
begin
subsection "Orderings"
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Thu Feb 20 21:45:08 2014 +0100
@@ -166,13 +166,13 @@
I (max_option False (l1 + Some 1) l2) h2)
else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
-interpretation Rep rep_ivl
+permanent_interpretation Rep rep_ivl
proof
case goal1 thus ?case
by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
qed
-interpretation Val_abs rep_ivl num_ivl plus_ivl
+permanent_interpretation Val_abs rep_ivl num_ivl plus_ivl
proof
case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)
next
@@ -180,7 +180,7 @@
by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
qed
-interpretation Rep1 rep_ivl
+permanent_interpretation Rep1 rep_ivl
proof
case goal1 thus ?case
by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
@@ -188,7 +188,7 @@
case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
qed
-interpretation
+permanent_interpretation
Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
proof
case goal1 thus ?case
@@ -200,12 +200,12 @@
auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
qed
-interpretation
+permanent_interpretation
Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
-defines afilter_ivl is afilter
-and bfilter_ivl is bfilter
-and AI_ivl is AI
-and aval_ivl is aval'
+defining afilter_ivl = afilter
+and bfilter_ivl = bfilter
+and AI_ivl = AI
+and aval_ivl = aval'
proof qed (auto simp: iter'_pfp_above)
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Thu Feb 20 21:45:08 2014 +0100
@@ -192,12 +192,12 @@
end
-interpretation
+permanent_interpretation
Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
-defines afilter_ivl' is afilter
-and bfilter_ivl' is bfilter
-and AI_ivl' is AI
-and aval_ivl' is aval'
+defining afilter_ivl' = afilter
+and bfilter_ivl' = bfilter
+and AI_ivl' = AI
+and aval_ivl' = aval'
proof qed (auto simp: iter'_pfp_above)
value [code] "list_up(AI_ivl' test3_ivl Top)"
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Thu Feb 20 21:45:08 2014 +0100
@@ -1,7 +1,7 @@
(* Author: Tobias Nipkow *)
theory Abs_Int0_ITP
-imports "~~/src/HOL/ex/Interpretation_with_Defs"
+imports "~~/src/Tools/Permanent_Interpretation"
"~~/src/HOL/Library/While_Combinator"
"Collecting_ITP"
begin
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Thu Feb 20 21:45:08 2014 +0100
@@ -52,7 +52,7 @@
end
-interpretation Val_abs
+permanent_interpretation Val_abs
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
proof
case goal1 thus ?case
@@ -66,9 +66,9 @@
by(auto simp: plus_const_cases split: const.split)
qed
-interpretation Abs_Int
+permanent_interpretation Abs_Int
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
-defines AI_const is AI and step_const is step' and aval'_const is aval'
+defining AI_const = AI and step_const = step' and aval'_const = aval'
..
@@ -114,7 +114,7 @@
text{* Monotonicity: *}
-interpretation Abs_Int_mono
+permanent_interpretation Abs_Int_mono
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
proof
case goal1 thus ?case
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Thu Feb 20 21:45:08 2014 +0100
@@ -113,9 +113,9 @@
proofs (they happened in the instatiation above) but delivers the
instantiated abstract interpreter which we call AI: *}
-interpretation Abs_Int
+permanent_interpretation Abs_Int
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
-defines aval_parity is aval' and step_parity is step' and AI_parity is AI
+defining aval_parity = aval' and step_parity = step' and AI_parity = AI
..
@@ -141,7 +141,7 @@
subsubsection "Termination"
-interpretation Abs_Int_mono
+permanent_interpretation Abs_Int_mono
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
proof
case goal1 thus ?case
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Thu Feb 20 21:45:08 2014 +0100
@@ -165,7 +165,7 @@
I (max_option False (l1 + Some 1) l2) h2)
else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
-interpretation Val_abs
+permanent_interpretation Val_abs
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
proof
case goal1 thus ?case
@@ -179,9 +179,9 @@
by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split option.splits)
qed
-interpretation Val_abs1_gamma
+permanent_interpretation Val_abs1_gamma
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
-defines aval_ivl is aval'
+defining aval_ivl = aval'
proof
case goal1 thus ?case
by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
@@ -198,7 +198,7 @@
done
-interpretation Val_abs1
+permanent_interpretation Val_abs1
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
@@ -215,21 +215,21 @@
auto simp: \<gamma>_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
qed
-interpretation Abs_Int1
+permanent_interpretation Abs_Int1
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
-defines afilter_ivl is afilter
-and bfilter_ivl is bfilter
-and step_ivl is step'
-and AI_ivl is AI
-and aval_ivl' is aval''
+defining afilter_ivl = afilter
+and bfilter_ivl = bfilter
+and step_ivl = step'
+and AI_ivl = AI
+and aval_ivl' = aval''
..
text{* Monotonicity: *}
-interpretation Abs_Int1_mono
+permanent_interpretation Abs_Int1_mono
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Thu Feb 20 21:45:08 2014 +0100
@@ -225,11 +225,11 @@
end
-interpretation Abs_Int2
+permanent_interpretation Abs_Int2
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
-defines AI_ivl' is AI_wn
+defining AI_ivl' = AI_wn
..
--- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Thu Feb 20 21:45:08 2014 +0100
@@ -89,7 +89,7 @@
WHILE b DO lift F c (sub\<^sub>1 ` M)
{F (post ` M)}"
-interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
+permanent_interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
proof
case goal1
have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"
--- a/src/HOL/IMP/Collecting.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Collecting.thy Thu Feb 20 21:45:08 2014 +0100
@@ -1,6 +1,6 @@
theory Collecting
imports Complete_Lattice Big_Step ACom
- "~~/src/HOL/ex/Interpretation_with_Defs"
+ "~~/src/Tools/Permanent_Interpretation"
begin
subsection "The generic Step function"
@@ -95,7 +95,7 @@
definition Inf_acom :: "com \<Rightarrow> 'a::complete_lattice acom set \<Rightarrow> 'a acom" where
"Inf_acom c M = annotate (\<lambda>p. INF C:M. anno C p) c"
-interpretation
+permanent_interpretation
Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c
proof
case goal1 thus ?case
--- a/src/HOL/IMP/Sem_Equiv.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/IMP/Sem_Equiv.thy Thu Feb 20 21:45:08 2014 +0100
@@ -75,10 +75,10 @@
P \<Turnstile> (c;; d) \<sim> (c';; d')"
by (clarsimp simp: equiv_up_to_def) blast
-lemma equiv_up_to_while_lemma:
+lemma equiv_up_to_while_lemma_weak:
shows "(d,s) \<Rightarrow> s' \<Longrightarrow>
P \<Turnstile> b <\<sim>> b' \<Longrightarrow>
- (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow>
+ P \<Turnstile> c \<sim> c' \<Longrightarrow>
(\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s') \<Longrightarrow>
P s \<Longrightarrow>
d = WHILE b DO c \<Longrightarrow>
@@ -92,7 +92,7 @@
have "bval b' s1" by (simp add: bequiv_up_to_def)
moreover
from WhileTrue.prems
- have "(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c'" by simp
+ have "P \<Turnstile> c \<sim> c'" by simp
with `bval b s1` `P s1` `(c, s1) \<Rightarrow> s2`
have "(c', s1) \<Rightarrow> s2" by (simp add: equiv_up_to_def)
moreover
@@ -108,45 +108,29 @@
thus ?case by (auto simp: bequiv_up_to_def)
qed (fastforce simp: equiv_up_to_def bequiv_up_to_def)+
-lemma bequiv_context_subst:
- "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)"
- by (auto simp: bequiv_up_to_def)
-
-lemma equiv_up_to_while:
+lemma equiv_up_to_while_weak:
assumes b: "P \<Turnstile> b <\<sim>> b'"
- assumes c: "(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c'"
+ assumes c: "P \<Turnstile> c \<sim> c'"
assumes I: "\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s'"
shows "P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
proof -
from b have b': "P \<Turnstile> b' <\<sim>> b" by (simp add: bequiv_up_to_sym)
- from c b have c': "(\<lambda>s. P s \<and> bval b' s) \<Turnstile> c' \<sim> c"
- by (simp add: equiv_up_to_sym bequiv_context_subst)
+ from c b have c': "P \<Turnstile> c' \<sim> c" by (simp add: equiv_up_to_sym)
from I
have I': "\<And>s s'. (c', s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b' s \<Longrightarrow> P s'"
by (auto dest!: equiv_up_toD1 [OF c'] simp: bequiv_up_to_subst [OF b'])
- note equiv_up_to_while_lemma [OF _ b c]
- equiv_up_to_while_lemma [OF _ b' c']
+ note equiv_up_to_while_lemma_weak [OF _ b c]
+ equiv_up_to_while_lemma_weak [OF _ b' c']
thus ?thesis using I I' by (auto intro!: equiv_up_toI)
qed
-lemma equiv_up_to_while_weak:
- "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow>
- (\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s') \<Longrightarrow>
- P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
- by (fastforce elim!: equiv_up_to_while equiv_up_to_weaken)
-
-lemma equiv_up_to_if:
- "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow>
- P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
- by (auto simp: bequiv_up_to_def equiv_up_to_def)
-
lemma equiv_up_to_if_weak:
"P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> d \<sim> d' \<Longrightarrow>
P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
- by (fastforce elim!: equiv_up_to_if equiv_up_to_weaken)
+ by (auto simp: bequiv_up_to_def equiv_up_to_def)
lemma equiv_up_to_if_True [intro!]:
"(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1"
--- a/src/HOL/Inductive.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/Inductive.thy Thu Feb 20 21:45:08 2014 +0100
@@ -177,12 +177,13 @@
text{*strong version, thanks to Coen and Frost*}
lemma coinduct_set: "[| mono(f); a: X; X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
- by (blast intro: weak_coinduct [OF _ coinduct_lemma])
+ by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
apply (rule order_trans)
apply (rule sup_ge1)
- apply (erule gfp_upperbound [OF coinduct_lemma])
+ apply (rule gfp_upperbound)
+ apply (erule coinduct_lemma)
apply assumption
done
--- a/src/HOL/Lifting.thy Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/Lifting.thy Thu Feb 20 21:45:08 2014 +0100
@@ -155,6 +155,10 @@
using a unfolding Quotient_def
by blast
+lemma Quotient_rep_abs_eq: "R t t \<Longrightarrow> R \<le> op= \<Longrightarrow> Rep (Abs t) = t"
+ using a unfolding Quotient_def
+ by blast
+
lemma Quotient_rep_abs_fold_unmap:
assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'"
shows "R (Rep' x') x"
@@ -455,13 +459,13 @@
assumes "left_unique T"
assumes "R \<le> op="
shows "(T OO R OO T\<inverse>\<inverse>) \<le> op="
-using assms unfolding left_unique_def by fast
+using assms unfolding left_unique_def by blast
lemma left_total_composition: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
unfolding left_total_def OO_def by fast
lemma left_unique_composition: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
-unfolding left_unique_def OO_def by fast
+unfolding left_unique_def OO_def by blast
lemma invariant_le_eq:
"invariant P \<le> op=" unfolding invariant_def by blast
--- a/src/HOL/ROOT Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/ROOT Thu Feb 20 21:45:08 2014 +0100
@@ -111,7 +111,7 @@
session "HOL-IMP" in IMP = HOL +
options [document_graph, document_variants=document]
theories [document = false]
- "~~/src/HOL/ex/Interpretation_with_Defs"
+ "~~/src/Tools/Permanent_Interpretation"
"~~/src/HOL/Library/While_Combinator"
"~~/src/HOL/Library/Char_ord"
"~~/src/HOL/Library/List_lexord"
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Feb 20 21:45:08 2014 +0100
@@ -1500,7 +1500,6 @@
val UNIVs = map HOLogic.mk_UNIV Ts;
val FTs = mk_FTs (passiveAs @ Ts);
- val FTs' = mk_FTs (passiveBs @ Ts);
val prodTs = map (HOLogic.mk_prodT o `I) Ts;
val prodFTs = mk_FTs (passiveAs @ prodTs);
val FTs_setss = mk_setss (passiveAs @ Ts);
@@ -2172,14 +2171,13 @@
(mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_Jmap),
HOLogic.mk_comp (Term.list_comb (map, fs @ fs_Jmaps), dtor)));
val goals = map4 mk_goal fs_Jmaps map_FTFT's dtors dtor's;
- val cTs = map (SOME o certifyT lthy) FTs';
val maps =
- map5 (fn goal => fn cT => fn unfold => fn map_comp => fn map_cong0 =>
+ map5 (fn goal => fn unfold => fn map_comp => fn map_cong0 => fn map_arg_cong =>
Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
- mk_map_tac m n cT unfold map_comp map_cong0)
+ mk_map_tac m n map_arg_cong unfold map_comp map_cong0)
|> Thm.close_derivation)
- goals cTs dtor_unfold_thms map_comps map_cong0s;
+ goals dtor_unfold_thms map_comps map_cong0s map_arg_cong_thms;
in
map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps
end;
@@ -2398,10 +2396,10 @@
val zipFTs = mk_FTs zip_ranTs;
val zipTs = map3 (fn T => fn T' => fn FT => T --> T' --> FT) Ts Ts' zipFTs;
val zip_zTs = mk_Ts passiveABs;
- val (((zips, (abs, abs')), zip_zs), names_lthy) = names_lthy
+ val (((zips, (abs, abs')), (zip_zs, zip_zs')), names_lthy) = names_lthy
|> mk_Frees "zip" zipTs
||>> mk_Frees' "ab" passiveABs
- ||>> mk_Frees "z" zip_zTs;
+ ||>> mk_Frees' "z" zip_zTs;
val Iphi_sets =
map2 (fn phi => fn T => HOLogic.Collect_const T $ HOLogic.mk_split phi) allJphis zip_ranTs;
@@ -2424,6 +2422,7 @@
fun Jrel_coinduct_tac {context = ctxt, prems = CIHs} =
let
+val lthy = Config.put quick_and_dirty false lthy (*XXX*)
fun mk_helper_prem phi in_phi zip x y map map' dtor dtor' =
let
val zipxy = zip $ x $ y;
@@ -2435,53 +2434,76 @@
end;
val helper_prems = map9 mk_helper_prem
activeJphis in_phis zips Jzs Jz's map_all_fsts map_all_snds dtors dtor's;
- fun mk_helper_coind_concl fst phi x alt y map zip_unfold =
- HOLogic.mk_imp (list_exists_free [if fst then y else x] (HOLogic.mk_conj (phi $ x $ y,
- HOLogic.mk_eq (alt, map $ (zip_unfold $ HOLogic.mk_prod (x, y))))),
- HOLogic.mk_eq (alt, if fst then x else y));
+ fun mk_helper_coind_phi fst phi x alt y map zip_unfold =
+ list_exists_free [if fst then y else x] (HOLogic.mk_conj (phi $ x $ y,
+ HOLogic.mk_eq (alt, map $ (zip_unfold $ HOLogic.mk_prod (x, y)))))
+ val coind1_phis = map6 (mk_helper_coind_phi true)
+ activeJphis Jzs Jzs_copy Jz's Jmap_fsts zip_unfolds;
+ val coind2_phis = map6 (mk_helper_coind_phi false)
+ activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds;
+ fun mk_cts zs z's phis =
+ map3 (fn z => fn z' => fn phi =>
+ SOME (certify lthy (fold_rev (Term.absfree o Term.dest_Free) [z', z] phi)))
+ zs z's phis @
+ map (SOME o certify lthy) (splice z's zs);
+ val cts1 = mk_cts Jzs Jzs_copy coind1_phis;
+ val cts2 = mk_cts Jz's Jz's_copy coind2_phis;
+
+ fun mk_helper_coind_concl z alt coind_phi =
+ HOLogic.mk_imp (coind_phi, HOLogic.mk_eq (alt, z));
val helper_coind1_concl =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map6 (mk_helper_coind_concl true)
- activeJphis Jzs Jzs_copy Jz's Jmap_fsts zip_unfolds));
+ (map3 mk_helper_coind_concl Jzs Jzs_copy coind1_phis));
val helper_coind2_concl =
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map6 (mk_helper_coind_concl false)
- activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds));
- fun mk_helper_coind_thms vars concl =
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Jphis @ activeJphis @ vars @ zips)
- (Logic.list_implies (helper_prems, concl)))
+ (map3 mk_helper_coind_concl Jz's Jz's_copy coind2_phis));
+
+ fun mk_helper_coind_thms concl cts =
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl))
(fn {context = ctxt, prems = _} => mk_rel_coinduct_coind_tac ctxt m
- dtor_map_coinduct_thm ks map_comps map_cong0s map_arg_cong_thms set_mapss
- dtor_unfold_thms dtor_Jmap_thms)
+ (cterm_instantiate_pos cts dtor_map_coinduct_thm) ks map_comps map_cong0s
+ map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms)
|> Thm.close_derivation
- |> split_conj_thm;
- val helper_coind1_thms = mk_helper_coind_thms (Jzs @ Jzs_copy) helper_coind1_concl;
- val helper_coind2_thms = mk_helper_coind_thms (Jz's @ Jz's_copy) helper_coind2_concl;
-
- fun mk_helper_ind_concl phi ab' ab fst snd z active_phi x y zip_unfold set =
- mk_Ball (set $ z) (Term.absfree ab' (list_all_free [x, y] (HOLogic.mk_imp
+ |> split_conj_thm
+ |> Proof_Context.export names_lthy lthy;
+
+ val helper_coind1_thms = mk_helper_coind_thms helper_coind1_concl cts1;
+ val helper_coind2_thms = mk_helper_coind_thms helper_coind2_concl cts2;
+
+ fun mk_helper_ind_phi phi ab fst snd z active_phi x y zip_unfold =
+ list_all_free [x, y] (HOLogic.mk_imp
(HOLogic.mk_conj (active_phi $ x $ y,
HOLogic.mk_eq (z, zip_unfold $ HOLogic.mk_prod (x, y))),
- phi $ (fst $ ab) $ (snd $ ab)))));
+ phi $ (fst $ ab) $ (snd $ ab)));
+ val helper_ind_phiss =
+ map4 (fn Jphi => fn ab => fn fst => fn snd =>
+ map5 (mk_helper_ind_phi Jphi ab fst snd)
+ zip_zs activeJphis Jzs Jz's zip_unfolds)
+ Jphis abs fstABs sndABs;
+ val ctss = map2 (fn ab' => fn phis =>
+ map2 (fn z' => fn phi =>
+ SOME (certify lthy (Term.absfree ab' (Term.absfree z' phi))))
+ zip_zs' phis @
+ map (SOME o certify lthy) zip_zs)
+ abs' helper_ind_phiss;
+ fun mk_helper_ind_concl ab' z ind_phi set =
+ mk_Ball (set $ z) (Term.absfree ab' ind_phi);
val mk_helper_ind_concls =
- map6 (fn Jphi => fn ab' => fn ab => fn fst => fn snd => fn zip_sets =>
- map6 (mk_helper_ind_concl Jphi ab' ab fst snd)
- zip_zs activeJphis Jzs Jz's zip_unfolds zip_sets)
- Jphis abs' abs fstABs sndABs zip_setss
+ map3 (fn ab' => fn ind_phis => fn zip_sets =>
+ map3 (mk_helper_ind_concl ab') zip_zs ind_phis zip_sets)
+ abs' helper_ind_phiss zip_setss
|> map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj);
-
+
val helper_ind_thmss = if m = 0 then replicate n [] else
- map3 (fn concl => fn j => fn set_induct =>
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Jphis @ activeJphis @ zip_zs @ zips)
- (Logic.list_implies (helper_prems, concl)))
+ map4 (fn concl => fn j => fn set_induct => fn cts =>
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl))
(fn {context = ctxt, prems = _} => mk_rel_coinduct_ind_tac ctxt m ks
- dtor_unfold_thms set_mapss j set_induct)
+ dtor_unfold_thms set_mapss j (cterm_instantiate_pos cts set_induct))
|> Thm.close_derivation
- |> split_conj_thm)
- mk_helper_ind_concls ls dtor_Jset_induct_thms
+ |> split_conj_thm
+ |> Proof_Context.export names_lthy lthy)
+ mk_helper_ind_concls ls dtor_Jset_induct_thms ctss
|> transpose;
in
mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Feb 20 21:45:08 2014 +0100
@@ -43,7 +43,7 @@
val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
thm list list -> thm list list -> thm list list list -> tactic
val mk_map_id0_tac: thm list -> thm -> thm -> tactic
- val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
+ val mk_map_tac: int -> int -> thm -> thm -> thm -> thm -> tactic
val mk_dtor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
val mk_mor_Abs_tac: Proof.context -> thm list -> thm list -> tactic
val mk_mor_Rep_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list ->
@@ -427,16 +427,16 @@
CONJ_WRAP' (fn rv_Cons =>
CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac exI,
rtac (@{thm append_Nil} RS arg_cong RS trans),
- rtac (rv_Cons RS trans), rtac (mk_sum_caseN n i RS arg_cong RS trans), rtac rv_Nil]))
+ rtac (rv_Cons RS trans), rtac (mk_sum_caseN n i RS trans), rtac rv_Nil]))
(ks ~~ rv_Nils))
rv_Conss,
REPEAT_DETERM o rtac allI, rtac (mk_sumEN n),
EVERY' (map (fn i =>
CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
- rtac (@{thm append_Cons} RS arg_cong RS trans),
- rtac (rv_Cons RS trans), etac (sum_weak_case_cong RS arg_cong RS trans),
- rtac (mk_sum_caseN n i RS arg_cong RS trans), atac])
+ rtac (@{thm append_Cons} RS arg_cong RS trans), rtac (rv_Cons RS trans),
+ if n = 1 then K all_tac else etac (sum_weak_case_cong RS trans),
+ rtac (mk_sum_caseN n i RS trans), atac])
ks])
rv_Conss)
ks)] 1
@@ -795,12 +795,12 @@
rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
end;
-fun mk_map_tac m n cT unfold map_comp map_cong0 =
+fun mk_map_tac m n map_arg_cong unfold map_comp map_cong0 =
EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS box_equals)), rtac map_cong0,
REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
- rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1;
+ rtac map_arg_cong, rtac (o_apply RS sym)] 1;
fun mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss =
EVERY' [rtac hset_minimal,
@@ -1018,7 +1018,7 @@
dtor_unfolds dtor_maps =
let val n = length ks;
in
- EVERY' [DETERM o rtac coinduct,
+ EVERY' [rtac coinduct,
EVERY' (map7 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s =>
fn dtor_unfold => fn dtor_map =>
EVERY' [REPEAT_DETERM o eresolve_tac [exE, conjE],
--- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Feb 20 21:39:38 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu Feb 20 21:45:08 2014 +0100
@@ -27,28 +27,28 @@
(* Reflexivity prover *)
-fun refl_tac ctxt =
+fun mono_eq_prover ctxt prop =
+ let
+ val rules = ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt))
+ in
+ SOME (Goal.prove ctxt [] [] prop (K (REPEAT_ALL_NEW (resolve_tac rules) 1)))
+ handle ERROR _ => NONE
+ end
+
+fun try_prove_reflexivity ctxt prop =
let
- fun intro_reflp_tac (ct, i) =
- let
- val rule = Thm.incr_indexes (#maxidx (rep_cterm ct) + 1) @{thm ge_eq_refl}
- val concl_pat = Drule.strip_imp_concl (cprop_of rule)
- val insts = Thm.first_order_match (concl_pat, ct)
- in
- rtac (Drule.instantiate_normalize insts rule) i
- end
- handle Pattern.MATCH => no_tac
-
- val rules = @{thm is_equality_eq} ::
- ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt))
+ val thy = Proof_Context.theory_of ctxt
+ val cprop = cterm_of thy prop
+ val rule = @{thm ge_eq_refl}
+ val concl_pat = Drule.strip_imp_concl (cprop_of rule)
+ val insts = Thm.first_order_match (concl_pat, cprop)
+ val rule = Drule.instantiate_normalize insts rule
+ val prop = hd (prems_of rule)
in
- EVERY' [CSUBGOAL intro_reflp_tac,
- REPEAT_ALL_NEW (resolve_tac rules)]
+ case mono_eq_prover ctxt prop of
+ SOME thm => SOME (thm RS rule)
+ | NONE => NONE
end
-
-fun try_prove_reflexivity ctxt prop =
- SOME (Goal.prove ctxt [] [] prop (fn {context, ...} => refl_tac context 1))
- handle ERROR _ => NONE
(*
Generates a parametrized transfer rule.
@@ -259,50 +259,35 @@
| Const (@{const_name invariant}, _) $ _ => true
| _ => false
-fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) =
+fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) =
let
- val thy = Proof_Context.theory_of ctxt
- val quot_thm = Lifting_Term.prove_quot_thm ctxt (get_body_types (rty, qty))
- val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
- val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs}
- val abs_rep_eq =
- case (HOLogic.dest_Trueprop o prop_of) fun_rel of
- Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm
- | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
- | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm
val unabs_def = unabs_all_def ctxt unfolded_def
- val rep = (cterm_of thy o quot_thm_rep) quot_thm
- val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
- val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
- val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans}
- in
- simplify_code_eq ctxt code_cert
+ in
+ if body_type rty = body_type qty then
+ SOME (simplify_code_eq ctxt unabs_def)
+ else
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val quot_thm = Lifting_Term.prove_quot_thm ctxt (get_body_types (rty, qty))
+ val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
+ val rep_abs_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs_eq}
+ in
+ case mono_eq_prover ctxt (hd(prems_of rep_abs_thm)) of
+ SOME mono_eq_thm =>
+ let
+ val rep_abs_eq = mono_eq_thm RS rep_abs_thm
+ val rep = (cterm_of thy o quot_thm_rep) quot_thm
+ val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
+ val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
+ val code_cert = [repped_eq, rep_abs_eq] MRSL trans
+ in
+ SOME (simplify_code_eq ctxt code_cert)
+ end
+ | NONE => NONE
+ end
end
-fun generate_trivial_rep_eq ctxt def_thm =
- let
- val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm
- val code_eq = unabs_all_def ctxt unfolded_def
- val simp_code_eq = simplify_code_eq ctxt code_eq
- in
- simp_code_eq
- end
-
-fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) =
- if body_type rty = body_type qty then
- SOME (generate_trivial_rep_eq ctxt def_thm)
- else
- let
- val (rty_body, qty_body) = get_body_types (rty, qty)
- val quot_thm = Lifting_Term.prove_quot_thm ctxt (rty_body, qty_body)
- in
- if can_generate_code_cert quot_thm then
- SOME (generate_code_cert ctxt def_thm rsp_thm (rty, qty))
- else
- NONE
- end
-
fun generate_abs_eq ctxt def_thm rsp_thm quot_thm =
let
val abs_eq_with_assms =
--- a/src/HOL/ex/Interpretation_with_Defs.thy Thu Feb 20 21:39:38 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(* Title: HOL/ex/Interpretation_with_Defs.thy
- Author: Florian Haftmann, TU Muenchen
-*)
-
-header {* Interpretation accompanied with mixin definitions. EXPERIMENTAL. *}
-
-theory Interpretation_with_Defs
-imports Pure
-begin
-
-ML_file "~~/src/Tools/interpretation_with_defs.ML"
-
-end
--- a/src/Tools/Code/code_namespace.ML Thu Feb 20 21:39:38 2014 +0100
+++ b/src/Tools/Code/code_namespace.ML Thu Feb 20 21:45:08 2014 +0100
@@ -245,17 +245,20 @@
val (nsps', nodes') = (nsps, nodes)
|> fold (declare (K namify_module)) module_fragments
|> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_syms;
- fun zip_fillup xs ys = xs ~~ ys @ replicate (length xs - length ys) NONE;
fun select_syms syms = case filter (member (op =) stmt_syms) syms
of [] => NONE
| syms => SOME syms;
- val modify_stmts' = AList.make (snd o Code_Symbol.Graph.get_node nodes)
- #> split_list
- ##> map (fn Stmt stmt => stmt)
- #> (fn (syms, stmts) => zip_fillup syms (modify_stmts (syms ~~ stmts)));
+ fun select_stmt (sym, SOME stmt) = SOME (sym, stmt)
+ | select_stmt _ = NONE;
+ fun modify_stmts' syms =
+ let
+ val stmts = map ((fn Stmt stmt => stmt) o snd o Code_Symbol.Graph.get_node nodes) syms;
+ val stmts' = modify_stmts (syms ~~ stmts);
+ val stmts'' = stmts' @ replicate (length syms - length stmts') NONE;
+ in map_filter select_stmt (syms ~~ stmts'') end;
val stmtss' = (maps modify_stmts' o map_filter select_syms o Code_Symbol.Graph.strong_conn) nodes;
val nodes'' = Code_Symbol.Graph.map (fn sym => apsnd (fn Module content => Module (make_declarations nsps' content)
- | _ => case AList.lookup (op =) stmtss' sym of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes';
+ | _ => case AList.lookup (op =) stmtss' sym of SOME stmt => Stmt stmt | _ => Dummy)) nodes';
val data' = fold memorize_data stmt_syms data;
in (data', nodes'') end;
val (_, hierarchical_program) = make_declarations empty_nsp proto_program;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Permanent_Interpretation.thy Thu Feb 20 21:45:08 2014 +0100
@@ -0,0 +1,14 @@
+(* Title: Tools/Permanent_Interpretation.thy
+ Author: Florian Haftmann, TU Muenchen
+*)
+
+header {* Permanent interpretation accompanied with mixin definitions. *}
+
+theory Permanent_Interpretation
+imports Pure
+keywords "defining" and "permanent_interpretation" :: thy_goal
+begin
+
+ML_file "~~/src/Tools/permanent_interpretation.ML"
+
+end
--- a/src/Tools/interpretation_with_defs.ML Thu Feb 20 21:39:38 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,92 +0,0 @@
-(* Title: Tools/interpretation_with_defs.ML
- Author: Florian Haftmann, TU Muenchen
-
-Interpretation accompanied with mixin definitions. EXPERIMENTAL.
-*)
-
-signature INTERPRETATION_WITH_DEFS =
-sig
- val interpretation: Expression.expression_i ->
- (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list ->
- theory -> Proof.state
- val interpretation_cmd: Expression.expression ->
- (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list ->
- theory -> Proof.state
-end;
-
-structure Interpretation_With_Defs : INTERPRETATION_WITH_DEFS =
-struct
-
-fun note_eqns_register deps witss def_eqns attrss eqns export export' =
- let
- fun meta_rewrite context =
- map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
- maps snd;
- in
- Attrib.generic_notes Thm.lemmaK
- (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
- #-> (fn facts => `(fn context => meta_rewrite context facts))
- #-> (fn eqns => fold (fn ((dep, morph), wits) =>
- fn context =>
- Locale.add_registration
- (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
- (Element.eq_morphism (Context.theory_of context) (def_eqns @ eqns) |>
- Option.map (rpair true))
- export context) (deps ~~ witss))
- end;
-
-local
-
-fun gen_interpretation prep_expr prep_decl parse_term parse_prop prep_attr
- expression raw_defs raw_eqns theory =
- let
- val (_, (_, defs_ctxt)) =
- prep_decl expression I [] (Proof_Context.init_global theory);
-
- val rhss = map (parse_term defs_ctxt o snd o snd) raw_defs
- |> Syntax.check_terms defs_ctxt;
- val defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
- ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
-
- val (def_eqns, theory') = theory
- |> Named_Target.theory_init
- |> fold_map (Local_Theory.define) defs
- |>> map (Thm.symmetric o snd o snd)
- |> Local_Theory.exit_result_global (map o Morphism.thm);
-
- val ((propss, deps, export), expr_ctxt) = theory'
- |> Proof_Context.init_global
- |> prep_expr expression;
-
- val eqns = map (parse_prop expr_ctxt o snd) raw_eqns
- |> Syntax.check_terms expr_ctxt;
- val attrss = map ((apsnd o map) (prep_attr theory) o fst) raw_eqns;
- val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
- val export' = Variable.export_morphism goal_ctxt expr_ctxt;
-
- fun after_qed witss eqns =
- (Proof_Context.background_theory o Context.theory_map)
- (note_eqns_register deps witss def_eqns attrss eqns export export');
-
- in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
-
-in
-
-fun interpretation x = gen_interpretation Expression.cert_goal_expression
- Expression.cert_declaration (K I) (K I) (K I) x;
-fun interpretation_cmd x = gen_interpretation Expression.read_goal_expression
- Expression.read_declaration Syntax.parse_term Syntax.parse_prop Attrib.intern_src x;
-
-end;
-
-val _ =
- Outer_Syntax.command @{command_spec "interpretation"}
- "prove interpretation of locale expression in theory"
- (Parse.!!! (Parse_Spec.locale_expression true) --
- Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
- -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] --
- Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
- >> (fn ((expr, defs), equations) => Toplevel.print o
- Toplevel.theory_to_proof (interpretation_cmd expr defs equations)));
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/permanent_interpretation.ML Thu Feb 20 21:45:08 2014 +0100
@@ -0,0 +1,110 @@
+(* Title: Tools/permanent_interpretation.ML
+ Author: Florian Haftmann, TU Muenchen
+
+Permanent interpretation accompanied with mixin definitions.
+*)
+
+signature PERMANENT_INTERPRETATION =
+sig
+ val permanent_interpretation: Expression.expression_i ->
+ (Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list ->
+ local_theory -> Proof.state
+ val permanent_interpretation_cmd: Expression.expression ->
+ (Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list ->
+ local_theory -> Proof.state
+end;
+
+structure Permanent_Interpretation : PERMANENT_INTERPRETATION =
+struct
+
+local
+
+(* reading *)
+
+fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt =
+ let
+ (*reading*)
+ val ((_, deps, _), proto_deps_ctxt) = prep_expr expression initial_ctxt;
+ val deps_ctxt = fold Locale.activate_declarations deps proto_deps_ctxt;
+ val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt;
+ val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs;
+ val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns;
+
+ (*defining*)
+ val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
+ ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
+ val (defs, defs_ctxt) = fold_map Local_Theory.define pre_defs initial_ctxt;
+ val def_eqns = map (Thm.symmetric o Morphism.thm (Local_Theory.standard_morphism defs_ctxt initial_ctxt) o snd o snd) defs;
+ val base_ctxt = if null def_eqns then defs_ctxt else Local_Theory.restore defs_ctxt;
+ (*the "if" prevents restoring a proof context which is no local theory*)
+
+ (*setting up*)
+ val ((propss, deps, export), expr_ctxt) = prep_expr expression base_ctxt;
+ (*FIXME: only re-prepare if defs are given*)
+ val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of expr_ctxt))) o fst) raw_eqns;
+ val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
+ val export' = Variable.export_morphism goal_ctxt expr_ctxt;
+ in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
+
+val cert_interpretation = prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I);
+val read_interpretation = prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.intern_src;
+
+
+(* generic interpretation machinery *)
+
+fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
+
+fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt =
+ let
+ val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])])
+ :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
+ val (eqns', ctxt') = ctxt
+ |> note Thm.lemmaK facts
+ |-> meta_rewrite;
+ val dep_morphs = map2 (fn (dep, morph) => fn wits =>
+ (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss;
+ fun activate' dep_morph ctxt = activate dep_morph
+ (Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt;
+ in
+ ctxt'
+ |> fold activate' dep_morphs
+ end;
+
+fun generic_interpretation prep_interpretation setup_proof note add_registration
+ expression raw_defs raw_eqns initial_ctxt =
+ let
+ val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) =
+ prep_interpretation expression raw_defs raw_eqns initial_ctxt;
+ fun after_qed witss eqns =
+ note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';
+ in setup_proof after_qed propss eqns goal_ctxt end;
+
+
+(* interpretation with permanent registration *)
+
+fun subscribe lthy =
+ if Named_Target.is_theory lthy
+ then Generic_Target.theory_registration
+ else Generic_Target.locale_dependency (Named_Target.the_name lthy);
+
+fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns lthy =
+ generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind (subscribe lthy)
+ expression raw_defs raw_eqns lthy
+
+in
+
+fun permanent_interpretation x = gen_permanent_interpretation cert_interpretation x;
+fun permanent_interpretation_cmd x = gen_permanent_interpretation read_interpretation x;
+
+end;
+
+val _ =
+ Outer_Syntax.local_theory_to_proof @{command_spec "permanent_interpretation"}
+ "prove interpretation of locale expression into named theory"
+ (Parse.!!! (Parse_Spec.locale_expression true) --
+ Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
+ -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
+ Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
+ >> (fn ((expr, defs), eqns) => permanent_interpretation_cmd expr defs eqns));
+
+end;
