# HG changeset patch # User Cezary Kaliszyk # Date 1268811586 -3600 # Node ID 77b86f1fc93612339247a1f969f4fa77c89b8eb6 # Parent 1850361efb8f545b4100e94f0d3edb77185e4386 Lifting theorems with compound fv and compound alpha. diff -r 1850361efb8f -r 77b86f1fc936 Nominal/Abs.thy --- a/Nominal/Abs.thy Tue Mar 16 20:07:13 2010 +0100 +++ b/Nominal/Abs.thy Wed Mar 17 08:39:46 2010 +0100 @@ -718,6 +718,22 @@ apply (simp add: swap_fresh_fresh) done +(* TODO: The following lemmas can be moved somewhere... *) +lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===> + prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split" + by auto + +lemma split_prs2[quot_preserve]: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split" + by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + +lemma alpha_gen2: + "(bs, x1, x2) \gen (\(x1, y1) (x2, y2). R1 x1 x2 \ R2 y1 y2) (\(a, b). f1 a \ f2 b) pi (cs, y1, y2) = + (f1 x1 \ f2 x2 - bs = f1 y1 \ f2 y2 - cs \ (f1 x1 \ f2 x2 - bs) \* pi \ R1 (pi \ x1) y1 \ R2 (pi \ x2) y2)" +by (simp add: alpha_gen) + end diff -r 1850361efb8f -r 77b86f1fc936 Nominal/Parser.thy --- a/Nominal/Parser.thy Tue Mar 16 20:07:13 2010 +0100 +++ b/Nominal/Parser.thy Wed Mar 17 08:39:46 2010 +0100 @@ -416,9 +416,11 @@ val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; val q_bn = map (lift_thm lthy16) raw_bn_eqs; val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; - val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj - val q_inj_pre = map (lift_thm lthy17) inj_unfolded; - val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre + val inj_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_inj + val inj_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) inj_unfolded1 + val q_inj_pre1 = map (lift_thm lthy17) inj_unfolded2; + val q_inj_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_inj_pre1 + val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre2 val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17; val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))