# HG changeset patch
# User haftmann
# Date 1156854674 -7200
# Node ID 0b102b4182defd4e170faf00d3fd9c89cd261bf0
# Parent  9ffea7a8b31c56765b083d9100ec3e88d6b407fe
added and refined some exmples

diff -r 9ffea7a8b31c -r 0b102b4182de src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Tue Aug 29 14:31:13 2006 +0200
+++ b/src/HOL/ex/Classpackage.thy	Tue Aug 29 14:31:14 2006 +0200
@@ -288,15 +288,27 @@
   "\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>"
 using pow_def nat_pow_one inv_one by simp
 
-instance group_prod_def: (group, group) * :: group
+instance semigroup_prod_def: (semigroup, semigroup) * :: semigroup
   mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
               (x1 \<otimes> y1, x2 \<otimes> y2)"
-  mult_one_def: "\<one> \<equiv> (\<one>, \<one>)"
-  mult_inv_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
-by default (simp_all add: split_paired_all group_prod_def assoc neutl invl)
+by default (simp_all add: split_paired_all semigroup_prod_def assoc)
+
+instance monoidl_prod_def: (monoidl, monoidl) * :: monoidl
+  one_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
+by default (simp_all add: split_paired_all monoidl_prod_def neutl)
+
+instance monoid_prod_def: (monoid, monoid) * :: monoid
+by default (simp_all add: split_paired_all monoid_prod_def neutr)
+
+instance monoid_comm_prod_def: (monoid_comm, monoid_comm) * :: monoid_comm
+by default (simp_all add: split_paired_all monoidl_prod_def comm)
+
+instance group_prod_def: (group, group) * :: group
+  inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
+by default (simp_all add: split_paired_all group_prod_def invl)
 
 instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm
-by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm)
+by default (simp_all add: split_paired_all group_prod_def comm)
 
 definition
   "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
