2 imports QuotScript QuotList Prove |
2 imports QuotScript QuotList Prove |
3 uses ("quotient_info.ML") |
3 uses ("quotient_info.ML") |
4 ("quotient.ML") |
4 ("quotient.ML") |
5 ("quotient_def.ML") |
5 ("quotient_def.ML") |
6 begin |
6 begin |
7 |
|
8 |
|
9 ML {* |
|
10 let |
|
11 val parser = Args.context -- Scan.lift Args.name_source |
|
12 fun term_pat (ctxt, str) = |
|
13 str |> ProofContext.read_term_pattern ctxt |
|
14 |> ML_Syntax.print_term |
|
15 |> ML_Syntax.atomic |
|
16 in |
|
17 ML_Antiquote.inline "term_pat" (parser >> term_pat) |
|
18 end |
|
19 *} |
|
20 |
|
21 ML {* |
|
22 fun pretty_helper aux env = |
|
23 env |> Vartab.dest |
|
24 |> map ((fn (s1, s2) => s1 ^ " := " ^ s2) o aux) |
|
25 |> commas |
|
26 |> enclose "[" "]" |
|
27 |> tracing |
|
28 *} |
|
29 |
|
30 ML {* |
|
31 fun pretty_env ctxt env = |
|
32 let |
|
33 fun get_trms (v, (T, t)) = (Var (v, T), t) |
|
34 val print = pairself (Syntax.string_of_term ctxt) |
|
35 in |
|
36 pretty_helper (print o get_trms) env |
|
37 end |
|
38 *} |
|
39 |
|
40 ML {* val pat = @{term_pat "\<lambda>(x::'a list \<Rightarrow> bool). |
|
41 (?f) |
|
42 ((g::('a list \<Rightarrow> bool)\<Rightarrow>'a list \<Rightarrow> bool) x)"} *} |
|
43 ML {* val trm = @{term_pat "\<lambda>(x::'a list \<Rightarrow> bool). |
|
44 (f::('a List.list \<Rightarrow> bool) \<Rightarrow> ('a List.list \<Rightarrow> bool) \<Rightarrow> 'b) |
|
45 ((g::('a list \<Rightarrow> bool)\<Rightarrow>'a list \<Rightarrow> bool) x) ((g::('a list \<Rightarrow> bool)\<Rightarrow>'a list \<Rightarrow> bool) x)"} *} |
|
46 |
|
47 ML {* val univ = let |
|
48 val init = Envir.empty 0 |
|
49 in |
|
50 Unify.unifiers (@{theory}, init, [(pat, trm)]) |
|
51 end |
|
52 *} |
|
53 |
|
54 ML {* val SOME ((u1, _), next) = Seq.pull univ *} |
|
55 ML {* val NEXT = Seq.pull next *} |
|
56 |
|
57 ML {* show_types := true *} |
|
58 ML {* pretty_env @{context} (Envir.term_env u1); *} |
|
59 |
7 |
60 locale QUOT_TYPE = |
8 locale QUOT_TYPE = |
61 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
9 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
62 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
10 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
63 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
11 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
1642 fun allex_prs_tac lthy quot = |
1590 fun allex_prs_tac lthy quot = |
1643 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
1591 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
1644 THEN' (quotient_tac quot); |
1592 THEN' (quotient_tac quot); |
1645 *} |
1593 *} |
1646 |
1594 |
|
1595 ML {* |
|
1596 fun prep_trm thy (x, (T, t)) = |
|
1597 (cterm_of thy (Var (x, T)), cterm_of thy t) |
|
1598 |
|
1599 fun prep_ty thy (x, (S, ty)) = |
|
1600 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
|
1601 *} |
|
1602 |
|
1603 ML {* |
|
1604 fun unify_prs thy pat trm = |
|
1605 let |
|
1606 val init = Envir.empty 0 (* FIXME: get the max-index *) |
|
1607 val univ = Unify.smash_unifiers thy [(pat, trm)] init |
|
1608 val SOME (env, _) = Seq.pull univ |
|
1609 val tenv = Vartab.dest (Envir.term_env env) |
|
1610 val tyenv = Vartab.dest (Envir.type_env env) |
|
1611 in |
|
1612 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
|
1613 end |
|
1614 *} |
|
1615 |
|
1616 |
1647 ML {* |
1617 ML {* |
1648 fun lambda_prs_tac lthy quot = |
1618 fun lambda_prs_tac lthy quot = |
1649 (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS} |
1619 (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS} |
1650 THEN' (RANGE [quotient_tac quot, quotient_tac quot])); |
1620 THEN' (RANGE [quotient_tac quot, quotient_tac quot])); |
1651 *} |
1621 *} |