--- a/Quot/Nominal/Fv.thy Thu Feb 18 23:07:28 2010 +0100
+++ b/Quot/Nominal/Fv.thy Thu Feb 18 23:07:52 2010 +0100
@@ -1,5 +1,5 @@
theory Fv
-imports "Nominal2_Atoms"
+imports "Nominal2_Atoms" "Abs"
begin
(* Bindings are given as a list which has a length being equal
@@ -23,6 +23,35 @@
[],
[[], [], [(NONE, 0)]],
[[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]]
+
+A SOME binding has to have a function returning an atom set,
+and a NONE binding has to be on an argument that is an atom
+or an atom set.
+
+How the procedure works:
+ For each of the defined datatypes,
+ For each of the constructors,
+ It creates a union of free variables for each argument.
+
+ For an argument the free variables are the variables minus
+ bound variables.
+
+ The variables are:
+ For an atom, a singleton set with the atom itself.
+ For an atom set, the atom set itself.
+ For a recursive argument, the appropriate fv function applied to it.
+ (* TODO: This one is not implemented *)
+ For other arguments it should be an appropriate fv function stored
+ in the database.
+ The bound variables are a union of results of all bindings that
+ involve the given argument. For a paricular binding the result is:
+ For a function applied to an argument this function with the argument.
+ For an atom, a singleton set with the atom itself.
+ For an atom set, the atom set itself.
+ For a recursive argument, the appropriate fv function applied to it.
+ (* TODO: This one is not implemented *)
+ For other arguments it should be an appropriate fv function stored
+ in the database.
*)
ML {*
@@ -40,13 +69,32 @@
if b = noatoms then a else
if b = a then noatoms else
HOLogic.mk_binop @{const_name minus} (a, b);
+ fun mk_atoms t =
+ let
+ val ty = fastype_of t;
+ val atom_ty = HOLogic.dest_setT ty --> @{typ atom};
+ val img_ty = atom_ty --> ty --> @{typ "atom set"};
+ in
+ (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t)
+ end;
+ (* Copy from Term *)
+ fun is_funtype (Type ("fun", [_, _])) = true
+ | is_funtype _ = false;
+ (* Similar to one in USyntax *)
+ fun mk_pair (fst, snd) =
+ let val ty1 = fastype_of fst
+ val ty2 = fastype_of snd
+ val c = HOLogic.pair_const ty1 ty2
+ in c $ fst $ snd
+ end;
+
*}
ML {*
(* Currently needs just one full_tname to access Datatype *)
-fun define_raw_fv full_tname bindsall lthy =
+fun define_fv_alpha full_tname bindsall lthy =
let
- val thy = ProofContext.theory_of lthy
+ val thy = ProofContext.theory_of lthy;
val {descr, ...} = Datatype.the_info thy full_tname;
val sorts = []; (* TODO *)
fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
@@ -54,46 +102,92 @@
"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);
- fun fv_eq_constr i (cname, dts) bindcs =
+ val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
+ "alpha_" ^ name_of_typ (nth_dtyp i)) descr);
+ val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
+ val alpha_frees = map Free (alpha_names ~~ alpha_types);
+ fun fv_alpha_constr i (cname, dts) bindcs =
let
val Ts = map (typ_of_dtyp descr sorts) dts;
val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
val args = map Free (names ~~ Ts);
+ val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);
+ val args2 = map Free (names2 ~~ Ts);
val c = Const (cname, Ts ---> (nth_dtyp i));
- val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"});
- fun fv_bind (NONE, i) =
+ val fv_c = nth fv_frees i;
+ val alpha = nth alpha_frees i;
+ fun fv_bind args (NONE, i) =
if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
(* TODO we assume that all can be 'atomized' *)
+ if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else
mk_single_atom (nth args i)
- | fv_bind (SOME f, i) = f $ (nth args i);
+ | fv_bind args (SOME f, i) = f $ (nth args i);
fun fv_arg ((dt, x), bindxs) =
let
val arg =
if is_rec_type dt then nth fv_frees (body_index dt) $ x else
(* TODO: we just assume everything can be 'atomized' *)
- HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x]
- val sub = mk_union (map fv_bind bindxs)
+ if (is_funtype o fastype_of) x then mk_atoms x else
+ HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x]
+ val sub = mk_union (map (fv_bind args) bindxs)
in
mk_diff arg sub
end;
- val _ = tracing ("d" ^ string_of_int (length dts));
- val _ = tracing (string_of_int (length args));
- val _ = tracing (string_of_int (length bindcs));
+ val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))
+ val alpha_rhs =
+ HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));
+ fun alpha_arg ((dt, bindxs), (arg, arg2)) =
+ if bindxs = [] then (
+ if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
+ else (HOLogic.mk_eq (arg, arg2)))
+ else
+ if is_rec_type dt then let
+ (* THE HARD CASE *)
+ val lhs_binds = mk_union (map (fv_bind args) bindxs);
+ val lhs = mk_pair (lhs_binds, arg);
+ val rhs_binds = mk_union (map (fv_bind args2) bindxs);
+ val rhs = mk_pair (rhs_binds, arg2);
+ val alpha = nth alpha_frees (body_index dt);
+ val fv = nth fv_frees (body_index dt);
+ val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ (Free ("pi", @{typ perm})) $ rhs;
+ val alpha_gen_t = Syntax.check_term lthy alpha_gen_pre
+ in
+ HOLogic.mk_exists ("pi", @{typ perm}, alpha_gen_t)
+ (* TODO Add some test that is makes sense *)
+ end else @{term "True"}
+ val alpha_lhss = map (HOLogic.mk_Trueprop o alpha_arg) (dts ~~ bindcs ~~ (args ~~ args2))
+ val alpha_eq = Logic.list_implies (alpha_lhss, alpha_rhs)
in
- (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
- (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs)))))
+ (fv_eq, alpha_eq)
end;
- fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds;
- val fv_eqs = flat (map2 fv_eq descr bindsall)
+ fun fv_alpha_eq (i, (_, _, constrs)) binds = map2 (fv_alpha_constr i) constrs binds;
+ val (fv_eqs, alpha_eqs) = split_list (flat (map2 fv_alpha_eq descr bindsall))
+ val add_binds = map (fn x => (Attrib.empty_binding, x))
+ val (fvs, lthy') = (Primrec.add_primrec
+ (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy)
+ val (alphas, lthy'') = (Inductive.add_inductive_i
+ {quiet_mode = false, verbose = true, alt_name = Binding.empty,
+ coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
+ (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) []
+ (add_binds alpha_eqs) [] lthy')
in
- snd (Primrec.add_primrec
- (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy)
+ ((fvs, alphas), lthy'')
end
*}
-(* test
+(* tests
atom_decl name
+datatype ty =
+ Var "name set"
+
+ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *}
+
+local_setup {* define_fv_alpha "Fv.ty" [[[[]]]] *}
+print_theorems
+
+
datatype rtrm1 =
rVr1 "name"
| rAp1 "rtrm1" "rtrm1"
@@ -113,11 +207,12 @@
| "bv1 (BVr x) = {atom x}"
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
-local_setup {* define_raw_fv "Fv.rtrm1"
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
+setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Fv.rtrm1", "Fv.bp"] *}
+
+local_setup {* define_fv_alpha "Fv.rtrm1"
+ [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
[[], [[]], [[], []]]] *}
print_theorems
-
*)
end
--- a/Quot/Nominal/Perm.thy Thu Feb 18 23:07:28 2010 +0100
+++ b/Quot/Nominal/Perm.thy Thu Feb 18 23:07:52 2010 +0100
@@ -55,7 +55,7 @@
val lthy =
Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
(* TODO: Use the version of prmrec that gives the names explicitely. *)
- val (perm_ldef, lthy') =
+ val ((_, perm_ldef), lthy') =
Primrec.add_primrec
(map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;
val perm_frees =
--- a/Quot/Nominal/Terms.thy Thu Feb 18 23:07:28 2010 +0100
+++ b/Quot/Nominal/Terms.thy Thu Feb 18 23:07:52 2010 +0100
@@ -25,52 +25,71 @@
where
"bv1 (BUnit) = {}"
| "bv1 (BVr x) = {atom x}"
-| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
-
-local_setup {* define_raw_fv "Terms.rtrm1"
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
- [[], [[]], [[], []]]] *}
-print_theorems
+| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
-inductive
- alpha1 :: "rtrm1 \<Rightarrow> rtrm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (rVr1 a) \<approx>1 (rVr1 b)"
-| a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> rAp1 t1 s1 \<approx>1 rAp1 t2 s2"
-| a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 fv_rtrm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s"
-| a4: "t1 \<approx>1 t2 \<Longrightarrow> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2"
+local_setup {* snd o define_fv_alpha "Terms.rtrm1"
+ [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
+ [[], [[]], [[], []]]] *}
+print_theorems
+notation
+ alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
+ alpha_bp ("_ \<approx>1b _" [100, 100] 100)
+thm alpha_rtrm1_alpha_bp.intros
lemma alpha1_inj:
"(rVr1 a \<approx>1 rVr1 b) = (a = b)"
"(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)"
-"(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 fv_rtrm1 pi ({atom ab}, s)))"
-"(rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2) = (t1 \<approx>1 t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))))"
+"(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha_rtrm1 fv_rtrm1 pi ({atom ab}, s)))"
+"(rLt1 bp rtrm11 rtrm12 \<approx>1 rLt1 bpa rtrm11a rtrm12a) =
+ ((\<exists>pi. (bv1 bp, bp) \<approx>gen alpha_bp fv_bp pi (bv1 bpa, bpa)) \<and> rtrm11 \<approx>1 rtrm11a \<and>
+ (\<exists>pi. (bv1 bp, rtrm12) \<approx>gen alpha_rtrm1 fv_rtrm1 pi (bv1 bpa, rtrm12a)))"
+"alpha_bp BUnit BUnit"
+"(alpha_bp (BVr name) (BVr namea)) = (name = namea)"
+"(alpha_bp (BPr bp1 bp2) (BPr bp1a bp2a)) = (alpha_bp bp1 bp1a \<and> alpha_bp bp2 bp2a)"
apply -
-apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
-apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
-apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
-apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
+apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
+apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
+apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
+apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
+apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros)
done
-(* Shouyld we derive it? But bv is given by the user? *)
+lemma alpha_bp_refl: "alpha_bp a a"
+apply induct
+apply (simp_all add: alpha1_inj)
+done
+
+lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)"
+apply rule
+apply (induct a b rule: alpha_rtrm1_alpha_bp.inducts(2))
+apply (simp_all add: alpha_bp_refl)
+done
+
+lemma alpha_bp_eq: "alpha_bp = (op =)"
+apply (rule ext)+
+apply (rule alpha_bp_eq_eq)
+done
+
lemma bv1_eqvt[eqvt]:
shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
apply (induct x)
-apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt)
+apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt eqvts)
done
lemma fv_rtrm1_eqvt[eqvt]:
- shows "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
- apply (induct t)
+ "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
+ "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"
+ apply (induct t and b)
apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)
done
-
lemma alpha1_eqvt:
- shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
- apply (induct t s rule: alpha1.inducts)
+ "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
+ "alpha_bp a b \<Longrightarrow> alpha_bp (pi \<bullet> a) (pi \<bullet> b)"
+ apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts)
apply (simp_all add:eqvts alpha1_inj)
apply (erule exE)
apply (rule_tac x="pi \<bullet> pia" in exI)
@@ -84,6 +103,8 @@
apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt)
apply(simp add: permute_eqvt[symmetric])
apply (erule exE)
+ apply (erule exE)
+ apply (rule conjI)
apply (rule_tac x="pi \<bullet> pia" in exI)
apply (simp add: alpha_gen)
apply(erule conjE)+
@@ -94,63 +115,60 @@
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
apply(simp add: permute_eqvt[symmetric])
+ apply (rule_tac x="pi \<bullet> piaa" in exI)
+ apply (simp add: alpha_gen)
+ apply(erule conjE)+
+ apply(rule conjI)
+ apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
+ apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
+ apply(rule conjI)
+ apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
+ apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
+ apply(simp add: permute_eqvt[symmetric])
done
-lemma alpha1_equivp: "equivp alpha1"
+lemma alpha1_equivp: "equivp alpha_rtrm1"
sorry
-quotient_type trm1 = rtrm1 / alpha1
+quotient_type trm1 = rtrm1 / alpha_rtrm1
by (rule alpha1_equivp)
-quotient_definition
- "Vr1 :: name \<Rightarrow> trm1"
-is
- "rVr1"
-
-quotient_definition
- "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
-is
- "rAp1"
-
-quotient_definition
- "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1"
-is
- "rLm1"
-
-quotient_definition
- "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
-is
- "rLt1"
-
-quotient_definition
- "fv_trm1 :: trm1 \<Rightarrow> atom set"
-is
- "fv_rtrm1"
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lm1", @{term rLm1}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1})))
+*}
+print_theorems
lemma alpha_rfv1:
shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"
- apply(induct rule: alpha1.induct)
+ apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1))
apply(simp_all add: alpha_gen.simps)
done
lemma [quot_respect]:
- "(op = ===> alpha1) rVr1 rVr1"
- "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1"
- "(op = ===> alpha1 ===> alpha1) rLm1 rLm1"
- "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1"
+ "(op = ===> alpha_rtrm1) rVr1 rVr1"
+ "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1"
+ "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1"
+ "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1"
apply (auto simp add: alpha1_inj)
apply (rule_tac x="0" in exI)
apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
apply (rule_tac x="0" in exI)
+apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq)
+apply (rule_tac x="0" in exI)
apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1)
done
lemma [quot_respect]:
- "(op = ===> alpha1 ===> alpha1) permute permute"
+ "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute"
by (simp add: alpha1_eqvt)
lemma [quot_respect]:
- "(alpha1 ===> op =) fv_rtrm1 fv_rtrm1"
+ "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1"
by (simp add: alpha_rfv1)
lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
@@ -224,6 +242,17 @@
apply(simp add: supp_Pair supp_atom bp_supp)
done
+lemma fv_eq_bv: "fv_bp bp = bv1 bp"
+apply(induct bp rule: trm1_bp_inducts(2))
+apply(simp_all)
+done
+
+lemma helper: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}"
+apply auto
+apply (rule_tac x="(x \<rightleftharpoons> a)" in exI)
+apply auto
+done
+
lemma supp_fv:
shows "supp t = fv_trm1 t"
apply(induct t rule: trm1_bp_inducts(1))
@@ -240,13 +269,13 @@
apply(simp add: alpha_gen.simps)
apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
-apply(simp add: supp_Abs fv_trm1)
+apply(simp add: supp_Abs fv_trm1 fv_eq_bv)
apply(simp (no_asm) add: supp_def)
-apply(simp add: alpha1_INJ)
+apply(simp add: alpha1_INJ alpha_bp_eq)
apply(simp add: Abs_eq_iff)
apply(simp add: alpha_gen)
-apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt)
-apply(simp add: Collect_imp_eq Collect_neg_eq)
+apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)
+apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper)
done
lemma trm1_supp:
@@ -254,7 +283,7 @@
"supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
"supp (Lm1 x t) = (supp t) - {atom x}"
"supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"
- by (simp_all only: supp_fv fv_trm1)
+by (simp_all add: supp_fv fv_trm1 fv_eq_bv)
lemma trm1_induct_strong:
assumes "\<And>name b. P b (Vr1 name)"
@@ -280,37 +309,40 @@
where
"rbv2 (rAs x t) = {atom x}"
-local_setup {* define_raw_fv "Terms.rtrm2"
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]],
- [[[(NONE, 0)], []]]] *}
-print_theorems
-
setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}
-inductive
- alpha2 :: "rtrm2 \<Rightarrow> rtrm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
-and
- alpha2a :: "rassign \<Rightarrow> rassign \<Rightarrow> bool" ("_ \<approx>2a _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (rVr2 a) \<approx>2 (rVr2 b)"
-| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rAp2 t1 s1 \<approx>2 rAp2 t2 s2"
-| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rLm2 a t \<approx>2 rLm2 b s"
-| a4: "\<lbrakk>\<exists>pi. ((rbv2 bt, t) \<approx>gen alpha2 fv_rtrm2 pi ((rbv2 bs), s));
- \<exists>pi. ((rbv2 bt, bt) \<approx>gen alpha2a fv_rassign pi (rbv2 bs, bs))\<rbrakk>
- \<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s"
-| a5: "\<lbrakk>a = b; t \<approx>2 s\<rbrakk> \<Longrightarrow> rAs a t \<approx>2a rAs b s" (* This way rbv2 can be lifted *)
+local_setup {* snd o define_fv_alpha "Terms.rtrm2"
+ [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]],
+ [[[], []]]] *}
+print_theorems
+
+notation
+ alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and
+ alpha_rassign ("_ \<approx>2b _" [100, 100] 100)
+thm alpha_rtrm2_alpha_rassign.intros
lemma alpha2_equivp:
- "equivp alpha2"
- "equivp alpha2a"
+ "equivp alpha_rtrm2"
+ "equivp alpha_rassign"
sorry
quotient_type
- trm2 = rtrm2 / alpha2
+ trm2 = rtrm2 / alpha_rtrm2
and
- assign = rassign / alpha2a
+ assign = rassign / alpha_rassign
by (auto intro: alpha2_equivp)
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lm2", @{term rLm2}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lt2", @{term rLt2}))
+ |> snd o (Quotient_Def.quotient_lift_const ("As", @{term rAs}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2}))
+ |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2})))
+*}
+print_theorems
section {*** lets with many assignments ***}
@@ -331,36 +363,27 @@
"bv3 ANil = {}"
| "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
-local_setup {* define_raw_fv "Terms.trm3"
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],
- [[], [[(NONE, 0)], [], []]]] *}
-print_theorems
-
setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *}
-inductive
- alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100)
-and
- alpha3a :: "assigns \<Rightarrow> assigns \<Rightarrow> bool" ("_ \<approx>3a _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)"
-| a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2"
-| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha3 fv_rtrm3 pi ({atom b}, s))) \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"
-| a4: "\<lbrakk>\<exists>pi. ((bv3 bt, t) \<approx>gen alpha3 fv_trm3 pi ((bv3 bs), s));
- \<exists>pi. ((bv3 bt, bt) \<approx>gen alpha3a fv_assign pi (bv3 bs, bs))\<rbrakk>
- \<Longrightarrow> Lt3 bt t \<approx>3 Lt3 bs s"
-| a5: "ANil \<approx>3a ANil"
-| a6: "\<lbrakk>a = b; t \<approx>3 s; tt \<approx>3a st\<rbrakk> \<Longrightarrow> ACons a t tt \<approx>3a ACons b s st"
+local_setup {* snd o define_fv_alpha "Terms.trm3"
+ [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv3}, 0)], [(SOME @{term bv3}, 0)]]],
+ [[], [[], [], []]]] *}
+print_theorems
+
+notation
+ alpha_trm3 ("_ \<approx>3 _" [100, 100] 100) and
+ alpha_assigns ("_ \<approx>3a _" [100, 100] 100)
+thm alpha_trm3_alpha_assigns.intros
lemma alpha3_equivp:
- "equivp alpha3"
- "equivp alpha3a"
+ "equivp alpha_trm3"
+ "equivp alpha_assigns"
sorry
quotient_type
- qtrm3 = trm3 / alpha3
+ qtrm3 = trm3 / alpha_trm3
and
- qassigns = assigns / alpha3a
+ qassigns = assigns / alpha_assigns
by (auto intro: alpha3_equivp)
@@ -374,10 +397,6 @@
thm trm4.recs
-local_setup {* define_raw_fv "Terms.trm4" [
- [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *}
-print_theorems
-
(* there cannot be a clause for lists, as *)
(* permutations are already defined in Nominal (also functions, options, and so on) *)
setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *}
@@ -393,22 +412,21 @@
thm permute_trm4_permute_trm4_list.simps
thm permute_trm4_permute_trm4_list.simps[simplified repaired]
-inductive
- alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100)
-and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)"
-| a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2"
-| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha4 fv_rtrm4 pi ({atom b}, s))) \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s"
-| a5: "[] \<approx>4list []"
-| a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)"
+local_setup {* snd o define_fv_alpha "Terms.trm4" [
+ [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *}
+print_theorems
-lemma alpha4_equivp: "equivp alpha4" sorry
-lemma alpha4list_equivp: "equivp alpha4list" sorry
+notation
+ alpha_trm4 ("_ \<approx>4 _" [100, 100] 100) and
+ alpha_trm4_list ("_ \<approx>4l _" [100, 100] 100)
+thm alpha_trm4_alpha_trm4_list.intros
+
+lemma alpha4_equivp: "equivp alpha_trm4" sorry
+lemma alpha4list_equivp: "equivp alpha_trm4_list" sorry
quotient_type
- qtrm4 = trm4 / alpha4 and
- qtrm4list = "trm4 list" / alpha4list
+ qtrm4 = trm4 / alpha_trm4 and
+ qtrm4list = "trm4 list" / alpha_trm4_list
by (simp_all add: alpha4_equivp alpha4list_equivp)
@@ -426,101 +444,70 @@
"rbv5 rLnil = {}"
| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
-local_setup {* define_raw_fv "Terms.rtrm5" [
- [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE, 0)], [], []]] ] *}
-print_theorems
setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}
print_theorems
-inductive
- alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100)
-and
- alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"
-| a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
-| a3: "\<lbrakk>\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 fv_rtrm5 pi (rbv5 l2, t2));
- \<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts pi (rbv5 l2, l2))\<rbrakk>
- \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
-| a4: "rLnil \<approx>l rLnil"
-| a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
+local_setup {* snd o define_fv_alpha "Terms.rtrm5" [
+ [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *}
+print_theorems
-print_theorems
+(* Alternate version with additional binding of name in rlts in rLcons *)
+(*local_setup {* snd o define_fv_alpha "Terms.rtrm5" [
+ [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *}
+print_theorems*)
+
+notation
+ alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and
+ alpha_rlts ("_ \<approx>l _" [100, 100] 100)
+thm alpha_rtrm5_alpha_rlts.intros
lemma alpha5_inj:
"((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
"(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
- "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 fv_rtrm5 pi (rbv5 l2, t2))) \<and>
- (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts pi (rbv5 l2, l2))))"
+ "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha_rtrm5 fv_rtrm5 pi (rbv5 l2, t2))) \<and>
+ (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alpha_rlts fv_rlts pi (rbv5 l2, l2))))"
"rLnil \<approx>l rLnil"
"(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)"
apply -
-apply (simp_all add: alpha5_alphalts.intros)
+apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
apply rule
-apply (erule alpha5.cases)
-apply (simp_all add: alpha5_alphalts.intros)
+apply (erule alpha_rtrm5.cases)
+apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
apply rule
-apply (erule alpha5.cases)
-apply (simp_all add: alpha5_alphalts.intros)
+apply (erule alpha_rtrm5.cases)
+apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
apply rule
-apply (erule alpha5.cases)
-apply (simp_all add: alpha5_alphalts.intros)
+apply (erule alpha_rtrm5.cases)
+apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
apply rule
-apply (erule alphalts.cases)
-apply (simp_all add: alpha5_alphalts.intros)
+apply (erule alpha_rlts.cases)
+apply (simp_all add: alpha_rtrm5_alpha_rlts.intros)
done
lemma alpha5_equivps:
- shows "equivp alpha5"
- and "equivp alphalts"
+ shows "equivp alpha_rtrm5"
+ and "equivp alpha_rlts"
sorry
quotient_type
- trm5 = rtrm5 / alpha5
+ trm5 = rtrm5 / alpha_rtrm5
and
- lts = rlts / alphalts
+ lts = rlts / alpha_rlts
by (auto intro: alpha5_equivps)
-quotient_definition
- "Vr5 :: name \<Rightarrow> trm5"
-is
- "rVr5"
-
-quotient_definition
- "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5"
-is
- "rAp5"
-
-quotient_definition
- "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5"
-is
- "rLt5"
-
-quotient_definition
- "Lnil :: lts"
-is
- "rLnil"
-
-quotient_definition
- "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts"
-is
- "rLcons"
-
-quotient_definition
- "fv_trm5 :: trm5 \<Rightarrow> atom set"
-is
- "fv_rtrm5"
-
-quotient_definition
- "fv_lts :: lts \<Rightarrow> atom set"
-is
- "fv_rlts"
-
-quotient_definition
- "bv5 :: lts \<Rightarrow> atom set"
-is
- "rbv5"
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil}))
+ |> 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 ("bv5", @{term rbv5})))
+*}
+print_theorems
lemma rbv5_eqvt:
"pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
@@ -537,13 +524,13 @@
lemma alpha5_eqvt:
"xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
"xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
- apply(induct rule: alpha5_alphalts.inducts)
+ apply(induct rule: alpha_rtrm5_alpha_rlts.inducts)
apply (simp_all add: alpha5_inj)
apply (erule exE)+
apply(unfold alpha_gen)
apply (erule conjE)+
apply (rule conjI)
- apply (rule_tac x="x \<bullet> pi" in exI)
+ apply (rule_tac x="x \<bullet> pia" in exI)
apply (rule conjI)
apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
@@ -552,7 +539,7 @@
apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
apply (subst permute_eqvt[symmetric])
apply (simp)
- apply (rule_tac x="x \<bullet> pia" in exI)
+ apply (rule_tac x="x \<bullet> pi" in exI)
apply (rule conjI)
apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
@@ -566,27 +553,27 @@
lemma alpha5_rfv:
"(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
"(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)"
- apply(induct rule: alpha5_alphalts.inducts)
+ apply(induct rule: alpha_rtrm5_alpha_rlts.inducts)
apply(simp_all add: alpha_gen)
done
lemma bv_list_rsp:
shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
- apply(induct rule: alpha5_alphalts.inducts(2))
+ apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2))
apply(simp_all)
done
lemma [quot_respect]:
- "(alphalts ===> op =) fv_rlts fv_rlts"
- "(alpha5 ===> op =) fv_rtrm5 fv_rtrm5"
- "(alphalts ===> op =) rbv5 rbv5"
- "(op = ===> alpha5) rVr5 rVr5"
- "(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5"
- "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
- "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
- "(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons"
- "(op = ===> alpha5 ===> alpha5) permute permute"
- "(op = ===> alphalts ===> alphalts) permute permute"
+ "(alpha_rlts ===> op =) fv_rlts fv_rlts"
+ "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5"
+ "(alpha_rlts ===> op =) rbv5 rbv5"
+ "(op = ===> alpha_rtrm5) rVr5 rVr5"
+ "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5"
+ "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5"
+ "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5"
+ "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons"
+ "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"
+ "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"
apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
apply (clarify) apply (rule conjI)
apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
@@ -597,7 +584,7 @@
done
lemma
- shows "(alphalts ===> op =) rbv5 rbv5"
+ shows "(alpha_rlts ===> op =) rbv5 rbv5"
by (simp add: bv_list_rsp)
lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]
@@ -686,7 +673,7 @@
lemma distinct_helper:
shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
apply auto
- apply (erule alpha5.cases)
+ apply (erule alpha_rtrm5.cases)
apply (simp_all only: rtrm5.distinct)
done
@@ -719,13 +706,15 @@
| "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t"
| "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"
-local_setup {* define_raw_fv "Terms.rtrm6" [
- [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *}
-print_theorems
-
setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *}
print_theorems
+local_setup {* snd o define_fv_alpha "Terms.rtrm6" [
+ [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv6}, 0)], [(SOME @{term rbv6}, 0)]]]] *}
+notation alpha_rtrm6 ("_ \<approx>6a _" [100, 100] 100)
+(* HERE THE RULES DIFFER *)
+thm alpha_rtrm6.intros
+
inductive
alpha6 :: "rtrm6 \<Rightarrow> rtrm6 \<Rightarrow> bool" ("_ \<approx>6 _" [100, 100] 100)
where
@@ -741,30 +730,15 @@
trm6 = rtrm6 / alpha6
by (auto intro: alpha6_equivps)
-quotient_definition
- "Vr6 :: name \<Rightarrow> trm6"
-is
- "rVr6"
-
-quotient_definition
- "Lm6 :: name \<Rightarrow> trm6 \<Rightarrow> trm6"
-is
- "rLm6"
-
-quotient_definition
- "Lt6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6"
-is
- "rLt6"
-
-quotient_definition
- "fv_trm6 :: trm6 \<Rightarrow> atom set"
-is
- "fv_rtrm6"
-
-quotient_definition
- "bv6 :: trm6 \<Rightarrow> atom set"
-is
- "rbv6"
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lt6", @{term rLt6}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_trm6", @{term fv_rtrm6}))
+ |> snd o (Quotient_Def.quotient_lift_const ("bv6", @{term rbv6})))
+*}
+print_theorems
lemma [quot_respect]:
"(op = ===> alpha6 ===> alpha6) permute permute"
@@ -772,7 +746,6 @@
sorry
(* Definitely not true , see lemma below *)
-
lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6"
apply simp apply clarify
apply (erule alpha6.induct)
@@ -875,13 +848,16 @@
| "rbv7 (rLm7 n t) = rbv7 t - {atom n}"
| "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"
-local_setup {* define_raw_fv "Terms.rtrm7" [
- [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *}
-print_theorems
-
setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *}
print_theorems
+local_setup {* snd o define_fv_alpha "Terms.rtrm7" [
+ [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *}
+notation
+ alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100)
+(* HERE THE RULES DIFFER *)
+thm alpha_rtrm7.intros
+
inductive
alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)
where
@@ -889,11 +865,6 @@
| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
| a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"
-lemma bvfv7: "rbv7 x = fv_rtrm7 x"
- apply induct
- apply simp_all
-done
-
lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"
apply simp
apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI)
@@ -923,13 +894,18 @@
"rbv8 (Bar0 x) = {}"
| "rbv8 (Bar1 v x b) = {atom v}"
-local_setup {* define_raw_fv "Terms.rfoo8" [
- [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
-print_theorems
-
setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *}
print_theorems
+local_setup {* snd o define_fv_alpha "Terms.rfoo8" [
+ [[[]], [[(SOME @{term rbv8}, 0)], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+notation
+ alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and
+ alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100)
+(* HERE THE RULE DIFFERS *)
+thm alpha_rfoo8_alpha_rbar8.intros
+
+
inductive
alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)
and
@@ -958,6 +934,9 @@
apply simp apply clarify
apply (erule alpha8f_alpha8b.inducts(1))
apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)
+ apply clarify
+ apply (erule alpha8f_alpha8b.inducts(2))
+ apply (simp_all)
done
@@ -977,12 +956,17 @@
"rbv9 (Var9 x) = {}"
| "rbv9 (Lam9 x b) = {atom x}"
-local_setup {* define_raw_fv "Terms.rlam9" [
- [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *}
+setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *}
print_theorems
-setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *}
-print_theorems
+local_setup {* snd o define_fv_alpha "Terms.rlam9" [
+ [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[(SOME @{term rbv9}, 0)], [(SOME @{term rbv9}, 0)]]]] *}
+notation
+ alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and
+ alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100)
+(* HERE THE RULES DIFFER *)
+thm alpha_rlam9_alpha_rbla9.intros
+
inductive
alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100)
@@ -997,35 +981,16 @@
lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b
sorry
-quotient_definition
- "qVar9 :: name \<Rightarrow> lam9"
-is
- "Var9"
-
-quotient_definition
- "qLam :: name \<Rightarrow> lam9 \<Rightarrow> lam9"
-is
- "Lam9"
-
-quotient_definition
- "qBla9 :: lam9 \<Rightarrow> lam9 \<Rightarrow> bla9"
-is
- "Bla9"
-
-quotient_definition
- "fv_lam9 :: lam9 \<Rightarrow> atom set"
-is
- "fv_rlam9"
-
-quotient_definition
- "fv_bla9 :: bla9 \<Rightarrow> atom set"
-is
- "fv_rbla9"
-
-quotient_definition
- "bv9 :: lam9 \<Rightarrow> atom set"
-is
- "rbv9"
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("qVar9", @{term Var9}))
+ |> snd o (Quotient_Def.quotient_lift_const ("qLam9", @{term Lam9}))
+ |> snd o (Quotient_Def.quotient_lift_const ("qBla9", @{term Bla9}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_lam9", @{term fv_rlam9}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_bla9", @{term fv_rbla9}))
+ |> snd o (Quotient_Def.quotient_lift_const ("bv9", @{term rbv9})))
+*}
+print_theorems
instantiation lam9 and bla9 :: pt
begin
@@ -1072,14 +1037,11 @@
setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *}
print_theorems
-abbreviation
- "atoms xs \<equiv> {atom x| x. x \<in> xs}"
-
local_setup {* define_raw_fv "Terms.ty" [[[[]], [[], []]]] *}
print_theorems
(*
-doesn't work yet
+Doesnot work yet since we do not refer to fv_ty
local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *}
print_theorems
*)
@@ -1087,12 +1049,12 @@
primrec
fv_tyS
where
- "fv_tyS (All xs T) = (fv_ty T - atoms xs)"
+ "fv_tyS (All xs T) = (fv_ty T - atom ` xs)"
inductive
alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)
where
- a1: "\<exists>pi. ((atoms xs1, T1) \<approx>gen (op =) fv_ty pi (atoms xs2, T2))
+ a1: "\<exists>pi. ((atom ` xs1, T1) \<approx>gen (op =) fv_ty pi (atom ` xs2, T2))
\<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"
lemma
--- a/Quot/Nominal/Terms2.thy Thu Feb 18 23:07:28 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1141 +0,0 @@
-theory Terms
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv"
-begin
-
-atom_decl name
-
-text {* primrec seems to be genarally faster than fun *}
-
-section {*** lets with binding patterns ***}
-
-datatype rtrm1 =
- rVr1 "name"
-| rAp1 "rtrm1" "rtrm1"
-| rLm1 "name" "rtrm1" --"name is bound in trm1"
-| rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1"
-and bp =
- BUnit
-| BVr "name"
-| BPr "bp" "bp"
-
-(* to be given by the user *)
-
-primrec
- bv1
-where
- "bv1 (BUnit) = {}"
-| "bv1 (BVr x) = {atom x}"
-| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
-
-local_setup {* define_raw_fv "Terms.rtrm1"
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
- [[], [[]], [[], []]]] *}
-print_theorems
-
-setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
-
-inductive
- alpha1 :: "rtrm1 \<Rightarrow> rtrm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (rVr1 a) \<approx>1 (rVr1 b)"
-| a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> rAp1 t1 s1 \<approx>1 rAp1 t2 s2"
-| a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 fv_rtrm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s"
-| a4: "t1 \<approx>1 t2 \<Longrightarrow> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2"
-
-lemma alpha1_inj:
-"(rVr1 a \<approx>1 rVr1 b) = (a = b)"
-"(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)"
-"(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 fv_rtrm1 pi ({atom ab}, s)))"
-"(rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2) = (t1 \<approx>1 t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))))"
-apply -
-apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
-apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
-apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
-apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
-done
-
-(* Shouyld we derive it? But bv is given by the user? *)
-lemma bv1_eqvt[eqvt]:
- shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
- apply (induct x)
-apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt)
-done
-
-lemma fv_rtrm1_eqvt[eqvt]:
- "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
- "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"
- apply (induct t and b)
- apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)
- done
-
-
-lemma alpha1_eqvt:
- shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
- apply (induct t s rule: alpha1.inducts)
- apply (simp_all add:eqvts alpha1_inj)
- apply (erule exE)
- apply (rule_tac x="pi \<bullet> pia" in exI)
- apply (simp add: alpha_gen)
- apply(erule conjE)+
- apply(rule conjI)
- apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
- apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt fv_rtrm1_eqvt)
- apply(rule conjI)
- apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
- apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt)
- apply(simp add: permute_eqvt[symmetric])
- apply (erule exE)
- apply (rule_tac x="pi \<bullet> pia" in exI)
- apply (simp add: alpha_gen)
- apply(erule conjE)+
- apply(rule conjI)
- apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
- apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
- apply(rule conjI)
- apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
- apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
- apply(simp add: permute_eqvt[symmetric])
- done
-
-lemma alpha1_equivp: "equivp alpha1"
- sorry
-
-quotient_type trm1 = rtrm1 / alpha1
- by (rule alpha1_equivp)
-
-quotient_definition
- "Vr1 :: name \<Rightarrow> trm1"
-is
- "rVr1"
-
-quotient_definition
- "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
-is
- "rAp1"
-
-quotient_definition
- "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1"
-is
- "rLm1"
-
-quotient_definition
- "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
-is
- "rLt1"
-
-quotient_definition
- "fv_trm1 :: trm1 \<Rightarrow> atom set"
-is
- "fv_rtrm1"
-
-lemma alpha_rfv1:
- shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"
- apply(induct rule: alpha1.induct)
- apply(simp_all add: alpha_gen.simps)
- sorry
-
-lemma [quot_respect]:
- "(op = ===> alpha1) rVr1 rVr1"
- "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1"
- "(op = ===> alpha1 ===> alpha1) rLm1 rLm1"
- "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1"
-apply (auto simp add: alpha1_inj)
-apply (rule_tac x="0" in exI)
-apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
-apply (rule_tac x="0" in exI)
-apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1)
-done
-
-lemma [quot_respect]:
- "(op = ===> alpha1 ===> alpha1) permute permute"
- by (simp add: alpha1_eqvt)
-
-lemma [quot_respect]:
- "(alpha1 ===> op =) fv_rtrm1 fv_rtrm1"
- by (simp add: alpha_rfv1)
-
-lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
-lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
-
-instantiation trm1 and bp :: pt
-begin
-
-quotient_definition
- "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"
-is
- "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
-
-lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]
-
-instance
-apply default
-apply(induct_tac [!] x rule: trm1_bp_inducts(1))
-apply(simp_all)
-done
-
-end
-
-lemmas fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]
-
-lemmas fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted]
-
-lemmas alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
-
-lemma lm1_supp_pre:
- shows "(supp (atom x, t)) supports (Lm1 x t) "
-apply(simp add: supports_def)
-apply(fold fresh_def)
-apply(simp add: fresh_Pair swap_fresh_fresh)
-apply(clarify)
-apply(subst swap_at_base_simps(3))
-apply(simp_all add: fresh_atom)
-done
-
-lemma lt1_supp_pre:
- shows "(supp (x, t, s)) supports (Lt1 t x s) "
-apply(simp add: supports_def)
-apply(fold fresh_def)
-apply(simp add: fresh_Pair swap_fresh_fresh)
-done
-
-lemma bp_supp: "finite (supp (bp :: bp))"
- apply (induct bp)
- apply(simp_all add: supp_def)
- apply (fold supp_def)
- apply (simp add: supp_at_base)
- apply(simp add: Collect_imp_eq)
- apply(simp add: Collect_neg_eq[symmetric])
- apply (fold supp_def)
- apply (simp)
- done
-
-instance trm1 :: fs
-apply default
-apply(induct_tac x rule: trm1_bp_inducts(1))
-apply(simp_all)
-apply(simp add: supp_def alpha1_INJ eqvts)
-apply(simp add: supp_def[symmetric] supp_at_base)
-apply(simp only: supp_def alpha1_INJ eqvts permute_trm1)
-apply(simp add: Collect_imp_eq Collect_neg_eq)
-apply(rule supports_finite)
-apply(rule lm1_supp_pre)
-apply(simp add: supp_Pair supp_atom)
-apply(rule supports_finite)
-apply(rule lt1_supp_pre)
-apply(simp add: supp_Pair supp_atom bp_supp)
-done
-
-lemma supp_fv:
- shows "supp t = fv_trm1 t"
-apply(induct t rule: trm1_bp_inducts(1))
-apply(simp_all)
-apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
-apply(simp only: supp_at_base[simplified supp_def])
-apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
-apply(simp add: Collect_imp_eq Collect_neg_eq)
-apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
-apply(simp add: supp_Abs fv_trm1)
-apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
-apply(simp add: alpha1_INJ)
-apply(simp add: Abs_eq_iff)
-apply(simp add: alpha_gen.simps)
-apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
-(*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
-apply(simp add: supp_Abs fv_trm1)
-apply(simp (no_asm) add: supp_def)
-apply(simp add: alpha1_INJ)
-apply(simp add: Abs_eq_iff)
-apply(simp add: alpha_gen)
-apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt)
-apply(simp add: Collect_imp_eq Collect_neg_eq)
-done*)
-sorry
-
-lemma trm1_supp:
- "supp (Vr1 x) = {atom x}"
- "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
- "supp (Lm1 x t) = (supp t) - {atom x}"
- "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"
-sorry (* by (simp_all only: supp_fv fv_trm1)
-
-lemma trm1_induct_strong:
- assumes "\<And>name b. P b (Vr1 name)"
- and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"
- and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
- and "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bv1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
- shows "P a rtrma"
-sorry *)
-
-section {*** lets with single assignments ***}
-
-datatype rtrm2 =
- rVr2 "name"
-| rAp2 "rtrm2" "rtrm2"
-| rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)"
-| rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)"
-and rassign =
- rAs "name" "rtrm2"
-
-(* to be given by the user *)
-primrec
- rbv2
-where
- "rbv2 (rAs x t) = {atom x}"
-
-local_setup {* define_raw_fv "Terms.rtrm2"
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]],
- [[[], []]]] *}
-print_theorems
-
-setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}
-
-inductive
- alpha2 :: "rtrm2 \<Rightarrow> rtrm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
-and
- alpha2a :: "rassign \<Rightarrow> rassign \<Rightarrow> bool" ("_ \<approx>2a _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (rVr2 a) \<approx>2 (rVr2 b)"
-| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rAp2 t1 s1 \<approx>2 rAp2 t2 s2"
-| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rLm2 a t \<approx>2 rLm2 b s"
-| a4: "\<lbrakk>\<exists>pi. ((rbv2 bt, t) \<approx>gen alpha2 fv_rtrm2 pi ((rbv2 bs), s));
- \<exists>pi. ((rbv2 bt, bt) \<approx>gen alpha2a fv_rassign pi (rbv2 bs, bs))\<rbrakk>
- \<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s"
-| a5: "\<lbrakk>a = b; t \<approx>2 s\<rbrakk> \<Longrightarrow> rAs a t \<approx>2a rAs b s" (* This way rbv2 can be lifted *)
-
-lemma alpha2_equivp:
- "equivp alpha2"
- "equivp alpha2a"
- sorry
-
-quotient_type
- trm2 = rtrm2 / alpha2
-and
- assign = rassign / alpha2a
- by (auto intro: alpha2_equivp)
-
-
-
-section {*** lets with many assignments ***}
-
-datatype trm3 =
- Vr3 "name"
-| Ap3 "trm3" "trm3"
-| Lm3 "name" "trm3" --"bind (name) in (trm3)"
-| Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)"
-and assigns =
- ANil
-| ACons "name" "trm3" "assigns"
-
-(* to be given by the user *)
-primrec
- bv3
-where
- "bv3 ANil = {}"
-| "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
-
-local_setup {* define_raw_fv "Terms.trm3"
- [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv3}, 0)], [(SOME @{term bv3}, 0)]]],
- [[], [[], [], []]]] *}
-print_theorems
-
-setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *}
-
-inductive
- alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100)
-and
- alpha3a :: "assigns \<Rightarrow> assigns \<Rightarrow> bool" ("_ \<approx>3a _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)"
-| a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2"
-| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha3 fv_rtrm3 pi ({atom b}, s))) \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"
-| a4: "\<lbrakk>\<exists>pi. ((bv3 bt, t) \<approx>gen alpha3 fv_trm3 pi ((bv3 bs), s));
- \<exists>pi. ((bv3 bt, bt) \<approx>gen alpha3a fv_assign pi (bv3 bs, bs))\<rbrakk>
- \<Longrightarrow> Lt3 bt t \<approx>3 Lt3 bs s"
-| a5: "ANil \<approx>3a ANil"
-| a6: "\<lbrakk>a = b; t \<approx>3 s; tt \<approx>3a st\<rbrakk> \<Longrightarrow> ACons a t tt \<approx>3a ACons b s st"
-
-lemma alpha3_equivp:
- "equivp alpha3"
- "equivp alpha3a"
- sorry
-
-quotient_type
- qtrm3 = trm3 / alpha3
-and
- qassigns = assigns / alpha3a
- by (auto intro: alpha3_equivp)
-
-
-section {*** lam with indirect list recursion ***}
-
-datatype trm4 =
- Vr4 "name"
-| Ap4 "trm4" "trm4 list"
-| Lm4 "name" "trm4" --"bind (name) in (trm)"
-print_theorems
-
-thm trm4.recs
-
-local_setup {* define_raw_fv "Terms.trm4" [
- [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *}
-print_theorems
-
-(* there cannot be a clause for lists, as *)
-(* permutations are already defined in Nominal (also functions, options, and so on) *)
-setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *}
-
-(* "repairing" of the permute function *)
-lemma repaired:
- fixes ts::"trm4 list"
- shows "permute_trm4_list p ts = p \<bullet> ts"
- apply(induct ts)
- apply(simp_all)
- done
-
-thm permute_trm4_permute_trm4_list.simps
-thm permute_trm4_permute_trm4_list.simps[simplified repaired]
-
-inductive
- alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100)
-and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)"
-| a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2"
-| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha4 fv_rtrm4 pi ({atom b}, s))) \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s"
-| a5: "[] \<approx>4list []"
-| a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)"
-
-lemma alpha4_equivp: "equivp alpha4" sorry
-lemma alpha4list_equivp: "equivp alpha4list" sorry
-
-quotient_type
- qtrm4 = trm4 / alpha4 and
- qtrm4list = "trm4 list" / alpha4list
- by (simp_all add: alpha4_equivp alpha4list_equivp)
-
-
-datatype rtrm5 =
- rVr5 "name"
-| rAp5 "rtrm5" "rtrm5"
-| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
-and rlts =
- rLnil
-| rLcons "name" "rtrm5" "rlts"
-
-primrec
- rbv5
-where
- "rbv5 rLnil = {}"
-| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
-
-local_setup {* define_raw_fv "Terms.rtrm5" [
- [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *}
-print_theorems
-
-setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}
-print_theorems
-
-inductive
- alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100)
-and
- alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"
-| a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
-| a3: "\<lbrakk>\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 fv_rtrm5 pi (rbv5 l2, t2));
- \<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts pi (rbv5 l2, l2))\<rbrakk>
- \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
-| a4: "rLnil \<approx>l rLnil"
-| a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
-
-print_theorems
-
-lemma alpha5_inj:
- "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
- "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
- "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 fv_rtrm5 pi (rbv5 l2, t2))) \<and>
- (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts pi (rbv5 l2, l2))))"
- "rLnil \<approx>l rLnil"
- "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)"
-apply -
-apply (simp_all add: alpha5_alphalts.intros)
-apply rule
-apply (erule alpha5.cases)
-apply (simp_all add: alpha5_alphalts.intros)
-apply rule
-apply (erule alpha5.cases)
-apply (simp_all add: alpha5_alphalts.intros)
-apply rule
-apply (erule alpha5.cases)
-apply (simp_all add: alpha5_alphalts.intros)
-apply rule
-apply (erule alphalts.cases)
-apply (simp_all add: alpha5_alphalts.intros)
-done
-
-lemma alpha5_equivps:
- shows "equivp alpha5"
- and "equivp alphalts"
-sorry
-
-quotient_type
- trm5 = rtrm5 / alpha5
-and
- lts = rlts / alphalts
- by (auto intro: alpha5_equivps)
-
-quotient_definition
- "Vr5 :: name \<Rightarrow> trm5"
-is
- "rVr5"
-
-quotient_definition
- "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5"
-is
- "rAp5"
-
-quotient_definition
- "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5"
-is
- "rLt5"
-
-quotient_definition
- "Lnil :: lts"
-is
- "rLnil"
-
-quotient_definition
- "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts"
-is
- "rLcons"
-
-quotient_definition
- "fv_trm5 :: trm5 \<Rightarrow> atom set"
-is
- "fv_rtrm5"
-
-quotient_definition
- "fv_lts :: lts \<Rightarrow> atom set"
-is
- "fv_rlts"
-
-quotient_definition
- "bv5 :: lts \<Rightarrow> atom set"
-is
- "rbv5"
-
-lemma rbv5_eqvt:
- "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
-sorry
-
-lemma fv_rtrm5_eqvt:
- "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"
-sorry
-
-lemma fv_rlts_eqvt:
- "pi \<bullet> (fv_rlts x) = fv_rlts (pi \<bullet> x)"
-sorry
-
-lemma alpha5_eqvt:
- "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
- "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
- apply(induct rule: alpha5_alphalts.inducts)
- apply (simp_all add: alpha5_inj)
- apply (erule exE)+
- apply(unfold alpha_gen)
- apply (erule conjE)+
- apply (rule conjI)
- apply (rule_tac x="x \<bullet> pi" in exI)
- apply (rule conjI)
- apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
- apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
- apply(rule conjI)
- apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
- apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
- apply (subst permute_eqvt[symmetric])
- apply (simp)
- apply (rule_tac x="x \<bullet> pia" in exI)
- apply (rule conjI)
- apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
- apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
- apply(rule conjI)
- apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
- apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
- apply (subst permute_eqvt[symmetric])
- apply (simp)
- done
-
-lemma alpha5_rfv:
- "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
- "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)"
- apply(induct rule: alpha5_alphalts.inducts)
- apply(simp_all add: alpha_gen)
- done
-
-lemma bv_list_rsp:
- shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
- apply(induct rule: alpha5_alphalts.inducts(2))
- apply(simp_all)
- done
-
-lemma [quot_respect]:
- "(alphalts ===> op =) fv_rlts fv_rlts"
- "(alpha5 ===> op =) fv_rtrm5 fv_rtrm5"
- "(alphalts ===> op =) rbv5 rbv5"
- "(op = ===> alpha5) rVr5 rVr5"
- "(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5"
- "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
- "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
- "(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons"
- "(op = ===> alpha5 ===> alpha5) permute permute"
- "(op = ===> alphalts ===> alphalts) permute permute"
- apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
- apply (clarify) apply (rule conjI)
- apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
- apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
- apply (clarify) apply (rule conjI)
- apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
- apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
- done
-
-lemma
- shows "(alphalts ===> op =) rbv5 rbv5"
- by (simp add: bv_list_rsp)
-
-lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]
-
-instantiation trm5 and lts :: pt
-begin
-
-quotient_definition
- "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"
-is
- "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"
-
-quotient_definition
- "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"
-is
- "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
-
-lemma trm5_lts_zero:
- "0 \<bullet> (x\<Colon>trm5) = x"
- "0 \<bullet> (y\<Colon>lts) = y"
-apply(induct x and y rule: trm5_lts_inducts)
-apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
-done
-
-lemma trm5_lts_plus:
- "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x"
- "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y"
-apply(induct x and y rule: trm5_lts_inducts)
-apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
-done
-
-instance
-apply default
-apply (simp_all add: trm5_lts_zero trm5_lts_plus)
-done
-
-end
-
-lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
-
-lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
-
-lemmas bv5[simp] = rbv5.simps[quot_lifted]
-
-lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
-
-lemma lets_ok:
- "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
-apply (subst alpha5_INJ)
-apply (rule conjI)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-done
-
-lemma lets_ok2:
- "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
- (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (subst alpha5_INJ)
-apply (rule conjI)
-apply (rule_tac x="0 :: perm" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp only: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-done
-
-
-lemma lets_not_ok1:
- "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
- (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (subst alpha5_INJ(3))
-apply(clarify)
-apply (simp add: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-apply (simp add: alpha5_INJ(5))
-apply(clarify)
-apply (simp add: alpha5_INJ(2))
-apply (simp only: alpha5_INJ(1))
-done
-
-lemma distinct_helper:
- shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
- apply auto
- apply (erule alpha5.cases)
- apply (simp_all only: rtrm5.distinct)
- done
-
-lemma distinct_helper2:
- shows "(Vr5 x) \<noteq> (Ap5 y z)"
- by (lifting distinct_helper)
-
-lemma lets_nok:
- "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
- (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
- (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (subst alpha5_INJ)
-apply (simp only: alpha_gen permute_trm5_lts fresh_star_def)
-apply (subst alpha5_INJ(5))
-apply (subst alpha5_INJ(5))
-apply (simp add: distinct_helper2)
-done
-
-
-(* example with a bn function defined over the type itself *)
-datatype rtrm6 =
- rVr6 "name"
-| rLm6 "name" "rtrm6"
-| rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)"
-
-primrec
- rbv6
-where
- "rbv6 (rVr6 n) = {}"
-| "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t"
-| "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"
-
-local_setup {* define_raw_fv "Terms.rtrm6" [
- [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv6}, 0)], [(SOME @{term rbv6}, 0)]]]] *}
-print_theorems
-
-setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *}
-print_theorems
-
-inductive
- alpha6 :: "rtrm6 \<Rightarrow> rtrm6 \<Rightarrow> bool" ("_ \<approx>6 _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (rVr6 a) \<approx>6 (rVr6 b)"
-| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha6 fv_rtrm6 pi ({atom b}, s))) \<Longrightarrow> rLm6 a t \<approx>6 rLm6 b s"
-| a3: "(\<exists>pi. (((rbv6 t1), s1) \<approx>gen alpha6 fv_rtrm6 pi ((rbv6 t2), s2))) \<Longrightarrow> rLt6 t1 s1 \<approx>6 rLt6 t2 s2"
-
-lemma alpha6_equivps:
- shows "equivp alpha6"
-sorry
-
-quotient_type
- trm6 = rtrm6 / alpha6
- by (auto intro: alpha6_equivps)
-
-quotient_definition
- "Vr6 :: name \<Rightarrow> trm6"
-is
- "rVr6"
-
-quotient_definition
- "Lm6 :: name \<Rightarrow> trm6 \<Rightarrow> trm6"
-is
- "rLm6"
-
-quotient_definition
- "Lt6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6"
-is
- "rLt6"
-
-quotient_definition
- "fv_trm6 :: trm6 \<Rightarrow> atom set"
-is
- "fv_rtrm6"
-
-quotient_definition
- "bv6 :: trm6 \<Rightarrow> atom set"
-is
- "rbv6"
-
-lemma [quot_respect]:
- "(op = ===> alpha6 ===> alpha6) permute permute"
-apply auto (* will work with eqvt *)
-sorry
-
-(* Definitely not true , see lemma below *)
-
-lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6"
-apply simp apply clarify
-apply (erule alpha6.induct)
-oops
-
-lemma "(a :: name) \<noteq> b \<Longrightarrow> \<not> (alpha6 ===> op =) rbv6 rbv6"
-apply simp
-apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in exI)
-apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in exI)
-apply simp
-apply (rule a2)
-apply (rule_tac x="(a \<leftrightarrow> b)" in exI)
-apply (simp add: alpha_gen fresh_star_def)
-apply (rule a1)
-apply (rule refl)
-done
-
-lemma [quot_respect]:"(alpha6 ===> op =) fv_rtrm6 fv_rtrm6"
-apply simp apply clarify
-apply (induct_tac x y rule: alpha6.induct)
-apply simp_all
-apply (erule exE)
-apply (simp_all add: alpha_gen)
-apply (erule conjE)+
-apply (erule exE)
-apply (erule conjE)+
-apply (simp)
-oops
-
-
-lemma [quot_respect]: "(op = ===> alpha6) rVr6 rVr6"
-by (simp_all add: a1)
-
-lemma [quot_respect]:
- "(op = ===> alpha6 ===> alpha6) rLm6 rLm6"
- "(alpha6 ===> alpha6 ===> alpha6) rLt6 rLt6"
-apply simp_all apply (clarify)
-apply (rule a2)
-apply (rule_tac x="0::perm" in exI)
-apply (simp add: alpha_gen)
-(* needs rfv6_rsp *) defer
-apply clarify
-apply (rule a3)
-apply (rule_tac x="0::perm" in exI)
-apply (simp add: alpha_gen)
-(* needs rbv6_rsp *)
-oops
-
-instantiation trm6 :: pt begin
-
-quotient_definition
- "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6"
-is
- "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"
-
-instance
-apply default
-sorry
-end
-
-lemma lifted_induct:
-"\<lbrakk>x1 = x2; \<And>a b. a = b \<Longrightarrow> P (Vr6 a) (Vr6 b);
- \<And>a t b s.
- \<exists>pi. fv_trm6 t - {atom a} = fv_trm6 s - {atom b} \<and>
- (fv_trm6 t - {atom a}) \<sharp>* pi \<and> pi \<bullet> t = s \<and> P (pi \<bullet> t) s \<Longrightarrow>
- P (Lm6 a t) (Lm6 b s);
- \<And>t1 s1 t2 s2.
- \<exists>pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \<and>
- (fv_trm6 s1 - bv6 t1) \<sharp>* pi \<and> pi \<bullet> s1 = s2 \<and> P (pi \<bullet> s1) s2 \<Longrightarrow>
- P (Lt6 t1 s1) (Lt6 t2 s2)\<rbrakk>
- \<Longrightarrow> P x1 x2"
-unfolding alpha_gen
-apply (lifting alpha6.induct[unfolded alpha_gen])
-apply injection
-(* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *)
-oops
-
-lemma lifted_inject_a3:
- "\<exists>pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \<and>
- (fv_trm6 s1 - bv6 t1) \<sharp>* pi \<and> pi \<bullet> s1 = s2 \<Longrightarrow> Lt6 t1 s1 = Lt6 t2 s2"
-apply(lifting a3[unfolded alpha_gen])
-apply injection
-(* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *)
-oops
-
-
-
-
-(* example with a respectful bn function defined over the type itself *)
-
-datatype rtrm7 =
- rVr7 "name"
-| rLm7 "name" "rtrm7"
-| rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)"
-
-primrec
- rbv7
-where
- "rbv7 (rVr7 n) = {atom n}"
-| "rbv7 (rLm7 n t) = rbv7 t - {atom n}"
-| "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"
-
-local_setup {* define_raw_fv "Terms.rtrm7" [
- [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *}
-print_theorems
-
-setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *}
-print_theorems
-
-inductive
- alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)"
-| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
-| a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"
-
-lemma bvfv7: "rbv7 x = fv_rtrm7 x"
- apply induct
- apply simp_all
-sorry (*done*)
-
-lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"
- apply simp
- apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI)
- apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI)
- apply simp
- apply (rule a3)
- apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
- apply (simp_all add: alpha_gen fresh_star_def)
- apply (rule a1)
- apply (rule refl)
-done
-
-
-
-
-
-datatype rfoo8 =
- Foo0 "name"
-| Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo"
-and rbar8 =
- Bar0 "name"
-| Bar1 "name" "name" "rbar8" --"bind second name in b"
-
-primrec
- rbv8
-where
- "rbv8 (Bar0 x) = {}"
-| "rbv8 (Bar1 v x b) = {atom v}"
-
-local_setup {* define_raw_fv "Terms.rfoo8" [
- [[[]], [[(SOME @{term rbv8}, 0)], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
-print_theorems
-
-setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *}
-print_theorems
-
-inductive
- alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)
-and
- alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)"
-| a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)"
-| a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"
-| a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2"
-
-lemma "(alpha8b ===> op =) rbv8 rbv8"
- apply simp apply clarify
- apply (erule alpha8f_alpha8b.inducts(2))
- apply (simp_all)
-done
-
-lemma fv_rbar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> fv_rbar8 x = fv_rbar8 y"
- apply (erule alpha8f_alpha8b.inducts(2))
- apply (simp_all add: alpha_gen)
-done
-lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8"
- apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp)
-done
-
-lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8"
- apply simp apply clarify
- apply (erule alpha8f_alpha8b.inducts(1))
- apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)
-sorry (*done*)
-
-
-
-
-
-
-datatype rlam9 =
- Var9 "name"
-| Lam9 "name" "rlam9" --"bind name in rlam"
-and rbla9 =
- Bla9 "rlam9" "rlam9" --"bind bv(first) in second"
-
-primrec
- rbv9
-where
- "rbv9 (Var9 x) = {}"
-| "rbv9 (Lam9 x b) = {atom x}"
-
-local_setup {* define_raw_fv "Terms.rlam9" [
- [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[(SOME @{term rbv9}, 0)], [(SOME @{term rbv9}, 0)]]]] *}
-print_theorems
-
-setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *}
-print_theorems
-
-inductive
- alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100)
-and
- alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100)
-where
- a1: "a = b \<Longrightarrow> (Var9 a) \<approx>9l (Var9 b)"
-| a4: "(\<exists>pi. (({atom x1}, t1) \<approx>gen alpha9l fv_rlam9 pi ({atom x2}, t2))) \<Longrightarrow> Lam9 x1 t1 \<approx>9l Lam9 x2 t2"
-| a3: "b1 \<approx>9l b2 \<Longrightarrow> (\<exists>pi. (((rbv9 b1), t1) \<approx>gen alpha9l fv_rlam9 pi ((rbv9 b2), t2))) \<Longrightarrow> Bla9 b1 t1 \<approx>9b Bla9 b2 t2"
-
-quotient_type
- lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b
-sorry
-
-quotient_definition
- "qVar9 :: name \<Rightarrow> lam9"
-is
- "Var9"
-
-quotient_definition
- "qLam :: name \<Rightarrow> lam9 \<Rightarrow> lam9"
-is
- "Lam9"
-
-quotient_definition
- "qBla9 :: lam9 \<Rightarrow> lam9 \<Rightarrow> bla9"
-is
- "Bla9"
-
-quotient_definition
- "fv_lam9 :: lam9 \<Rightarrow> atom set"
-is
- "fv_rlam9"
-
-quotient_definition
- "fv_bla9 :: bla9 \<Rightarrow> atom set"
-is
- "fv_rbla9"
-
-quotient_definition
- "bv9 :: lam9 \<Rightarrow> atom set"
-is
- "rbv9"
-
-instantiation lam9 and bla9 :: pt
-begin
-
-quotient_definition
- "permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9"
-is
- "permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9"
-
-quotient_definition
- "permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9"
-is
- "permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9"
-
-instance
-sorry
-
-end
-
-lemma "\<lbrakk>b1 = b2; \<exists>pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \<and> (fv_lam9 t1 - bv9 b1) \<sharp>* pi \<and> pi \<bullet> t1 = t2\<rbrakk>
- \<Longrightarrow> qBla9 b1 t1 = qBla9 b2 t2"
-apply (lifting a3[unfolded alpha_gen])
-apply injection
-sorry
-
-
-
-
-
-
-
-
-text {* type schemes *}
-datatype ty =
- Var "name"
-| Fun "ty" "ty"
-
-setup {* snd o define_raw_perms ["ty"] ["Terms.ty"] *}
-print_theorems
-
-datatype tyS =
- All "name set" "ty"
-
-setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *}
-print_theorems
-
-abbreviation
- "atoms xs \<equiv> {atom x| x. x \<in> xs}"
-
-local_setup {* define_raw_fv "Terms.ty" [[[[]], [[], []]]] *}
-print_theorems
-
-(*
-doesn't work yet
-local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *}
-print_theorems
-*)
-
-primrec
- fv_tyS
-where
- "fv_tyS (All xs T) = (fv_ty T - atoms xs)"
-
-inductive
- alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)
-where
- a1: "\<exists>pi. ((atoms xs1, T1) \<approx>gen (op =) fv_ty pi (atoms xs2, T2))
- \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"
-
-lemma
- shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))"
- apply(rule a1)
- apply(simp add: alpha_gen)
- apply(rule_tac x="0::perm" in exI)
- apply(simp add: fresh_star_def)
- done
-
-lemma
- shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))"
- apply(rule a1)
- apply(simp add: alpha_gen)
- apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
- apply(simp add: fresh_star_def)
- done
-
-lemma
- shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))"
- apply(rule a1)
- apply(simp add: alpha_gen)
- apply(rule_tac x="0::perm" in exI)
- apply(simp add: fresh_star_def)
- done
-
-lemma
- assumes a: "a \<noteq> b"
- shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))"
- using a
- apply(clarify)
- apply(erule alpha_tyS.cases)
- apply(simp add: alpha_gen)
- apply(erule conjE)+
- apply(erule exE)
- apply(erule conjE)+
- apply(clarify)
- apply(simp)
- apply(simp add: fresh_star_def)
- apply(auto)
- done
-
-
-end
--- a/Quot/quotient_def.ML Thu Feb 18 23:07:28 2010 +0100
+++ b/Quot/quotient_def.ML Thu Feb 18 23:07:52 2010 +0100
@@ -12,6 +12,8 @@
val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
local_theory -> (term * thm) * local_theory
+
+ val quotient_lift_const: string * term -> local_theory -> (term * thm) * local_theory
end;
structure Quotient_Def: QUOTIENT_DEF =
@@ -85,6 +87,10 @@
quotient_def (decl, (attr, (lhs, rhs))) lthy''
end
+fun quotient_lift_const (b, t) ctxt =
+ quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
+ (Quotient_Term.quotient_lift_const (b, t) ctxt, t))) ctxt
+
local
structure P = OuterParse;
in
--- a/Quot/quotient_term.ML Thu Feb 18 23:07:28 2010 +0100
+++ b/Quot/quotient_term.ML Thu Feb 18 23:07:52 2010 +0100
@@ -26,6 +26,7 @@
val inj_repabs_trm: Proof.context -> term * term -> term
val inj_repabs_trm_chk: Proof.context -> term * term -> term
+ val quotient_lift_const: string * term -> local_theory -> term
val quotient_lift_all: Proof.context -> term -> term
end;
@@ -732,6 +733,15 @@
(ty_substs, const_substs @ rel_substs)
end
+fun quotient_lift_const (b, t) ctxt =
+let
+ val thy = ProofContext.theory_of ctxt
+ val (ty_substs, _) = get_ty_trm_substs ctxt;
+ val (_, ty) = dest_Const t;
+ val nty = subst_tys thy ty_substs ty;
+in
+ Free(b, nty)
+end
(*
Takes a term and