fixes
authorhaftmann
Wed Aug 30 08:30:09 2006 +0200 (2006-08-30)
changeset 20435d2a30fed7596
parent 20434 110a223ba63c
child 20436 0af8655ab0bb
fixes
src/HOL/Tools/datatype_codegen.ML
src/HOL/Wellfounded_Recursion.thy
src/HOL/ex/CodeEval.thy
src/HOL/ex/CodeOperationalEquality.thy
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Aug 30 08:29:30 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Aug 30 08:30:09 2006 +0200
     1.3 @@ -370,6 +370,7 @@
     1.4    in map mk_dist (sym_product cos) end;
     1.5  
     1.6  local
     1.7 +  val not_sym = thm "HOL.not_sym";
     1.8    val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
     1.9  in fun get_eq thy dtco =
    1.10    let
    1.11 @@ -396,6 +397,7 @@
    1.12      val distinct =
    1.13        mk_distinct cos
    1.14        |> map (fn t => Goal.prove_global thy [] [] t (K tac))
    1.15 +      |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
    1.16    in inject1 @ inject2 @ distinct end;
    1.17  end (*local*);
    1.18  
     2.1 --- a/src/HOL/Wellfounded_Recursion.thy	Wed Aug 30 08:29:30 2006 +0200
     2.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Wed Aug 30 08:30:09 2006 +0200
     2.3 @@ -298,7 +298,7 @@
     2.4  code_constapp
     2.5    wfrec
     2.6      ml (target_atom "(let fun wfrec f x = f (wfrec f) x in wfrec end)")
     2.7 -    haskell (target_atom "(wfrec where wfrec f x = f (wfrec f) x)")
     2.8 +    haskell (target_atom "(let wfrec f x = f (wfrec f) x in wfrec)")
     2.9  
    2.10  subsection{*Variants for TFL: the Recdef Package*}
    2.11  
     3.1 --- a/src/HOL/ex/CodeEval.thy	Wed Aug 30 08:29:30 2006 +0200
     3.2 +++ b/src/HOL/ex/CodeEval.thy	Wed Aug 30 08:30:09 2006 +0200
     3.3 @@ -154,7 +154,6 @@
     3.4  
     3.5  val oracle_name = NameSpace.pack [Context.theory_name (the_context ()), fst oracle];
     3.6  
     3.7 -
     3.8  fun conv ct =
     3.9    let
    3.10      val {thy, t, ...} = rep_cterm ct;
    3.11 @@ -206,6 +205,6 @@
    3.12    "rev [0, Suc 0, Suc 0] = [Suc 0, Suc 0, 0]" by eval
    3.13  
    3.14  lemma
    3.15 -  "fst (snd (fst ( ((Some (2::nat), (Suc 0, ())), [0::nat]) ))) = Suc 0" by eval
    3.16 +  "fst (snd (fst ( ((Some (2::nat), (Suc 0, ())), [0::nat]) ))) = Suc (Suc 0) - 1" by eval
    3.17  
    3.18  end
     4.1 --- a/src/HOL/ex/CodeOperationalEquality.thy	Wed Aug 30 08:29:30 2006 +0200
     4.2 +++ b/src/HOL/ex/CodeOperationalEquality.thy	Wed Aug 30 08:30:09 2006 +0200
     4.3 @@ -35,14 +35,12 @@
     4.4  ML {*
     4.5  fun constrain_op_eq thy thms =
     4.6    let
     4.7 -    fun dest_eq (Const ("op =", ty)) =
     4.8 -          (SOME o hd o fst o strip_type) ty
     4.9 -      | dest_eq _ = NONE
    4.10 -    fun eqs_of t =
    4.11 -      fold_aterms (fn t => case dest_eq t
    4.12 -       of SOME (TVar v_sort) => cons v_sort
    4.13 -        | _ => I) t [];
    4.14 -    val eqs = maps (eqs_of o Thm.prop_of) thms;
    4.15 +    fun add_eq (Const ("op =", ty)) =
    4.16 +          fold (insert (eq_fst (op = : indexname * indexname -> bool)))
    4.17 +            (Term.add_tvarsT ty [])
    4.18 +      | add_eq _ =
    4.19 +          I
    4.20 +    val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
    4.21      val instT = map (fn (v_i, sort) =>
    4.22        (Thm.ctyp_of thy (TVar (v_i, sort)),
    4.23           Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
    4.24 @@ -82,14 +80,24 @@
    4.25  
    4.26  setup {*
    4.27  let
    4.28 +  val lift_not_thm = thm "HOL.Eq_FalseI";
    4.29 +  val lift_thm = thm "HOL.eq_reflection";
    4.30 +  val eq_def_thm = Thm.symmetric (thm "eq_def");
    4.31    fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
    4.32     of SOME _ => DatatypeCodegen.get_eq thy tyco
    4.33      | NONE => case TypedefCodegen.get_triv_typedef thy tyco
    4.34         of SOME (_ ,(_, thm)) => [thm]
    4.35          | NONE => [];
    4.36 -  fun get_eq_thms_eq thy ("OperationalEquality.eq", ty) = (case strip_type ty
    4.37 +  fun get_eq_thms_eq thy ("CodeOperationalEquality.eq", ty) = (case strip_type ty
    4.38         of (Type (tyco, _) :: _, _) =>
    4.39               get_eq_thms thy tyco
    4.40 +             |> map (perhaps (try (fn thm => lift_not_thm OF [thm])))
    4.41 +             |> map (perhaps (try (fn thm => lift_thm OF [thm])))
    4.42 +             (*|> tap (writeln o cat_lines o map string_of_thm)*)
    4.43 +             |> constrain_op_eq thy
    4.44 +             (*|> tap (writeln o cat_lines o map string_of_thm)*)
    4.45 +             |> map (Tactic.rewrite_rule [eq_def_thm])
    4.46 +             (*|> tap (writeln o cat_lines o map string_of_thm)*)
    4.47          | _ => [])
    4.48      | get_eq_thms_eq _ _ = [];
    4.49  in
    4.50 @@ -138,8 +146,6 @@
    4.51    (eq :: int) haskell
    4.52  
    4.53  code_constapp
    4.54 -  "eq"
    4.55 -    haskell (infixl 4 "==")
    4.56    "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
    4.57      haskell (infixl 4 "==")
    4.58    "eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
    4.59 @@ -154,5 +160,7 @@
    4.60      haskell (infixl 4 "==")
    4.61    "eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    4.62      haskell (infixl 4 "==")
    4.63 +  "eq"
    4.64 +    haskell (infixl 4 "==")
    4.65  
    4.66  end
    4.67 \ No newline at end of file