cleaned up
authorhaftmann
Thu Jul 30 13:52:18 2009 +0200 (2009-07-30)
changeset 32340b4632820e74c
parent 32339 40612b7ace87
child 32341 c8c17c2e6ceb
cleaned up
src/HOL/ex/Predicate_Compile.thy
src/HOL/ex/Predicate_Compile_ex.thy
     1.1 --- a/src/HOL/ex/Predicate_Compile.thy	Thu Jul 30 13:52:17 2009 +0200
     1.2 +++ b/src/HOL/ex/Predicate_Compile.thy	Thu Jul 30 13:52:18 2009 +0200
     1.3 @@ -1,61 +1,8 @@
     1.4  theory Predicate_Compile
     1.5 -imports Complex_Main Lattice_Syntax Code_Eval
     1.6 +imports Complex_Main
     1.7  uses "predicate_compile.ML"
     1.8  begin
     1.9  
    1.10 -text {* Package setup *}
    1.11 -
    1.12  setup {* Predicate_Compile.setup *}
    1.13  
    1.14 -text {* Experimental code *}
    1.15 -
    1.16 -ML {*
    1.17 -structure Predicate_Compile =
    1.18 -struct
    1.19 -
    1.20 -open Predicate_Compile;
    1.21 -
    1.22 -fun eval thy t_compr =
    1.23 -  let
    1.24 -    val t = Predicate_Compile.analyze_compr thy t_compr;
    1.25 -    val Type (@{type_name Predicate.pred}, [T]) = fastype_of t;
    1.26 -    fun mk_predT T = Type (@{type_name Predicate.pred}, [T]);
    1.27 -    val T1 = T --> @{typ term};
    1.28 -    val T2 = T1 --> mk_predT T --> mk_predT @{typ term};
    1.29 -    val t' = Const (@{const_name Predicate.map}, T2) (*FIXME*)
    1.30 -      $ Const (@{const_name Code_Eval.term_of}, T1) $ t;
    1.31 -  in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) Predicate.map thy t' []) end;
    1.32 -
    1.33 -fun values ctxt k t_compr =
    1.34 -  let
    1.35 -    val thy = ProofContext.theory_of ctxt;
    1.36 -    val (T, t') = eval thy t_compr;
    1.37 -  in t' |> Predicate.yieldn k |> fst |> HOLogic.mk_list T end;
    1.38 -
    1.39 -fun values_cmd modes k raw_t state =
    1.40 -  let
    1.41 -    val ctxt = Toplevel.context_of state;
    1.42 -    val t = Syntax.read_term ctxt raw_t;
    1.43 -    val t' = values ctxt k t;
    1.44 -    val ty' = Term.type_of t';
    1.45 -    val ctxt' = Variable.auto_fixes t' ctxt;
    1.46 -    val p = PrintMode.with_modes modes (fn () =>
    1.47 -      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    1.48 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
    1.49 -  in Pretty.writeln p end;
    1.50 -
    1.51 -end;
    1.52 -
    1.53 -local structure P = OuterParse in
    1.54 -
    1.55 -val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
    1.56 -
    1.57 -val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
    1.58 -  (opt_modes -- Scan.optional P.nat ~1 -- P.term
    1.59 -    >> (fn ((modes, k), t) => Toplevel.no_timing o Toplevel.keep
    1.60 -        (Predicate_Compile.values_cmd modes k t)));
    1.61 -
    1.62 -end;
    1.63 -*}
    1.64 -
    1.65  end
    1.66 \ No newline at end of file
     2.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Thu Jul 30 13:52:17 2009 +0200
     2.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Thu Jul 30 13:52:18 2009 +0200
     2.3 @@ -17,17 +17,11 @@
     2.4  values 10 "{n. even n}"
     2.5  values 10 "{n. odd n}"
     2.6  
     2.7 -
     2.8  inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
     2.9 -    append_Nil: "append [] xs xs"
    2.10 -  | append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
    2.11 +    "append [] xs xs"
    2.12 +  | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
    2.13  
    2.14 -inductive rev
    2.15 -where
    2.16 -"rev [] []"
    2.17 -| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
    2.18 -
    2.19 -code_pred rev .
    2.20 +code_pred append .
    2.21  
    2.22  thm append.equation
    2.23  
    2.24 @@ -35,6 +29,16 @@
    2.25  values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
    2.26  values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0,5]}"
    2.27  
    2.28 +inductive rev where
    2.29 +    "rev [] []"
    2.30 +  | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
    2.31 +
    2.32 +code_pred rev .
    2.33 +
    2.34 +thm rev.equation
    2.35 +
    2.36 +values "{xs. rev [0, 1, 2, 3::nat] xs}"
    2.37 +values "Collect (rev [0, 1, 2, 3::nat])"
    2.38  
    2.39  inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    2.40    for f where
    2.41 @@ -57,9 +61,9 @@
    2.42  
    2.43  
    2.44  lemma [code_pred_intros]:
    2.45 -"r a b ==> tranclp r a b"
    2.46 -"r a b ==> tranclp r b c ==> tranclp r a c"
    2.47 -by auto
    2.48 +  "r a b \<Longrightarrow> tranclp r a b"
    2.49 +  "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
    2.50 +  by auto
    2.51  
    2.52  (* Setup requires quick and dirty proof *)
    2.53  (*
    2.54 @@ -71,6 +75,7 @@
    2.55  
    2.56  thm tranclp.equation
    2.57  *)
    2.58 +
    2.59  inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
    2.60      "succ 0 1"
    2.61    | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
    2.62 @@ -78,6 +83,11 @@
    2.63  code_pred succ .
    2.64  
    2.65  thm succ.equation
    2.66 +
    2.67 +values 10 "{(m, n). succ n m}"
    2.68 +values "{m. succ 0 m}"
    2.69 +values "{m. succ m 0}"
    2.70 +
    2.71  (* FIXME: why does this not terminate? *)
    2.72  (*
    2.73  values 20 "{n. tranclp succ 10 n}"