Re: [isabelle] induction over mutually-inductively-defined predicate



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) = 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)
> -- 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.