add fixrec support for HOL pair constructor patterns
authorhuffman
Mon Nov 02 18:39:41 2009 -0800 (2009-11-02)
changeset 33401fc43fa403a69
parent 33400 7c4ab69a15c3
child 33402 d9a25a87da4a
add fixrec support for HOL pair constructor patterns
src/HOLCF/Fixrec.thy
src/HOLCF/Tools/fixrec.ML
src/HOLCF/ex/Fixrec_ex.thy
     1.1 --- a/src/HOLCF/Fixrec.thy	Mon Nov 02 17:29:34 2009 -0800
     1.2 +++ b/src/HOLCF/Fixrec.thy	Mon Nov 02 18:39:41 2009 -0800
     1.3 @@ -526,7 +526,8 @@
     1.4  
     1.5  lemma match_cpair_simps [simp]:
     1.6    "match_cpair\<cdot>\<langle>x, y\<rangle>\<cdot>k = k\<cdot>x\<cdot>y"
     1.7 -by (simp add: match_cpair_def)
     1.8 +  "match_cpair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
     1.9 +by (simp_all add: match_cpair_def)
    1.10  
    1.11  lemma match_spair_simps [simp]:
    1.12    "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x, y:)\<cdot>k = k\<cdot>x\<cdot>y"
    1.13 @@ -610,6 +611,7 @@
    1.14        (@{const_name sinr}, @{const_name match_sinr}),
    1.15        (@{const_name spair}, @{const_name match_spair}),
    1.16        (@{const_name cpair}, @{const_name match_cpair}),
    1.17 +      (@{const_name Pair}, @{const_name match_cpair}),
    1.18        (@{const_name ONE}, @{const_name match_ONE}),
    1.19        (@{const_name TT}, @{const_name match_TT}),
    1.20        (@{const_name FF}, @{const_name match_FF}),
     2.1 --- a/src/HOLCF/Tools/fixrec.ML	Mon Nov 02 17:29:34 2009 -0800
     2.2 +++ b/src/HOLCF/Tools/fixrec.ML	Mon Nov 02 18:39:41 2009 -0800
     2.3 @@ -36,20 +36,9 @@
     2.4  
     2.5  infixr 6 ->>; val (op ->>) = cfunT;
     2.6  
     2.7 -fun cfunsT (Ts, U) = List.foldr cfunT U Ts;
     2.8 -
     2.9  fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
    2.10    | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
    2.11  
    2.12 -fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
    2.13 -  | binder_cfun _   =  [];
    2.14 -
    2.15 -fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
    2.16 -  | body_cfun T   =  T;
    2.17 -
    2.18 -fun strip_cfun T : typ list * typ =
    2.19 -  (binder_cfun T, body_cfun T);
    2.20 -
    2.21  fun maybeT T = Type(@{type_name "maybe"}, [T]);
    2.22  
    2.23  fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T
    2.24 @@ -59,9 +48,27 @@
    2.25    | tupleT [T] = T
    2.26    | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
    2.27  
    2.28 +local
    2.29 +
    2.30 +fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
    2.31 +  | binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U
    2.32 +  | binder_cfun _   =  [];
    2.33 +
    2.34 +fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
    2.35 +  | body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U
    2.36 +  | body_cfun T   =  T;
    2.37 +
    2.38 +fun strip_cfun T : typ list * typ =
    2.39 +  (binder_cfun T, body_cfun T);
    2.40 +
    2.41 +fun cfunsT (Ts, U) = List.foldr cfunT U Ts;
    2.42 +
    2.43 +in
    2.44 +
    2.45  fun matchT (T, U) =
    2.46    body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
    2.47  
    2.48 +end
    2.49  
    2.50  (*************************************************************************)
    2.51  (***************************** building terms ****************************)
    2.52 @@ -235,10 +242,16 @@
    2.53    | Const(@{const_name Rep_CFun},_)$f$x =>
    2.54        let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
    2.55        in pre_build match_name f rhs' (v::vs) taken' end
    2.56 +  | f$(v as Free(n,T)) =>
    2.57 +      pre_build match_name f rhs (v::vs) taken
    2.58 +  | f$x =>
    2.59 +      let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
    2.60 +      in pre_build match_name f rhs' (v::vs) taken' end
    2.61    | Const(c,T) =>
    2.62        let
    2.63          val n = Name.variant taken "v";
    2.64          fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
    2.65 +          | result_type (Type (@{type_name "fun"},[_,T])) (x::xs) = result_type T xs
    2.66            | result_type T _ = T;
    2.67          val v = Free(n, result_type T vs);
    2.68          val m = Const(match_name c, matchT (T, fastype_of rhs));
     3.1 --- a/src/HOLCF/ex/Fixrec_ex.thy	Mon Nov 02 17:29:34 2009 -0800
     3.2 +++ b/src/HOLCF/ex/Fixrec_ex.thy	Mon Nov 02 18:39:41 2009 -0800
     3.3 @@ -31,6 +31,11 @@
     3.4  fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
     3.5  where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
     3.6  
     3.7 +text {* Fixrec also works with the HOL pair constructor. *}
     3.8 +
     3.9 +fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b"
    3.10 +where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)"
    3.11 +
    3.12  
    3.13  subsection {* Examples using @{text fixpat} *}
    3.14