diff -r 9ffea7a8b31c -r 0b102b4182de src/HOL/ex/CodeEval.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/CodeEval.thy	Tue Aug 29 14:31:14 2006 +0200
@@ -0,0 +1,211 @@
+(*  ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* A simple embedded term evaluation mechanism *}
+
+theory CodeEval
+imports CodeEmbed
+begin
+
+section {* A simple embedded term evaluation mechanism *}
+
+subsection {* The typ_of class *}
+
+class typ_of =
+  fixes typ_of :: "'a option \<Rightarrow> typ"
+
+ML {*
+structure TypOf =
+struct
+
+local
+  val thy = the_context ();
+  val const_typ_of = Sign.intern_const thy "typ_of";
+  val const_None = Sign.intern_const thy "None";
+  fun typ_option ty = Type (Sign.intern_type (the_context ()) "option", [ty]);
+  fun term_typ_of ty = Const (const_typ_of, typ_option ty --> Embed.typ_typ);
+in
+  val class_typ_of = Sign.intern_class thy "typ_of";
+  fun term_typ_of_None ty =
+    term_typ_of ty $ Const (const_None, typ_option ty);
+  fun mk_typ_of_def ty =
+    let
+      val lhs = term_typ_of ty $ Free ("x", typ_option ty)
+      val rhs = Embed.term_typ (fn v => term_typ_of_None (TFree v)) ty
+    in Logic.mk_equals (lhs, rhs) end;
+end;
+
+end;
+*}
+
+setup {*
+let
+  fun mk _ arities _ =
+    maps (fn ((tyco, asorts), _) => [(("", []), TypOf.mk_typ_of_def
+      (Type (tyco, map TFree (Name.names Name.context "'a" asorts))))]) arities;
+  fun tac _ = ClassPackage.intro_classes_tac [];
+  fun hook specs =
+    DatatypeCodegen.prove_codetypes_arities tac
+      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
+      [TypOf.class_typ_of] mk
+in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
+*}
+
+
+subsection {* term_of class *}
+
+class term_of = typ_of +
+  constrains typ_of :: "'a option \<Rightarrow> typ"
+  fixes term_of :: "'a \<Rightarrow> term"
+
+ML {*
+structure TermOf =
+struct
+
+local
+  val thy = the_context ();
+  val const_term_of = Sign.intern_const thy "term_of";
+  fun term_term_of ty = Const (const_term_of, ty --> Embed.typ_term);
+in
+  val class_term_of = Sign.intern_class thy "term_of";
+  fun mk_terms_of_defs vs (tyco, cs) =
+    let
+      val dty = Type (tyco, map TFree vs);
+      fun mk_eq c =
+        let
+          val lhs : term = term_term_of dty $ c;
+          val rhs : term = Embed.term_term
+            (fn (v, ty) => term_term_of ty $ Free (v, ty))
+            (Embed.term_typ (fn (v, sort) => TypOf.term_typ_of_None (TFree (v, sort)))) c
+        in
+          HOLogic.mk_eq (lhs, rhs)
+        end;
+    in map mk_eq cs end;
+  fun mk_term_of t =
+    term_term_of (Term.fastype_of t) $ t;
+end;
+
+end;
+*}
+
+setup {*
+let
+  fun mk thy arities css =
+    let
+      val vs = (Name.names Name.context "'a" o snd o fst o hd) arities;
+      val raw_defs = map (TermOf.mk_terms_of_defs vs) css;
+      fun mk' thy' = map (apfst (rpair [])) ((PrimrecPackage.mk_combdefs thy' o flat) raw_defs)
+    in ClassPackage.assume_arities_thy thy arities mk' end;
+  fun tac _ = ClassPackage.intro_classes_tac [];
+  fun hook specs =
+    if (fst o hd) specs = (fst o dest_Type) Embed.typ_typ then I
+    else
+      DatatypeCodegen.prove_codetypes_arities tac
+      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
+      [TermOf.class_term_of] mk
+in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
+*}
+
+
+subsection {* Evaluation infrastructure *}
+
+lemma lift_eq_Trueprop:
+  "p == q \<Longrightarrow> Trueprop p == Trueprop q" by auto
+
+ML {*
+signature EVAL =
+sig
+  val eval_term: term -> theory -> term * theory
+  val eval_term' : theory -> term -> term
+  val term: string -> unit
+  val eval_ref: term ref
+  val oracle: string * (theory * exn -> term)
+  val method: Method.src -> Proof.context -> Method.method
+end;
+
+structure Eval : EVAL =
+struct
+
+val eval_ref = ref Logic.protectC;
+
+fun eval_term t =
+  CodegenPackage.eval_term
+    (("Eval.eval_ref", eval_ref), TermOf.mk_term_of t);
+
+fun eval_term' thy t =
+  let
+    val thy' = Theory.copy thy;
+    val (t', _) = eval_term t thy';
+  in t' end;
+
+fun term t =
+  let
+    val thy = the_context ();
+    val t' = eval_term' thy (Sign.read_term thy t);
+  in () end;
+
+val lift_eq_Trueprop = thm "lift_eq_Trueprop";
+
+exception Eval of term;
+
+val oracle = ("Eval", fn (thy, Eval t) =>
+  Logic.mk_equals (t, eval_term' thy t));
+
+val oracle_name = NameSpace.pack [Context.theory_name (the_context ()), fst oracle];
+
+
+fun conv ct =
+  let
+    val {thy, t, ...} = rep_cterm ct;
+    val t' = HOLogic.dest_Trueprop t;
+    val thm' = Thm.invoke_oracle_i thy oracle_name (thy, Eval t');
+  in
+    lift_eq_Trueprop OF [thm']
+  end;
+
+fun tac i = Tactical.PRIMITIVE (Drule.fconv_rule
+  (Drule.goals_conv (equal i) conv));
+
+val method =
+  Method.no_args (Method.METHOD (fn _ =>
+    tac 1 THEN rtac TrueI 1));
+
+end;
+*}
+
+setup {*
+  Theory.add_oracle Eval.oracle
+  #> Method.add_method ("eval", Eval.method, "solve goal by evaluation")
+*}
+
+
+subsection {* Small examples *}
+
+ML {* Eval.term "[]::nat list" *}
+ML {* Eval.term "(Suc 2 + Suc 0) * Suc 3" *}
+ML {* Eval.term "fst ([]::nat list, Suc 0) = []" *}
+
+text {* a fancy datatype *}
+
+datatype ('a, 'b) bair =
+    Bair "'a\<Colon>order" 'b
+  | Shift "('a, 'b) cair"
+  | Dummy unit
+and ('a, 'b) cair =
+    Cair 'a 'b
+
+code_generate term_of
+
+ML {* Eval.term "Shift (Cair (4::nat) [Suc 0])" *}
+
+lemma
+  "Suc 0 = 1" by eval
+
+lemma
+  "rev [0, Suc 0, Suc 0] = [Suc 0, Suc 0, 0]" by eval
+
+lemma
+  "fst (snd (fst ( ((Some (2::nat), (Suc 0, ())), [0::nat]) ))) = Suc 0" by eval
+
+end
diff -r 9ffea7a8b31c -r 0b102b4182de src/HOL/ex/CodeOperationalEquality.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/CodeOperationalEquality.thy	Tue Aug 29 14:31:14 2006 +0200
@@ -0,0 +1,158 @@
+(*  ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* Operational equality for code generation *}
+
+theory CodeOperationalEquality
+imports Main
+begin
+
+section {* Operational equality for code generation *}
+
+subsection {* eq class *}
+
+class eq =
+  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+
+defs
+  eq_def: "eq x y == (x = y)"
+
+ML {*
+local
+  val thy = the_context ();
+  val const_eq = Sign.intern_const thy "eq";
+  val type_bool = Type (Sign.intern_type thy "bool", []);
+in
+  val eq_def_sym = Thm.symmetric (thm "eq_def");
+  val class_eq = Sign.intern_class thy "eq";
+end
+*}
+
+
+subsection {* preprocessor *}
+
+ML {*
+fun constrain_op_eq thy thms =
+  let
+    fun dest_eq (Const ("op =", ty)) =
+          (SOME o hd o fst o strip_type) ty
+      | dest_eq _ = NONE
+    fun eqs_of t =
+      fold_aterms (fn t => case dest_eq t
+       of SOME (TVar v_sort) => cons v_sort
+        | _ => I) t [];
+    val eqs = maps (eqs_of o Thm.prop_of) thms;
+    val instT = map (fn (v_i, sort) =>
+      (Thm.ctyp_of thy (TVar (v_i, sort)),
+         Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
+  in
+    thms
+    |> map (Thm.instantiate (instT, []))
+  end;
+*}
+
+
+subsection {* codetypes hook *}
+
+setup {*
+let
+  fun add_eq_instance specs =
+    DatatypeCodegen.prove_codetypes_arities
+      (K (ClassPackage.intro_classes_tac []))
+      (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
+      [class_eq] ((K o K o K) []);
+  (* fun add_eq_thms dtco thy =
+    let
+      val thms =
+        DatatypeCodegen.get_eq thy dtco
+        |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
+        |> constrain_op_eq thy
+        |> map (Tactic.rewrite_rule [eq_def_sym])
+    in fold CodegenTheorems.add_fun thms thy end; *)
+  fun hook dtcos =
+    add_eq_instance dtcos (* #> fold add_eq_thms dtcos *);
+in
+  DatatypeCodegen.add_codetypes_hook_bootstrap hook
+end
+*}
+
+
+subsection {* extractor *}
+
+setup {*
+let
+  fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
+   of SOME _ => DatatypeCodegen.get_eq thy tyco
+    | NONE => case TypedefCodegen.get_triv_typedef thy tyco
+       of SOME (_ ,(_, thm)) => [thm]
+        | NONE => [];
+  fun get_eq_thms_eq thy ("OperationalEquality.eq", ty) = (case strip_type ty
+       of (Type (tyco, _) :: _, _) =>
+             get_eq_thms thy tyco
+        | _ => [])
+    | get_eq_thms_eq _ _ = [];
+in
+  CodegenTheorems.add_fun_extr get_eq_thms_eq
+end
+*}
+
+
+subsection {* integers *}
+
+definition
+  "eq_integer (k\<Colon>int) l = (k = l)"
+
+instance int :: eq ..
+
+lemma [code fun]:
+  "eq k l = eq_integer k l"
+unfolding eq_integer_def eq_def ..
+
+code_constapp eq_integer
+  ml (infixl 6 "=")
+  haskell (infixl 4 "==")
+
+
+subsection {* codegenerator setup *}
+
+setup {*
+  CodegenTheorems.add_preproc constrain_op_eq
+*}
+
+declare eq_def [symmetric, code inline]
+
+
+subsection {* haskell setup *}
+
+code_class eq
+  haskell "Eq" (eq "(==)")
+
+code_instance
+  (eq :: bool) haskell
+  (eq :: unit) haskell
+  (eq :: *) haskell
+  (eq :: option) haskell
+  (eq :: list) haskell
+  (eq :: char) haskell
+  (eq :: int) haskell
+
+code_constapp
+  "eq"
+    haskell (infixl 4 "==")
+  "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+    haskell (infixl 4 "==")
+  "eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
+    haskell (infixl 4 "==")
+  "eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+    haskell (infixl 4 "==")
+  "eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
+    haskell (infixl 4 "==")
+  "eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
+    haskell (infixl 4 "==")
+  "eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+    haskell (infixl 4 "==")
+  "eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+    haskell (infixl 4 "==")
+
+end
\ No newline at end of file
diff -r 9ffea7a8b31c -r 0b102b4182de src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue Aug 29 14:31:13 2006 +0200
+++ b/src/HOL/ex/ROOT.ML	Tue Aug 29 14:31:14 2006 +0200
@@ -6,9 +6,9 @@
 
 no_document time_use_thy "Classpackage";
 no_document time_use_thy "Codegenerator";
-no_document time_use_thy "CodeEmbed";
+no_document time_use_thy "CodeOperationalEquality";
+no_document time_use_thy "CodeEval";
 no_document time_use_thy "CodeRandom";
-no_document time_use_thy "CodeRevappl";
 
 time_use_thy "Higher_Order_Logic";
 time_use_thy "Abstract_NAT";