FSet: stronger fact in Isabelle.
theory FSet3+ −
imports "../../../Nominal/FSet"+ −
begin+ −
+ −
(* 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+ −
*}+ −
+ −
+ −
(* NEEDS FIXING *)+ −
(* 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 *)+ −
+ −
+ −
end+ −