[isabelle] induction over mutually-inductively-defined predicate



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.