src/HOL/Code_Generator.thy
author wenzelm
Fri, 17 Nov 2006 02:20:03 +0100
changeset 21404 eb85850d3eb7
parent 21378 cedfce6fc725
child 21454 a1937c51ed88
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21046
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
     1
(*  ID:         $Id$
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
     3
*)
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
     4
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
     5
header {* Setup of code generator tools *}
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
     6
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
     7
theory Code_Generator
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
     8
imports HOL
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
     9
begin
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    10
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    11
subsection {* ML code generator *}
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    12
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    13
types_code
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    14
  "bool"  ("bool")
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    15
attach (term_of) {*
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    16
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    17
*}
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    18
attach (test) {*
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    19
fun gen_bool i = one_of [false, true];
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    20
*}
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    21
  "prop"  ("bool")
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    22
attach (term_of) {*
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    23
fun term_of_prop b =
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    24
  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    25
*}
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    26
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    27
consts_code
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    28
  "Trueprop" ("(_)")
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    29
  "True"    ("true")
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    30
  "False"   ("false")
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    31
  "Not"     ("not")
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    32
  "op |"    ("(_ orelse/ _)")
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    33
  "op &"    ("(_ andalso/ _)")
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    34
  "HOL.If"      ("(if _/ then _/ else _)")
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    35
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    36
setup {*
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    37
let
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    38
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    39
fun eq_codegen thy defs gr dep thyname b t =
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    40
    (case strip_comb t of
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    41
       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    42
     | (Const ("op =", _), [t, u]) =>
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    43
          let
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    44
            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    45
            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    46
            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    47
          in
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    48
            SOME (gr''', Codegen.parens
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    49
              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    50
          end
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    51
     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    52
         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    53
     | _ => NONE);
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    54
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    55
in
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    56
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    57
Codegen.add_codegen "eq_codegen" eq_codegen
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    58
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    59
end
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    60
*}
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    61
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    62
text {* Evaluation *}
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    63
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    64
setup {*
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    65
let
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    66
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    67
fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    68
  (Drule.goals_conv (equal i) Codegen.evaluation_conv));
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    69
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    70
val evaluation_meth =
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    71
  Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac HOL.TrueI 1));
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    72
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    73
in
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    74
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    75
Method.add_method ("evaluation", evaluation_meth, "solve goal by evaluation")
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    76
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    77
end;
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    78
*}
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    79
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    80
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    81
subsection {* Generic code generator setup *}
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    82
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    83
text {* itself as a code generator datatype *}
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    84
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    85
setup {*
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    86
let fun add_itself thy =
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    87
  let
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    88
    val v = ("'a", []);
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    89
    val t = Logic.mk_type (TFree v);
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    90
    val Const (c, ty) = t;
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    91
    val (_, Type (dtco, _)) = strip_type ty;
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    92
  in
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    93
    thy
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    94
    |> CodegenData.add_datatype (dtco, (([v], [(c, [])]), CodegenData.lazy (fn () => [])))
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    95
  end
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    96
in add_itself end;
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    97
*} 
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    98
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
    99
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   100
text {* code generation for arbitrary as exception *}
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   101
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   102
setup {*
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   103
  CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   104
*}
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   105
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   106
code_const arbitrary
21110
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   107
  (Haskell "error/ \"arbitrary\"")
21046
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   108
21079
747d716e98d0 added reserved words for Haskell
haftmann
parents: 21059
diff changeset
   109
code_reserved SML Fail
747d716e98d0 added reserved words for Haskell
haftmann
parents: 21059
diff changeset
   110
code_reserved Haskell error
21046
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   111
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   112
21378
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   113
subsection {* Evaluation oracle *}
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   114
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   115
ML {*
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   116
signature HOL_EVAL =
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   117
sig
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   118
  val eval_ref: bool option ref
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   119
  val oracle: string * (theory * exn -> term)
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   120
  val tac: int -> tactic
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   121
  val method: Method.src -> Proof.context -> Method.method
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   122
end;
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   123
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   124
structure HOLEval : HOL_EVAL =
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   125
struct
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   126
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   127
val eval_ref : bool option ref = ref NONE;
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   128
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   129
fun eval_prop thy t =
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   130
  CodegenPackage.eval_term
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   131
    thy (("HOLEval.eval_ref", eval_ref), t);
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   132
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   133
exception Eval of term;
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   134
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   135
val oracle = ("Eval", fn (thy, Eval t) =>
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   136
  Logic.mk_equals (t, if eval_prop thy t then HOLogic.true_const else HOLogic.false_const));
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   137
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   138
val oracle_name = NameSpace.pack [Context.theory_name (the_context ()), fst oracle];
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   139
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   140
fun conv ct =
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   141
  let
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   142
    val {thy, t, ...} = rep_cterm ct;
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   143
  in Thm.invoke_oracle_i thy oracle_name (thy, Eval t) end;
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   144
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   145
fun tac i = Tactical.PRIMITIVE (Drule.fconv_rule
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   146
  (Drule.goals_conv (equal i) (HOL.Trueprop_conv conv)));
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   147
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   148
val method =
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   149
  Method.no_args (Method.METHOD (fn _ =>
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   150
    tac 1 THEN rtac TrueI 1));
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   151
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   152
end;
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   153
*}
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   154
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   155
setup {*
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   156
  Theory.add_oracle HOLEval.oracle
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   157
  #> Method.add_method ("eval", HOLEval.method, "solve goal by evaluation")
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   158
*}
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   159
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   160
cedfce6fc725 added evaluation oracle
haftmann
parents: 21149
diff changeset
   161
subsection {* Normalization by evaluation *}
21046
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   162
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   163
setup {*
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   164
let
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   165
  fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
21110
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   166
    (Drule.goals_conv (equal i) (HOL.Trueprop_conv
21149
ee207b9b8bf5 dropped equals_conv for nbe
haftmann
parents: 21110
diff changeset
   167
      NBE.normalization_conv)));
21046
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   168
  val normalization_meth =
21110
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   169
    Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI, refl] 1));
21046
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   170
in
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   171
  Method.add_method ("normalization", normalization_meth, "solve goal by normalization")
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   172
end;
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   173
*}
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   174
21059
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   175
text {* lazy @{const If} *}
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   176
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   177
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21378
diff changeset
   178
  if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
21059
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   179
  "if_delayed b f g = (if b then f True else g False)"
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   180
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   181
lemma [code func]:
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   182
  shows "if_delayed True f g = f True"
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   183
    and "if_delayed False f g = g False"
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   184
  unfolding if_delayed_def by simp_all
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   185
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   186
lemma [normal pre, symmetric, normal post]:
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   187
  "(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)"
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   188
  unfolding if_delayed_def ..
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   189
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   190
21110
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   191
subsection {* Operational equality for code generation *}
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   192
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   193
subsubsection {* eq class *}
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   194
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   195
class eq =
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   196
  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   197
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   198
defs
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   199
  eq_def [normal post]: "eq \<equiv> (op =)"
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   200
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   201
lemmas [symmetric, code inline, code func] = eq_def
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   202
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   203
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   204
subsubsection {* bool type *}
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   205
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   206
instance bool :: eq ..
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   207
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   208
lemma [code func]:
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   209
  "eq True p = p" unfolding eq_def by auto
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   210
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   211
lemma [code func]:
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   212
  "eq False p = (\<not> p)" unfolding eq_def by auto
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   213
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   214
lemma [code func]:
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   215
  "eq p True = p" unfolding eq_def by auto
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   216
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   217
lemma [code func]:
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   218
  "eq p False = (\<not> p)" unfolding eq_def by auto
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   219
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   220
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   221
subsubsection {* Haskell *}
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   222
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   223
code_class eq
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   224
  (Haskell "Eq" where eq \<equiv> "(==)")
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   225
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   226
code_const eq
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   227
  (Haskell infixl 4 "==")
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   228
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   229
code_instance bool :: eq
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   230
  (Haskell -)
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   231
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   232
code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   233
  (Haskell infixl 4 "==")
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   234
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   235
code_reserved Haskell
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   236
  Eq eq
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   237
fc98cb66c5c3 adaptions to changes in preprocessor
haftmann
parents: 21079
diff changeset
   238
21059
361e62500ab7 added if_delayed
haftmann
parents: 21046
diff changeset
   239
hide (open) const eq if_delayed
21046
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   240
fe1db2f991a7 moved HOL code generator setup to Code_Generator
haftmann
parents:
diff changeset
   241
end