# HG changeset patch # User Christian Urban # Date 1263490538 -3600 # Node ID 2cc520457e370974c1d7565644f06056c626d0fe # Parent cd3f1409780ad8ebbd87359cdd5f10a9f1740fbe nearly all of the proof diff -r cd3f1409780a -r 2cc520457e37 Quot/Examples/LamEx.thy --- a/Quot/Examples/LamEx.thy Thu Jan 14 17:57:20 2010 +0100 +++ b/Quot/Examples/LamEx.thy Thu Jan 14 18:35:38 2010 +0100 @@ -256,11 +256,15 @@ apply(default) sorry +lemma fresh_lam: + "(a \ Lam b t) \ (a = b) \ (a \ b \ a \ t)" +sorry + lemma lam_induct_strong: fixes a::"'a::fs_name" assumes a1: "\name b. P b (Var name)" and a2: "\lam1 lam2 b. \\c. P c lam1; \c. P c lam2\ \ P b (App lam1 lam2)" - and a3: "\name lam b. \\c. P c lam; name \ lam\ \ P b (Lam name lam)" + and a3: "\name lam b. \\c. P c lam; name \ b\ \ P b (Lam name lam)" shows "P a lam" proof - have "\(pi::name prm) a. P a (pi \ lam)" @@ -281,12 +285,27 @@ apply (rule b2) done next - case (3 name lam pi) - have b: "P a (pi \ lam)" by fact + case (3 name lam pi a) + have b: "\(pi::name prm) a. P a (pi \ lam)" by fact + obtain c::name where fr: "c\(a, pi\name, pi\lam)" sorry + from b fr have p: "P a (Lam c (([(c, pi\name)]@pi)\lam))" + apply - + apply(rule a3) + apply(blast) + apply(simp) + done + have eq: "[(c, pi\name)] \ Lam (pi \ name) (pi \ lam) = Lam (pi \ name) (pi \ lam)" + apply(rule perm_fresh_fresh) + using fr + apply(simp add: fresh_lam) + apply(simp add: fresh_lam) + done show "P a (pi \ Lam name lam)" apply (simp add: pi_lam) - using b - sorry + apply(subst eq[symmetric]) + using p + apply(simp only: pi_lam pt_name2 swap_simps) + done qed then have "P a (([]::name prm) \ lam)" by blast then show "P a lam" by simp