Email Gateway (Aug 18 2022 at 18:40): Email Gateway (Aug 18 2022 at 18:40):From: John Wickerson <jpw48@cam.ac.uk>
Hello,
I have a whole bunch of mutually-inductively-defined datatypes, functions and predicates in my theory, and I'm having difficulty doing structural and rule induction over them.
At the end of this email is my (slightly condensed) theory file. Apologies for not creating a minimal example exhibiting my problem -- I thought it better to leave the theory file mostly as-is, to ensure that your solutions apply to my real script and not just to some minimal example.
The problem is the last line ...
proof(induct rule: prov_dia_prov_col.induct)
... which gives an error ("Proof command failed"), despite my goal being of the required form "?P ?a \<and> ?Q ?A". My question is: How can I give Isabelle hints to help it work out how to apply the given induction rule?
Many thanks,
John
------------8<-------------
theory Ribbons imports Main
begin
typedecl bool_exp
consts Not :: "bool_exp \<Rightarrow> bool_exp"
consts rd_be :: "bool_exp \<Rightarrow> string set"
typedecl assertion
consts Emp :: "assertion"
consts Pure :: "bool_exp \<Rightarrow> assertion"
axiomatization
Star :: "assertion \<Rightarrow> assertion \<Rightarrow> assertion"
where star_comm: "Star p q = Star q p"
and star_assoc: "Star (Star p q) r = Star p (Star q r)"
and star_emp: "Star p Emp = p"
and emp_star: "Star Emp p = p"
consts Exists :: "string \<Rightarrow> assertion \<Rightarrow> assertion"
axiomatization
rd_ass :: "assertion \<Rightarrow> string set"
where rd_emp: "rd_ass Emp = {}"
and rd_star: "rd_ass (Star p q) = rd_ass p \<union> rd_ass q"
and rd_exists: "rd_ass (Exists x p) = rd_ass p"
typedecl atomic
consts rd_atm :: "atomic \<Rightarrow> string set"
consts wr_atm :: "atomic \<Rightarrow> string set"
datatype command =
Atomic "atomic"
| If "bool_exp" "command list" "command list"
| While "bool_exp" "command list"
fun
interleave_coms :: "(command list \<times> command list) \<Rightarrow> command list set"
where
"interleave_coms ([], C2) = {C2}"
| "interleave_coms (C1, []) = {C1}"
| "interleave_coms (c1#C1, c2#C2)
= {c1#C | C. C \<in> interleave_coms(C1, c2#C2)}
\<union> {c2#C | C. C \<in> interleave_coms(c1#C1, C2)}"
inductive
prov_com :: "assertion \<times> command \<times> assertion \<Rightarrow> bool"
and
prov_comlist :: "assertion \<times> command list \<times> assertion \<Rightarrow> bool"
where
exists:
"prov_com (p, c, q)
\<Longrightarrow> prov_com (Exists x p, c, Exists x q)"
| ifcom:
"\<lbrakk>prov_comlist (Star (Pure b) p, C1, q);
prov_comlist (Star (Pure (Not b)) p, C2, q)\<rbrakk>
\<Longrightarrow> prov_com (p, If b C1 C2, q)"
| while:
"prov_comlist (Star (Pure b) p, C, p)
\<Longrightarrow> prov_com (p, While b C, Star (Pure (Not b)) p)"
| frame:
"\<lbrakk>prov_com (p, c, q); wr_com(c) \<inter> rd_ass(r) = {}\<rbrakk>
\<Longrightarrow> prov_com (Star p r, c, Star q r)"
| skip:
"prov_comlist(p, [], p)"
| seq:
"\<lbrakk>prov_com (p, c, q); prov_comlist (q, C, r)\<rbrakk>
\<Longrightarrow> prov_comlist (p, c#C, r)"
datatype face =
Ribbon "assertion"
| Exists_int "string" "face list"
type_synonym interface = "face list"
fun
ass_face :: "face \<Rightarrow> assertion"
and
ass :: "interface \<Rightarrow> assertion"
where
"ass_face (Ribbon p) = p"
| "ass_face (Exists_int x P) = Exists x (ass P)"
| "ass [] = Emp"
| "ass (f#P) = Star (ass_face f) (ass P)"
datatype column =
Blank "interface"
| Basic "interface" "command" "interface"
| VComp_dia "column list" "column list"
| Exists_dia "string" "column list"
| If_dia "interface" "bool_exp" "column list" "column list" "interface"
| While_dia "interface" "bool_exp" "column list" "interface"
type_synonym diagram = "column list"
fun
top :: "diagram \<Rightarrow> interface"
and
top_col :: "column \<Rightarrow> interface"
where
"top_col (Blank P) = P"
| "top_col (Basic P c Q) = P"
| "top_col (VComp_dia A B) = top A"
| "top_col (Exists_dia x A) = [Exists_int x (top A)]"
| "top_col (If_dia P b A B Q) = P"
| "top_col (While_dia P b A Q) = P"
| "top [] = []"
| "top (a # A) = (top_col a) @ (top A)"
fun
bot :: "diagram \<Rightarrow> interface"
and
bot_col :: "column \<Rightarrow> interface"
where
"bot_col (Blank P) = P"
| "bot_col (Basic P c Q) = Q"
| "bot_col (VComp_dia A B) = bot B"
| "bot_col (Exists_dia x A) = [Exists_int x (bot A)]"
| "bot_col (If_dia P b A B Q) = Q"
| "bot_col (While_dia P b A Q) = Q"
| "bot [] = []"
| "bot (a # A) = (bot_col a) @ (bot A)"
fun
coms :: "diagram \<Rightarrow> command list set"
and
coms_col :: "column \<Rightarrow> command list set"
where
"coms_col (Blank P) = {}"
| "coms_col (Basic P c Q) = {[c]}"
| "coms_col (VComp_dia A B)
= {C @ C' | C C'. C \<in> coms A \<and> C' \<in> coms B}"
| "coms_col (Exists_dia x A) = coms A"
| "coms_col (If_dia P b A B Q)
= { [If b C C'] | C C'. C \<in> coms A \<and> C' \<in> coms B}"
| "coms_col (While_dia P b A Q) = { [While b C] | C. C \<in> coms A}"
| "coms [] = {}"
| "coms (a # A)
= \<Union>{interleave_coms (C, C') | C C'. C \<in> coms_col a \<and> C' \<in> coms A}"
consts
disj_col_dia :: "column \<Rightarrow> diagram \<Rightarrow> bool"
inductive
prov_dia :: "diagram \<Rightarrow> bool"
and
prov_col :: "column \<Rightarrow> bool"
where
Blank:
"prov_col (Blank P)"
| Basic:
"prov_com (ass P, c, ass Q) \<Longrightarrow> prov_col (Basic P c Q)"
| Exists:
"prov_dia A \<Longrightarrow> prov_col (Exists_dia x A)"
| VComp:
"\<lbrakk>prov_dia A; prov_dia B; bot A = top B\<rbrakk> \<Longrightarrow> prov_col (VComp_dia A B)"
| If:
"\<lbrakk>prov_dia A; prov_dia B; top A = (Ribbon (Pure b)) # P;
top B = (Ribbon (Pure (Not b))) # P; bot A = Q; bot B = Q\<rbrakk>
\<Longrightarrow> prov_col (If_dia P b A B Q)"
| While:
"\<lbrakk>prov_dia A; top A = (Ribbon(Pure b)) # P;
bot A = P; Q = (Ribbon(Pure (Not b))) # P\<rbrakk>
\<Longrightarrow> prov_col (While_dia P b A Q)"
| Nil:
"prov_dia []"
| Cons:
"\<lbrakk>prov_col a; prov_dia A; disj_col_dia a A\<rbrakk>
\<Longrightarrow> prov_dia (a # A)"
datatype chain =
cNil "assertion"
| cCons "assertion" "command" "chain"
fun
seq_chains :: "chain \<times> chain \<Rightarrow> chain"
where
"seq_chains (cNil _, G') = G'"
| "seq_chains (cCons p c G, G') = cCons p c (seq_chains (G, G'))"
fun
pre :: "chain \<Rightarrow> assertion"
where
"pre(cNil p) = p"
| "pre(cCons p c G) = p"
fun
post :: "chain \<Rightarrow> assertion"
where
"post(cNil p) = p"
| "post(cCons p c G) = post G"
fun
comlist :: "chain \<Rightarrow> command list"
where
"comlist(cNil p) = []"
| "comlist(cCons p c G) = c # (comlist G)"
fun
ass_map :: "(assertion \<Rightarrow> assertion) \<Rightarrow> chain \<Rightarrow> chain"
where
"ass_map f (cNil p) = cNil (f p)"
| "ass_map f (cCons p c G) = cCons (f p) c (ass_map f G)"
function
interleave_chains :: "(chain \<times> chain) \<Rightarrow> chain set"
where
"interleave_chains (cNil p, G) = {ass_map (\<lambda>q. Star p q) G}"
| "interleave_chains (G, cNil p) = {ass_map (\<lambda>q. Star q p) G}"
| "interleave_chains (cCons p1 c1 G1, cCons p2 c2 G2)
= {cCons (Star p1 p2) c1 G | G.
G \<in> interleave_chains(G1, cCons p2 c2 G2)}
\<union> {cCons (Star p1 p2) c2 G | G.
G \<in> interleave_chains(cCons p1 c1 G1, G2)}"
by pat_completeness auto
termination by lexicographic_order
lemma chainpair_induction [case_names Nil_Cons Cons_Nil Cons_Cons]:
assumes "\<And>p1 G2. \<Phi> (cNil p1) G2"
assumes "\<And>p2 G1. \<Phi> G1 (cNil p2)"
assumes "\<And>p1 p2 c1 c2 G1 G2.
\<lbrakk>\<Phi> G1 (cCons p2 c2 G2); \<Phi> (cCons p1 c1 G1) G2\<rbrakk>
\<Longrightarrow> \<Phi> (cCons p1 c1 G1) (cCons p2 c2 G2)"
shows "\<Phi> G1 G2"
using assms
by induction_schema (pat_completeness, lexicographic_order)
consts disj_chain :: "chain \<Rightarrow> chain \<Rightarrow> bool"
inductive
prov_chain :: "chain \<Rightarrow> bool"
where
skip: "prov_chain(cNil p)"
| seq: "\<lbrakk>prov_com(p, c, pre G); prov_chain G\<rbrakk>
\<Longrightarrow> prov_chain(cCons p c G)"
fun
chains :: "diagram \<Rightarrow> chain set"
and
chains_col :: "column \<Rightarrow> chain set"
where
"chains_col (Blank P) = {cNil (ass P)}"
| "chains_col (Basic P c Q) = {cCons (ass P) c (cNil (ass Q))}"
| "chains_col (VComp_dia A B) = {seq_chains (G1, G2)
| G1 G2. G1 \<in> chains A \<and> G2 \<in> chains B \<and> post G1 = pre G2}"
| "chains_col (Exists_dia x A) = {ass_map (Exists x) G
| G. G \<in> chains A}"
| "chains_col (If_dia P b A B Q) =
{cCons (ass P) (If b (comlist G1) (comlist G2)) (cNil (ass Q))
| G1 G2. G1 \<in> chains A \<and> G2 \<in> chains B
\<and> pre G1 = Star (Pure b) (ass P)
\<and> pre G2 = Star (Pure (Not b)) (ass P)
\<and> post G1 = ass Q \<and> post G2 = ass Q }"
| "chains_col (While_dia P b A Q) =
{ cCons (ass P) (While b (comlist G)) (cNil (ass Q))
| G. G \<in> chains A \<and> post G = ass P
\<and> pre G = Star (Pure b) (ass P)
\<and> ass Q = Star (Pure (Not b)) (ass P) }"
| "chains [] = {}"
| "chains (a # A) = \<Union> {interleave_chains (G1, G2)
| G1 G2. G1 \<in> chains_col a \<and> G2 \<in> chains A \<and> disj_chain G1 G2}"
lemma soundness_part_one:
fixes a and A
shows "(prov_col a \<longrightarrow> (\<forall>G \<in> chains_col a. prov_chain G)) \<and> (prov_dia A \<longrightarrow> (\<forall>G \<in> chains A. prov_chain G))"
proof(induct rule: prov_dia_prov_col.induct)
Email Gateway (Aug 18 2022 at 18:40):From: Tobias Nipkow <nipkow@in.tum.de>
You have given the two conjuncts in the wrong order. Swap them and it works.
Tobias
Email Gateway (Aug 18 2022 at 18:40):From: John Wickerson <jpw48@cam.ac.uk>
Thanks Christian. With a little more fiddling, I have found the following to be roughly equivalent. One can either use the *.induct rule, like so (I previously had the conjuncts the wrong way round):
lemma soundness_part_one:
shows "(prov_dia A \<longrightarrow> (\<forall>G \<in> chains A. prov_chain G)) \<and> (prov_col a \<longrightarrow> (\<forall>G \<in> chains_col a. prov_chain G))"
proof(induct rule: prov_dia_prov_col.induct)
or the *.inducts rule, like so:
lemma soundness_part_one:
shows "(prov_dia A \<Longrightarrow> (\<forall>G \<in> chains A. prov_chain G))"
and "(prov_col a \<Longrightarrow> (\<forall>G \<in> chains_col a. prov_chain G))"
proof(induct rule: prov_dia_prov_col.inducts)
Thanks for your help!
john
Email Gateway (Aug 18 2022 at 18:40):From: Lars Noschinski <noschinl@in.tum.de>
$ISABELLE_HOME/src/HOL/Induct/Common_Patterns.thy, I guess.
-- Lars
Email Gateway (Aug 18 2022 at 18:41):From: Christian Urban <urbanc@in.tum.de>
Yes, exactly! Christian
Lars Noschinski writes:
On 08.11.2011 17:45, Christian Urban wrote:
There used to be an example theory in the Isabelle
distribution which explains all bells and whistles of the
induct-method, but I cannot find it at the moment. Maybe others
can point to it.$ISABELLE_HOME/src/HOL/Induct/Common_Patterns.thy, I guess.
-- Lars
Email Gateway (Aug 18 2022 at 18:41):From: Christian Urban <urbanc@in.tum.de>
Hi John,
Just one minor point. The second version with *.inducts
has the slight advantage to be already "rule format"
ready to be used by other automated tools. The one
with induct is still in "object format" and would need
some further processing to be usable with for example, simp
or auto. Generally the rule of thumb should be to state
lemmas in terms of \<And> and ==>, instead of \<and>
and -->. This allows for more automation by Isabelle
and for cleaner proofs in Isar.
Best wishes,
Christian
John Wickerson writes:
Thanks Christian. With a little more fiddling, I have found the following to be roughly equivalent. One can either use the *.induct rule, like so (I previously had the conjuncts the wrong way round):
lemma soundness_part_one:
shows "(prov_dia A \<longrightarrow> (\<forall>G \<in> chains A. prov_chain G)) \<and> (prov_col a \<longrightarrow> (\<forall>G \<in> chains_col a. prov_chain G))"
proof(induct rule: prov_dia_prov_col.induct)or the *.inducts rule, like so:
lemma soundness_part_one:
shows "(prov_dia A \<Longrightarrow> (\<forall>G \<in> chains A. prov_chain G))"
and "(prov_col a \<Longrightarrow> (\<forall>G \<in> chains_col a. prov_chain G))"
proof(induct rule: prov_dia_prov_col.inducts)Thanks for your help!
john
On 8 Nov 2011, at 16:45, Christian Urban wrote:
Hi John,
Mutual inductions can be a bit fiddly. Therefore inductive,
datatype and other tools provide an "*.inducts" rule. This
rule is essentially the projection of the "*.induct" rule.
(So no need to state the rule using conjunctions.) With this
the induct method can more easily figure out which induction
to perform. There used to be an example theory in the Isabelle
distribution which explains all bells and whistles of the
induct-method, but I cannot find it at the moment. Maybe others
can point to it. Below is a theory that should work in your example.Hope this helps,
Christian<Ribbons.thy>
John Wickerson writes:
Hello,
I have a whole bunch of mutually-inductively-defined datatypes, functions and predicates in my theory, and I'm having difficulty doing structural and rule induction over them.
At the end of this email is my (slightly condensed) theory file. Apologies for not creating a minimal example exhibiting my problem -- I thought it better to leave the theory file mostly as-is, to ensure that your solutions apply to my real script and not just to some minimal example.
The problem is the last line ...
proof(induct rule: prov_dia_prov_col.induct)
... which gives an error ("Proof command failed"), despite my goal being of the required form "?P ?a \<and> ?Q ?A". My question is: How can I give Isabelle hints to help it work out how to apply the given induction rule?
Many thanks,
John------------8<-------------
theory Ribbons imports Main
begin
typedecl bool_exp
consts Not :: "bool_exp \<Rightarrow> bool_exp"
consts rd_be :: "bool_exp \<Rightarrow> string set"typedecl assertion
consts Emp :: "assertion"
consts Pure :: "bool_exp \<Rightarrow> assertion"axiomatization
Star :: "assertion \<Rightarrow> assertion \<Rightarrow> assertion"
where star_comm: "Star p q = Star q p"
and star_assoc: "Star (Star p q) r = Star p (Star q r)"
and star_emp: "Star p Emp = p"
and emp_star: "Star Emp p = p"consts Exists :: "string \<Rightarrow> assertion \<Rightarrow> assertion"
axiomatization
rd_ass :: "assertion \<Rightarrow> string set"
where rd_emp: "rd_ass Emp = {}"
and rd_star: "rd_ass (Star p q) = rd_ass p \<union> rd_ass q"
and rd_exists: "rd_ass (Exists x p) = rd_ass p"typedecl atomic
consts rd_atm :: "atomic \<Rightarrow> string set"
consts wr_atm :: "atomic \<Rightarrow> string set"datatype command =
Atomic "atomic"
| If "bool_exp" "command list" "command list"
| While "bool_exp" "command list"fun
interleave_coms :: "(command list \<times> command list) \<Rightarrow> command list set"
where
"interleave_coms ([], C2) = {C2}"
| "interleave_coms (C1, []) = {C1}"
| "interleave_coms (c1#C1, c2#C2)
= {c1#C | C. C \<in> interleave_coms(C1, c2#C2)}
\<union> {c2#C | C. C \<in> interleave_coms(c1#C1, C2)}"inductive
prov_com :: "assertion \<times> command \<times> assertion \<Rightarrow> bool"
and
prov_comlist :: "assertion \<times> command list \<times> assertion \<Rightarrow> bool"
where
exists:
"prov_com (p, c, q)
\<Longrightarrow> prov_com (Exists x p, c, Exists x q)"
| ifcom:
"\<lbrakk>prov_comlist (Star (Pure b) p, C1, q);
prov_comlist (Star (Pure (Not b)) p, C2, q)\<rbrakk>
\<Longrightarrow> prov_com (p, If b C1 C2, q)"
| while:
"prov_comlist (Star (Pure b) p, C, p)
\<Longrightarrow> prov_com (p, While b C, Star (Pure (Not b)) p)"
| frame:
"\<lbrakk>prov_com (p, c, q); wr_com(c) \<inter> rd_ass(r) = {}\<rbrakk>
\<Longrightarrow> prov_com (Star p r, c, Star q r)"
| skip:
"prov_comlist(p, [], p)"
| seq:
"\<lbrakk>prov_com (p, c, q); prov_comlist (q, C, r)\<rbrakk>
\<Longrightarrow> prov_comlist (p, c#C, r)"datatype face =
Ribbon "assertion"
| Exists_int "string" "face list"type_synonym interface = "face list"
fun
ass_face :: "face \<Rightarrow> assertion"
and
ass :: "interface \<Rightarrow> assertion"
where
"ass_face (Ribbon p) = p"
| "ass_face (Exists_int x P) = Exists x (ass P)"
| "ass [] = Emp"
| "ass (f#P) = Star (ass_face f) (ass P)"datatype column =
Blank "interface"
| Basic "interface" "command" "interface"
| VComp_dia "column list" "column list"
| Exists_dia "string" "column list"
| If_dia "interface" "bool_exp" "column list" "column list" "interface"
| While_dia "interface" "bool_exp" "column list" "interface"type_synonym diagram = "column list"
fun
top :: "diagram \<Rightarrow> interface"
and
top_col :: "column \<Rightarrow> interface"
where
"top_col (Blank P) = P"
| "top_col (Basic P c Q) = P"
| "top_col (VComp_dia A B) = top A"
| "top_col (Exists_dia x A) = [Exists_int x (top A)]"
| "top_col (If_dia P b A B Q) = P"
| "top_col (While_dia P b A Q) = P"
| "top [] = []"
| "top (a # A) = (top_col a) @ (top A)"fun
bot :: "diagram \<Rightarrow> interface"
and
bot_col :: "column \<Rightarrow> interface"
where
"bot_col (Blank P) = P"
| "bot_col (Basic P c Q) = Q"
| "bot_col (VComp_dia A B) = bot B"
| "bot_col (Exists_dia x A) = [Exists_int x (bot A)]"
| "bot_col (If_dia P b A B Q) = Q"
| "bot_col (While_dia P b A Q) = Q"
| "bot [] = []"
| "bot (a # A) = (bot_col a) @ (bot A)"fun
coms :: "diagram \<Rightarrow> command list set"
and
coms_col :: "column \<Rightarrow> command list set"
where
"coms_col (Blank P) = {}"
| "coms_col (Basic P c Q) = {[c]}"
| "coms_col (VComp_dia A B)
= {C @ C' | C C'. C \<in> coms A \<and> C' \<in> coms B}"
| "coms_col (Exists_dia x A) = coms A"
| "coms_col (If_dia P b A B Q)
= { [If b C C'] | C C'. C \<in> coms A \<and> C' \<in> coms B}"
| "coms_col (While_dia P b A Q) = { [While b C] | C. C \<in> coms A}"
| "coms [] = {}"
| "coms (a # A)
= \<Union>{interleave_coms (C, C') | C C'. C \<in> coms_col a \<and> C' \<in> coms A}"consts
disj_col_dia :: "column \<Rightarrow> diagram \<Rightarrow> bool"inductive
prov_dia :: "diagram \<Rightarrow> bool"
and
prov_col :: "column \<Rightarrow> bool"
where
Blank:
"prov_col (Blank P)"
| Basic:
"prov_com (ass P, c, ass Q) \<Longrightarrow> prov_col (Basic P c Q)"
| Exists:
"prov_dia A \<Longrightarrow> prov_col (Exists_dia x A)"
| VComp:
"\<lbrakk>prov_dia A; prov_dia B; bot A = top B\<rbrakk> \<Longrightarrow> prov_col (VComp_dia A B)"
| If:
"\<lbrakk>prov_dia A; prov_dia B; top A = (Ribbon (Pure b)) # P;
top B = (Ribbon (Pure (Not b))) # P; bot A = Q; bot B = Q\<rbrakk>
\<Longrightarrow> prov_col (If_dia P b A B Q)"
| While:
"\<lbrakk>prov_dia A; top A = (Ribbon(Pure b)) # P;
bot A = P; Q = (Ribbon(Pure (Not b))) # P\<rbrakk>
\<Longrightarrow> prov_col (While_dia P b A Q)"
| Nil:
"prov_dia []"
| Cons:
"\<lbrakk>prov_col a; prov_dia A; disj_col_dia a A\<rbrakk>
\<Longrightarrow> prov_dia (a # A)"datatype chain =
cNil "assertion"
| cCons "assertion" "command" "chain"fun
seq_chains :: "chain \<times> chain \<Rightarrow> chain"
where
"seq_chains (cNil _, G') = G'"
| "seq_chains (cCons p c G, G') = cCons p c (seq_chains (G, G'))"fun
pre :: "chain \<Rightarrow> assertion"
where
"pre(cNil p) = p"
| "pre(cCons p c G) = p"fun
post :: "chain \<Rightarrow> assertion"
where
"post(cNil p) = p"
| "post(cCons p c G) = post G"fun
comlist :: "chain \<Rightarrow> command list"
where
"comlist(cNil p) = []"
| "comlist(cCons p c G) =
[message truncated]
Last updated: Nov 21 2024 at 12:39 UTC