Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Prolog/Type.ML
author huffman
Wed, 12 Oct 2005 03:02:18 +0200
changeset 17840 11bcd77cfa22
parent 14981 e73f8140af78
child 20713 823967ef47f1
permissions -rw-r--r--
domain package generates compactness lemmas for new constructors

(*  Title:    HOL/Prolog/Type.ML
    ID:       $Id$
    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)

val prog_Type = prog_Func @ [good_typeof,common_typeof];
fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Type));
val p = ptac prog_Type 1;

pgoal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T";

pgoal "typeof (fix (%x. x)) ?T";

pgoal "typeof (fix (%fact. abs(%n. (app fact (n - 0))))) ?T";

pgoal "typeof (fix (%fact. abs(%n. cond (n eq 0) (S 0) \
				\(n * (app fact (n - (S 0))))))) ?T";

pgoal "typeof (abs(%v. 0)) ?T"; (*correct only solution (?A1 -> nat) *)
Goal "typeof (abs(%v. 0)) ?T";
by (prolog_tac [bad1_typeof,common_typeof]); (* 1st result ok*)
back(); (* 2nd result (?A1 -> ?A1) wrong *)

(*pgoal "typeof (abs(%v. abs(%v. app v v))) ?T"; correctly fails*)
Goal "typeof (abs(%v. abs(%v. app v v))) ?T";
by (prolog_tac [bad2_typeof,common_typeof]); 
	(* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
isabelle