# HG changeset patch # User Cezary Kaliszyk # Date 1263483677 -3600 # Node ID 09a64cb04851f764b53f3c131a6c8cf864bc8fda # Parent a6a4c88e1c9a091806d2ec65419dfc264bf8378a exported absrep_const for nitpick. diff -r a6a4c88e1c9a -r 09a64cb04851 Quot/Examples/LamEx.thy --- a/Quot/Examples/LamEx.thy Thu Jan 14 15:36:29 2010 +0100 +++ b/Quot/Examples/LamEx.thy Thu Jan 14 16:41:17 2010 +0100 @@ -242,11 +242,24 @@ by (lifting rvar_inject) lemma lam_induct: - "\\name. P (Var name); + "\\name. P (Var name); \lam1 lam2. \P lam1; P lam2\ \ P (App lam1 lam2); \name lam. P lam \ P (Lam name lam)\ \ P lam" by (lifting rlam.induct) +lemma lam_induct_strong_pre: + "\\name b. P b (Var name); + \lam1 lam2 b. \\c. P c lam1; \c. P c lam2\ \ P b (App lam1 lam2); + \name lam b. \\c. P c lam; name \ (c \ lam)\ \ P b (Lam name lam)\ \ P a lam" +sorry + +lemma lam_induct_strong: + "\\name. P (Var name); + \lam1 lam2. \P lam1; P lam2\ \ P (App lam1 lam2); + \name lam. P lam \ name \ lam \ P (Lam name lam)\ \ P lam" +sorry + + lemma var_supp: shows "supp (Var a) = ((supp a)::name set)" apply(simp add: supp_def) diff -r a6a4c88e1c9a -r 09a64cb04851 Quot/quotient_term.ML --- a/Quot/quotient_term.ML Thu Jan 14 15:36:29 2010 +0100 +++ b/Quot/quotient_term.ML Thu Jan 14 16:41:17 2010 +0100 @@ -4,6 +4,8 @@ datatype flag = absF | repF + val absrep_const_chk: flag -> Proof.context -> string -> term + val absrep_fun: flag -> Proof.context -> typ * typ -> term val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term @@ -126,6 +128,9 @@ | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) end +fun absrep_const_chk flag ctxt qty_str = + Syntax.check_term ctxt (absrep_const flag ctxt qty_str) + fun absrep_match_err ctxt ty_pat ty = let val ty_pat_str = Syntax.string_of_typ ctxt ty_pat