Proper context fixes lifting inside instantiations.
theory FSet3+ −
imports "../QuotMain" "../QuotList" List+ −
begin+ −
+ −
ML {*+ −
structure QuotientRules = Named_Thms+ −
(val name = "quot_thm"+ −
val description = "Quotient theorems.")+ −
*}+ −
+ −
ML {*+ −
open QuotientRules+ −
*}+ −
+ −
fun+ −
list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)+ −
where+ −
"list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)"+ −
+ −
lemma list_eq_equivp:+ −
shows "equivp list_eq"+ −
unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def+ −
by auto+ −
+ −
(* FIXME-TODO: because of beta-reduction, one cannot give the *)+ −
(* FIXME-TODO: relation as a term or abbreviation *) + −
quotient_type + −
'a fset = "'a list" / "list_eq"+ −
by (rule list_eq_equivp)+ −
+ −
+ −
section {* empty fset, finsert and membership *} + −
+ −
quotient_definition+ −
"fempty :: 'a fset" ("{||}")+ −
as "[]::'a list"+ −
+ −
quotient_definition+ −
"finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" + −
as "op #"+ −
+ −
syntax+ −
"@Finset" :: "args => 'a fset" ("{|(_)|}")+ −
+ −
translations+ −
"{|x, xs|}" == "CONST finsert x {|xs|}"+ −
"{|x|}" == "CONST finsert x {||}"+ −
+ −
definition + −
memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"+ −
where+ −
"memb x xs \<equiv> x \<in> set xs"+ −
+ −
quotient_definition+ −
"fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<in>| _" [50, 51] 50)+ −
as "memb"+ −
+ −
abbreviation+ −
fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)+ −
where+ −
"a |\<notin>| S \<equiv> \<not>(a |\<in>| S)"+ −
+ −
lemma memb_rsp[quot_respect]: + −
shows "(op = ===> op \<approx> ===> op =) memb memb"+ −
by (auto simp add: memb_def)+ −
+ −
lemma nil_rsp[quot_respect]:+ −
shows "[] \<approx> []"+ −
by simp+ −
+ −
lemma cons_rsp[quot_respect]: + −
shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"+ −
by simp+ −
+ −
+ −
section {* Augmenting a set -- @{const finsert} *}+ −
+ −
text {* raw section *}+ −
+ −
lemma nil_not_cons:+ −
shows "\<not>[] \<approx> x # xs"+ −
by auto+ −
+ −
lemma memb_cons_iff:+ −
shows "memb x (y # xs) = (x = y \<or> memb x xs)"+ −
by (induct xs) (auto simp add: memb_def)+ −
+ −
lemma memb_consI1:+ −
shows "memb x (x # xs)"+ −
by (simp add: memb_def)+ −
+ −
lemma memb_consI2:+ −
shows "memb x xs \<Longrightarrow> memb x (y # xs)"+ −
by (simp add: memb_def)+ −
+ −
lemma memb_absorb:+ −
shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"+ −
by (induct xs) (auto simp add: memb_def id_simps)+ −
+ −
text {* lifted section *}+ −
+ −
lemma fin_finsert_iff[simp]:+ −
"x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"+ −
by (lifting memb_cons_iff) + −
+ −
lemma+ −
shows finsertI1: "x |\<in>| finsert x S"+ −
and finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"+ −
by (lifting memb_consI1, lifting memb_consI2)+ −
+ −
+ −
lemma finsert_absorb [simp]: + −
shows "x |\<in>| S \<Longrightarrow> finsert x S = S"+ −
by (lifting memb_absorb)+ −
+ −
+ −
section {* Singletons *}+ −
+ −
text {* raw section *}+ −
+ −
lemma singleton_list_eq:+ −
shows "[x] \<approx> [y] \<longleftrightarrow> x = y"+ −
by (simp add: id_simps) auto+ −
+ −
text {* lifted section *}+ −
+ −
lemma fempty_not_finsert[simp]:+ −
shows "{||} \<noteq> finsert x S"+ −
by (lifting nil_not_cons)+ −
+ −
lemma fsingleton_eq[simp]:+ −
shows "{|x|} = {|y|} \<longleftrightarrow> x = y"+ −
by (lifting singleton_list_eq)+ −
+ −
section {* Union *}+ −
+ −
quotient_definition+ −
"funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65)+ −
as+ −
"op @"+ −
+ −
section {* Cardinality of finite sets *}+ −
+ −
fun+ −
fcard_raw :: "'a list \<Rightarrow> nat"+ −
where+ −
fcard_raw_nil: "fcard_raw [] = 0"+ −
| fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"+ −
+ −
quotient_definition+ −
"fcard :: 'a fset \<Rightarrow> nat" + −
as "fcard_raw"+ −
+ −
text {* raw section *}+ −
+ −
lemma fcard_raw_ge_0:+ −
assumes a: "x \<in> set xs"+ −
shows "0 < fcard_raw xs"+ −
using a+ −
by (induct xs) (auto simp add: memb_def)+ −
+ −
lemma fcard_raw_delete_one:+ −
"fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"+ −
by (induct xs) (auto dest: fcard_raw_ge_0 simp add: memb_def)+ −
+ −
lemma fcard_raw_rsp_aux:+ −
assumes a: "a \<approx> b"+ −
shows "fcard_raw a = fcard_raw b"+ −
using a+ −
apply(induct a arbitrary: b)+ −
apply(auto simp add: memb_def)+ −
apply(metis)+ −
apply(drule_tac x="[x \<leftarrow> b. x \<noteq> a1]" in meta_spec)+ −
apply(simp add: fcard_raw_delete_one)+ −
apply(metis Suc_pred' fcard_raw_ge_0 fcard_raw_delete_one memb_def)+ −
done+ −
+ −
lemma fcard_raw_rsp[quot_respect]:+ −
"(op \<approx> ===> op =) fcard_raw fcard_raw"+ −
by (simp add: fcard_raw_rsp_aux)+ −
+ −
text {* lifted section *}+ −
+ −
lemma fcard_fempty [simp]:+ −
shows "fcard {||} = 0"+ −
by (lifting fcard_raw_nil)+ −
+ −
lemma fcard_finsert_if [simp]:+ −
shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"+ −
by (lifting fcard_raw_cons)+ −
+ −
+ −
section {* Induction and Cases rules for finite sets *}+ −
+ −
lemma fset_exhaust[case_names fempty finsert, cases type: fset]:+ −
shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"+ −
by (lifting list.exhaust)+ −
+ −
lemma fset_induct[case_names fempty finsert]:+ −
shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"+ −
by (lifting list.induct)+ −
+ −
lemma fset_induct2[case_names fempty finsert, induct type: fset]:+ −
assumes prem1: "P {||}" + −
and prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"+ −
shows "P S"+ −
proof(induct S rule: fset_induct)+ −
case fempty+ −
show "P {||}" by (rule prem1)+ −
next+ −
case (finsert x S)+ −
have asm: "P S" by fact+ −
show "P (finsert x S)"+ −
proof(cases "x |\<in>| S")+ −
case True+ −
have "x |\<in>| S" by fact+ −
then show "P (finsert x S)" using asm by simp+ −
next+ −
case False+ −
have "x |\<notin>| S" by fact+ −
then show "P (finsert x S)" using prem2 asm by simp+ −
qed+ −
qed+ −
+ −
+ −
section {* fmap and fset comprehension *}+ −
+ −
quotient_definition+ −
"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"+ −
as+ −
"map"+ −
+ −
quotient_definition+ −
"fconcat :: ('a fset) fset => 'a fset"+ −
as+ −
"concat"+ −
+ −
(*lemma fconcat_rsp[quot_respect]:+ −
shows "((list_rel op \<approx>) ===> op \<approx>) concat concat"+ −
apply(auto)+ −
sorry+ −
*)+ −
+ −
(* PROBLEM: these lemmas needs to be restated, since *)+ −
(* concat.simps(1) and concat.simps(2) contain the *)+ −
(* type variables ?'a1.0 (which are turned into frees *)+ −
(* 'a_1 *)+ −
lemma concat1:+ −
shows "concat [] \<approx> []"+ −
by (simp add: id_simps)+ −
+ −
lemma concat2:+ −
shows "concat (x # xs) \<approx> x @ concat xs"+ −
by (simp add: id_simps)+ −
+ −
lemma concat_rsp[quot_respect]:+ −
shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"+ −
sorry+ −
+ −
lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"+ −
apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)+ −
done+ −
+ −
lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"+ −
apply (rule eq_reflection)+ −
apply auto+ −
done+ −
+ −
lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"+ −
unfolding list_eq.simps+ −
apply(simp only: set_map set_in_eq)+ −
done+ −
+ −
lemma quotient_compose_list_pre:+ −
"(list_rel op \<approx> OOO op \<approx>) r s =+ −
((list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s \<and>+ −
abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"+ −
apply rule+ −
apply rule+ −
apply rule+ −
apply (rule list_rel_refl)+ −
apply (metis equivp_def fset_equivp)+ −
apply rule+ −
apply (rule equivp_reflp[OF fset_equivp])+ −
apply (rule list_rel_refl)+ −
apply (metis equivp_def fset_equivp)+ −
apply(rule)+ −
apply rule+ −
apply (rule list_rel_refl)+ −
apply (metis equivp_def fset_equivp)+ −
apply rule+ −
apply (rule equivp_reflp[OF fset_equivp])+ −
apply (rule list_rel_refl)+ −
apply (metis equivp_def fset_equivp)+ −
apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")+ −
apply (metis Quotient_rel[OF Quotient_fset])+ −
apply (auto simp only:)[1]+ −
apply (subgoal_tac "map abs_fset r = map abs_fset b")+ −
prefer 2+ −
apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])+ −
apply (subgoal_tac "map abs_fset s = map abs_fset ba")+ −
prefer 2+ −
apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])+ −
apply (simp only: map_rel_cong)+ −
apply rule+ −
apply (rule rep_abs_rsp[of "list_rel op \<approx>" "map abs_fset"])+ −
apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})+ −
apply (rule list_rel_refl)+ −
apply (metis equivp_def fset_equivp)+ −
apply rule+ −
prefer 2+ −
apply (rule rep_abs_rsp_left[of "list_rel op \<approx>" "map abs_fset"])+ −
apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})+ −
apply (rule list_rel_refl)+ −
apply (metis equivp_def fset_equivp)+ −
apply (erule conjE)++ −
apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")+ −
prefer 2+ −
apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp)+ −
apply (rule map_rel_cong)+ −
apply (assumption)+ −
done+ −
+ −
lemma quotient_compose_list[quot_thm]:+ −
shows "Quotient ((list_rel op \<approx>) OOO (op \<approx>))+ −
(abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"+ −
unfolding Quotient_def comp_def+ −
apply (rule)++ −
apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset])+ −
apply (rule)+ −
apply (rule)+ −
apply (rule)+ −
apply (rule list_rel_refl)+ −
apply (metis equivp_def fset_equivp)+ −
apply (rule)+ −
apply (rule equivp_reflp[OF fset_equivp])+ −
apply (rule list_rel_refl)+ −
apply (metis equivp_def fset_equivp)+ −
apply rule+ −
apply rule+ −
apply(rule quotient_compose_list_pre)+ −
done+ −
+ −
lemma fconcat_empty:+ −
shows "fconcat {||} = {||}"+ −
apply(lifting concat1)+ −
apply(cleaning)+ −
apply(simp add: comp_def)+ −
apply(fold fempty_def[simplified id_simps])+ −
apply(rule refl)+ −
done+ −
+ −
(* Should be true *)+ −
+ −
lemma insert_rsp2[quot_respect]:+ −
"(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #"+ −
apply auto+ −
apply (simp add: set_in_eq)+ −
sorry+ −
+ −
lemma append_rsp[quot_respect]:+ −
"(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"+ −
by (auto)+ −
+ −
lemma fconcat_insert:+ −
shows "fconcat (finsert x S) = x |\<union>| fconcat S"+ −
apply(lifting concat2)+ −
apply(cleaning)+ −
apply (simp add: finsert_def fconcat_def comp_def)+ −
apply cleaning+ −
done+ −
+ −
text {* raw section *}+ −
+ −
lemma map_rsp_aux:+ −
assumes a: "a \<approx> b"+ −
shows "map f a \<approx> map f b"+ −
using a+ −
apply(induct a arbitrary: b)+ −
apply(auto)+ −
apply(metis rev_image_eqI)+ −
done+ −
+ −
lemma map_rsp[quot_respect]:+ −
shows "(op = ===> op \<approx> ===> op \<approx>) map map"+ −
by (auto simp add: map_rsp_aux)+ −
+ −
+ −
text {* lifted section *}+ −
+ −
(* TBD *)+ −
+ −
text {* syntax for fset comprehensions (adapted from lists) *}+ −
+ −
nonterminals fsc_qual fsc_quals+ −
+ −
syntax+ −
"_fsetcompr" :: "'a \<Rightarrow> fsc_qual \<Rightarrow> fsc_quals \<Rightarrow> 'a fset" ("{|_ . __")+ −
"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ <- _")+ −
"_fsc_test" :: "bool \<Rightarrow> fsc_qual" ("_")+ −
"_fsc_end" :: "fsc_quals" ("|}")+ −
"_fsc_quals" :: "fsc_qual \<Rightarrow> fsc_quals \<Rightarrow> fsc_quals" (", __")+ −
"_fsc_abs" :: "'a => 'b fset => 'b fset"+ −
+ −
syntax (xsymbols)+ −
"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")+ −
syntax (HTML output)+ −
"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")+ −
+ −
parse_translation (advanced) {*+ −
let+ −
val femptyC = Syntax.const @{const_name fempty};+ −
val finsertC = Syntax.const @{const_name finsert};+ −
val fmapC = Syntax.const @{const_name fmap};+ −
val fconcatC = Syntax.const @{const_name fconcat};+ −
val IfC = Syntax.const @{const_name If};+ −
fun fsingl x = finsertC $ x $ femptyC;+ −
+ −
fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)+ −
let+ −
val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);+ −
val e = if opti then fsingl e else e;+ −
val case1 = Syntax.const "_case1" $ p $ e;+ −
val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN+ −
$ femptyC;+ −
val cs = Syntax.const "_case2" $ case1 $ case2+ −
val ft = Datatype_Case.case_tr false Datatype.info_of_constr+ −
ctxt [x, cs]+ −
in lambda x ft end;+ −
+ −
fun abs_tr ctxt (p as Free(s,T)) e opti =+ −
let val thy = ProofContext.theory_of ctxt;+ −
val s' = Sign.intern_const thy s+ −
in if Sign.declared_const thy s'+ −
then (pat_tr ctxt p e opti, false)+ −
else (lambda p e, true)+ −
end+ −
| abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);+ −
+ −
fun fsc_tr ctxt [e, Const("_fsc_test",_) $ b, qs] =+ −
let + −
val res = case qs of + −
Const("_fsc_end",_) => fsingl e+ −
| Const("_fsc_quals",_)$ q $ qs => fsc_tr ctxt [e, q, qs];+ −
in + −
IfC $ b $ res $ femptyC + −
end+ −
+ −
| fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_end",_)] =+ −
(case abs_tr ctxt p e true of+ −
(f,true) => fmapC $ f $ es+ −
| (f, false) => fconcatC $ (fmapC $ f $ es))+ −
+ −
| fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_quals",_) $ q $ qs] =+ −
let+ −
val e' = fsc_tr ctxt [e, q, qs];+ −
in + −
fconcatC $ (fmapC $ (fst (abs_tr ctxt p e' false)) $ es) + −
end+ −
+ −
in [("_fsetcompr", fsc_tr)] end+ −
*}+ −
+ −
(* examles *)+ −
term "{|(x,y,z). b|}"+ −
term "{|x. x \<leftarrow> xs|}"+ −
term "{|(x,y,z). x\<leftarrow>xs|}"+ −
term "{|e x y. x\<leftarrow>xs, y\<leftarrow>ys|}"+ −
term "{|(x,y,z). x<a, x>b|}"+ −
term "{|(x,y,z). x\<leftarrow>xs, x>b|}"+ −
term "{|(x,y,z). x<a, x\<leftarrow>xs|}"+ −
term "{|(x,y). Cons True x \<leftarrow> xs|}"+ −
term "{|(x,y,z). Cons x [] \<leftarrow> xs|}"+ −
term "{|(x,y,z). x<a, x>b, x=d|}"+ −
term "{|(x,y,z). x<a, x>b, y\<leftarrow>ys|}"+ −
term "{|(x,y,z). x<a, x\<leftarrow>xs,y>b|}"+ −
term "{|(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys|}"+ −
term "{|(x,y,z). x\<leftarrow>xs, x>b, y<a|}"+ −
term "{|(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys|}"+ −
term "{|(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x|}"+ −
term "{|(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs|}"+ −
+ −
+ −
(* BELOW CONSTRUCTION SITE *)+ −
+ −
+ −
lemma no_mem_nil: + −
"(\<forall>a. a \<notin> set A) = (A = [])"+ −
by (induct A) (auto)+ −
+ −
lemma none_mem_nil: + −
"(\<forall>a. a \<notin> set A) = (A \<approx> [])"+ −
by simp+ −
+ −
lemma mem_cons: + −
"a \<in> set A \<Longrightarrow> a # A \<approx> A"+ −
by auto+ −
+ −
lemma cons_left_comm:+ −
"x # y # A \<approx> y # x # A"+ −
by (auto simp add: id_simps)+ −
+ −
lemma cons_left_idem:+ −
"x # x # A \<approx> x # A"+ −
by (auto simp add: id_simps)+ −
+ −
lemma finite_set_raw_strong_cases:+ −
"(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"+ −
apply (induct X)+ −
apply (simp)+ −
apply (rule disjI2)+ −
apply (erule disjE)+ −
apply (rule_tac x="a" in exI)+ −
apply (rule_tac x="[]" in exI)+ −
apply (simp)+ −
apply (erule exE)++ −
apply (case_tac "a = aa")+ −
apply (rule_tac x="a" in exI)+ −
apply (rule_tac x="Y" in exI)+ −
apply (simp)+ −
apply (rule_tac x="aa" in exI)+ −
apply (rule_tac x="a # Y" in exI)+ −
apply (auto)+ −
done+ −
+ −
fun+ −
delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"+ −
where+ −
"delete_raw [] x = []"+ −
| "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"+ −
+ −
lemma mem_delete_raw:+ −
"x \<in> set (delete_raw A a) = (x \<in> set A \<and> \<not>(x = a))"+ −
by (induct A arbitrary: x a) (auto)+ −
+ −
lemma mem_delete_raw_ident:+ −
"\<not>(a \<in> set (delete_raw A a))"+ −
by (induct A) (auto)+ −
+ −
lemma not_mem_delete_raw_ident:+ −
"b \<notin> set A \<Longrightarrow> (delete_raw A b = A)"+ −
by (induct A) (auto)+ −
+ −
lemma delete_raw_RSP:+ −
"A \<approx> B \<Longrightarrow> delete_raw A a \<approx> delete_raw B a"+ −
apply(induct A arbitrary: B a)+ −
apply(auto)+ −
sorry+ −
+ −
lemma cons_delete_raw:+ −
"a # (delete_raw A a) \<approx> (if a \<in> set A then A else (a # A))"+ −
sorry+ −
+ −
lemma mem_cons_delete_raw:+ −
"a \<in> set A \<Longrightarrow> a # (delete_raw A a) \<approx> A"+ −
sorry+ −
+ −
lemma finite_set_raw_delete_raw_cases:+ −
"X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"+ −
by (induct X) (auto)+ −
+ −
+ −
+ −
+ −
+ −
lemma list2set_thm:+ −
shows "set [] = {}"+ −
and "set (h # t) = insert h (set t)"+ −
by (auto)+ −
+ −
lemma list2set_RSP:+ −
"A \<approx> B \<Longrightarrow> set A = set B"+ −
by auto+ −
+ −
definition+ −
rsp_fold+ −
where+ −
"rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"+ −
+ −
primrec+ −
fold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"+ −
where+ −
"fold_raw f z [] = z"+ −
| "fold_raw f z (a # A) =+ −
(if (rsp_fold f) then+ −
if a mem A then fold_raw f z A+ −
else f a (fold_raw f z A)+ −
else z)"+ −
+ −
lemma mem_lcommuting_fold_raw:+ −
"rsp_fold f \<Longrightarrow> h mem B \<Longrightarrow> fold_raw f z B = f h (fold_raw f z (delete_raw B h))"+ −
sorry+ −
+ −
lemma fold_rsp[quot_respect]:+ −
"(op = ===> op = ===> op \<approx> ===> op =) fold_raw fold_raw"+ −
apply(auto)+ −
sorry+ −
+ −
primrec+ −
inter_raw+ −
where+ −
"inter_raw [] B = []"+ −
| "inter_raw (a # A) B = (if a mem B then a # inter_raw A B else inter_raw A B)"+ −
+ −
lemma mem_inter_raw:+ −
"x mem (inter_raw A B) = x mem A \<and> x mem B"+ −
sorry+ −
+ −
lemma inter_raw_RSP:+ −
"A1 \<approx> A2 \<and> B1 \<approx> B2 \<Longrightarrow> (inter_raw A1 B1) \<approx> (inter_raw A2 B2)"+ −
sorry+ −
+ −
+ −
(* LIFTING DEFS *)+ −
+ −
+ −
section {* Constants on the Quotient Type *} + −
+ −
+ −
quotient_definition+ −
"fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" + −
as "delete_raw"+ −
+ −
quotient_definition+ −
"finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)+ −
as "inter_raw"+ −
+ −
quotient_definition+ −
"ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" + −
as "fold_raw"+ −
+ −
quotient_definition+ −
"fset_to_set :: 'a fset \<Rightarrow> 'a set" + −
as "set"+ −
+ −
+ −
section {* Lifted Theorems *}+ −
+ −
thm list.cases (* ??? *)+ −
+ −
thm cons_left_comm+ −
lemma "finsert a (finsert b S) = finsert b (finsert a S)"+ −
by (lifting cons_left_comm)+ −
+ −
thm cons_left_idem+ −
lemma "finsert a (finsert a S) = finsert a S"+ −
by (lifting cons_left_idem)+ −
+ −
(* thm MEM:+ −
MEM x [] = F+ −
MEM x (h::t) = (x=h) \/ MEM x t *)+ −
thm none_mem_nil+ −
(*lemma "(\<forall>a. a \<notin>f A) = (A = fempty)"*)+ −
+ −
thm mem_cons+ −
thm finite_set_raw_strong_cases+ −
(*thm card_raw.simps*)+ −
(*thm not_mem_card_raw*)+ −
(*thm card_raw_suc*)+ −
+ −
lemma "fcard X = Suc n \<Longrightarrow> (\<exists>a S. a \<notin>f S & X = finsert a S)"+ −
(*by (lifting card_raw_suc)*)+ −
sorry+ −
+ −
(*thm card_raw_cons_gt_0+ −
thm mem_card_raw_gt_0+ −
thm not_nil_equiv_cons+ −
*)+ −
thm delete_raw.simps+ −
(*thm mem_delete_raw*)+ −
(*thm card_raw_delete_raw*)+ −
thm cons_delete_raw+ −
thm mem_cons_delete_raw+ −
thm finite_set_raw_delete_raw_cases+ −
thm append.simps+ −
(* MEM_APPEND: MEM e (APPEND l1 l2) = MEM e l1 \/ MEM e l2 *)+ −
thm inter_raw.simps+ −
thm mem_inter_raw+ −
thm fold_raw.simps+ −
thm list2set_thm+ −
thm list_eq_def+ −
thm list.induct+ −
lemma "\<lbrakk>P fempty; \<And>a x. P x \<Longrightarrow> P (finsert a x)\<rbrakk> \<Longrightarrow> P l"+ −
by (lifting list.induct)+ −
+ −
(* We also have map and some properties of it in FSet *)+ −
(* and the following which still lifts ok *)+ −
lemma "funion (funion x xa) xb = funion x (funion xa xb)"+ −
by (lifting append_assoc)+ −
+ −
quotient_definition+ −
"fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"+ −
as+ −
"list_case"+ −
+ −
(* NOT SURE IF TRUE *)+ −
lemma list_case_rsp[quot_respect]:+ −
"(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"+ −
apply (auto)+ −
sorry+ −
+ −
lemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa"+ −
apply (lifting list.cases(2))+ −
done+ −
+ −
thm quot_respect+ −
+ −
+ −
end+ −