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



You have given the two conjuncts in the wrong order. Swap them and it works.

Tobias

Am 08/11/2011 16:00, schrieb John Wickerson:
> 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.