added OperationalEquality.thy
authorhaftmann
Tue Sep 19 15:22:21 2006 +0200 (2006-09-19)
changeset 20598f8031b91c946
parent 20597 65fe827aa595
child 20599 65bd267ae23f
added OperationalEquality.thy
src/HOL/IsaMakefile
src/HOL/OperationalEquality.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue Sep 19 15:22:05 2006 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Sep 19 15:22:21 2006 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4    Integ/reflected_cooper.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML	\
     1.5    Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy		\
     1.6    Lattice_Locales.thy List.ML List.thy Main.ML Main.thy Map.thy			\
     1.7 -  Nat.ML Nat.thy NatArith.thy OrderedGroup.ML OrderedGroup.thy			\
     1.8 +  Nat.ML Nat.thy NatArith.thy OperationalEquality.thy OrderedGroup.ML OrderedGroup.thy	\
     1.9    Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy		\
    1.10    ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
    1.11    Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.ML		\
    1.12 @@ -647,7 +647,7 @@
    1.13    ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy			\
    1.14    ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/CodeCollections.thy \
    1.15    ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy			\
    1.16 -  ex/CodeOperationalEquality.thy ex/Codegenerator.thy ex/Commutative_RingEx.thy               \
    1.17 +  ex/Codegenerator.thy ex/Commutative_RingEx.thy               \
    1.18    ex/Commutative_Ring_Complete.thy ex/Guess.thy ex/Hebrew.thy			\
    1.19    ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy		\
    1.20    ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy			\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/OperationalEquality.thy	Tue Sep 19 15:22:21 2006 +0200
     2.3 @@ -0,0 +1,130 @@
     2.4 +(*  ID:         $Id$
     2.5 +    Author:     Florian Haftmann, TU Muenchen
     2.6 +*)
     2.7 +
     2.8 +header {* Operational equality for code generation *}
     2.9 +
    2.10 +theory OperationalEquality
    2.11 +imports HOL
    2.12 +begin
    2.13 +
    2.14 +section {* Operational equality for code generation *}
    2.15 +
    2.16 +subsection {* eq class *}
    2.17 +
    2.18 +class eq =
    2.19 +  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    2.20 +
    2.21 +defs
    2.22 +  eq_def: "eq x y \<equiv> (x = y)"
    2.23 +
    2.24 +ML {*
    2.25 +local
    2.26 +  val thy = the_context ();
    2.27 +  val const_eq = Sign.intern_const thy "eq";
    2.28 +  val type_bool = Type (Sign.intern_type thy "bool", []);
    2.29 +in
    2.30 +  val eq_def_sym = Thm.symmetric (thm "eq_def");
    2.31 +  val class_eq = Sign.intern_class thy "eq";
    2.32 +end
    2.33 +*}
    2.34 +
    2.35 +
    2.36 +subsection {* bool type *}
    2.37 +
    2.38 +instance bool :: eq ..
    2.39 +
    2.40 +lemma [code func]:
    2.41 +  "eq True p = p" unfolding eq_def by auto
    2.42 +
    2.43 +lemma [code func]:
    2.44 +  "eq False p = (\<not> p)" unfolding eq_def by auto
    2.45 +
    2.46 +lemma [code func]:
    2.47 +  "eq p True = p" unfolding eq_def by auto
    2.48 +
    2.49 +lemma [code func]:
    2.50 +  "eq p False = (\<not> p)" unfolding eq_def by auto
    2.51 +
    2.52 +
    2.53 +subsection {* preprocessor *}
    2.54 +
    2.55 +ML {*
    2.56 +fun constrain_op_eq thy thms =
    2.57 +  let
    2.58 +    fun add_eq (Const ("op =", ty)) =
    2.59 +          fold (insert (eq_fst (op = : indexname * indexname -> bool)))
    2.60 +            (Term.add_tvarsT ty [])
    2.61 +      | add_eq _ =
    2.62 +          I
    2.63 +    val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
    2.64 +    val instT = map (fn (v_i, sort) =>
    2.65 +      (Thm.ctyp_of thy (TVar (v_i, sort)),
    2.66 +         Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
    2.67 +  in
    2.68 +    thms
    2.69 +    |> map (Thm.instantiate (instT, []))
    2.70 +  end;
    2.71 +*}
    2.72 +
    2.73 +
    2.74 +subsection {* codegenerator setup *}
    2.75 +
    2.76 +setup {*
    2.77 +  CodegenData.add_preproc constrain_op_eq
    2.78 +*}
    2.79 +
    2.80 +declare eq_def [symmetric, code inline]
    2.81 +
    2.82 +code_constname
    2.83 +  "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" "HOL.eq_bool"
    2.84 +
    2.85 +
    2.86 +subsection {* haskell setup *}
    2.87 +
    2.88 +code_class eq
    2.89 +  (Haskell "Eq" where eq \<equiv> "(==)")
    2.90 +
    2.91 +code_const eq
    2.92 +  (Haskell infixl 4 "==")
    2.93 +
    2.94 +code_instance bool :: eq
    2.95 +  (Haskell -)
    2.96 +
    2.97 +code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
    2.98 +  (Haskell infixl 4 "==")
    2.99 +
   2.100 +
   2.101 +subsection {* nbe setup *}
   2.102 +
   2.103 +lemma eq_refl: "eq x x"
   2.104 +  unfolding eq_def ..
   2.105 +
   2.106 +setup {*
   2.107 +let
   2.108 +
   2.109 +val eq_refl = thm "eq_refl";
   2.110 +
   2.111 +fun Trueprop_conv conv ct = (case term_of ct of
   2.112 +    Const ("Trueprop", _) $ _ =>
   2.113 +      let val (ct1, ct2) = Thm.dest_comb ct
   2.114 +      in Thm.combination (Thm.reflexive ct1) (conv ct2) end
   2.115 +  | _ => raise TERM ("Trueprop_conv", []));
   2.116 +
   2.117 +fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
   2.118 +  (Drule.goals_conv (equal i) (Trueprop_conv NBE.normalization_conv)));
   2.119 +
   2.120 +val normalization_meth =
   2.121 +  Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI, refl, eq_refl] 1));
   2.122 +
   2.123 +in
   2.124 +
   2.125 +Method.add_method ("normalization", normalization_meth, "solve goal by normalization")
   2.126 +
   2.127 +end;
   2.128 +*}
   2.129 +
   2.130 +
   2.131 +hide (open) const eq
   2.132 +
   2.133 +end
   2.134 \ No newline at end of file