# HG changeset patch # User Cezary Kaliszyk # Date 1268766433 -3600 # Node ID 1850361efb8f545b4100e94f0d3edb77185e4386 # Parent 1909be313353b130e96fa4c0fb134d6f306049e4 Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not. diff -r 1909be313353 -r 1850361efb8f Nominal/Fv.thy --- a/Nominal/Fv.thy Tue Mar 16 18:19:00 2010 +0100 +++ b/Nominal/Fv.thy Tue Mar 16 20:07:13 2010 +0100 @@ -154,16 +154,6 @@ end *} -ML {* -fun all_binds l = -let - fun is_non_rec (SOME (f, _), _, _) = SOME f - | is_non_rec _ = NONE -in - distinct (op =) (map_filter is_non_rec (flat (flat l))) -end -*} - (* We assume no bindings in the type on which bn is defined *) ML {* fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bns) = @@ -266,9 +256,8 @@ "fv_" ^ name_of_typ (nth_dtyp i)) descr); val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; val fv_frees = map Free (fv_names ~~ fv_types); - val all_bns = all_binds bindsall; val nr_bns = non_rec_binds bindsall; - val rel_bns = filter (fn (bn, _, _) => bn mem all_bns) bns; + val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => @@ -307,21 +296,15 @@ @{term "{} :: atom set"} | fv_bind args (SOME (f, _), i, _) = f $ (nth args i); fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) + fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE + | find_nonrec_binder _ _ = NONE fun find_compound_binder j (SOME (f, r), i, _) = if i = j then SOME (f, r) else NONE | find_compound_binder _ _ = NONE fun fv_arg ((dt, x), arg_no) = - case get_first (find_compound_binder arg_no) bindcs of - SOME (f, is_rec) => + case get_first (find_nonrec_binder arg_no) bindcs of + SOME f => (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of - SOME fv_bn => - if is_rec then - let - val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; - val sub = fv_binds args relevant - in - mk_diff (fv_bn $ x) sub - end - else fv_bn $ x + SOME fv_bn => fv_bn $ x | NONE => error "bn specified in a non-rec binding but not in bn list") | NONE => let diff -r 1909be313353 -r 1850361efb8f Nominal/Parser.thy --- a/Nominal/Parser.thy Tue Mar 16 18:19:00 2010 +0100 +++ b/Nominal/Parser.thy Tue Mar 16 20:07:13 2010 +0100 @@ -337,14 +337,22 @@ val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; + val _ = tracing "3"; val fv_eqvt_tac = if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5 + val _ = tracing "4"; val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc_nobn fv_eqvt_tac lthy5; - val (fv_bn_eqvts, lthy6a) = fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) (fv_ts_loc_bn ~~ (map snd bns)) lthy6; + val _ = tracing "4a"; + val (fv_bn_eqvts, lthy6a) = + if fv_ts_loc_bn = [] then ([], lthy6) else + fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) + (fv_ts_loc_bn ~~ (map snd bns)) lthy6; + val _ = tracing "4b"; val lthy6 = lthy6a; val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; + val _ = tracing "5"; fun alpha_eqvt_tac' _ = if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc @ raw_fv_bv_eqvt_loc) lthy6 1 diff -r 1909be313353 -r 1850361efb8f Nominal/Term5.thy --- a/Nominal/Term5.thy Tue Mar 16 18:19:00 2010 +0100 +++ b/Nominal/Term5.thy Tue Mar 16 20:07:13 2010 +0100 @@ -43,7 +43,6 @@ lemma fv_rtrm5_rlts_eqvt[eqvt]: "pi \ (fv_rtrm5 x) = fv_rtrm5 (pi \ x)" "pi \ (fv_rlts l) = fv_rlts (pi \ l)" - "pi \ (fv_rbv5 l) = fv_rbv5 (pi \ l)" apply (induct x and l) apply (simp_all add: eqvts atom_eqvt) done @@ -134,7 +133,6 @@ |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_bv5", @{term fv_rbv5})) |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})) |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5}))) *} @@ -142,14 +140,14 @@ lemma alpha5_rfv: "(t \5 s \ fv_rtrm5 t = fv_rtrm5 s)" - "(l \l m \ (fv_rlts l = fv_rlts m \ fv_rbv5 l = fv_rbv5 m))" - "(alpha_rbv5 b c \ fv_rbv5 b = fv_rbv5 c)" + "(l \l m \ fv_rlts l = fv_rlts m)" + "(alpha_rbv5 b c \ True)" apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) apply(simp_all add: eqvts) apply(simp add: alpha_gen) apply(clarify) apply(simp) - sorry +done lemma bv_list_rsp: shows "x \l y \ rbv5 x = rbv5 y" @@ -159,9 +157,38 @@ apply simp done +local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} +print_theorems + + +lemma alpha_rbv_rsp_pre: + "x \l y \ \z. alpha_rbv5 x z = alpha_rbv5 y z" + apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) + apply (simp_all add: alpha_dis alpha5_inj) + apply clarify + apply (case_tac [!] z) + apply (simp_all add: alpha_dis alpha5_inj) + apply clarify + apply auto + apply (meson alpha5_symp alpha5_transp) + apply (meson alpha5_symp alpha5_transp) + done + +lemma alpha_rbv_rsp_pre2: + "x \l y \ \z. alpha_rbv5 z x = alpha_rbv5 z y" + apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) + apply (simp_all add: alpha_dis alpha5_inj) + apply clarify + apply (case_tac [!] z) + apply (simp_all add: alpha_dis alpha5_inj) + apply clarify + apply auto + apply (meson alpha5_symp alpha5_transp) + apply (meson alpha5_symp alpha5_transp) + done + lemma [quot_respect]: "(alpha_rlts ===> op =) fv_rlts fv_rlts" - "(alpha_rlts ===> op =) fv_rbv5 fv_rbv5" "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" "(alpha_rlts ===> op =) rbv5 rbv5" "(op = ===> alpha_rtrm5) rVr5 rVr5" @@ -176,15 +203,9 @@ apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) apply clarify - apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply simp_all - apply (erule_tac[!] alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply simp_all - defer defer (* Both sides false, so equal when we have distinct *) - apply (erule conjE)+ - apply clarify - apply (simp add: alpha5_inj) - sorry (* may be true? *) + apply (simp add: alpha_rbv_rsp_pre2) + apply (simp add: alpha_rbv_rsp_pre) +done lemma shows "(alpha_rlts ===> op =) rbv5 rbv5" @@ -212,9 +233,9 @@ lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] lemmas bv5[simp] = rbv5.simps[quot_lifted] -lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted] -lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted] +lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] +lemmas alpha5_DIS = alpha_dis[quot_lifted] lemma lets_bla: "x \ z \ y \ z \ x \ y \(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \ (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))" @@ -235,7 +256,6 @@ apply (rule_tac x="(x \ y)" in exI) apply (simp_all add: alpha_gen) apply (simp add: permute_trm5_lts fresh_star_def) -apply (metis flip_at_simps(1) supp_at_base supp_eqvt) done lemma lets_ok3: @@ -252,27 +272,15 @@ (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" apply (simp add: alpha5_INJ alpha_gen) apply (simp add: permute_trm5_lts eqvts) -apply (simp add: alpha5_INJ(5)) -apply (simp add: alpha5_INJ(1)) +apply (simp add: alpha5_INJ) done -lemma distinct_helper: - shows "\(rVr5 x \5 rAp5 y z)" - apply auto - apply (erule alpha_rtrm5.cases) - apply (simp_all only: rtrm5.distinct) - done - -lemma distinct_helper2: - shows "(Vr5 x) \ (Ap5 y z)" - by (lifting distinct_helper) - lemma lets_nok: "x \ y \ x \ z \ z \ y \ (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \ (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) -apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts) +apply (simp add: alpha5_DIS alpha5_INJ permute_trm5_lts) done end diff -r 1909be313353 -r 1850361efb8f Nominal/Term5n.thy --- a/Nominal/Term5n.thy Tue Mar 16 18:19:00 2010 +0100 +++ b/Nominal/Term5n.thy Tue Mar 16 20:07:13 2010 +0100 @@ -169,7 +169,6 @@ apply (rule_tac x="(x \ y)" in exI) apply (simp_all add: alpha_gen) apply (simp add: permute_trm5_lts fresh_star_def) -apply (metis flip_at_simps(1) supp_at_base supp_eqvt) done lemma lets_ok3: @@ -186,7 +185,6 @@ apply (simp add: alpha5_INJ alpha_gen) apply (rule_tac x="0::perm" in exI) apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts) -apply auto done lemma distinct_helper: