diff --git a/src/HOL/Datatype_Examples/Cyclic_List.thy b/src/HOL/Datatype_Examples/Cyclic_List.thy --- a/src/HOL/Datatype_Examples/Cyclic_List.thy +++ b/src/HOL/Datatype_Examples/Cyclic_List.thy @@ -1,42 +1,42 @@ theory Cyclic_List imports "HOL-Library.Confluent_Quotient" begin inductive cyclic1 :: "'a list \ 'a list \ bool" for xs where "cyclic1 xs (rotate1 xs)" abbreviation cyclic :: "'a list \ 'a list \ bool" where "cyclic \ equivclp cyclic1" lemma cyclic_mapI: "cyclic xs ys \ cyclic (map f xs) (map f ys)" by(induction rule: equivclp_induct) (auto 4 4 elim!: cyclic1.cases simp add: rotate1_map[symmetric] intro: equivclp_into_equivclp cyclic1.intros) quotient_type 'a cyclic_list = "'a list" / cyclic by simp lemma map_respect_cyclic: includes lifting_syntax shows "((=) ===> cyclic ===> cyclic) map map" by(auto simp add: rel_fun_def cyclic_mapI) lemma confluentp_cyclic1: "confluentp cyclic1" by(intro strong_confluentp_imp_confluentp strong_confluentpI)(auto simp add: cyclic1.simps) lemma cyclic_set_eq: "cyclic xs ys \ set xs = set ys" by(induction rule: converse_equivclp_induct)(simp_all add: cyclic1.simps, safe, simp_all) lemma retract_cyclic1: assumes "cyclic1 (map f xs) ys" - shows "\zs. cyclic xs zs \ ys = map f zs" - using assms by(auto simp add: cyclic1.simps rotate1_map intro: cyclic1.intros symclpI1) + shows "\zs. cyclic xs zs \ ys = map f zs \ set zs \ set xs" + using assms by(force simp add: cyclic1.simps rotate1_map intro: cyclic1.intros symclpI1) lemma confluent_quotient_cyclic1: "confluent_quotient cyclic1 cyclic cyclic cyclic cyclic cyclic (map fst) (map snd) (map fst) (map snd) list_all2 list_all2 list_all2 set set" by(unfold_locales) (auto dest: retract_cyclic1 cyclic_set_eq simp add: list.in_rel list.rel_compp map_respect_cyclic[THEN rel_funD, OF refl] confluentp_cyclic1 intro: rtranclp_mono[THEN predicate2D, OF symclp_greater]) lift_bnf 'a cyclic_list subgoal by(rule confluent_quotient.subdistributivity[OF confluent_quotient_cyclic1]) subgoal by(force dest: cyclic_set_eq) done end diff --git a/src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy b/src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy --- a/src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy +++ b/src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy @@ -1,264 +1,264 @@ theory Free_Idempotent_Monoid imports "HOL-Library.Confluent_Quotient" begin inductive cancel1 :: "'a list \ 'a list \ bool" where cancel1: "xs \ [] \ cancel1 (gs @ xs @ xs @ gs') (gs @ xs @ gs')" abbreviation cancel where "cancel \ cancel1\<^sup>*\<^sup>*" lemma cancel1_append_same1: assumes "cancel1 xs ys" shows "cancel1 (zs @ xs) (zs @ ys)" using assms proof cases case (cancel1 ys gs gs') from \ys \ []\ have "cancel1 ((zs @ gs) @ ys @ ys @ gs') ((zs @ gs) @ ys @ gs')" .. with cancel1 show ?thesis by simp qed lemma cancel_append_same1: "cancel (zs @ xs) (zs @ ys)" if "cancel xs ys" using that by induction(blast intro: rtranclp.rtrancl_into_rtrancl cancel1_append_same1)+ lemma cancel1_append_same2: "cancel1 xs ys \ cancel1 (xs @ zs) (ys @ zs)" by(cases rule: cancel1.cases)(auto intro: cancel1.intros) lemma cancel_append_same2: "cancel (xs @ zs) (ys @ zs)" if "cancel xs ys" using that by induction(blast intro: rtranclp.rtrancl_into_rtrancl cancel1_append_same2)+ lemma cancel1_same: assumes "xs \ []" shows "cancel1 (xs @ xs) xs" proof - have "cancel1 ([] @ xs @ xs @ []) ([] @ xs @ [])" using assms .. thus ?thesis by simp qed lemma cancel_same: "cancel (xs @ xs) xs" by(cases "xs = []")(auto intro: cancel1_same) abbreviation (input) eq :: "'a list \ 'a list \ bool" where "eq \ equivclp cancel1" lemma eq_sym: "eq x y \ eq y x" by(rule equivclp_sym) lemma equivp_eq: "equivp eq" by simp lemma eq_append_same1: "eq xs' ys' \ eq (xs @ xs') (xs @ ys')" by(induction rule: equivclp_induct)(auto intro: cancel1_append_same1 equivclp_into_equivclp) lemma append_eq_cong: "\eq xs ys; eq xs' ys'\ \ eq (xs @ xs') (ys @ ys')" by(induction rule: equivclp_induct)(auto intro: eq_append_same1 equivclp_into_equivclp cancel1_append_same2) quotient_type 'a fim = "'a list" / eq by simp instantiation fim :: (type) monoid_add begin lift_definition zero_fim :: "'a fim" is "[]" . lift_definition plus_fim :: "'a fim \ 'a fim \ 'a fim" is "(@)" by(rule append_eq_cong) instance by(intro_classes; transfer; simp) end lemma plus_idem_fim [simp]: fixes x :: "'a fim" shows "x + x = x" proof transfer fix xs :: "'a list" show "eq (xs @ xs) xs" proof(cases "xs = []") case False thus ?thesis using cancel1_same[of xs] by(auto) qed simp qed inductive pcancel1 :: "'a list \ 'a list \ bool" where pcancel1: "pcancel1 (concat xss) (concat yss)" if "list_all2 (\xs ys. xs = ys \ xs = ys @ ys) xss yss" lemma cancel1_into_pcancel1: "pcancel1 xs ys" if "cancel1 xs ys" using that proof cases case (cancel1 xs gs gs') let ?xss = "[gs, xs @ xs, gs']" and ?yss = "[gs, xs, gs']" have "pcancel1 (concat ?xss) (concat ?yss)" by(rule pcancel1.intros) simp then show ?thesis using cancel1 by simp qed lemma pcancel_into_cancel: "cancel1\<^sup>*\<^sup>* xs ys" if "pcancel1 xs ys" using that proof cases case (pcancel1 xss yss) from pcancel1(3) show ?thesis unfolding pcancel1(1-2) apply induction apply simp apply(auto intro: cancel_append_same1) apply(rule rtranclp_trans) apply(subst append_assoc[symmetric]) apply(rule cancel_append_same2) apply(rule cancel_same) apply(auto intro: cancel_append_same1) done qed lemma pcancel1_cancel1_confluent: assumes "pcancel1 xs ys" and "cancel1 zs ys" shows "\us. cancel us xs \ pcancel1 us zs" proof - let ?P = "\xs ys. xs = ys \ xs = ys @ ys" consider ass as2 bs1 bss bs2 cs1 css ass' as2bs1 bss' bs2cs1 css' where "ys = concat ass @ as2 @ bs1 @ concat bss @ bs2 @ cs1 @ concat css" and "xs = concat ass' @ as2bs1 @ concat bss' @ bs2cs1 @ concat css'" and "zs = concat ass @ as2 @ bs1 @ concat bss @ bs2 @ bs1 @ concat bss @ bs2 @ cs1 @ concat css" and "list_all2 ?P ass' ass" and "list_all2 ?P bss' bss" and "list_all2 ?P css' css" and "?P as2bs1 (as2 @ bs1)" and "?P bs2cs1 (bs2 @ cs1)" | ass as2 bs cs1 css ass' css' where "ys = concat ass @ as2 @ bs @ cs1 @ concat css" and "xs = concat ass' @ as2 @ bs @ cs1 @ as2 @ bs @ cs1 @ concat css'" and "zs = concat ass @ as2 @ bs @ bs @ cs1 @ concat css" and "list_all2 ?P ass' ass" and "list_all2 ?P css' css" proof - from assms obtain xss bs as cs yss where xs: "xs = concat xss" and zs: "zs = as @ bs @ bs @ cs" and xss: "list_all2 (\xs ys. xs = ys \ xs = ys @ ys) xss yss" and ys: "ys = as @ bs @ cs" and yss: "concat yss = as @ bs @ cs" and bs: "bs \ []" by(clarsimp simp add: pcancel1.simps cancel1.simps) from yss bs obtain ass as2 BS bcss where yss: "yss = ass @ (as2 @ BS) # bcss" and as: "as = concat ass @ as2" and eq: "bs @ cs = BS @ concat bcss" by(auto simp add: concat_eq_append_conv split: if_split_asm) define bcss' where "bcss' = (if bcss = [] then [[]] else bcss)" have bcss': "bcss' \ []" by(simp add: bcss'_def) from eq consider us where "bs = BS @ us" "concat bcss = us @ cs" "bcss \ []" | "BS = bs @ cs" "bcss = []" | us where "BS = bs @ us" "cs = us @ concat bcss" by(cases "bcss = []")(auto simp add: append_eq_append_conv2) then show thesis proof cases case 1 from 1(2,3) obtain bss bs2 cs1 css where "bcss = bss @ (bs2 @ cs1) # css" and us: "us = concat bss @ bs2" and cs: "cs = cs1 @ concat css" by(auto simp add: concat_eq_append_conv) with 1 xs xss ys yss zs as that(1)[of ass as2 BS bss bs2 cs1 css] show ?thesis by(clarsimp simp add: list_all2_append2 list_all2_Cons2) next case 2 with xs xss ys yss zs as show ?thesis using that(1)[of ass as2 bs "[]" "[]" "[]" "[cs]" _ "as2 @ bs" "[]" "[]" "[cs]"] using that(2)[of ass as2 bs cs "[]"] by(auto simp add: list_all2_append2 list_all2_Cons2) next case 3 with xs xss ys yss zs as show ?thesis using that(1)[of ass as2 "[]" "[bs]" "[]" "us" "bcss" _ "as2" "[bs]"] that(2)[of ass as2 bs us bcss] by(auto simp add: list_all2_append2 list_all2_Cons2) qed qed then show ?thesis proof cases case 1 let ?us = "concat ass' @ as2bs1 @ concat bss' @ bs2 @ bs1 @ concat bss' @ bs2cs1 @ concat css'" have "?us = concat (ass' @ [as2bs1] @ bss' @ [bs2 @ bs1] @ bss' @ [bs2cs1] @ css')" by simp also have "pcancel1 \ (concat (ass @ [as2 @ bs1] @ bss @ [bs2 @ bs1] @ bss @ [bs2 @ cs1] @ css))" by(rule pcancel1.intros)(use 1 in \simp add: list_all2_appendI\) also have "\ = zs" using 1 by simp also have "cancel ?us xs" proof - define as2b where "as2b = (if as2bs1 = as2 @ bs1 then as2 else as2 @ bs1 @ as2)" have as2bs1: "as2bs1 = as2b @ bs1" using 1 by(auto simp add: as2b_def) define b2cs where "b2cs = (if bs2cs1 = bs2 @ cs1 then cs1 else cs1 @ bs2 @ cs1)" have bs2cs1: "bs2cs1 = bs2 @ b2cs" using 1 by(auto simp add: b2cs_def) have "?us = (concat ass' @ as2b) @ ((bs1 @ concat bss' @ bs2) @ (bs1 @ concat bss' @ bs2)) @ b2cs @ concat css'" by(simp add: as2bs1 bs2cs1) also have "cancel \ ((concat ass' @ as2b) @ (bs1 @ concat bss' @ bs2) @ b2cs @ concat css')" by(rule cancel_append_same1 cancel_append_same2 cancel_same)+ also have "\ = xs" using 1 bs2cs1 as2bs1 by simp finally show ?thesis . qed ultimately show ?thesis by blast next case 2 let ?us = "concat ass' @ as2 @ bs @ bs @ cs1 @ as2 @ bs @ bs @ cs1 @ concat css'" have "?us = concat (ass' @ [as2 @ bs @ bs @ cs1 @ as2 @ bs @ bs @ cs1] @ css')" by simp also have "pcancel1 \ (concat (ass @ [as2 @ bs @ bs @ cs1] @ css))" by(intro pcancel1.intros list_all2_appendI)(simp_all add: 2) also have "\ = zs" using 2 by simp also have "cancel ?us xs" proof - have "?us = (concat ass' @ as2) @ (bs @ bs) @ cs1 @ as2 @ bs @ bs @ cs1 @ concat css'" by simp also have "cancel \ ((concat ass' @ as2) @ bs @ cs1 @ as2 @ bs @ bs @ cs1 @ concat css')" by(rule cancel_append_same1 cancel_append_same2 cancel_same)+ also have "\ = (concat ass' @ as2 @ bs @ cs1 @ as2) @ (bs @ bs) @ cs1 @ concat css'" by simp also have "cancel \ ((concat ass' @ as2 @ bs @ cs1 @ as2) @ bs @ cs1 @ concat css')" by(rule cancel_append_same1 cancel_append_same2 cancel_same)+ also have "\ = xs" using 2 by simp finally show ?thesis . qed ultimately show ?thesis by blast qed qed lemma pcancel1_cancel_confluent: assumes "pcancel1 xs ys" and "cancel zs ys" shows "\us. cancel us xs \ pcancel1 us zs" using assms(2,1) by(induction arbitrary: xs)(fastforce elim!: rtranclp_trans dest: pcancel1_cancel1_confluent)+ lemma cancel1_semiconfluent: assumes "cancel1 xs ys" and "cancel zs ys" shows "\us. cancel us xs \ cancel us zs" using pcancel1_cancel_confluent[OF cancel1_into_pcancel1, OF assms] by(blast intro: pcancel_into_cancel) lemma semiconfluentp_cancel1: "semiconfluentp cancel1\\" by(auto simp add: semiconfluentp_def rtranclp_conversep dest: cancel1_semiconfluent) lemma retract_cancel1_aux: assumes "cancel1 ys (map f xs)" - shows "\zs. cancel1 zs xs \ ys = map f zs" + shows "\zs. cancel1 zs xs \ ys = map f zs \ set zs \ set xs" using assms by cases(fastforce simp add: map_eq_append_conv append_eq_map_conv intro: cancel1.intros) lemma retract_cancel1: assumes "cancel1 ys (map f xs)" - shows "\zs. eq xs zs \ ys = map f zs" + shows "\zs. eq xs zs \ ys = map f zs \ set zs \ set xs" using retract_cancel1_aux[OF assms] by(blast intro: symclpI) lemma cancel1_set_eq: assumes "cancel1 ys xs" shows "set ys = set xs" using assms by cases auto lemma eq_set_eq: "set xs = set ys" if "eq xs ys" using that by(induction)(auto dest!: cancel1_set_eq elim!: symclpE) context includes lifting_syntax begin lemma map_respect_cancel1: "((=) ===> cancel1 ===> eq) map map" by(auto 4 4 simp add: rel_fun_def cancel1.simps intro: symclpI cancel1.intros) lemma map_respect_eq: "((=) ===> eq ===> eq) map map" apply(intro rel_funI; hypsubst) subgoal for _ f x y by(induction rule: equivclp_induct) (auto dest: map_respect_cancel1[THEN rel_funD, THEN rel_funD, OF refl] intro: eq_sym equivclp_trans) done end lemma confluent_quotient_fim: "confluent_quotient cancel1\\ eq eq eq eq eq (map fst) (map snd) (map fst) (map snd) list_all2 list_all2 list_all2 set set" by(unfold_locales)(auto dest: retract_cancel1 eq_set_eq simp add: list.in_rel list.rel_compp map_respect_eq[THEN rel_funD, OF refl] semiconfluentp_imp_confluentp semiconfluentp_cancel1)+ lift_bnf 'a fim subgoal for A B by(rule confluent_quotient.subdistributivity[OF confluent_quotient_fim]) subgoal by(force dest: eq_set_eq) done end diff --git a/src/HOL/Datatype_Examples/LDL.thy b/src/HOL/Datatype_Examples/Regex_ACI.thy rename from src/HOL/Datatype_Examples/LDL.thy rename to src/HOL/Datatype_Examples/Regex_ACI.thy --- a/src/HOL/Datatype_Examples/LDL.thy +++ b/src/HOL/Datatype_Examples/Regex_ACI.thy @@ -1,339 +1,342 @@ -theory LDL imports - "HOL-Library.Confluent_Quotient" +theory Regex_ACI + imports "HOL-Library.Confluent_Quotient" begin -datatype 'a rexp = Atom 'a | Alt "'a rexp" "'a rexp" | Conc "'a rexp" "'a rexp" | Star "'a rexp" +datatype 'a rexp = Zero | Eps | Atom 'a | Alt "'a rexp" "'a rexp" | Conc "'a rexp" "'a rexp" | Star "'a rexp" inductive ACI (infix "~" 64) where a1: "Alt (Alt r s) t ~ Alt r (Alt s t)" | a2: "Alt r (Alt s t) ~ Alt (Alt r s) t" | c: "Alt r s ~ Alt s r" | i: "r ~ Alt r r" | R: "r ~ r" | A: "r ~ r' \ s ~ s' \ Alt r s ~ Alt r' s'" | C: "r ~ r' \ s ~ s' \ Conc r s ~ Conc r' s'" | S: "r ~ r' \ Star r ~ Star r'" declare ACI.intros[intro] abbreviation ACIcl (infix "~~" 64) where "(~~) \ equivclp (~)" lemma eq_set_preserves_inter: fixes eq set assumes "\r s. eq r s \ set r = set s" and "Ss \ {}" shows "(\As\Ss. {(x, x'). eq x x'} `` {x. set x \ As}) \ {(x, x'). eq x x'} `` {x. set x \ \ Ss}" using assms by (auto simp: subset_eq) metis lemma ACI_map_respects: fixes f :: "'a \ 'b" and r s :: "'a rexp" assumes "r ~ s" shows "map_rexp f r ~ map_rexp f s" using assms by (induct r s rule: ACI.induct) auto lemma ACIcl_map_respects: fixes f :: "'a \ 'b" and r s :: "'a rexp" assumes "r ~~ s" shows "map_rexp f r ~~ map_rexp f s" using assms by (induct rule: equivclp_induct) (auto intro: ACI_map_respects equivclp_trans) lemma ACI_set_eq: fixes r s :: "'a rexp" assumes "r ~ s" shows "set_rexp r = set_rexp s" using assms by (induct r s rule: ACI.induct) auto lemma ACIcl_set_eq: fixes r s :: "'a rexp" assumes "r ~~ s" shows "set_rexp r = set_rexp s" using assms by (induct rule: equivclp_induct) (auto dest: ACI_set_eq) lemma Alt_eq_map_rexp_iff: "Alt r s = map_rexp f x \ (\r' s'. x = Alt r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" "map_rexp f x = Alt r s \ (\r' s'. x = Alt r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" by (cases x; auto)+ lemma Conc_eq_map_rexp_iff: "Conc r s = map_rexp f x \ (\r' s'. x = Conc r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" "map_rexp f x = Conc r s \ (\r' s'. x = Conc r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" by (cases x; auto)+ lemma Star_eq_map_rexp_iff: "Star r = map_rexp f x \ (\r'. x = Star r' \ map_rexp f r' = r)" "map_rexp f x = Star r \ (\r'. x = Star r' \ map_rexp f r' = r)" by (cases x; auto)+ lemma AA: "r ~~ r' \ s ~~ s' \ Alt r s ~~ Alt r' s'" proof (induct rule: equivclp_induct) case base then show ?case by (induct rule: equivclp_induct) (auto elim!: equivclp_trans) next case (step s t) then show ?case by (auto elim!: equivclp_trans) qed lemma AAA: "(~)\<^sup>*\<^sup>* r r' \ (~)\<^sup>*\<^sup>* s s' \ (~)\<^sup>*\<^sup>* (Alt r s) (Alt r' s')" proof (induct r r' rule: rtranclp.induct) case (rtrancl_refl r) then show ?case by (induct s s' rule: rtranclp.induct) (auto elim!: rtranclp.rtrancl_into_rtrancl) next case (rtrancl_into_rtrancl a b c) then show ?case by (auto elim!: rtranclp.rtrancl_into_rtrancl) qed lemma CC: "r ~~ r' \ s ~~ s' \ Conc r s ~~ Conc r' s'" proof (induct rule: equivclp_induct) case base then show ?case by (induct rule: equivclp_induct) (auto elim!: equivclp_trans) next case (step s t) then show ?case by (auto elim!: equivclp_trans) qed lemma CCC: "(~)\<^sup>*\<^sup>* r r' \ (~)\<^sup>*\<^sup>* s s' \ (~)\<^sup>*\<^sup>* (Conc r s) (Conc r' s')" proof (induct r r' rule: rtranclp.induct) case (rtrancl_refl r) then show ?case by (induct s s' rule: rtranclp.induct) (auto elim!: rtranclp.rtrancl_into_rtrancl) next case (rtrancl_into_rtrancl a b c) then show ?case by (auto elim!: rtranclp.rtrancl_into_rtrancl) qed lemma SS: "r ~~ r' \ Star r ~~ Star r'" proof (induct rule: equivclp_induct) case (step s t) then show ?case by (auto elim!: equivclp_trans) qed auto lemma SSS: "(~)\<^sup>*\<^sup>* r r' \ (~)\<^sup>*\<^sup>* (Star r) (Star r')" proof (induct r r' rule: rtranclp.induct) case (rtrancl_into_rtrancl a b c) then show ?case by (auto elim!: rtranclp.rtrancl_into_rtrancl) qed auto -lemma map_rexp_ACI_inv: "map_rexp f x ~ y \ \z. x ~~ z \ y = map_rexp f z" +lemma map_rexp_ACI_inv: "map_rexp f x ~ y \ \z. x ~~ z \ y = map_rexp f z \ set_rexp z \ set_rexp x" proof (induct "map_rexp f x" y arbitrary: x rule: ACI.induct) case (a1 r s t) then obtain r' s' t' where "x = Alt (Alt r' s') t'" "map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t" by (auto simp: Alt_eq_map_rexp_iff) then show ?case by (intro exI[of _ "Alt r' (Alt s' t')"]) auto next case (a2 r s t) then obtain r' s' t' where "x = Alt r' (Alt s' t')" "map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t" by (auto simp: Alt_eq_map_rexp_iff) then show ?case by (intro exI[of _ "Alt (Alt r' s') t'"]) auto next case (c r s) then obtain r' s' where "x = Alt r' s'" "map_rexp f r' = r" "map_rexp f s' = s" by (auto simp: Alt_eq_map_rexp_iff) then show ?case by (intro exI[of _ "Alt s' r'"]) auto next case (i r) then show ?case by (intro exI[of _ "Alt r r"]) auto next case (R r) then show ?case by (auto intro: exI[of _ r]) next case (A r rr s ss) then obtain r' s' where "x = Alt r' s'" "map_rexp f r' = r" "map_rexp f s' = s" by (auto simp: Alt_eq_map_rexp_iff) moreover from A(2)[OF this(2)[symmetric]] A(4)[OF this(3)[symmetric]] obtain rr' ss' where "r' ~~ rr'" "rr = map_rexp f rr'" "s' ~~ ss'" "ss = map_rexp f ss'" + "set_rexp rr' \ set_rexp r'" "set_rexp ss' \ set_rexp s'" by blast ultimately show ?case using A(1,3) by (intro exI[of _ "Alt rr' ss'"]) (auto intro!: AA) next case (C r rr s ss) then obtain r' s' where "x = Conc r' s'" "map_rexp f r' = r" "map_rexp f s' = s" by (auto simp: Conc_eq_map_rexp_iff) moreover from C(2)[OF this(2)[symmetric]] C(4)[OF this(3)[symmetric]] obtain rr' ss' where "r' ~~ rr'" "rr = map_rexp f rr'" "s' ~~ ss'" "ss = map_rexp f ss'" + "set_rexp rr' \ set_rexp r'" "set_rexp ss' \ set_rexp s'" by blast ultimately show ?case using C(1,3) by (intro exI[of _ "Conc rr' ss'"]) (auto intro!: CC) next case (S r rr) then obtain r' where "x = Star r'" "map_rexp f r' = r" by (auto simp: Star_eq_map_rexp_iff) moreover from S(2)[OF this(2)[symmetric]] obtain rr' where "r' ~~ rr'" "rr = map_rexp f rr'" + "set_rexp rr' \ set_rexp r'" by blast ultimately show ?case by (intro exI[of _ "Star rr'"]) (auto intro!: SS) qed lemma reflclp_ACI: "(~)\<^sup>=\<^sup>= = (~)" unfolding fun_eq_iff by auto lemma strong_confluentp_ACI: "strong_confluentp (~)" apply (rule strong_confluentpI, unfold reflclp_ACI) subgoal for x y z proof (induct x y arbitrary: z rule: ACI.induct) case (a1 r s t) then show ?case by (auto intro: AAA converse_rtranclp_into_rtranclp) next case (a2 r s t) then show ?case by (auto intro: AAA converse_rtranclp_into_rtranclp) next case (c r s) then show ?case by (cases rule: ACI.cases) (auto intro: AAA) next case (i r) then show ?case by (auto intro: AAA) next case (R r) then show ?case by auto next note A1 = ACI.A[OF _ R] note A2 = ACI.A[OF R] case (A r r' s s') from A(5,1-4) show ?case proof (cases rule: ACI.cases) case inner: (a1 r'' s'') from A(1,3) show ?thesis unfolding inner proof (elim ACI.cases[of _ r'], goal_cases Xa1 Xa2 XC XI XR XP XT XS) case (Xa1 rr ss tt) with A(3) show ?case by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A2[OF A2]], rotated]) (metis a1 a2 A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) next case (Xa2 r s t) then show ?case by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A2[OF A2]], rotated]) (metis a1 A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) next case (XC r s) then show ?case by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A2[OF A2]], rotated]) (metis a1 c A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) next case (XI r) then show ?case apply (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ ACI.A[OF i ACI.A[OF i]]], rotated]) apply hypsubst apply (rule converse_rtranclp_into_rtranclp, rule a1) apply (rule converse_rtranclp_into_rtranclp, rule a1) apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c) apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) apply (rule converse_rtranclp_into_rtranclp, rule a2) apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) apply blast done qed auto next case inner: (a2 s'' t'') with A(1,3) show ?thesis unfolding inner proof (elim ACI.cases[of _ s'], goal_cases Xa1 Xa2 XC XI XR XP XT XS) case (Xa1 rr ss tt) with A(3) show ?case by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A1[OF A1]], rotated]) (metis a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) next case (Xa2 r s t) then show ?case by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A1[OF A1]], rotated]) (metis a1 a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) next case (XC r s) then show ?case by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A1[OF A1]], rotated]) (metis a2 c A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) next case (XI r) then show ?case apply (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ ACI.A[OF ACI.A[OF _ i] i]], rotated]) apply hypsubst apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c) apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A2, rule a1) apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) apply (rule converse_rtranclp_into_rtranclp, rule a2) apply blast done qed auto qed (auto 5 0 intro: AAA) next case (C r r' s s') from C(5,1-4) show ?case by (cases rule: ACI.cases) (auto 5 0 intro: CCC) next case (S r r') from S(3,1,2) show ?case by (cases rule: ACI.cases) (auto intro: SSS) qed done lemma confluent_quotient_ACI: "confluent_quotient (~) (~~) (~~) (~~) (~~) (~~) (map_rexp fst) (map_rexp snd) (map_rexp fst) (map_rexp snd) rel_rexp rel_rexp rel_rexp set_rexp set_rexp" - by unfold_locales (auto dest: ACIcl_set_eq simp: rexp.in_rel rexp.rel_compp map_rexp_ACI_inv - intro: equivpI reflpI sympI transpI ACIcl_map_respects + by unfold_locales (auto dest: ACIcl_set_eq ACIcl_map_respects simp: rexp.in_rel rexp.rel_compp map_rexp_ACI_inv + intro: equivpI reflpI sympI transpI strong_confluentp_imp_confluentp[OF strong_confluentp_ACI]) inductive ACIEQ (infix "\" 64) where a: "Alt (Alt r s) t \ Alt r (Alt s t)" | c: "Alt r s \ Alt s r" | i: "Alt r r \ r" | A: "r \ r' \ s \ s' \ Alt r s \ Alt r' s'" | C: "r \ r' \ s \ s' \ Conc r s \ Conc r' s'" | S: "r \ r' \ Star r \ Star r'" | r: "r \ r" | s: "r \ s \ s \ r" | t: "r \ s \ s \ t \ r \ t" lemma ACIEQ_le_ACIcl: "r \ s \ r ~~ s" by (induct r s rule: ACIEQ.induct) (auto intro: AA CC SS equivclp_sym equivclp_trans) lemma ACI_le_ACIEQ: "r ~ s \ r \ s" by (induct r s rule: ACI.induct) (auto intro: ACIEQ.intros) lemma ACIcl_le_ACIEQ: "r ~~ s \ r \ s" by (induct rule: equivclp_induct) (auto 0 3 intro: ACIEQ.intros ACI_le_ACIEQ) lemma ACIEQ_alt: "(\) = (~~)" by (simp add: ACIEQ_le_ACIcl ACIcl_le_ACIEQ antisym predicate2I) quotient_type 'a ACI_rexp = "'a rexp" / "(\)" unfolding ACIEQ_alt by (auto intro!: equivpI reflpI sympI transpI) lift_bnf 'a ACI_rexp unfolding ACIEQ_alt subgoal for A Q by (rule confluent_quotient.subdistributivity[OF confluent_quotient_ACI]) subgoal for Ss by (intro eq_set_preserves_inter[rotated] ACIcl_set_eq; auto) done datatype ldl = Prop string | And ldl ldl | Not ldl | Match "ldl ACI_rexp" end \ No newline at end of file diff --git a/src/HOL/Datatype_Examples/Regex_ACIDZ.thy b/src/HOL/Datatype_Examples/Regex_ACIDZ.thy new file mode 100644 --- /dev/null +++ b/src/HOL/Datatype_Examples/Regex_ACIDZ.thy @@ -0,0 +1,481 @@ +theory Regex_ACIDZ + imports "HOL-Library.Confluent_Quotient" +begin + +datatype (discs_sels) 'a rexp = Zero | Eps | Atom 'a + | Alt "'a rexp" "'a rexp" | Conc "'a rexp" "'a rexp" | Star "'a rexp" + +fun elim_zeros where + "elim_zeros (Alt r s) = + (let r' = elim_zeros r; s' = elim_zeros s in + if r' = Zero then s' else if s' = Zero then r' else Alt r' s')" +| "elim_zeros (Conc r s) = (let r' = elim_zeros r in if r' = Zero then Zero else Conc r' s)" +| "elim_zeros r = r" + +fun distribute where + "distribute t (Alt r s) = Alt (distribute t r) (distribute t s)" +| "distribute t (Conc r s) = Conc (distribute s r) t" +| "distribute t r = Conc r t" + +inductive ACIDZ (infix "~" 64) where + a1: "Alt (Alt r s) t ~ Alt r (Alt s t)" +| a2: "Alt r (Alt s t) ~ Alt (Alt r s) t" +| c: "Alt r s ~ Alt s r" +| i: "r ~ Alt r r" +| z: "r ~ s \ r ~ elim_zeros s" +| d: "Conc r t ~ distribute t r" +| R: "r ~ r" +| A: "r ~ r' \ s ~ s' \ Alt r s ~ Alt r' s'" +| C: "r ~ r' \ Conc r s ~ Conc r' s" + +inductive_cases ACIDZ_AltE[elim]: "Alt r s ~ t" +inductive_cases ACIDZ_ConcE[elim]: "Conc r s ~ t" +inductive_cases ACIDZ_StarE[elim]: "Star r ~ t" + +declare ACIDZ.intros[intro] + +abbreviation ACIDZcl (infix "~~" 64) where "(~~) \ equivclp (~)" + +lemma map_rexp_distribute[simp]: "map_rexp f (distribute t r) = distribute (map_rexp f t) (map_rexp f r)" + by (induct r arbitrary: t) auto + +lemma set_rexp_distribute[simp]: "set_rexp (distribute t r) = set_rexp r \ set_rexp t" + by (induct r arbitrary: t) auto + +lemma Zero_eq_map_rexp_iff[simp]: + "Zero = map_rexp f x \ x = Zero" + "map_rexp f x = Zero \ x = Zero" + by (cases x; auto)+ + +lemma Alt_eq_map_rexp_iff: + "Alt r s = map_rexp f x \ (\r' s'. x = Alt r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" + "map_rexp f x = Alt r s \ (\r' s'. x = Alt r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" + by (cases x; auto)+ + +lemma map_rexp_elim_zeros[simp]: "map_rexp f (elim_zeros r) = elim_zeros (map_rexp f r)" + by (induct r rule: elim_zeros.induct) (auto simp: Let_def) + +lemma set_rexp_elim_zeros: "set_rexp (elim_zeros r) \ set_rexp r" + by (induct r rule: elim_zeros.induct) (auto simp: Let_def) + +lemma ACIDZ_map_respects: + fixes f :: "'a \ 'b" and r s :: "'a rexp" + assumes "r ~ s" + shows "map_rexp f r ~ map_rexp f s" + using assms by (induct r s rule: ACIDZ.induct) (auto simp: Let_def) + +lemma ACIDZcl_map_respects: + fixes f :: "'a \ 'b" and r s :: "'a rexp" + assumes "r ~~ s" + shows "map_rexp f r ~~ map_rexp f s" + using assms by (induct rule: equivclp_induct) (auto intro: ACIDZ_map_respects equivclp_trans) + +lemma finite_set_rexp: "finite (set_rexp r)" + by (induct r) auto + +lemma ACIDZ_set_rexp: "r ~ s \ set_rexp s \ set_rexp r" + by (induct r s rule: ACIDZ.induct) (auto dest: set_mp[OF set_rexp_elim_zeros] simp: Let_def) + +lemma ACIDZ_set_rexp': "(~)\<^sup>*\<^sup>* r s \ set_rexp s \ set_rexp r" + by (induct rule: rtranclp.induct) (auto dest: ACIDZ_set_rexp) + + +lemma Conc_eq_map_rexp_iff: + "Conc r s = map_rexp f x \ (\r' s'. x = Conc r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" + "map_rexp f x = Conc r s \ (\r' s'. x = Conc r' s' \ map_rexp f r' = r \ map_rexp f s' = s)" + by (cases x; auto)+ + +lemma Star_eq_map_rexp_iff: + "Star r = map_rexp f x \ (\r'. x = Star r' \ map_rexp f r' = r)" + "map_rexp f x = Star r \ (\r'. x = Star r' \ map_rexp f r' = r)" + by (cases x; auto)+ + +lemma AAA: "(~)\<^sup>*\<^sup>* r r' \ (~)\<^sup>*\<^sup>* s s' \ (~)\<^sup>*\<^sup>* (Alt r s) (Alt r' s')" +proof (induct r r' rule: rtranclp.induct) + case (rtrancl_refl r) + then show ?case + by (induct s s' rule: rtranclp.induct) + (auto elim!: rtranclp.rtrancl_into_rtrancl) +next + case (rtrancl_into_rtrancl a b c) + then show ?case + by (auto elim!: rtranclp.rtrancl_into_rtrancl) +qed + +lemma CCC: "(~)\<^sup>*\<^sup>* r r' \ (~)\<^sup>*\<^sup>* (Conc r s) (Conc r' s)" +proof (induct r r' rule: rtranclp.induct) + case (rtrancl_refl r) + then show ?case + by simp +next + case (rtrancl_into_rtrancl a b c) + then show ?case + by (auto elim!: rtranclp.rtrancl_into_rtrancl) +qed + +lemma map_rexp_ACIDZ_inv: "map_rexp f x ~ y \ \z. (~)\<^sup>*\<^sup>* x z \ y = map_rexp f z" +proof (induct "map_rexp f x" y arbitrary: x rule: ACIDZ.induct) + case (a1 r s t) + then obtain r' s' t' where "x = Alt (Alt r' s') t'" + "map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t" + by (auto simp: Alt_eq_map_rexp_iff) + then show ?case + by (intro exI[of _ "Alt r' (Alt s' t')"]) auto +next + case (a2 r s t) + then obtain r' s' t' where "x = Alt r' (Alt s' t')" + "map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t" + by (auto simp: Alt_eq_map_rexp_iff) + then show ?case + by (intro exI[of _ "Alt (Alt r' s') t'"]) auto +next + case (c r s) + then obtain r' s' where "x = Alt r' s'" + "map_rexp f r' = r" "map_rexp f s' = s" + by (auto simp: Alt_eq_map_rexp_iff) + then show ?case + by (intro exI[of _ "Alt s' r'"]) auto +next + case (i r) + then show ?case + by (intro exI[of _ "Alt r r"]) auto +next + case (z r) + then show ?case + by (metis ACIDZ.z R map_rexp_elim_zeros rtranclp.simps) +next + case (d r s) + then obtain r' s' where "x = Conc r' s'" + "map_rexp f r' = r" "map_rexp f s' = s" + by (auto simp: Conc_eq_map_rexp_iff) + then show ?case + by (intro exI[of _ "distribute s' r'"]) auto +next + case (R r) + then show ?case by (auto intro: exI[of _ r]) +next + case (A r rr s ss) + then obtain r' s' where "x = Alt r' s'" + "map_rexp f r' = r" "map_rexp f s' = s" + by (auto simp: Alt_eq_map_rexp_iff) + moreover from A(2)[OF this(2)[symmetric]] A(4)[OF this(3)[symmetric]] obtain rr' ss' where + "(~)\<^sup>*\<^sup>* r' rr'" "rr = map_rexp f rr'" "(~)\<^sup>*\<^sup>* s' ss'" "ss = map_rexp f ss'" + by blast + ultimately show ?case using A(1,3) + by (intro exI[of _ "Alt rr' ss'"]) (auto intro!: AAA) +next + case (C r rr s) + then obtain r' s' where "x = Conc r' s'" + "map_rexp f r' = r" "map_rexp f s' = s" + by (auto simp: Conc_eq_map_rexp_iff) + moreover from C(2)[OF this(2)[symmetric]] obtain rr' where + "(~)\<^sup>*\<^sup>* r' rr'" "rr = map_rexp f rr'" + by blast + ultimately show ?case using C(1,3) + by (intro exI[of _ "Conc rr' s'"]) (auto intro!: CCC) +qed + +lemma reflclp_ACIDZ: "(~)\<^sup>=\<^sup>= = (~)" + unfolding fun_eq_iff + by auto + +lemma elim_zeros_distribute_Zero: "elim_zeros r = Zero \ elim_zeros (distribute t r) = Zero" + by (induct r arbitrary: t) (auto simp: Let_def split: if_splits) + +lemma elim_zeros_ACIDZ_Zero: "r ~ s \ elim_zeros r = Zero \ elim_zeros s = Zero" + by (induct r s rule: ACIDZ.induct) (auto simp: Let_def elim_zeros_distribute_Zero split: if_splits) + +lemma AZZ[simp]: "Alt Zero Zero ~ Zero" + by (metis elim_zeros.simps(3) elim_zeros_ACIDZ_Zero i z) + +lemma elim_zeros_idem[simp]: "elim_zeros (elim_zeros r) = elim_zeros r" + by (induct r rule: elim_zeros.induct) (auto simp: Let_def) + +lemma elim_zeros_distribute_idem: "elim_zeros (distribute s (elim_zeros r)) = elim_zeros (distribute s r)" + by (induct r arbitrary: s rule: elim_zeros.induct) (auto simp: Let_def) + +lemma zz: "r ~ s \ t = elim_zeros s \ r ~ t" + by (metis z) + +lemma elim_zeros_ACIDZ1: "r ~ s \ elim_zeros r ~ elim_zeros s" +proof (induct r s rule: ACIDZ.induct) + case (c r s) + then show ?case by (auto simp: Let_def) +next + case (d r t) + then show ?case + by (smt (z3) ACIDZ.d R distribute.simps(3) elim_zeros.simps(2) elim_zeros.simps(3) elim_zeros_distribute_idem z) +next + case (A r r' s s') + then show ?case + by (auto 0 2 simp: Let_def dest: elim_zeros_ACIDZ_Zero elim: zz[OF ACIDZ.A]) +next + case (C r r' s) + then show ?case + by (smt (z3) ACIDZ.C elim_zeros.simps(2,3) z elim_zeros_ACIDZ_Zero) +qed (auto simp: Let_def) + +lemma AA': "r ~ r' \ s ~ s' \ t = elim_zeros (Alt r' s') \ Alt r s ~ t" + by (auto simp del: elim_zeros.simps) + +lemma distribute_ACIDZ1: "r ~ r' \ distribute s r ~ elim_zeros (distribute s r')" +proof (induct r r' arbitrary: s rule: ACIDZ.induct) + case (A r r' s s' u) + from A(2,4)[of u] show ?case + by (auto simp: Let_def elim: zz[OF ACIDZ.A]) +next + case (C r r' s) + then show ?case + by (smt (verit, best) ACIDZ.C distribute.simps(2,3) elim_zeros.simps(2,3) z) +qed (auto simp del: elim_zeros.simps simp: elim_zeros_distribute_idem) + +lemma elim_zeros_ACIDZ: "r ~ s \ (~)\<^sup>*\<^sup>* (elim_zeros r) (elim_zeros s)" + using elim_zeros_ACIDZ1 by blast + +lemma elim_zeros_ACIDZ_rtranclp: "(~)\<^sup>*\<^sup>* r s \ (~)\<^sup>*\<^sup>* (elim_zeros r) (elim_zeros s)" + by (induct rule: rtranclp_induct) (auto elim!: rtranclp_trans elim_zeros_ACIDZ) + +lemma distribute_ACIDZ: "(~) r r' \ (~)\<^sup>*\<^sup>* (distribute s r) (elim_zeros (distribute s r'))" + by (metis distribute_ACIDZ1 rtranclp.simps) + +lemma ACIDZ_elim_zeros: "(~) r s \ elim_zeros r = Zero \ elim_zeros s = Zero" + by (meson elim_zeros_ACIDZ1 elim_zeros_ACIDZ_Zero) + +lemma ACIDZ_elim_zeros_rtranclp: + "(~)\<^sup>*\<^sup>* r s \ elim_zeros r = Zero \ elim_zeros s = Zero" + by (induct rule: rtranclp_induct) (auto elim: ACIDZ_elim_zeros) + +lemma Alt_elim_zeros[simp]: + "Alt (elim_zeros r) s ~ elim_zeros (Alt r s)" + "Alt r (elim_zeros s) ~ elim_zeros (Alt r s)" + by (smt (verit, ccfv_threshold) ACIDZ.simps elim_zeros.simps(1) elim_zeros_idem)+ + +lemma strong_confluentp_ACIDZ: "strong_confluentp (~)" +proof (rule strong_confluentpI, unfold reflclp_ACIDZ) + fix x y z :: "'a rexp" + assume "x ~ y" "x ~ z" + then show "\u. (~)\<^sup>*\<^sup>* y u \ z ~ u" + proof (induct x y arbitrary: z rule: ACIDZ.induct) + case (a1 r s t) + then show ?case + by (auto intro: AAA converse_rtranclp_into_rtranclp) + next + case (a2 r s t) + then show ?case + by (auto intro: AAA converse_rtranclp_into_rtranclp) + next + case (c r s) + then show ?case + by (cases rule: ACIDZ.cases) + (auto 0 4 intro: exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ R], rotated] + converse_rtranclp_into_rtranclp[where r="(~)", OF ACIDZ.c]) + next + case (i r) + then show ?case + by (auto intro: AAA) + next + case (z r s) + then show ?case + by (meson ACIDZ.z elim_zeros_ACIDZ_rtranclp) + next + case (d r s t) + then show ?case + by (induct "Conc r s" t rule: ACIDZ.induct) + (force intro: exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ z], rotated] + exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ z[OF elim_zeros_ACIDZ1]], rotated] + distribute_ACIDZ1 elim!: rtranclp_trans)+ + next + case (R r) + then show ?case + by auto + next + note A1 = ACIDZ.A[OF _ R] + note A2 = ACIDZ.A[OF R] + case (A r r' s s') + from A(5,1-4) show ?case + proof (induct "Alt r s" z rule: ACIDZ.induct) + case inner: (a1 r'' s'') + from A(1,3) show ?case + unfolding inner.hyps[symmetric] + proof (induct "Alt r'' s''" r' rule: ACIDZ.induct[consumes 1, case_names Xa1 Xa2 Xc Xi Xz Xd XR XA XC]) + case Xa1 + with A(3) show ?case + by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A2[OF A2]], rotated]) + (metis A1 a1 a2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) + next + case Xa2 + then show ?case + by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A2[OF A2]], rotated]) + (metis a1 A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) + next + case Xc + then show ?case + by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A2[OF A2]], rotated]) + (metis a1 c A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) + next + case Xi + then show ?case + apply (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ ACIDZ.A[OF i ACIDZ.A[OF i]]], rotated]) + apply (rule converse_rtranclp_into_rtranclp, rule a1) + apply (rule converse_rtranclp_into_rtranclp, rule a1) + apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) + apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c) + apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) + apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) + apply (rule converse_rtranclp_into_rtranclp, rule a2) + apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) + apply blast + done + next + case Xz + with A show ?case + by (auto elim!: exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ z], rotated] + converse_rtranclp_into_rtranclp[rotated, OF elim_zeros_ACIDZ_rtranclp] + simp del: elim_zeros.simps) + qed auto + next + case inner: (a2 s'' t'') + from A(3,1) show ?case + unfolding inner.hyps[symmetric] + proof (induct "Alt s'' t''" s' rule: ACIDZ.induct[consumes 1, case_names Xa1 Xa2 Xc Xi Xz Xd XR XA XC]) + case Xa1 + with A(3) show ?case + by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A1[OF A1]], rotated]) + (metis a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) + next + case Xa2 + then show ?case + by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A1[OF A1]], rotated]) + (metis a1 a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) + next + case Xc + then show ?case + by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A1[OF A1]], rotated]) + (metis a2 c A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) + next + case Xi + then show ?case + apply (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ ACIDZ.A[OF ACIDZ.A[OF _ i] i]], rotated]) + apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) + apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c) + apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) + apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A2, rule a1) + apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) + apply (rule converse_rtranclp_into_rtranclp, rule a2) + apply blast + done + next + case Xz + then show ?case + by (auto elim!: exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ z], rotated] + converse_rtranclp_into_rtranclp[rotated, OF elim_zeros_ACIDZ_rtranclp] + simp del: elim_zeros.simps) + qed auto + next + case (z rs) with A show ?case + by (auto elim!: rtranclp_trans + intro!: exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ elim_zeros_ACIDZ1], rotated]) + qed (auto 5 0 intro: AAA) + next + case (C r r' s s') + from C(3,1-2) show ?case + by (induct "Conc r s" s' rule: ACIDZ.induct) + (auto intro: CCC elim!: rtranclp_trans + exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ elim_zeros_ACIDZ1], rotated] + exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ distribute_ACIDZ1], rotated]) + qed +qed + +lemma confluent_quotient_ACIDZ: + "confluent_quotient (~) (~~) (~~) (~~) (~~) (~~) + (map_rexp fst) (map_rexp snd) (map_rexp fst) (map_rexp snd) + rel_rexp rel_rexp rel_rexp set_rexp set_rexp" + by unfold_locales + (auto 4 4 dest: ACIDZ_set_rexp' simp: rexp.in_rel rexp.rel_compp dest: map_rexp_ACIDZ_inv intro: rtranclp_into_equivclp + intro: equivpI reflpI sympI transpI ACIDZcl_map_respects + strong_confluentp_imp_confluentp[OF strong_confluentp_ACIDZ]) + +lemma wide_intersection_finite_ACIDZ: "wide_intersection_finite (~~) map_rexp set_rexp" + by unfold_locales + (auto intro: ACIDZcl_map_respects rexp.map_cong simp: rexp.map_id rexp.set_map finite_set_rexp) + +inductive ACIDZEQ (infix "\" 64) where + a: "Alt (Alt r s) t \ Alt r (Alt s t)" +| c: "Alt r s \ Alt s r" +| i: "Alt r r \ r" +| cz: "Conc Zero r \ Zero" +| az: "Alt Zero r \ r" +| d: "Conc (Alt r s) t \ Alt (Conc r t) (Conc s t)" +| A: "r \ r' \ s \ s' \ Alt r s \ Alt r' s'" +| C: "r \ r' \ Conc r s \ Conc r' s" +| r: "r \ r" +| s: "r \ s \ s \ r" +| t: "r \ s \ s \ t \ r \ t" + +context begin + +private lemma AA: "r ~~ r' \ s ~~ s' \ Alt r s ~~ Alt r' s'" +proof (induct rule: equivclp_induct) + case base + then show ?case + by (induct rule: equivclp_induct) (auto elim!: equivclp_trans) +next + case (step s t) + then show ?case + by (auto elim!: equivclp_trans) +qed + +private lemma CC: "r ~~ r' \ Conc r s ~~ Conc r' s" +proof (induct rule: equivclp_induct) + case base + then show ?case + by simp +next + case (step s t) + then show ?case + by (auto elim!: equivclp_trans) +qed + +private lemma CZ: "Conc Zero r ~~ Zero" + by (smt (z3) R elim_zeros.simps(2) elim_zeros.simps(3) r_into_equivclp z) + +private lemma AZ: "Alt Zero r ~~ r" + by (smt (verit, ccfv_threshold) converse_r_into_equivclp converse_rtranclp_into_rtranclp + elim_zeros.simps(1) elim_zeros.simps(3) equivclp_def symclpI1 z R) + +private lemma D: "Conc (Alt r s) t ~~ Alt (Conc r t) (Conc s t)" + by (smt (verit, ccfv_threshold) AA ACIDZ.d converse_r_into_equivclp distribute.simps(1) + equivclp_sym rtranclp.simps rtranclp_equivclp) + +lemma ACIDZEQ_le_ACIDZcl: "r \ s \ r ~~ s" + by (induct r s rule: ACIDZEQ.induct) (auto intro: AA CC AZ CZ D equivclp_sym equivclp_trans) + +end + +lemma ACIDZEQ_z[simp]: "r \ elim_zeros r" + by (induct r rule: elim_zeros.induct) (auto 0 3 intro: ACIDZEQ.intros simp: Let_def) + +lemma ACIDZEQ_d[simp]: "Conc r s \ distribute s r" + by (induct s r rule: distribute.induct) (auto 0 3 intro: ACIDZEQ.intros) + +lemma ACIDZ_le_ACIDZEQ: "r ~ s \ r \ s" + by (induct r s rule: ACIDZ.induct) (auto 0 2 intro: ACIDZEQ.intros simp: Let_def) + +lemma ACIDZcl_le_ACIDZEQ: "r ~~ s \ r \ s" + by (induct rule: equivclp_induct) (auto 0 3 intro: ACIDZEQ.intros ACIDZ_le_ACIDZEQ) + +lemma ACIDZEQ_alt: "(\) = (~~)" + by (simp add: ACIDZEQ_le_ACIDZcl ACIDZcl_le_ACIDZEQ antisym predicate2I) + +quotient_type 'a rexp_ACIDZ = "'a rexp" / "(\)" + unfolding ACIDZEQ_alt by (auto intro!: equivpI reflpI sympI transpI) + +lift_bnf 'a rexp_ACIDZ + unfolding ACIDZEQ_alt + subgoal for A Q by (rule confluent_quotient.subdistributivity[OF confluent_quotient_ACIDZ]) + subgoal for Ss by (elim wide_intersection_finite.wide_intersection[OF wide_intersection_finite_ACIDZ]) + done + +datatype ldl = Prop string | And ldl ldl | Not ldl | Match "ldl rexp_ACIDZ" + +end diff --git a/src/HOL/Library/Confluent_Quotient.thy b/src/HOL/Library/Confluent_Quotient.thy --- a/src/HOL/Library/Confluent_Quotient.thy +++ b/src/HOL/Library/Confluent_Quotient.thy @@ -1,74 +1,175 @@ -theory Confluent_Quotient imports +theory Confluent_Quotient imports Confluence begin -section \Subdistributivity for quotients via confluence\ +text \Functors with finite setters preserve wide intersection for any equivalence relation that respects the mapper.\ + +lemma Inter_finite_subset: + assumes "\A \ \. finite A" + shows "\\\\. finite \ \ (\\) = (\\)" +proof(cases "\ = {}") + case False + then obtain A where A: "A \ \" by auto + then have finA: "finite A" using assms by auto + hence fin: "finite (A - \\)" by(rule finite_subset[rotated]) auto + let ?P = "\x A. A \ \ \ x \ A" + define f where "f x = Eps (?P x)" for x + let ?\ = "insert A (f ` (A - \\))" + have "?P x (f x)" if "x \ A - \\" for x unfolding f_def by(rule someI_ex)(use that A in auto) + hence "(\?\) = (\\)" "?\ \ \" using A by auto + moreover have "finite ?\" using fin by simp + ultimately show ?thesis by blast +qed simp + +locale wide_intersection_finite = + fixes E :: "'Fa \ 'Fa \ bool" + and mapFa :: "('a \ 'a) \ 'Fa \ 'Fa" + and setFa :: "'Fa \ 'a set" + assumes equiv: "equivp E" + and map_E: "E x y \ E (mapFa f x) (mapFa f y)" + and map_id: "mapFa id x = x" + and map_cong: "\a\setFa x. f a = g a \ mapFa f x = mapFa g x" + and set_map: "setFa (mapFa f x) = f ` setFa x" + and finite: "finite (setFa x)" +begin + +lemma binary_intersection: + assumes "E y z" and y: "setFa y \ Y" and z: "setFa z \ Z" and a: "a \ Y" "a \ Z" + shows "\x. E x y \ setFa x \ Y \ setFa x \ Z" +proof - + let ?f = "\b. if b \ Z then b else a" + let ?u = "mapFa ?f y" + from \E y z\ have "E ?u (mapFa ?f z)" by(rule map_E) + also have "mapFa ?f z = mapFa id z" by(rule map_cong)(use z in auto) + also have "\ = z" by(rule map_id) + finally have "E ?u y" using \E y z\ equivp_symp[OF equiv] equivp_transp[OF equiv] by blast + moreover have "setFa ?u \ Y" using a y by(subst set_map) auto + moreover have "setFa ?u \ Z" using a by(subst set_map) auto + ultimately show ?thesis by blast +qed + +lemma finite_intersection: + assumes E: "\y\A. E y z" + and fin: "finite A" + and sub: "\y\A. setFa y \ Y y \ a \ Y y" + shows "\x. E x z \ (\y\A. setFa x \ Y y)" + using fin E sub +proof(induction) + case empty + then show ?case using equivp_reflp[OF equiv, of z] by(auto) +next + case (insert y A) + then obtain x where x: "E x z" "\y\A. setFa x \ Y y \ a \ Y y" by auto + hence set_x: "setFa x \ (\y\A. Y y)" "a \ (\y\A. Y y)" by auto + from insert.prems have "E y z" and set_y: "setFa y \ Y y" "a \ Y y" by auto + from \E y z\ \E x z\ have "E x y" using equivp_symp[OF equiv] equivp_transp[OF equiv] by blast + from binary_intersection[OF this set_x(1) set_y(1) set_x(2) set_y(2)] + obtain x' where "E x' x" "setFa x' \ \ (Y ` A)" "setFa x' \ Y y" by blast + then show ?case using \E x z\ equivp_transp[OF equiv] by blast +qed + +lemma wide_intersection: + assumes inter_nonempty: "\ Ss \ {}" + shows "(\As \ Ss. {(x, x'). E x x'} `` {x. setFa x \ As}) \ {(x, x'). E x x'} `` {x. setFa x \ \ Ss}" (is "?lhs \ ?rhs") +proof + fix x + assume lhs: "x \ ?lhs" + from inter_nonempty obtain a where a: "\As \ Ss. a \ As" by auto + from lhs obtain y where y: "\As. As \ Ss \ E (y As) x \ setFa (y As) \ As" + by atomize_elim(rule choice, auto) + define Ts where "Ts = (\As. insert a (setFa (y As))) ` Ss" + have Ts_subset: "(\Ts) \ (\Ss)" using a unfolding Ts_def by(auto dest: y) + have Ts_finite: "\Bs \ Ts. finite Bs" unfolding Ts_def by(auto dest: y intro: finite) + from Inter_finite_subset[OF this] obtain Us + where Us: "Us \ Ts" and finite_Us: "finite Us" and Int_Us: "(\Us) \ (\Ts)" by force + let ?P = "\U As. As \ Ss \ U = insert a (setFa (y As))" + define Y where "Y U = Eps (?P U)" for U + have Y: "?P U (Y U)" if "U \ Us" for U unfolding Y_def + by(rule someI_ex)(use that Us in \auto simp add: Ts_def\) + let ?f = "\U. y (Y U)" + have *: "\z\(?f ` Us). E z x" by(auto dest!: Y y) + have **: "\z\(?f ` Us). setFa z \ insert a (setFa z) \ a \ insert a (setFa z)" by auto + from finite_intersection[OF * _ **] finite_Us obtain u + where u: "E u x" and set_u: "\z\(?f ` Us). setFa u \ insert a (setFa z)" by auto + from set_u have "setFa u \ (\ Us)" by(auto dest: Y) + with Int_Us Ts_subset have "setFa u \ (\ Ss)" by auto + with u show "x \ ?rhs" by auto +qed + +end + +text \Subdistributivity for quotients via confluence\ + +lemma rtranclp_transp_reflp: "R\<^sup>*\<^sup>* = R" if "transp R" "reflp R" + apply(rule ext iffI)+ + subgoal premises prems for x y using prems by(induction)(use that in \auto intro: reflpD transpD\) + subgoal by(rule r_into_rtranclp) + done + +lemma rtranclp_equivp: "R\<^sup>*\<^sup>* = R" if "equivp R" + using that by(simp add: rtranclp_transp_reflp equivp_reflp_symp_transp) locale confluent_quotient = - fixes R :: "'Fb \ 'Fb \ bool" + fixes Rb :: "'Fb \ 'Fb \ bool" and Ea :: "'Fa \ 'Fa \ bool" and Eb :: "'Fb \ 'Fb \ bool" and Ec :: "'Fc \ 'Fc \ bool" and Eab :: "'Fab \ 'Fab \ bool" and Ebc :: "'Fbc \ 'Fbc \ bool" and \_Faba :: "'Fab \ 'Fa" and \_Fabb :: "'Fab \ 'Fb" and \_Fbcb :: "'Fbc \ 'Fb" and \_Fbcc :: "'Fbc \ 'Fc" and rel_Fab :: "('a \ 'b \ bool) \ 'Fa \ 'Fb \ bool" and rel_Fbc :: "('b \ 'c \ bool) \ 'Fb \ 'Fc \ bool" and rel_Fac :: "('a \ 'c \ bool) \ 'Fa \ 'Fc \ bool" and set_Fab :: "'Fab \ ('a \ 'b) set" and set_Fbc :: "'Fbc \ ('b \ 'c) set" - assumes confluent: "confluentp R" - and retract1_ab: "\x y. R (\_Fabb x) y \ \z. Eab x z \ y = \_Fabb z" - and retract1_bc: "\x y. R (\_Fbcb x) y \ \z. Ebc x z \ y = \_Fbcb z" - and generated: "Eb \ equivclp R" - and set_ab: "\x y. Eab x y \ set_Fab x = set_Fab y" - and set_bc: "\x y. Ebc x y \ set_Fbc x = set_Fbc y" + assumes confluent: "confluentp Rb" + and retract1_ab: "\x y. Rb (\_Fabb x) y \ \z. Eab x z \ y = \_Fabb z \ set_Fab z \ set_Fab x" + and retract1_bc: "\x y. Rb (\_Fbcb x) y \ \z. Ebc x z \ y = \_Fbcb z \ set_Fbc z \ set_Fbc x" + and generated_b: "Eb \ equivclp Rb" and transp_a: "transp Ea" and transp_c: "transp Ec" and equivp_ab: "equivp Eab" and equivp_bc: "equivp Ebc" and in_rel_Fab: "\A x y. rel_Fab A x y \ (\z. z \ {x. set_Fab x \ {(x, y). A x y}} \ \_Faba z = x \ \_Fabb z = y)" and in_rel_Fbc: "\B x y. rel_Fbc B x y \ (\z. z \ {x. set_Fbc x \ {(x, y). B x y}} \ \_Fbcb z = x \ \_Fbcc z = y)" and rel_compp: "\A B. rel_Fac (A OO B) = rel_Fab A OO rel_Fbc B" and \_Faba_respect: "rel_fun Eab Ea \_Faba \_Faba" and \_Fbcc_respect: "rel_fun Ebc Ec \_Fbcc \_Fbcc" begin -lemma retract_ab: "R\<^sup>*\<^sup>* (\_Fabb x) y \ \z. Eab x z \ y = \_Fabb z" +lemma retract_ab: "Rb\<^sup>*\<^sup>* (\_Fabb x) y \ \z. Eab x z \ y = \_Fabb z \ set_Fab z \ set_Fab x" by(induction rule: rtranclp_induct)(blast dest: retract1_ab intro: equivp_transp[OF equivp_ab] equivp_reflp[OF equivp_ab])+ -lemma retract_bc: "R\<^sup>*\<^sup>* (\_Fbcb x) y \ \z. Ebc x z \ y = \_Fbcb z" +lemma retract_bc: "Rb\<^sup>*\<^sup>* (\_Fbcb x) y \ \z. Ebc x z \ y = \_Fbcb z \ set_Fbc z \ set_Fbc x" by(induction rule: rtranclp_induct)(blast dest: retract1_bc intro: equivp_transp[OF equivp_bc] equivp_reflp[OF equivp_bc])+ lemma subdistributivity: "rel_Fab A OO Eb OO rel_Fbc B \ Ea OO rel_Fac (A OO B) OO Ec" proof(rule predicate2I; elim relcomppE) fix x y y' z assume "rel_Fab A x y" and "Eb y y'" and "rel_Fbc B y' z" then obtain xy y'z where xy: "set_Fab xy \ {(a, b). A a b}" "x = \_Faba xy" "y = \_Fabb xy" and y'z: "set_Fbc y'z \ {(a, b). B a b}" "y' = \_Fbcb y'z" "z = \_Fbcc y'z" by(auto simp add: in_rel_Fab in_rel_Fbc) - from \Eb y y'\ have "equivclp R y y'" using generated by blast - then obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u" + from \Eb y y'\ have "equivclp Rb y y'" using generated_b by blast + then obtain u where u: "Rb\<^sup>*\<^sup>* y u" "Rb\<^sup>*\<^sup>* y' u" unfolding semiconfluentp_equivclp[OF confluent[THEN confluentp_imp_semiconfluentp]] by(auto simp add: rtranclp_conversep) with xy y'z obtain xy' y'z' - where retract1: "Eab xy xy'" "\_Fabb xy' = u" - and retract2: "Ebc y'z y'z'" "\_Fbcb y'z' = u" + where retract1: "Eab xy xy'" "\_Fabb xy' = u" "set_Fab xy' \ set_Fab xy" + and retract2: "Ebc y'z y'z'" "\_Fbcb y'z' = u" "set_Fbc y'z' \ set_Fbc y'z" by(auto dest!: retract_ab retract_bc) from retract1(1) xy have "Ea x (\_Faba xy')" by(auto dest: \_Faba_respect[THEN rel_funD]) - moreover have "rel_Fab A (\_Faba xy') u" using xy retract1 - by(auto simp add: in_rel_Fab dest: set_ab) - moreover have "rel_Fbc B u (\_Fbcc y'z')" using y'z retract2 - by(auto simp add: in_rel_Fbc dest: set_bc) + moreover have "rel_Fab A (\_Faba xy') u" using xy retract1 by(auto simp add: in_rel_Fab) + moreover have "rel_Fbc B u (\_Fbcc y'z')" using y'z retract2 by(auto simp add: in_rel_Fbc) moreover have "Ec (\_Fbcc y'z') z" using retract2 y'z equivp_symp[OF equivp_bc] - by(auto dest: \_Fbcc_respect[THEN rel_funD]) + by(auto intro: \_Fbcc_respect[THEN rel_funD]) ultimately show "(Ea OO rel_Fac (A OO B) OO Ec) x z" unfolding rel_compp by blast qed end end \ No newline at end of file diff --git a/src/HOL/Library/Dlist.thy b/src/HOL/Library/Dlist.thy --- a/src/HOL/Library/Dlist.thy +++ b/src/HOL/Library/Dlist.thy @@ -1,323 +1,322 @@ (* Author: Florian Haftmann, TU Muenchen Author: Andreas Lochbihler, ETH Zurich *) section \Lists with elements distinct as canonical example for datatype invariants\ theory Dlist imports Confluent_Quotient begin subsection \The type of distinct lists\ typedef 'a dlist = "{xs::'a list. distinct xs}" morphisms list_of_dlist Abs_dlist proof show "[] \ {xs. distinct xs}" by simp qed context begin qualified definition dlist_eq where "dlist_eq = BNF_Def.vimage2p remdups remdups (=)" qualified lemma equivp_dlist_eq: "equivp dlist_eq" unfolding dlist_eq_def by(rule equivp_vimage2p)(rule identity_equivp) qualified definition abs_dlist :: "'a list \ 'a dlist" where "abs_dlist = Abs_dlist o remdups" definition qcr_dlist :: "'a list \ 'a dlist \ bool" where "qcr_dlist x y \ y = abs_dlist x" qualified lemma Quotient_dlist_remdups: "Quotient dlist_eq abs_dlist list_of_dlist qcr_dlist" unfolding Quotient_def dlist_eq_def qcr_dlist_def vimage2p_def abs_dlist_def by (auto simp add: fun_eq_iff Abs_dlist_inject list_of_dlist[simplified] list_of_dlist_inverse distinct_remdups_id) end locale Quotient_dlist begin setup_lifting Dlist.Quotient_dlist_remdups Dlist.equivp_dlist_eq[THEN equivp_reflp2] end setup_lifting type_definition_dlist lemma dlist_eq_iff: "dxs = dys \ list_of_dlist dxs = list_of_dlist dys" by (simp add: list_of_dlist_inject) lemma dlist_eqI: "list_of_dlist dxs = list_of_dlist dys \ dxs = dys" by (simp add: dlist_eq_iff) text \Formal, totalized constructor for \<^typ>\'a dlist\:\ definition Dlist :: "'a list \ 'a dlist" where "Dlist xs = Abs_dlist (remdups xs)" lemma distinct_list_of_dlist [simp, intro]: "distinct (list_of_dlist dxs)" using list_of_dlist [of dxs] by simp lemma list_of_dlist_Dlist [simp]: "list_of_dlist (Dlist xs) = remdups xs" by (simp add: Dlist_def Abs_dlist_inverse) lemma remdups_list_of_dlist [simp]: "remdups (list_of_dlist dxs) = list_of_dlist dxs" by simp lemma Dlist_list_of_dlist [simp, code abstype]: "Dlist (list_of_dlist dxs) = dxs" by (simp add: Dlist_def list_of_dlist_inverse distinct_remdups_id) text \Fundamental operations:\ context begin qualified definition empty :: "'a dlist" where "empty = Dlist []" qualified definition insert :: "'a \ 'a dlist \ 'a dlist" where "insert x dxs = Dlist (List.insert x (list_of_dlist dxs))" qualified definition remove :: "'a \ 'a dlist \ 'a dlist" where "remove x dxs = Dlist (remove1 x (list_of_dlist dxs))" qualified definition map :: "('a \ 'b) \ 'a dlist \ 'b dlist" where "map f dxs = Dlist (remdups (List.map f (list_of_dlist dxs)))" qualified definition filter :: "('a \ bool) \ 'a dlist \ 'a dlist" where "filter P dxs = Dlist (List.filter P (list_of_dlist dxs))" qualified definition rotate :: "nat \ 'a dlist \ 'a dlist" where "rotate n dxs = Dlist (List.rotate n (list_of_dlist dxs))" end text \Derived operations:\ context begin qualified definition null :: "'a dlist \ bool" where "null dxs = List.null (list_of_dlist dxs)" qualified definition member :: "'a dlist \ 'a \ bool" where "member dxs = List.member (list_of_dlist dxs)" qualified definition length :: "'a dlist \ nat" where "length dxs = List.length (list_of_dlist dxs)" qualified definition fold :: "('a \ 'b \ 'b) \ 'a dlist \ 'b \ 'b" where "fold f dxs = List.fold f (list_of_dlist dxs)" qualified definition foldr :: "('a \ 'b \ 'b) \ 'a dlist \ 'b \ 'b" where "foldr f dxs = List.foldr f (list_of_dlist dxs)" end subsection \Executable version obeying invariant\ lemma list_of_dlist_empty [simp, code abstract]: "list_of_dlist Dlist.empty = []" by (simp add: Dlist.empty_def) lemma list_of_dlist_insert [simp, code abstract]: "list_of_dlist (Dlist.insert x dxs) = List.insert x (list_of_dlist dxs)" by (simp add: Dlist.insert_def) lemma list_of_dlist_remove [simp, code abstract]: "list_of_dlist (Dlist.remove x dxs) = remove1 x (list_of_dlist dxs)" by (simp add: Dlist.remove_def) lemma list_of_dlist_map [simp, code abstract]: "list_of_dlist (Dlist.map f dxs) = remdups (List.map f (list_of_dlist dxs))" by (simp add: Dlist.map_def) lemma list_of_dlist_filter [simp, code abstract]: "list_of_dlist (Dlist.filter P dxs) = List.filter P (list_of_dlist dxs)" by (simp add: Dlist.filter_def) lemma list_of_dlist_rotate [simp, code abstract]: "list_of_dlist (Dlist.rotate n dxs) = List.rotate n (list_of_dlist dxs)" by (simp add: Dlist.rotate_def) text \Explicit executable conversion\ definition dlist_of_list [simp]: "dlist_of_list = Dlist" lemma [code abstract]: "list_of_dlist (dlist_of_list xs) = remdups xs" by simp text \Equality\ instantiation dlist :: (equal) equal begin definition "HOL.equal dxs dys \ HOL.equal (list_of_dlist dxs) (list_of_dlist dys)" instance by standard (simp add: equal_dlist_def equal list_of_dlist_inject) end declare equal_dlist_def [code] lemma [code nbe]: "HOL.equal (dxs :: 'a::equal dlist) dxs \ True" by (fact equal_refl) subsection \Induction principle and case distinction\ lemma dlist_induct [case_names empty insert, induct type: dlist]: assumes empty: "P Dlist.empty" assumes insrt: "\x dxs. \ Dlist.member dxs x \ P dxs \ P (Dlist.insert x dxs)" shows "P dxs" proof (cases dxs) case (Abs_dlist xs) then have "distinct xs" and dxs: "dxs = Dlist xs" by (simp_all add: Dlist_def distinct_remdups_id) from \distinct xs\ have "P (Dlist xs)" proof (induct xs) case Nil from empty show ?case by (simp add: Dlist.empty_def) next case (Cons x xs) then have "\ Dlist.member (Dlist xs) x" and "P (Dlist xs)" by (simp_all add: Dlist.member_def List.member_def) with insrt have "P (Dlist.insert x (Dlist xs))" . with Cons show ?case by (simp add: Dlist.insert_def distinct_remdups_id) qed with dxs show "P dxs" by simp qed lemma dlist_case [cases type: dlist]: obtains (empty) "dxs = Dlist.empty" | (insert) x dys where "\ Dlist.member dys x" and "dxs = Dlist.insert x dys" proof (cases dxs) case (Abs_dlist xs) then have dxs: "dxs = Dlist xs" and distinct: "distinct xs" by (simp_all add: Dlist_def distinct_remdups_id) show thesis proof (cases xs) case Nil with dxs have "dxs = Dlist.empty" by (simp add: Dlist.empty_def) with empty show ?thesis . next case (Cons x xs) with dxs distinct have "\ Dlist.member (Dlist xs) x" and "dxs = Dlist.insert x (Dlist xs)" by (simp_all add: Dlist.member_def List.member_def Dlist.insert_def distinct_remdups_id) with insert show ?thesis . qed qed subsection \Functorial structure\ functor map: map by (simp_all add: remdups_map_remdups fun_eq_iff dlist_eq_iff) subsection \Quickcheck generators\ quickcheck_generator dlist predicate: distinct constructors: Dlist.empty, Dlist.insert subsection \BNF instance\ context begin qualified inductive double :: "'a list \ 'a list \ bool" where "double (xs @ ys) (xs @ x # ys)" if "x \ set ys" qualified lemma strong_confluentp_double: "strong_confluentp double" proof fix xs ys zs :: "'a list" assume ys: "double xs ys" and zs: "double xs zs" consider (left) as y bs z cs where "xs = as @ bs @ cs" "ys = as @ y # bs @ cs" "zs = as @ bs @ z # cs" "y \ set (bs @ cs)" "z \ set cs" | (right) as y bs z cs where "xs = as @ bs @ cs" "ys = as @ bs @ y # cs" "zs = as @ z # bs @ cs" "y \ set cs" "z \ set (bs @ cs)" proof - show thesis using ys zs by(clarsimp simp add: double.simps append_eq_append_conv2)(auto intro: that) qed then show "\us. double\<^sup>*\<^sup>* ys us \ double\<^sup>=\<^sup>= zs us" proof cases case left let ?us = "as @ y # bs @ z # cs" have "double ys ?us" "double zs ?us" using left by(auto 4 4 simp add: double.simps)(metis append_Cons append_assoc)+ then show ?thesis by blast next case right let ?us = "as @ z # bs @ y # cs" have "double ys ?us" "double zs ?us" using right by(auto 4 4 simp add: double.simps)(metis append_Cons append_assoc)+ then show ?thesis by blast qed qed qualified lemma double_Cons1 [simp]: "double xs (x # xs)" if "x \ set xs" using double.intros[of x xs "[]"] that by simp qualified lemma double_Cons_same [simp]: "double xs ys \ double (x # xs) (x # ys)" by(auto simp add: double.simps Cons_eq_append_conv) qualified lemma doubles_Cons_same: "double\<^sup>*\<^sup>* xs ys \ double\<^sup>*\<^sup>* (x # xs) (x # ys)" by(induction rule: rtranclp_induct)(auto intro: rtranclp.rtrancl_into_rtrancl) qualified lemma remdups_into_doubles: "double\<^sup>*\<^sup>* (remdups xs) xs" by(induction xs)(auto intro: doubles_Cons_same rtranclp.rtrancl_into_rtrancl) qualified lemma dlist_eq_into_doubles: "Dlist.dlist_eq \ equivclp double" by(auto 4 4 simp add: Dlist.dlist_eq_def vimage2p_def intro: equivclp_trans converse_rtranclp_into_equivclp rtranclp_into_equivclp remdups_into_doubles) -qualified lemma factor_double_map: "double (map f xs) ys \ \zs. Dlist.dlist_eq xs zs \ ys = map f zs" +qualified lemma factor_double_map: "double (map f xs) ys \ \zs. Dlist.dlist_eq xs zs \ ys = map f zs \ set zs \ set xs" by(auto simp add: double.simps Dlist.dlist_eq_def vimage2p_def map_eq_append_conv) - (metis list.simps(9) map_append remdups.simps(2) remdups_append2) + (metis (no_types, hide_lams) list.simps(9) map_append remdups.simps(2) remdups_append2 set_append set_eq_subset set_remdups) qualified lemma dlist_eq_set_eq: "Dlist.dlist_eq xs ys \ set xs = set ys" by(simp add: Dlist.dlist_eq_def vimage2p_def)(metis set_remdups) qualified lemma dlist_eq_map_respect: "Dlist.dlist_eq xs ys \ Dlist.dlist_eq (map f xs) (map f ys)" by(clarsimp simp add: Dlist.dlist_eq_def vimage2p_def)(metis remdups_map_remdups) qualified lemma confluent_quotient_dlist: "confluent_quotient double Dlist.dlist_eq Dlist.dlist_eq Dlist.dlist_eq Dlist.dlist_eq Dlist.dlist_eq (map fst) (map snd) (map fst) (map snd) list_all2 list_all2 list_all2 set set" by(unfold_locales)(auto intro: strong_confluentp_imp_confluentp strong_confluentp_double dest: factor_double_map dlist_eq_into_doubles[THEN predicate2D] dlist_eq_set_eq simp add: list.in_rel list.rel_compp dlist_eq_map_respect Dlist.equivp_dlist_eq equivp_imp_transp) - lifting_update dlist.lifting lifting_forget dlist.lifting end context begin interpretation Quotient_dlist: Quotient_dlist . lift_bnf (plugins del: code) 'a dlist subgoal for A B by(rule confluent_quotient.subdistributivity[OF Dlist.confluent_quotient_dlist]) subgoal by(force dest: Dlist.dlist_eq_set_eq intro: equivp_reflp[OF Dlist.equivp_dlist_eq]) done qualified lemma list_of_dlist_transfer[transfer_rule]: "bi_unique R \ (rel_fun (Quotient_dlist.pcr_dlist R) (list_all2 R)) remdups list_of_dlist" unfolding rel_fun_def Quotient_dlist.pcr_dlist_def qcr_dlist_def Dlist.abs_dlist_def by (auto simp: Abs_dlist_inverse intro!: remdups_transfer[THEN rel_funD]) lemma list_of_dlist_map_dlist[simp]: "list_of_dlist (map_dlist f xs) = remdups (map f (list_of_dlist xs))" by transfer (auto simp: remdups_map_remdups) end end diff --git a/src/HOL/ROOT b/src/HOL/ROOT --- a/src/HOL/ROOT +++ b/src/HOL/ROOT @@ -1,1193 +1,1194 @@ chapter HOL session HOL (main) = Pure + description " Classical Higher-order Logic. " options [strict_facts] sessions Tools theories Main (global) Complex_Main (global) document_theories Tools.Code_Generator document_files "root.bib" "root.tex" session "HOL-Examples" in Examples = HOL + description " Notable Examples in Isabelle/HOL. " sessions "HOL-Library" theories Adhoc_Overloading_Examples Ackermann Cantor Coherent Commands Drinker Groebner_Examples Iff_Oracle Induction_Schema Knaster_Tarski "ML" Peirce Records Seq document_files "root.bib" "root.tex" session "HOL-Proofs" (timing) in Proofs = Pure + description " HOL-Main with explicit proof terms. " options [quick_and_dirty = false, record_proofs = 2, parallel_limit = 500] sessions "HOL-Library" theories "HOL-Library.Realizers" session "HOL-Library" (main timing) in Library = HOL + description " Classical Higher-order Logic -- batteries included. " theories Library (*conflicting type class instantiations and dependent applications*) Finite_Lattice List_Lexorder List_Lenlexorder Prefix_Order Product_Lexorder Product_Order Subseq_Order (*conflicting syntax*) Datatype_Records (*data refinements and dependent applications*) AList_Mapping Code_Binary_Nat Code_Prolog Code_Real_Approx_By_Float Code_Target_Numeral DAList DAList_Multiset RBT_Mapping RBT_Set (*printing modifications*) OptionalSugar (*prototypic tools*) Predicate_Compile_Quickcheck (*legacy tools*) Old_Datatype Old_Recdef Realizers Refute document_files "root.bib" "root.tex" session "HOL-Analysis" (main timing) in Analysis = HOL + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Library" "HOL-Computational_Algebra" theories Analysis document_files "root.tex" "root.bib" session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] theories Complex_Analysis document_files "root.tex" "root.bib" session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" + theories Approximations Metric_Arith_Examples session "HOL-Homology" (timing) in Homology = "HOL-Analysis" + options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", document_variants = "document:manual=-proof,-ML,-unimportant"] sessions "HOL-Algebra" theories Homology document_files "root.tex" session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" + theories Computational_Algebra (*conflicting type class instantiations and dependent applications*) Field_as_Ring session "HOL-Real_Asymp" in Real_Asymp = HOL + sessions "HOL-Decision_Procs" theories Real_Asymp Real_Asymp_Approx Real_Asymp_Examples session "HOL-Real_Asymp-Manual" in "Real_Asymp/Manual" = "HOL-Real_Asymp" + theories Real_Asymp_Doc document_files (in "~~/src/Doc") "iman.sty" "extra.sty" "isar.sty" document_files "root.tex" "style.sty" session "HOL-Hahn_Banach" in Hahn_Banach = HOL + description " Author: Gertrud Bauer, TU Munich The Hahn-Banach theorem for real vector spaces. This is the proof of the Hahn-Banach theorem for real vectorspaces, following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach theorem is one of the fundamental theorems of functional analysis. It is a conclusion of Zorn's lemma. Two different formaulations of the theorem are presented, one for general real vectorspaces and its application to normed vectorspaces. The theorem says, that every continous linearform, defined on arbitrary subspaces (not only one-dimensional subspaces), can be extended to a continous linearform on the whole vectorspace. " sessions "HOL-Analysis" theories Hahn_Banach document_files "root.bib" "root.tex" session "HOL-Induct" in Induct = HOL + description " Examples of (Co)Inductive Definitions. Comb proves the Church-Rosser theorem for combinators (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz). Mutil is the famous Mutilated Chess Board problem (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz). PropLog proves the completeness of a formalization of propositional logic (see http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz). Exp demonstrates the use of iterated inductive definitions to reason about mutually recursive relations. " sessions "HOL-Library" theories [quick_and_dirty] Common_Patterns theories Nested_Datatype QuoDataType QuoNestedDataType Term SList ABexp Infinitely_Branching_Tree Ordinals Sigma_Algebra Comb PropLog Com document_files "root.tex" session "HOL-IMP" (timing) in IMP = "HOL-Library" + options [document_variants = document] theories BExp ASM Finite_Reachable Denotational Compiler2 Poly_Types Sec_Typing Sec_TypingT Def_Init_Big Def_Init_Small Fold Live Live_True Hoare_Examples Hoare_Sound_Complete VCG Hoare_Total VCG_Total_EX VCG_Total_EX2 Collecting1 Collecting_Examples Abs_Int_Tests Abs_Int1_parity Abs_Int1_const Abs_Int3 Procs_Dyn_Vars_Dyn Procs_Stat_Vars_Dyn Procs_Stat_Vars_Stat C_like OO document_files "root.bib" "root.tex" session "HOL-IMPP" in IMPP = HOL + description \ Author: David von Oheimb Copyright 1999 TUM IMPP -- An imperative language with procedures. This is an extension of IMP with local variables and mutually recursive procedures. For documentation see "Hoare Logic for Mutual Recursion and Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). \ theories EvenOdd session "HOL-Data_Structures" (timing) in Data_Structures = HOL + options [document_variants = document] sessions "HOL-Number_Theory" theories [document = false] Less_False theories Sorting Balance Tree_Map Interval_Tree AVL_Map AVL_Bal_Set AVL_Bal2_Set Height_Balanced_Tree RBT_Set2 RBT_Map Tree23_Map Tree23_of_List Tree234_Map Brother12_Map AA_Map Set2_Join_RBT Array_Braun Trie_Fun Trie_Map Tries_Binary Queue_2Lists Heaps Leftist_Heap Binomial_Heap Selection document_files "root.tex" "root.bib" session "HOL-Import" in Import = HOL + theories HOL_Light_Maps theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" + description " Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity. " sessions "HOL-Algebra" theories Number_Theory document_files "root.tex" session "HOL-Hoare" in Hoare = HOL + description " Verification of imperative programs (verification conditions are generated automatically from pre/post conditions and loop invariants). " theories Examples ExamplesAbort ExamplesTC Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation document_files "root.bib" "root.tex" session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL + description " Verification of shared-variable imperative programs a la Owicki-Gries. (verification conditions are generated automatically). " theories Hoare_Parallel document_files "root.bib" "root.tex" session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" + sessions "HOL-Number_Theory" "HOL-Data_Structures" "HOL-Examples" theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Code_Lazy_Test Code_Test_PolyML Code_Test_Scala theories [condition = ISABELLE_GHC] Code_Test_GHC theories [condition = ISABELLE_MLTON] Code_Test_MLton theories [condition = ISABELLE_OCAMLFIND] Code_Test_OCaml theories [condition = ISABELLE_SMLNJ] Code_Test_SMLNJ session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" + description " Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Testing Metis and Sledgehammer. " sessions "HOL-Decision_Procs" theories Abstraction Big_O Binary_Tree Clausification Message Proxies Tarski Trans_Closure Sets session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL + description " Author: Jasmin Blanchette, TU Muenchen Copyright 2009 " options [kodkod_scala] sessions "HOL-Library" theories [quick_and_dirty] Nitpick_Examples session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" + description " Author: Clemens Ballarin, started 24 September 1999, and many others The Isabelle Algebraic Library. " sessions "HOL-Cardinals" theories (* Orders and Lattices *) Galois_Connection (* Knaster-Tarski theorem and Galois connections *) (* Groups *) FiniteProduct (* Product operator for commutative groups *) Sylow (* Sylow's theorem *) Bij (* Automorphism Groups *) Multiplicative_Group Zassenhaus (* The Zassenhaus lemma *) (* Rings *) Divisibility (* Rings *) IntRing (* Ideals and residue classes *) UnivPoly (* Polynomials *) (* Main theory *) Algebra document_files "root.bib" "root.tex" session "HOL-Auth" (timing) in Auth = HOL + description " A new approach to verifying authentication protocols. " sessions "HOL-Library" directories "Smartcard" "Guard" theories Auth_Shared Auth_Public "Smartcard/Auth_Smartcard" "Guard/Auth_Guard_Shared" "Guard/Auth_Guard_Public" document_files "root.tex" session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" + description " Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Verifying security protocols using Chandy and Misra's UNITY formalism. " directories "Simple" "Comp" theories (*Basic meta-theory*) UNITY_Main (*Simple examples: no composition*) "Simple/Deadlock" "Simple/Common" "Simple/Network" "Simple/Token" "Simple/Channel" "Simple/Lift" "Simple/Mutex" "Simple/Reach" "Simple/Reachability" (*Verifying security protocols using UNITY*) "Simple/NSP_Bad" (*Example of composition*) "Comp/Handshake" (*Universal properties examples*) "Comp/Counter" "Comp/Counterc" "Comp/Priority" "Comp/TimerArray" "Comp/Progress" "Comp/Alloc" "Comp/AllocImpl" "Comp/Client" (*obsolete*) ELT document_files "root.tex" session "HOL-Unix" in Unix = HOL + options [print_mode = "no_brackets,no_type_brackets"] sessions "HOL-Library" theories Unix document_files "root.bib" "root.tex" session "HOL-ZF" in ZF = HOL + sessions "HOL-Library" theories MainZF Games document_files "root.tex" session "HOL-Imperative_HOL" (timing) in Imperative_HOL = HOL + options [print_mode = "iff,no_brackets"] sessions "HOL-Library" directories "ex" theories Imperative_HOL_ex document_files "root.bib" "root.tex" session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" + description " Various decision procedures, typically involving reflection. " directories "ex" theories Decision_Procs session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + sessions "HOL-Examples" theories Hilbert_Classical Proof_Terms XML_Data session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" + description " Examples for program extraction in Higher-Order Logic. " options [quick_and_dirty = false] sessions "HOL-Computational_Algebra" theories Greatest_Common_Divisor Warshall Higman_Extraction Pigeonhole Euclid document_files "root.bib" "root.tex" session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" + description \ Lambda Calculus in de Bruijn's Notation. This session defines lambda-calculus terms with de Bruijn indixes and proves confluence of beta, eta and beta+eta. The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html). \ options [print_mode = "no_brackets", quick_and_dirty = false] sessions "HOL-Library" theories Eta StrongNorm Standardization WeakNorm document_files "root.bib" "root.tex" session "HOL-Prolog" in Prolog = HOL + description " Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) A bare-bones implementation of Lambda-Prolog. This is a simple exploratory implementation of Lambda-Prolog in HOL, including some minimal examples (in Test.thy) and a more typical example of a little functional language and its type system. " theories Test Type session "HOL-MicroJava" (timing) in MicroJava = HOL + description " Formalization of a fragment of Java, together with a corresponding virtual machine and a specification of its bytecode verifier and a lightweight bytecode verifier, including proofs of type-safety. " sessions "HOL-Library" "HOL-Eisbach" directories "BV" "Comp" "DFA" "J" "JVM" theories MicroJava document_files "introduction.tex" "root.bib" "root.tex" session "HOL-NanoJava" in NanoJava = HOL + description " Hoare Logic for a tiny fragment of Java. " theories Example document_files "root.bib" "root.tex" session "HOL-Bali" (timing) in Bali = HOL + sessions "HOL-Library" theories AxExample AxSound AxCompl Trans TypeSafe document_files "root.tex" session "HOL-IOA" in IOA = HOL + description \ Author: Tobias Nipkow and Konrad Slind and Olaf Müller Copyright 1994--1996 TU Muenchen The meta-theory of I/O-Automata in HOL. This formalization has been significantly changed and extended, see HOLCF/IOA. There are also the proofs of two communication protocols which formerly have been here. @inproceedings{Nipkow-Slind-IOA, author={Tobias Nipkow and Konrad Slind}, title={{I/O} Automata in {Isabelle/HOL}}, booktitle={Proc.\ TYPES Workshop 1994}, publisher=Springer, series=LNCS, note={To appear}} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz and @inproceedings{Mueller-Nipkow, author={Olaf M\"uller and Tobias Nipkow}, title={Combining Model Checking and Deduction for {I/O}-Automata}, booktitle={Proc.\ TACAS Workshop}, organization={Aarhus University, BRICS report}, year=1995} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz \ theories Solve session "HOL-Lattice" in Lattice = HOL + description " Author: Markus Wenzel, TU Muenchen Basic theory of lattices and orders. " theories CompleteLattice document_files "root.tex" session "HOL-ex" (timing) in ex = "HOL-Number_Theory" + description " Miscellaneous examples for Higher-Order Logic. " theories Antiquote Argo_Examples Arith_Examples Ballot BinEx Birthday_Paradox Bit_Lists Bubblesort CTL Cartouche_Examples Case_Product Chinese Classical Code_Binary_Nat_examples Code_Lazy_Demo Code_Timing Coercion_Examples Computations Conditional_Parametricity_Examples Cubic_Quartic Datatype_Record_Examples Dedekind_Real Erdoes_Szekeres Eval_Examples Executable_Relation Execute_Choice Functions Function_Growth Gauge_Integration Guess HarmonicSeries Hebrew Hex_Bin_Examples IArray_Examples Intuitionistic Join_Theory Lagrange List_to_Set_Comprehension_Examples LocaleTest2 MergeSort MonoidGroup Multiquote NatSum Normalization_by_Evaluation PER Parallel_Example Peano_Axioms Perm_Fragments PresburgerEx Primrec Pythagoras Quicksort Radix_Sort Reflection_Examples Refute_Examples Residue_Ring Rewrite_Examples SOS SOS_Cert Serbian Set_Comprehension_Pointfree_Examples Set_Theory Simproc_Tests Simps_Case_Conv_Examples Sketch_and_Explore Sorting_Algorithms_Examples Specifications_with_bundle_mixins Sqrt Sqrt_Script Sudoku Sum_of_Powers Tarski Termination ThreeDivides Transfer_Debug Transfer_Int_Nat Transitive_Closure_Table_Ex Tree23 Triangular_Numbers Unification While_Combinator_Example veriT_Preprocessing theories [skip_proofs = false] SAT_Examples Meson_Test session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" + description " Miscellaneous Isabelle/Isar examples. " options [quick_and_dirty] sessions "HOL-Hoare" theories Structured_Statements Basic_Logic Expr_Compiler Fibonacci Group Group_Context Group_Notepad Hoare_Ex Mutilated_Checkerboard Puzzle Summation document_files "root.bib" "root.tex" session "HOL-Eisbach" in Eisbach = HOL + description \ The Eisbach proof method language and "match" method. \ sessions FOL "HOL-Analysis" theories Eisbach Tests Examples Examples_FOL Example_Metric session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL + description " Verification of the SET Protocol. " sessions "HOL-Library" theories SET_Protocol document_files "root.tex" session "HOL-Matrix_LP" in Matrix_LP = HOL + description " Two-dimensional matrices and linear programming. " sessions "HOL-Library" directories "Compute_Oracle" theories Cplex document_files "root.tex" session "HOL-TLA" in TLA = HOL + description " Lamport's Temporal Logic of Actions. " theories TLA session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" + theories Inc session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" + theories DBuffer session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" + theories MemoryImplementation session "HOL-TPTP" in TPTP = HOL + description " Author: Jasmin Blanchette, TU Muenchen Author: Nik Sultana, University of Cambridge Copyright 2011 TPTP-related extensions. " sessions "HOL-Library" theories ATP_Theory_Export MaSh_Eval TPTP_Interpret THF_Arith TPTP_Proof_Reconstruction theories ATP_Problem_Import session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" + theories Probability document_files "root.tex" session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" + theories Dining_Cryptographers Koepf_Duermuth_Countermeasure Measure_Not_CCC session "HOL-Nominal" in Nominal = HOL + sessions "HOL-Library" theories Nominal session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" + theories Class3 CK_Machine Compile Contexts Crary CR_Takahashi CR Fsub Height Lambda_mu Lam_Funs LocalWeakening Pattern SN SOS Standardization Support Type_Preservation Weakening W theories [quick_and_dirty] VC_Condition session "HOL-Cardinals" (timing) in Cardinals = HOL + description " Ordinals and Cardinals, Full Theories. " theories Cardinals Bounded_Set document_files "intro.tex" "root.tex" "root.bib" session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" + description " (Co)datatype Examples. " directories "Derivation_Trees" theories Compat Lambda_Term Process TreeFsetI "Derivation_Trees/Gram_Lang" "Derivation_Trees/Parallel_Composition" Koenig Lift_BNF Milner_Tofte Stream_Processor Cyclic_List Free_Idempotent_Monoid - LDL + Regex_ACI + Regex_ACIDZ TLList Misc_Codatatype Misc_Datatype Misc_Primcorec Misc_Primrec Datatype_Simproc_Tests session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" + description " Corecursion Examples. " directories "Tests" theories LFilter Paper_Examples Stream_Processor "Tests/Simple_Nesting" "Tests/Iterate_GPV" theories [quick_and_dirty] "Tests/GPV_Bare_Bones" "Tests/Merge_D" "Tests/Merge_Poly" "Tests/Misc_Mono" "Tests/Misc_Poly" "Tests/Small_Concrete" "Tests/Stream_Friends" "Tests/TLList_Friends" "Tests/Type_Class" session "HOL-Statespace" in Statespace = HOL + theories [skip_proofs = false] StateSpaceEx document_files "root.tex" session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" + description " Nonstandard analysis. " theories Nonstandard_Analysis document_files "root.tex" session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" + theories NSPrimes session "HOL-Mirabelle" in Mirabelle = HOL + theories Mirabelle_Test session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" + options [timeout = 60] theories Ex session "HOL-SMT_Examples" (timing) in SMT_Examples = HOL + options [quick_and_dirty] sessions "HOL-Library" theories Boogie SMT_Examples SMT_Word_Examples SMT_Tests SMT_Tests_Verit SMT_Examples_Verit session "HOL-SPARK" in "SPARK" = HOL + sessions "HOL-Library" theories SPARK session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" + directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt" theories "Gcd/Greatest_Common_Divisor" "Liseq/Longest_Increasing_Subsequence" "RIPEMD-160/F" "RIPEMD-160/Hash" "RIPEMD-160/K_L" "RIPEMD-160/K_R" "RIPEMD-160/R_L" "RIPEMD-160/Round" "RIPEMD-160/R_R" "RIPEMD-160/S_L" "RIPEMD-160/S_R" "Sqrt/Sqrt" export_files (in ".") "*:**.prv" session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" + options [show_question_marks = false] sessions "HOL-Library" "HOL-SPARK-Examples" theories Example_Verification VC_Principles Reference Complex_Types document_theories "HOL-SPARK-Examples.Greatest_Common_Divisor" document_files "complex_types.ads" "complex_types_app.adb" "complex_types_app.ads" "Gcd.adb" "Gcd.ads" "intro.tex" "loop_invariant.adb" "loop_invariant.ads" "root.bib" "root.tex" "Simple_Gcd.adb" "Simple_Gcd.ads" session "HOL-Mutabelle" in Mutabelle = HOL + sessions "HOL-Library" theories MutabelleExtra session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL + sessions "HOL-Library" theories Quickcheck_Examples Quickcheck_Lattice_Examples Completeness Quickcheck_Interfaces Quickcheck_Nesting_Example theories [condition = ISABELLE_GHC] Hotel_Example Quickcheck_Narrowing_Examples session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" + description " Author: Cezary Kaliszyk and Christian Urban " theories DList Quotient_FSet Quotient_Int Quotient_Message Lift_FSet Lift_Set Lift_Fun Quotient_Rat Lift_DList Int_Pow Lifting_Code_Dt_Test session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL + sessions "HOL-Library" theories Examples Predicate_Compile_Tests Predicate_Compile_Quickcheck_Examples Specialisation_Examples IMP_1 IMP_2 (* FIXME since 21-Jul-2011 Hotel_Example_Small_Generator *) IMP_3 IMP_4 theories [condition = ISABELLE_SWIPL] Code_Prolog_Examples Context_Free_Grammar_Example Hotel_Example_Prolog Lambda_Example List_Examples theories [condition = ISABELLE_SWIPL, quick_and_dirty] Reg_Exp_Example session "HOL-Types_To_Sets" in Types_To_Sets = HOL + description " Experimental extension of Higher-Order Logic to allow translation of types to sets. " directories "Examples" theories Types_To_Sets "Examples/Prerequisites" "Examples/Finite" "Examples/T2_Spaces" "Examples/Unoverload_Def" "Examples/Linear_Algebra_On" session HOLCF (main timing) in HOLCF = HOL + description " Author: Franz Regensburger Author: Brian Huffman HOLCF -- a semantic extension of HOL by the LCF logic. " sessions "HOL-Library" theories HOLCF (global) document_files "root.tex" session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF + theories Domain_ex Fixrec_ex New_Domain document_files "root.tex" session "HOLCF-Library" in "HOLCF/Library" = HOLCF + theories HOLCF_Library HOL_Cpo session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF + description " IMP -- A WHILE-language and its Semantics. This is the HOLCF-based denotational semantics of a simple WHILE-language. " sessions "HOL-IMP" theories HoareEx document_files "isaverbatimwrite.sty" "root.tex" "root.bib" session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" + description " Miscellaneous examples for HOLCF. " theories Dnat Dagstuhl Focus_ex Fix2 Hoare Concurrency_Monad Loop Powerdomain_ex Domain_Proofs Letrec Pattern_Match session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" + description \ FOCUS: a theory of stream-processing functions Isabelle/HOLCF. For introductions to FOCUS, see "The Design of Distributed Systems - An Introduction to FOCUS" http://www4.in.tum.de/publ/html.php?e=2 "Specification and Refinement of a Buffer of Length One" http://www4.in.tum.de/publ/html.php?e=15 "Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321 \ theories Fstreams FOCUS Buffer_adm session IOA (timing) in "HOLCF/IOA" = HOLCF + description " Author: Olaf Müller Copyright 1997 TU München A formalization of I/O automata in HOLCF. The distribution contains simulation relations, temporal logic, and an abstraction theory. Everything is based upon a domain-theoretic model of finite and infinite sequences. " theories Abstraction session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA + description " Author: Olaf Müller The Alternating Bit Protocol performed in I/O-Automata: combining IOA with Model Checking. Theory Correctness contains the proof of the abstraction from unbounded channels to finite ones. File Check.ML contains a simple ModelChecker prototype checking Spec against the finite version of the ABP-protocol. " theories Correctness Spec session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA + description " Author: Tobias Nipkow & Konrad Slind A network transmission protocol, performed in the I/O automata formalization by Olaf Müller. " theories Overview Correctness session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA + description " Author: Olaf Müller Memory storage case study. " theories Correctness session "IOA-ex" in "HOLCF/IOA/ex" = IOA + description " Author: Olaf Müller " theories TrivEx TrivEx2