added and refined some exmples
authorhaftmann
Tue Aug 29 14:31:14 2006 +0200 (2006-08-29)
changeset 204270b102b4182de
parent 20426 9ffea7a8b31c
child 20428 67fa1c6ba89e
added and refined some exmples
src/HOL/ex/Classpackage.thy
src/HOL/ex/CodeEval.thy
src/HOL/ex/CodeOperationalEquality.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/ex/Classpackage.thy	Tue Aug 29 14:31:13 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Tue Aug 29 14:31:14 2006 +0200
     1.3 @@ -288,15 +288,27 @@
     1.4    "\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>"
     1.5  using pow_def nat_pow_one inv_one by simp
     1.6  
     1.7 -instance group_prod_def: (group, group) * :: group
     1.8 +instance semigroup_prod_def: (semigroup, semigroup) * :: semigroup
     1.9    mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
    1.10                (x1 \<otimes> y1, x2 \<otimes> y2)"
    1.11 -  mult_one_def: "\<one> \<equiv> (\<one>, \<one>)"
    1.12 -  mult_inv_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
    1.13 -by default (simp_all add: split_paired_all group_prod_def assoc neutl invl)
    1.14 +by default (simp_all add: split_paired_all semigroup_prod_def assoc)
    1.15 +
    1.16 +instance monoidl_prod_def: (monoidl, monoidl) * :: monoidl
    1.17 +  one_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
    1.18 +by default (simp_all add: split_paired_all monoidl_prod_def neutl)
    1.19 +
    1.20 +instance monoid_prod_def: (monoid, monoid) * :: monoid
    1.21 +by default (simp_all add: split_paired_all monoid_prod_def neutr)
    1.22 +
    1.23 +instance monoid_comm_prod_def: (monoid_comm, monoid_comm) * :: monoid_comm
    1.24 +by default (simp_all add: split_paired_all monoidl_prod_def comm)
    1.25 +
    1.26 +instance group_prod_def: (group, group) * :: group
    1.27 +  inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
    1.28 +by default (simp_all add: split_paired_all group_prod_def invl)
    1.29  
    1.30  instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm
    1.31 -by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm)
    1.32 +by default (simp_all add: split_paired_all group_prod_def comm)
    1.33  
    1.34  definition
    1.35    "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/CodeEval.thy	Tue Aug 29 14:31:14 2006 +0200
     2.3 @@ -0,0 +1,211 @@
     2.4 +(*  ID:         $Id$
     2.5 +    Author:     Florian Haftmann, TU Muenchen
     2.6 +*)
     2.7 +
     2.8 +header {* A simple embedded term evaluation mechanism *}
     2.9 +
    2.10 +theory CodeEval
    2.11 +imports CodeEmbed
    2.12 +begin
    2.13 +
    2.14 +section {* A simple embedded term evaluation mechanism *}
    2.15 +
    2.16 +subsection {* The typ_of class *}
    2.17 +
    2.18 +class typ_of =
    2.19 +  fixes typ_of :: "'a option \<Rightarrow> typ"
    2.20 +
    2.21 +ML {*
    2.22 +structure TypOf =
    2.23 +struct
    2.24 +
    2.25 +local
    2.26 +  val thy = the_context ();
    2.27 +  val const_typ_of = Sign.intern_const thy "typ_of";
    2.28 +  val const_None = Sign.intern_const thy "None";
    2.29 +  fun typ_option ty = Type (Sign.intern_type (the_context ()) "option", [ty]);
    2.30 +  fun term_typ_of ty = Const (const_typ_of, typ_option ty --> Embed.typ_typ);
    2.31 +in
    2.32 +  val class_typ_of = Sign.intern_class thy "typ_of";
    2.33 +  fun term_typ_of_None ty =
    2.34 +    term_typ_of ty $ Const (const_None, typ_option ty);
    2.35 +  fun mk_typ_of_def ty =
    2.36 +    let
    2.37 +      val lhs = term_typ_of ty $ Free ("x", typ_option ty)
    2.38 +      val rhs = Embed.term_typ (fn v => term_typ_of_None (TFree v)) ty
    2.39 +    in Logic.mk_equals (lhs, rhs) end;
    2.40 +end;
    2.41 +
    2.42 +end;
    2.43 +*}
    2.44 +
    2.45 +setup {*
    2.46 +let
    2.47 +  fun mk _ arities _ =
    2.48 +    maps (fn ((tyco, asorts), _) => [(("", []), TypOf.mk_typ_of_def
    2.49 +      (Type (tyco, map TFree (Name.names Name.context "'a" asorts))))]) arities;
    2.50 +  fun tac _ = ClassPackage.intro_classes_tac [];
    2.51 +  fun hook specs =
    2.52 +    DatatypeCodegen.prove_codetypes_arities tac
    2.53 +      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
    2.54 +      [TypOf.class_typ_of] mk
    2.55 +in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
    2.56 +*}
    2.57 +
    2.58 +
    2.59 +subsection {* term_of class *}
    2.60 +
    2.61 +class term_of = typ_of +
    2.62 +  constrains typ_of :: "'a option \<Rightarrow> typ"
    2.63 +  fixes term_of :: "'a \<Rightarrow> term"
    2.64 +
    2.65 +ML {*
    2.66 +structure TermOf =
    2.67 +struct
    2.68 +
    2.69 +local
    2.70 +  val thy = the_context ();
    2.71 +  val const_term_of = Sign.intern_const thy "term_of";
    2.72 +  fun term_term_of ty = Const (const_term_of, ty --> Embed.typ_term);
    2.73 +in
    2.74 +  val class_term_of = Sign.intern_class thy "term_of";
    2.75 +  fun mk_terms_of_defs vs (tyco, cs) =
    2.76 +    let
    2.77 +      val dty = Type (tyco, map TFree vs);
    2.78 +      fun mk_eq c =
    2.79 +        let
    2.80 +          val lhs : term = term_term_of dty $ c;
    2.81 +          val rhs : term = Embed.term_term
    2.82 +            (fn (v, ty) => term_term_of ty $ Free (v, ty))
    2.83 +            (Embed.term_typ (fn (v, sort) => TypOf.term_typ_of_None (TFree (v, sort)))) c
    2.84 +        in
    2.85 +          HOLogic.mk_eq (lhs, rhs)
    2.86 +        end;
    2.87 +    in map mk_eq cs end;
    2.88 +  fun mk_term_of t =
    2.89 +    term_term_of (Term.fastype_of t) $ t;
    2.90 +end;
    2.91 +
    2.92 +end;
    2.93 +*}
    2.94 +
    2.95 +setup {*
    2.96 +let
    2.97 +  fun mk thy arities css =
    2.98 +    let
    2.99 +      val vs = (Name.names Name.context "'a" o snd o fst o hd) arities;
   2.100 +      val raw_defs = map (TermOf.mk_terms_of_defs vs) css;
   2.101 +      fun mk' thy' = map (apfst (rpair [])) ((PrimrecPackage.mk_combdefs thy' o flat) raw_defs)
   2.102 +    in ClassPackage.assume_arities_thy thy arities mk' end;
   2.103 +  fun tac _ = ClassPackage.intro_classes_tac [];
   2.104 +  fun hook specs =
   2.105 +    if (fst o hd) specs = (fst o dest_Type) Embed.typ_typ then I
   2.106 +    else
   2.107 +      DatatypeCodegen.prove_codetypes_arities tac
   2.108 +      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
   2.109 +      [TermOf.class_term_of] mk
   2.110 +in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
   2.111 +*}
   2.112 +
   2.113 +
   2.114 +subsection {* Evaluation infrastructure *}
   2.115 +
   2.116 +lemma lift_eq_Trueprop:
   2.117 +  "p == q \<Longrightarrow> Trueprop p == Trueprop q" by auto
   2.118 +
   2.119 +ML {*
   2.120 +signature EVAL =
   2.121 +sig
   2.122 +  val eval_term: term -> theory -> term * theory
   2.123 +  val eval_term' : theory -> term -> term
   2.124 +  val term: string -> unit
   2.125 +  val eval_ref: term ref
   2.126 +  val oracle: string * (theory * exn -> term)
   2.127 +  val method: Method.src -> Proof.context -> Method.method
   2.128 +end;
   2.129 +
   2.130 +structure Eval : EVAL =
   2.131 +struct
   2.132 +
   2.133 +val eval_ref = ref Logic.protectC;
   2.134 +
   2.135 +fun eval_term t =
   2.136 +  CodegenPackage.eval_term
   2.137 +    (("Eval.eval_ref", eval_ref), TermOf.mk_term_of t);
   2.138 +
   2.139 +fun eval_term' thy t =
   2.140 +  let
   2.141 +    val thy' = Theory.copy thy;
   2.142 +    val (t', _) = eval_term t thy';
   2.143 +  in t' end;
   2.144 +
   2.145 +fun term t =
   2.146 +  let
   2.147 +    val thy = the_context ();
   2.148 +    val t' = eval_term' thy (Sign.read_term thy t);
   2.149 +  in () end;
   2.150 +
   2.151 +val lift_eq_Trueprop = thm "lift_eq_Trueprop";
   2.152 +
   2.153 +exception Eval of term;
   2.154 +
   2.155 +val oracle = ("Eval", fn (thy, Eval t) =>
   2.156 +  Logic.mk_equals (t, eval_term' thy t));
   2.157 +
   2.158 +val oracle_name = NameSpace.pack [Context.theory_name (the_context ()), fst oracle];
   2.159 +
   2.160 +
   2.161 +fun conv ct =
   2.162 +  let
   2.163 +    val {thy, t, ...} = rep_cterm ct;
   2.164 +    val t' = HOLogic.dest_Trueprop t;
   2.165 +    val thm' = Thm.invoke_oracle_i thy oracle_name (thy, Eval t');
   2.166 +  in
   2.167 +    lift_eq_Trueprop OF [thm']
   2.168 +  end;
   2.169 +
   2.170 +fun tac i = Tactical.PRIMITIVE (Drule.fconv_rule
   2.171 +  (Drule.goals_conv (equal i) conv));
   2.172 +
   2.173 +val method =
   2.174 +  Method.no_args (Method.METHOD (fn _ =>
   2.175 +    tac 1 THEN rtac TrueI 1));
   2.176 +
   2.177 +end;
   2.178 +*}
   2.179 +
   2.180 +setup {*
   2.181 +  Theory.add_oracle Eval.oracle
   2.182 +  #> Method.add_method ("eval", Eval.method, "solve goal by evaluation")
   2.183 +*}
   2.184 +
   2.185 +
   2.186 +subsection {* Small examples *}
   2.187 +
   2.188 +ML {* Eval.term "[]::nat list" *}
   2.189 +ML {* Eval.term "(Suc 2 + Suc 0) * Suc 3" *}
   2.190 +ML {* Eval.term "fst ([]::nat list, Suc 0) = []" *}
   2.191 +
   2.192 +text {* a fancy datatype *}
   2.193 +
   2.194 +datatype ('a, 'b) bair =
   2.195 +    Bair "'a\<Colon>order" 'b
   2.196 +  | Shift "('a, 'b) cair"
   2.197 +  | Dummy unit
   2.198 +and ('a, 'b) cair =
   2.199 +    Cair 'a 'b
   2.200 +
   2.201 +code_generate term_of
   2.202 +
   2.203 +ML {* Eval.term "Shift (Cair (4::nat) [Suc 0])" *}
   2.204 +
   2.205 +lemma
   2.206 +  "Suc 0 = 1" by eval
   2.207 +
   2.208 +lemma
   2.209 +  "rev [0, Suc 0, Suc 0] = [Suc 0, Suc 0, 0]" by eval
   2.210 +
   2.211 +lemma
   2.212 +  "fst (snd (fst ( ((Some (2::nat), (Suc 0, ())), [0::nat]) ))) = Suc 0" by eval
   2.213 +
   2.214 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/CodeOperationalEquality.thy	Tue Aug 29 14:31:14 2006 +0200
     3.3 @@ -0,0 +1,158 @@
     3.4 +(*  ID:         $Id$
     3.5 +    Author:     Florian Haftmann, TU Muenchen
     3.6 +*)
     3.7 +
     3.8 +header {* Operational equality for code generation *}
     3.9 +
    3.10 +theory CodeOperationalEquality
    3.11 +imports Main
    3.12 +begin
    3.13 +
    3.14 +section {* Operational equality for code generation *}
    3.15 +
    3.16 +subsection {* eq class *}
    3.17 +
    3.18 +class eq =
    3.19 +  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    3.20 +
    3.21 +defs
    3.22 +  eq_def: "eq x y == (x = y)"
    3.23 +
    3.24 +ML {*
    3.25 +local
    3.26 +  val thy = the_context ();
    3.27 +  val const_eq = Sign.intern_const thy "eq";
    3.28 +  val type_bool = Type (Sign.intern_type thy "bool", []);
    3.29 +in
    3.30 +  val eq_def_sym = Thm.symmetric (thm "eq_def");
    3.31 +  val class_eq = Sign.intern_class thy "eq";
    3.32 +end
    3.33 +*}
    3.34 +
    3.35 +
    3.36 +subsection {* preprocessor *}
    3.37 +
    3.38 +ML {*
    3.39 +fun constrain_op_eq thy thms =
    3.40 +  let
    3.41 +    fun dest_eq (Const ("op =", ty)) =
    3.42 +          (SOME o hd o fst o strip_type) ty
    3.43 +      | dest_eq _ = NONE
    3.44 +    fun eqs_of t =
    3.45 +      fold_aterms (fn t => case dest_eq t
    3.46 +       of SOME (TVar v_sort) => cons v_sort
    3.47 +        | _ => I) t [];
    3.48 +    val eqs = maps (eqs_of o Thm.prop_of) thms;
    3.49 +    val instT = map (fn (v_i, sort) =>
    3.50 +      (Thm.ctyp_of thy (TVar (v_i, sort)),
    3.51 +         Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
    3.52 +  in
    3.53 +    thms
    3.54 +    |> map (Thm.instantiate (instT, []))
    3.55 +  end;
    3.56 +*}
    3.57 +
    3.58 +
    3.59 +subsection {* codetypes hook *}
    3.60 +
    3.61 +setup {*
    3.62 +let
    3.63 +  fun add_eq_instance specs =
    3.64 +    DatatypeCodegen.prove_codetypes_arities
    3.65 +      (K (ClassPackage.intro_classes_tac []))
    3.66 +      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
    3.67 +      [class_eq] ((K o K o K) []);
    3.68 +  (* fun add_eq_thms dtco thy =
    3.69 +    let
    3.70 +      val thms =
    3.71 +        DatatypeCodegen.get_eq thy dtco
    3.72 +        |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
    3.73 +        |> constrain_op_eq thy
    3.74 +        |> map (Tactic.rewrite_rule [eq_def_sym])
    3.75 +    in fold CodegenTheorems.add_fun thms thy end; *)
    3.76 +  fun hook dtcos =
    3.77 +    add_eq_instance dtcos (* #> fold add_eq_thms dtcos *);
    3.78 +in
    3.79 +  DatatypeCodegen.add_codetypes_hook_bootstrap hook
    3.80 +end
    3.81 +*}
    3.82 +
    3.83 +
    3.84 +subsection {* extractor *}
    3.85 +
    3.86 +setup {*
    3.87 +let
    3.88 +  fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
    3.89 +   of SOME _ => DatatypeCodegen.get_eq thy tyco
    3.90 +    | NONE => case TypedefCodegen.get_triv_typedef thy tyco
    3.91 +       of SOME (_ ,(_, thm)) => [thm]
    3.92 +        | NONE => [];
    3.93 +  fun get_eq_thms_eq thy ("OperationalEquality.eq", ty) = (case strip_type ty
    3.94 +       of (Type (tyco, _) :: _, _) =>
    3.95 +             get_eq_thms thy tyco
    3.96 +        | _ => [])
    3.97 +    | get_eq_thms_eq _ _ = [];
    3.98 +in
    3.99 +  CodegenTheorems.add_fun_extr get_eq_thms_eq
   3.100 +end
   3.101 +*}
   3.102 +
   3.103 +
   3.104 +subsection {* integers *}
   3.105 +
   3.106 +definition
   3.107 +  "eq_integer (k\<Colon>int) l = (k = l)"
   3.108 +
   3.109 +instance int :: eq ..
   3.110 +
   3.111 +lemma [code fun]:
   3.112 +  "eq k l = eq_integer k l"
   3.113 +unfolding eq_integer_def eq_def ..
   3.114 +
   3.115 +code_constapp eq_integer
   3.116 +  ml (infixl 6 "=")
   3.117 +  haskell (infixl 4 "==")
   3.118 +
   3.119 +
   3.120 +subsection {* codegenerator setup *}
   3.121 +
   3.122 +setup {*
   3.123 +  CodegenTheorems.add_preproc constrain_op_eq
   3.124 +*}
   3.125 +
   3.126 +declare eq_def [symmetric, code inline]
   3.127 +
   3.128 +
   3.129 +subsection {* haskell setup *}
   3.130 +
   3.131 +code_class eq
   3.132 +  haskell "Eq" (eq "(==)")
   3.133 +
   3.134 +code_instance
   3.135 +  (eq :: bool) haskell
   3.136 +  (eq :: unit) haskell
   3.137 +  (eq :: *) haskell
   3.138 +  (eq :: option) haskell
   3.139 +  (eq :: list) haskell
   3.140 +  (eq :: char) haskell
   3.141 +  (eq :: int) haskell
   3.142 +
   3.143 +code_constapp
   3.144 +  "eq"
   3.145 +    haskell (infixl 4 "==")
   3.146 +  "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   3.147 +    haskell (infixl 4 "==")
   3.148 +  "eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   3.149 +    haskell (infixl 4 "==")
   3.150 +  "eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   3.151 +    haskell (infixl 4 "==")
   3.152 +  "eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
   3.153 +    haskell (infixl 4 "==")
   3.154 +  "eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
   3.155 +    haskell (infixl 4 "==")
   3.156 +  "eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   3.157 +    haskell (infixl 4 "==")
   3.158 +  "eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   3.159 +    haskell (infixl 4 "==")
   3.160 +
   3.161 +end
   3.162 \ No newline at end of file
     4.1 --- a/src/HOL/ex/ROOT.ML	Tue Aug 29 14:31:13 2006 +0200
     4.2 +++ b/src/HOL/ex/ROOT.ML	Tue Aug 29 14:31:14 2006 +0200
     4.3 @@ -6,9 +6,9 @@
     4.4  
     4.5  no_document time_use_thy "Classpackage";
     4.6  no_document time_use_thy "Codegenerator";
     4.7 -no_document time_use_thy "CodeEmbed";
     4.8 +no_document time_use_thy "CodeOperationalEquality";
     4.9 +no_document time_use_thy "CodeEval";
    4.10  no_document time_use_thy "CodeRandom";
    4.11 -no_document time_use_thy "CodeRevappl";
    4.12  
    4.13  time_use_thy "Higher_Order_Logic";
    4.14  time_use_thy "Abstract_NAT";